Page 96 - Textos de Matemática Vol. 40

84 Chapter 2. Explicit Mathematics Thus lst a is i (l a, ar a). The following Theorem shows that the closed term lst
produces for each name a the least universe containing a.
Theorem 2.3.15. For each LEM formula φ(u) one can prove in T0 + (Lim) +
(LEM -UG):
1. R(a)→U(lsta)∧a∈˙ lsta,
2. R(a) ∧ (∀x.C(φ, x) → φ(x)) ∧ φ(a) → ∀x ∈˙ lst a.φ(x).
Proof. In view of the preceding remarks, the proof of the first assertion should be more or less obvious. For showing the second assertion, suppose R(a), ∀x.C(φ,x) → φ(x) and φ(a). Then by some intermediate calculations we get Closed(l a, ar a, φ). From this we conclude ∀x ∈˙ lst a.φ(x) by the induction prin- ciple of inductive generation. ⊣
We simply translate the language L′EM of LUN into the language LEM of T0 +(Lim)+(LEM-UG) by interpreting the generator lt of L′EM by the closed term lst of LEM. Hence, the previous Theorem yields the translation of the axioms (L.1) and (L.2). The treatment of the other axioms of LUN in T0 + (Lim) + (LEM-UG) is not problematic.
Corollary 2.3.16. The theory LUN is contained in T0 +(Lim)+(LEM-UG). More- over, the subsystems of LUN which are obtained by restricting (L.2) or complete induction on the natural numbers plus (L.2) to types are contained in the corre- sponding subsystems of T0 + (Lim) + (LEM-UG).
2.3.6 Strict universes
In this Section we discuss the notion of name strictness, as it was introduced in Section 2.2.1 for the theory NEM, but relativized to a type W. By reflecting name strictness on universes, one obtains name strict universes. In the next Section, we will also consider name induction, as in NEM. Adding name in- duction to the theory of name strict universes proves inductive generation and yields, thereby, an alternative to LUN.
One has to observe that name strictness depends on the generators which are available in the underlying language. Since we have to consider here, in addition to the generators available in NEM, the generators l and i (even if the latter one will not be used later on), we need two extra formulae in the definition of Str(W ); thus Str(W ) is the conjuntion of the following formulae, of which the first five correspond to the definition in NEM:
(1) ∀x.co(x)∈W →x∈W,
(2) ∀x, y.int(x, y) ∈ W → x ∈ W ∧ y ∈ W, (3) ∀x.dom(x)∈W →x∈W,