Page 98 - Textos de Matemática Vol. 40

86 Chapter 2. Explicit Mathematics
strictness, it is easy to check that the universe with this name contains a and b. If only the axiom (Lim) is available, then l (du(a, b)) can be formed as well, but now we cannot conclude that a ∈˙ l (du(a, b)) and b ∈˙ l (du(a, b)). It merely follows that there are names a′, b′ ∈˙ l (du(a, b)) so that a′ =˙ a and b′ =˙ b.
2.3.7 Name induction
As an alternative to least universes, we can add name induction to the theory EETJ + (sLim) + (LEM-UG) to obtain inductive generation.
In order to state the axiom schema of name induction, we introduce the closure condition Cl(S, a) which extends C(S, a) by a new clause for the universe generator l,
Cl(S, a) := C(S, a) ∨ ∃x.a = l x ∧ x ∈ S.
The type existence axioms of EETJ + (Lim) and EETJ + (sLim) guarantee
that the names are closed under this closure condition, ∀x.Cl(R, x) → R(x).
The schema of name induction on the other hand, is the principle that there are no definable subcollections of the names with this closure property. It is given by
(LlEM-IR) (∀x.Cl(φ, x) → φ(x)) → ∀x.R(x) → φ(x)
for all LEM formulae φ(u).2 This form of name induction will be considered now in the context of EETJ with the strict limit axiom, uniqueness of generators and the schema of complete induction on the natural numbers,
NAI := EETJ + (sLim) + (LEM-UG) + (LEM-IN) + (LlEM-IR). Remark 2.3.19. As for NEM we have that NAI proves Str(R).
In the proof of Theorem 2.3.13 which provides for inductive generation in the theory LUN, we made essential use of the fifth assertion of Lemma 2.3.11. Working in the theory NAI, an even slightly stronger property follows immedi- ately from the name strictness of normal universes.
Lemma 2.3.20. In NAI, one can prove that
R(a)∧j(b,f)∈˙ la→b∈˙ la∧∀x∈˙ b.fx∈˙ la.
With this Lemma available, we can now simulate inductive generation in the theory NAI in the same way as we did it in LUN.
2The superscript l in (LlEM-IR) is used to distinguish this scheme from the one in NEM where we did not take the universe generator in consideration.