Page 93 - Textos de Matemática Vol. 40

2.3. Universes in explicit mathematics 81 to reduce the closure principle of inductive generation to the closure condition
for universes,
ψφ(u,v,w):=∀y.y∈˙ acc(u,v)∧w=f(u,v,y)→φ(y).
R(u) ∧ R(v) ∧ Closed(u, v, φ) ∧ C(ψφ(u, v, .), w) → ψφ(u, v, w). (B) Proof of (B). Assuming the left hand side of this implication, we have to
show that φ(c) follows from
c∈˙ acc(u,v)∧w=f(u,v,c) (6)
for all c. So we also assume (6). Then equation (1) implies w = j(pd (u, v, c), λy.f(u, v, y)).
Hence, the uniqueness of generators and C(ψφ(u, v, .), w) yield ∀x∈˙ pd(u,v,c).ψφ(u,v,f(u,v,x)),
and the definition of ψφ therefore implies
∀x∈˙ pd(u,v,c).∀y.y∈˙ acc(u,v)∧f(u,v,x)=f(u,v,y)→φ(y).
¿From this we immediately obtain
∀x ∈˙ pd(u,v,c).x ∈˙ acc(u,v) → φ(x).
Because of c ∈˙ acc (u, v), applying (A) gives ∀x ∈˙ pd (u, v, c).φ(x) and, therefore, φ(c) follows from Closed(u, v, φ). Thus (B) is proven.
Now we are ready for the third assertion of our Theorem. Take an arbitrary L′EM formula φ(u) and assume R(a), R(b), R(acc (a, b), S) and Closed(a, b, φ). We apply the auxiliary assertion (B) and obtain
∀x.C(ψφ(a, b, .), x) → ψφ(a, b, x).
Because of the uniqueness of generators, we also have ψφ (a, b, du (a, b)). Thus, the leastness principle (L.2) yields ∀x ∈˙ lt (du (a, b)).ψφ (a, b, x). Hence, by the definition of ψφ, we conclude that
∀x∈˙ lt(du(a,b)).∀y.y∈˙ acc(a,b)∧x=f(a,b,y)→φ(y).
Since acc(a,b) is a name of S and f(a,b,c) ∈˙ lt(du(a,b)) for all elements c of S, it follows ∀x ∈ S.φ(x). This finishes the proof of the third assertion of our Theorem. ⊣