Page 91 - Textos de Matemática Vol. 40

2.3. Universes in explicit mathematics 79 is also true that lt nat ∈/˙ lt c. ¿From lt nat = a ∈˙ lt a, we thus conclude that
˙
lt a ̸⊂ lt c. Hence ¬(Ult -Tran).
To finish the proof of this Theorem, we can proceed as in the proof of Theorem 2.3.8 and derive ¬(Ult-Con) from the just shown ¬(Ult-Tran) and the fact that (Ult-Con) implies (Ult-Tran). ⊣
Our next aim is to show that inductive generation (IG) can be handled in LUN. The basic idea is to make use of the induction schema (L.2) of LUN for dealing with the induction schema of inductive generation. Please keep in mind the definition of the formula Closed(a, b, φ) from Section 2.2.2.
Theorem 2.3.13. There exists a closed individual term acc of L′EM so that LUN proves for arbitrary L′EM formulae φ(u):
1. R(a)∧R(b)→R(acc(a,b)),
2. R(a)∧R(b)→Closed(a,b,acc(a,b)),
3. R(a) ∧ R(b) ∧ Closed(a, b, φ) → ∀x ∈˙ acc (a, b).φ(x).
This Theorem is a version of Theorem 2.2.2, but with a type of names named by acc (a, b) instead of a formula Acc(a, b, ·). In fact the following proof may be seen as a extended version of the proof of Theorem 2.2.2.
Proof. As in the proof of Theorem 2.2.2 we have a term term pd such that pd(u,v,w) is the name of the type of all predecessors of w in U with respect to V , if R(v, V ) and R(u, U). And as in that proof (see equation (⋆)), we can choose a term f satisfying the equation:
f (u,v,w) ≃ j(pd(u,v,w),λy.f(u,v,y)). (1) In addition, given two types U and V , we write U ⊎ V for the disjoint union of
U and V :
U⊎V :={(0,x):x∈U}∪{(1,x):x∈V}.
By elementary comprehension we know that U ⊎ V is a type and that there is
a term du to provide a name for it:
R(u, U ) ∧ R(v, V ) → R(du (u, v), U ⊎ V ).
Moreover, because of Lemma 2.3.2, we can relativize du and pd to universes: U(W ) ∧ u ∈ W ∧ v ∈ W → du (u, v) ∈ W, (2)
U(W)∧R(u)∧R(v)∧du(u,v)∈W →pd(u,v,w)∈W. (3)
Because of the uniqueness of generators du can even be chosen so that du (u, v) is different from j(w,f) for arbitrary u, v, w and f.