Page 89 - Textos de Matemática Vol. 40

2.3. Universes in explicit mathematics 77 2.3.3 Proof theory.
Here we do not discuss the semantics of theories for explicit mathematics with universes and its model constructions. This issue is treated in some detail in Ja¨ger and Studer [JS02b] for impredicative systems and in Ja¨ger and Strahm [JS01] for their (meta)predicative variants. These articles also contain the proof-theoretic analysis of a series of theories for explicit mathematics with universes.
Some relevant results are listed in the following Theorem. Parts one and two follow from Ja¨ger and Studer [JS02b]. For parts three and four, see Strahm [Str99] and Kahle [Kah97b], respectively.
Theorem 2.3.10. 1. The theory T0 +(Lim)+(LEM-UG)+(Ul-Lin)+(Ul-Con) is consistent and of the same proof-theoretic strength as T0.
2. This proof-theoretic equivalence remains true if, on both sides, inductive generation or complete induction on the natural numbers plus inductive generation are restricted to types.
3. The theory EETJ + (Lim) + (Ul-Lin) + (Ul-Con) + (LEM-IN) is proof-theo- retically equivalent to ID<ε0 .
4. Moreover, if complete induction on the natural numbers in the previous system is restricted to types, then the resulting theory is proof-theoretically equivalent to ID<ω and ATR0.
The model constructions in Kahle [Kah97b] and Strahm [Str99] em-
ployed for establishing the proof-theoretic upper bounds of EETJ + (Lim) + (Ul-Lin) + (Ul-Con) plus type or formula induction on the natural numbers may easily be adapted to satisfying (LEM-UG) as well. Hence, the addition of unique- ness of generators with respect to LEM to these two theories does not increase their respective proof-theoretic strength.
2.3.4 Least universes
The limit axiom (Lim) claims that every name a is contained in a normal universe named by la. It does not claim, however, that this universe is a minimal or least universe containing a. In this Section we want more and introduce the theory LUN which requires each name to be element of a least universe. Then we deal with consequences of the existence of least universes.
In the following, we make a careful distinction between the normal uni- verses considered in the previous Section and the least universes to be generated now. Accordingly, LUN is formulated in the language L′EM which is the variant of LEM using the generator lt instead of the generator l; the generator i is not needed in L′EM. The L′EM formulae and other syntactic categories of L′EM are defined in analogy to those of LEM.