Page 114 - Textos de Matemática Vol. 40
P. 114
102 Chapter 3. Truth Theories
Proof. The proof is by induction on the build up of weakly T-positive formulae and we look at the case of disjunctions φ ∨ ψ ≡ ¬(¬φ ∧ ¬ψ). Just in the same
˙
way as in the previous Lemma, we get the equivalence of T(¬(¬φ ∧ ¬ψ)) with
˙
T(¬¬φ)∨T(¬¬ψ). Axiom II.(5) and the induction hypothesis yield immediately
˙
φ∨ψ. ⊣
Like in FON this Proposition yields an abstraction principle t ∈ {x|φ} ↔ φ[t/x] for weakly T-positive formulae φ in FDA+(AllN), if we set {x|φ} := λx.φ˙ and t ∈ s := T(s t).
To embed ID1 within FDA + (AllN) + (F-IN) like in FON + (F-IN), we have to show first that the positive arithmetical operator forms φ(P, x) can be translated by weakly T-positive formulae of LFd . The canonical embedding of PA within BON + (F-IN), cf. [FJ93, Section 5], guarantees that all translated terms belong to N and are defined. If we use the negation normal form of a formula of ID1 for its translation, subformulae of the form ¬t = s are the only prime formulae which are not directly weakly T-positive. So we translate them by ∃x,y.t = x ∧ s = y ∧ ¬x = y. With this modification the translation of a positive arithmetical operator form becomes weakly T-positive in FDA.
Proposition 3.2.6. ID1 can be embedded within FDA + (AllN) + (F-IN) .
Proof. We have to check the fixed point axioms only, and like in FON we in- terpret the fixed point constants as the recursion theoretic fixed point of the
appropriate functional: with
Pφ(t) := T(pφ t)
˙
pφ :=rec(λp,x.φ(T(p·),x)).
T(pφ x)
˙
˙
≃ φ(T(p ·), x)[pφ /p].
The Recursion Theorem yields the partial equality pφ x
Since the term pφ is defined and the translation of the arithmetical operator form φ(Pφ,x) is a weakly T-positive formula, the previous Lemma and Proposition allow to verify the fixed point axiom on the same lines like in FON:
Pφ(x) ↔
↔ T(φ(T(p ·), x)[pφ /p])
˙
↔ T(φ(T(pφ ·), x))
↔ φ(T(pφ ·), x)
↔ φ(Pφ,x).
So the fixed point axioms of ID1 are verified. ⊣