Constructing the Constructible Universe Constructively

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.