{
  "id": "2206.08283",
  "version": "v1",
  "published": "2022-06-16T16:28:54.000Z",
  "updated": "2022-06-16T16:28:54.000Z",
  "title": "Constructing the Constructible Universe Constructively",
  "authors": [
    "Richard Matthews",
    "Michael Rathjen"
  ],
  "comment": "31 pages",
  "categories": [
    "math.LO"
  ],
  "abstract": "We study the properties of the constructible universe, L, over intuitionistic theories. We give an extended set of fundamental operations which is sufficient to generate the universe over Intuitionistic Kripke-Platek set theory without Infinity. Following this, we investigate when L can fail to be an inner model in the traditional sense. Namely, we first show that, over Intuitionistic Zermelo-Fraenkel, it is possible for there to be an ordinal which is not in the constructible universe. Then we show that Constructive Zermelo-Fraenkel (even with the Power Set axiom) cannot prove that the Axiom of Exponentiation holds in L.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2022-06-16T16:28:54.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03E45",
      "03E70",
      "03D65",
      "03E10",
      "03F55"
    ],
    "keywords": [
      "constructible universe",
      "intuitionistic kripke-platek set theory",
      "power set axiom",
      "fundamental operations",
      "intuitionistic zermelo-fraenkel"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 31,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}