Page 99 - Textos de Matemática Vol. 40

2.3. Universes in explicit mathematics 87 Theorem 2.3.21. There exists a closed individual term ig of LEM so that NAI
proves for arbitrary LEM formulae φ(u):
1. R(a) ∧ R(b) → R(ig(a, b)),
2. R(a)∧R(b)→Closed(a,b,ig(a,b)),
3. R(a) ∧ R(b) ∧ Closed(a, b, A) → ∀x ∈˙ ig(a, b).φ(x).
Proof. This proof is literally the same as the proof of Theorem 2.3.13, provided that we make the following changes: instead of the generator lt, we use the generator l and instead of the induction schema (L.2), we apply name induction (LlEM -IR ). ⊣
Since the generator i does not play any role in the theory NAI, it has no function for the embedding of T0 + (sLim); the part of the generator i in T0 + (sLim) is taken over by the closed term ig which we have just defined. Hence, if φ∗ is the LEM formula which results from the LEM formula φ by replacing all occurrences of i by ig, we see that NAI proves φ∗ for all axioms φ of T0 + (sLim).
Corollary 2.3.22. The theory T0 + (sLim) is contained in NAI. Moreover, the subsystems of T0 + (sLim) which are obtained by restricting inductive generation or complete induction on the natural numbers plus inductive generation to types are contained in the corresponding subsystems of NAI.
For determining the upper proof-theoretic bounds of NAI, we refer again to the model construction in Ja¨ger and Studer [JS02b]. It follows that NAI, together with the axioms (Ul-Lin) and (Ul-Con), is valid in this model. The results of [JS02b] thus show that the proof-theoretic strength of NAI+(Ul-Lin)+ (Ul-Con) cannot be greater than that of T0.
Now, let us recapitulate several results concerning theories of explicit math- ematics with universes. One important aspect is that the addition of (Lim) or (sLim) plus certain ordering principles for normal universes does not increase the proof-theoretic strength of T0; another observation says that inductive gen- eration may be replaced by leastness of universes or name induction.
Conclusion 2.3.23. The following theories with universes have the same proof- theoretic strength as the theory T0:
1. T0 + (Lim) and T0 + (Lim) + (Ul-Lin) + (Ul-Con), 2. T0 + (sLim) and T0 + (sLim) + (Ul-Lin) + (Ul-Con), 3. LUN, NAI and NAI + (Ul-Lin) + (Ul-Con).
A survey on further theories of explicit mathematics comprising Mahlo universes and 2-universes (corresponding to Π3 reflection) may be found in Ja¨ger and Strahm [JS05].