Page 90 - Textos de Matemática Vol. 40

78 Chapter 2. Explicit Mathematics
The axioms of LUN are the axioms of EETJ formulated for L′EM, uniqueness of generators (L′EM-UG) with respect to the language L′EM, the schema (L′EM-IN) of complete induction on the natural numbers for all L′EM formulae plus the following leastness axioms:
(L.1) ∀x.R(x) → U(lt x) ∧ x ∈˙ lt x,
(L.2) ∀x.R(x) ∧ (∀y.C(φ, y) → φ(y)) ∧ φ(x) → ∀y ∈˙ lt x.φ(y)
for all L′EM formulae φ(u). The schema (L.2) is an induction principle establish- ing that there are no definable proper subcollections of the type with name lt a with the closure properties of a universe and a as an element.
The proof of the following Lemma, which lists some further properties of the generator lt, is straightforward and left to the reader. The uniqueness of generators (L′EM-UG) with respect to L′EM is used several times.
Lemma 2.3.11. In LUN, one can prove:
1. R(a)∧R(lta,S)→∀x.(C(S,x)∨x=a)↔x∈S,
2. R(a)∧ltb∈˙ lta→ltb=a,
3. a=˙ b→lta∈/˙ ltb, ˙
4. R(a)→a̸=lta,
5. R(a)∧j(b,f)∈˙ lta∧a̸=j(b,f)→b∈˙ lta∧∀x∈˙ b.fx∈˙ lta.
Taking up the arguments of the previous Section one may see immediately that (U-Lin), (U-Tran) and (U-Con) are inconsistent with LUN. However, the situation is even worse in LUN with reference to our ordering principles for universes: even linearity, transitivity and connectivity for normal names are inconsistent. In analogy to EETJ + (Lim), normal (names of) universes are defined in LUN by
Ult(x) := ∃y.R(y) ∧ x = lt y.
Linearity (Ult-Lin), transitivity (Ult-Tran) and connectivity (Ult-Con) of normal
names of universes are then formulated as expected.
Theorem 2.3.12. In LUN, one can prove that
¬(Ult-Lin) ∧ ¬(Ult-Tran) ∧ ¬(Ult-Con).
Proof. Let a be the name lt nat and S the universe named by a. Now choose a
different name b of S. Then lta ∈/˙ ltb and ltb ∈/˙ lta follow from the third part of
Lemma 2.3.11. Since a is the term lt nat, the second part of this Lemma yields ˙˙
a ∈/ lt b. Hence, we also have lt a ̸= lt b, and ¬(Ult -Lin) is proven.
We continue by defining c to be the name lt a. This implies lt a ∈˙ lt c. Furthermore, in view of the second and the fourth part of Lemma 2.3.11, it