On the Constructive Constructible Universe
Gödel’s Constructible Universe, L, was introduced to show the consistency of the Axiom of Choice and the Generalized Continuum Hypothesis with the axioms of ZF and is the smallest inner model of ZF. That is, it is the minimal submodel that satisfies ZF and contains all the ordinals of the background universe. In this talk we shall see how vastly different the situation can be in constructive set theories.
Firstly, we shall investigate L over CZF. Via a proof-theoretic ordinal analysis of Power Kripke Platek combined with realizability, we shall show that it is not possible to prove that Exponentiation holds in L. Therefore, over CZF, the Constructible Universe may fail to be an inner model of full CZF. Secondly, we shall explore the concept of an ordinal in the constructive setting. We shall see that, without the law of excluded middle, ordinals need not satisfy many of the standard, expected properties and instead can have very strange behaviour. In particular, over IZF, we shall see that it is possible for there to be an ordinal which is not in the constructible universe, answering a question of Lubarsky. This is joint work with Michael Rathjen.
This document was translated from LATEX by HEVEA.