Constructing the Constructible Universe Constructively
Richard Matthews, Michael Rathjen

TL;DR
This paper explores the properties of the constructible universe within intuitionistic set theories, extending fundamental operations and examining conditions under which L may not be an inner model, especially regarding the Axiom of Exponentiation.
Contribution
It introduces an extended set of operations to generate the constructible universe over intuitionistic theories and analyzes its limitations as an inner model.
Findings
L may fail to satisfy the Axiom of Exponentiation in constructive set theories
Extended operations suffice to construct L over Intuitionistic KP without Infinity
L's status as an inner model is not guaranteed in constructive ZF with Power Set
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 show that over Constructive Zermelo-Fraenkel (even with the Power Set axiom) one cannot prove that the Axiom of Exponentiation holds in L.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · Logic, Reasoning, and Knowledge · Advanced Algebra and Logic
