Page 94 - Textos de Matemática Vol. 40

82 Chapter 2. Explicit Mathematics
This Theorem provides the desired reduction of T0 to LUN: (i) the language LEM is translated into the language L′EM by interpreting the generator i of LEM as the closed individual term acc of L′EM and leaving the remaining vocabulary unchanged; (ii) then the translations of all instances of inductive generation obtained in this way are provable in LUN according to the previous Theorem; (iii) the (translations of the) remaining axioms of T0 are obviously provable in LUN. A careful inspection of the previous proof also establishes the second part of the following Corollary.
Corollary 2.3.14. The theory T0 is contained in LUN. Moreover, the subsystems of T0 which are obtained by restricting inductive generation or complete induc- tion on the natural numbers plus inductive generation to types are contained in the corresponding subsystems of LUN.
2.3.5 Embedding of LUN within T0 + (Lim) + (LEM-UG)
In the previous Section, we have shown how T0 can be embedded within LUN. Therefore, we have a lower bound for the proof-theoretic strength of LUN. It remains to be proven that this bound is sharp. This aim will be achieved by interpreting LUN in the extension T0 +(Lim)+(LEM-UG) of T0 and by exploiting a result of Ja¨ger and Studer [JS02b] implying the proof-theoretic equivalence of T0 and T0 + (Lim) + (LEM-UG).
The crucial step in the interpretation of LUN in T0 +(Lim)+(LEM-UG) is to construct a closed term lst of the language LEM so that for each name a the term lst a names, provable in T0 +(Lim)+(LEM -UG), the least universe containing a. In general, the generator l will not do this job since the universe denoted by l a may be too big. And we know more: according to Theorem 2.3.12, it is inconsistent with T0 +(Lim)+(LEM-UG) and linearity, transitivity or connectivity of normal names to assume that each l a is a name of the least universe containing a.
For defining the closed term lst we proceed as follows: given a name a, we go to the normal universe provided by l a. Then we use inductive generation on this universe in order to single out those names which are absolutely needed for a universe containing a. This means we employ a binary relation on the universe (named by) l a according to the “date of generation” of the respective names. Because of the uniqueness of generators, the history of the elements of l a relevant for this construction is well-determined in the theory T0 + (Lim) + (LEM -UG).
Now we define an LEM formula `a which says that b and c are elements of the universe la and b comes before c in the inductive construction of the least universe containing a. Let Bef(a,b,c) be the disjunction of the following formulae:
(1) c = co(b),
(2) ∃x.c = int(b, x) ∨ c = int(x, b),