Page 77 - Textos de Matemática Vol. 40

2.2. Name induction 65
Assuming Acc(a,b,c), we get by (⋆) that R(j(pd(a,b,c),λy.f(a,b,y))) holds. Then ∀x ∈˙ pd (a, b, c).R(f(a, b, x)) is a consequence of Lemma 2.2.1 about name strictness. To complete the proof of (A), we have to check that ∀x ∈˙ pd (a, b, c). x ∈˙ a, which immediately follows from the definition of pd.
In order to formulate the assertion (B), we define an additional formula ψφ(u, v, w) depending on a formula φ(x) which will be used as induction formula in the schema of name induction. Using the definition of f, here we “replace” arbitrary objects by their associated names.
ψφ(a, b, u) := ∀y.Acc(a, b, y) ∧ f (a, b, y) = u → φ(y). Now, the statement (B) reads as
Closed(a, b, φ) ∧ C(ψφ(a, b, ·), u) → ψφ(a, b, u). (B)
For the proof of (B), we can assume Closed(a,b,φ) ∧ C(ψφ(a,b,·),u) and Acc(a, b, c) ∧ f (a, b, c) = u, from which we have to show φ(c). From the last assumption, we get by (⋆):
u = j(pd(a,b,c),λy.f(a,b,y)). Uniqueness of generators and clause (5) of C(ψφ(a, b, ·), u) yield
∀x∈˙ pd(a,b,c).ψφ(a,b,f(a,b,x))). By the definition of ψφ, this reads
∀x∈˙ pd(a,b,c).∀y.Acc(a,b,y)∧f(a,b,y)=f(a,b,x)→φ(y). Choosing x for y, we get
∀x∈˙ pd(a,b,c).Acc(a,b,x)→φ(x). Assuming Acc(a, b, c), we obtain by (A) that
holds. So we have
∀x∈˙ pd(a,b,c).Acc(a,b,x) ∀x∈˙ pd(a,b,c).φ(x).
But this is the premiss of the assumption Closed(a, b, φ) and we get A(c). Thus, (B) is proven.
To prove the second assertion (Acc.2), we now take an arbitrary formula φ(x) and assume Closed(a,b,φ) and Acc(a,b,x). For the first assumption (B) yields
∀y.C(ψφ(a, b, ·), y) → ψφ(a, b, y).