Page 88 - Textos de Matemática Vol. 40

76 Chapter 2. Explicit Mathematics
According to the following Lemma, (Ul-Tran) is provable in every theory of the form T + (Lim) + (Ul-Con), provided that T comprises EETJ; therefore, it need not be included in the list of axioms. To be more precise: EETJ+(Lim)+(Ul-Con) proves (Ul-Tran), and EETJ+(Lim)+(Ul-Lin) proves the equivalence of (Ul-Con) and (Ul-Tran).
Lemma 2.3.9. In EETJ + (Lim) + (Ul-Con), one can prove that ∀x,y,z.Ul(x)∧Ul(y)∧z=˙ x∧z∈˙ y→x⊂˙ y.
Since this formula is a (useful) generalization of (Ul-Tran), (Ul-Tran) is also provable in EETJ + (Lim) + (Ul-Con).
Proof. Assume that a is a normal name of the universe S, b a normal name of the universe T, a =˙ c and c ∈ T. Then c is also a name of S and, therefore, we have c ∈/ S according to Lemma 2.3.3. Hence T is not contained in S. Because of (Ul-Con), we thus have S ⊂ T. ⊣
2.3.2 The theory T0.
The most famous system of explicit mathematics is the theory T0 introduced in Feferman [Fef75]. It is obtained from EETJ+(LEM-IN) by adding the principle of inductive generation (IG). This principle ensures the existence of accessible parts as in Section 2.2.2, but now not only on the level of formulae, but as sets. Using the names of these types we may iterate the process of generating accessible parts. For the formulation of the axioms we use again the abbreviation Closed(a, b, φ) from Section 2.2.2. Inductive generation (IG) is now given by the following axioms:1
(IG.1) R(a) ∧ R(b) → ∃X.R(i (a, b), X) ∧ Closed(a, b, X),
(IG.2) R(a) ∧ R(b) ∧ Closed(a, b, φ) → ∀x ∈˙ i (a, b).φ(x)
for all LEM formulae φ(u). Thus (IG), i.e., (IG.1) + (IG.2), states the existence of accessible parts and, again, everything is uniform in the corresponding names. As mentioned before, Feferman’s T0 is given by
T0 := EETJ + (LEM-IN) + (IG).
The proof theory of T0 is well-known, cf. Feferman [Fef75, Fef79], Fe- ferman and Sieg [FS81], Ja¨ger [J¨ag83], and Ja¨ger and Pohlers [JP82]. As being equivalent to the subsystem of second order analysis (∆12-CA) + (BI), T0 played an important role in the proof-theoretic analysis of this system, which was for a long time the strongest system accessible to an ordinal analysis.
1The original definition of T0 does not restrict the quantification over y in the Closed(a, b, S) to a. However, this restriction, introduced in [JKS01], is technical helpful, and in full accor- dance with the underlying intuition.