Page 92 - Textos de Matemática Vol. 40

80 Chapter 2. Explicit Mathematics
Making use of the term f and the generator lt, we can now apply modified elementary comprehension (cf. Lemma 2.1.2) in order to obtain a closed term acc so that acc (u, v) uniformly names the type
{x:x∈˙ u∧f(u,v,x)∈˙ lt(du(u,v))}, provided that u and v are names, i.e.,
R(u) ∧ R(v) → R(acc (u, v)), (4) R(u)∧R(v)→∀x.x∈˙ acc(u,v)↔x∈˙ u∧f(u,v,x)∈˙ lt(du(u,v)). (5)
Thus, the first assertion of our Theorem is obviously satisfied. To deal with the second assertion, assume R(a), R(b) and R(acc (a, b), S); we have to show Closed(a, b, S). To this end, take an individual c ∈˙ a with the property
∀x∈˙ a.(x,c)∈˙ b→x∈S. ¿From this we conclude that
∀x.x ∈˙ pd(a,b,c) → f(a,b,x) ∈˙ lt(du(a,b)).
Together with (3), the closure properties of universes and equation (1) we obtain f(a,b,c)≃j(pd(a,b,c),λy.f(a,b,y))∈˙ lt(du(a,b)).
Therefore, c is an element of S, and the proof of Closed(a,b,S) is complete. Hence, the second assertion of our Theorem is established as well.
Before turning to the proof of the third assertion, which requires a bit more effort, we show two auxiliary assertions (A) and (B).
R(u)∧R(v)∧w∈˙ acc(u,v)→∀x∈˙ pd(u,v,w).x∈˙ acc(u,v). (A) Proof of (A). Let u and v be names. Then w ∈˙ acc (u, v) implies in view
of equation (1) and property (5) that j(pd(u,v,w),λy.f(u,v,y))∈˙ lt(du(u,v)).
Remember that du(u,v) is different from j(pd(u,v,w),λy.f(u,v,y)) according to our choice of du. Hence, assertion 5 of Lemma 2.3.11 yields
∀x∈˙ pd(u,v,w).f(u,v,x)∈˙ lt(du(u,v)).
Thus, we have ∀x ∈˙ pd (u, v, w).x ∈˙ acc (u, v), and the proof of the first auxiliary assertion (A) is complete.
Depending on the closed terms t and acc and the parameters u and v, we now define for each L′EM formula φ(w) an L′EM formula ψφ(u, v, w) which helps