Page 148 - Textos de Matemática Vol. 40
P. 148
136 Chapter 3. Truth Theories
For the second assertion, we assume Pφ(x), i.e., ∀z.Closφ(T(z ·)) → T(z x). ˙ ˙ ˙
By substituting λx.ψ′(x) for z, we get Closφ(T(ψ′(·))) → T(ψ′(x)). Lemma ˙
3.5.6.2 yields T(ψ′(x)) and with axiom T-out, we get ψ′(x), i.e., Closφ(ψ) → ψ(x), or, in other words,
(∀y.φ(ψ, y) → ψ(y)) → ψ(x).
Thus, the second assertion is shown. ⊣
By use of this Proposition, we easily may extend the translation ·N of the language of Peano Arithmetic into Lp to a translation of LID into LFt which verifies the fixed point axioms. Induction on the natural number of ID1 is obviously included in (LFt -IN) and, by Proposition 3.5.2, also in (T-IN). Thus, we have:
Theorem 3.5.8. There exists a translation ·N of LID into LFt such that ID1 ⊢φ ⇒ SON+(T-IN)⊢φN.
