Page 119 - Textos de Matemática Vol. 40

3.2. Truth theories in the partial setting 107
axiom I.(2) can be applied and we get ¬(val (λy.s)[t/x] ↓), what is equivalent to ˙
¬ s[t/x] ↓. On the same lines we can trace back, and get T(¬ s[t/x] ↓). ⊣ For the following Theorem let T-positiveness be defined like in FON, in-
cluding the additional prime formulae t ↓ and ¬ t ↓. Proposition 3.2.13. If φ is T-positive then
FPA ⊢ T(φ˙) ↔ φ.
Proof. The statement is provable by induction on φ. We present the cases of negated existence and disjunction where the use of pointers is crucial.
˙ ˙
T(¬ t ↓) is by definition T(¬˙ ((λy.t) ↓)), y ̸∈ FV(t). Axiom I.(2) yields
¬(val (λy.t) ↓), which is equivalent to ¬ t ↓.
˙ ˙ ˙ ˙ ˙
T(φ ∨ ψ) ≡ T(¬(¬φ ∧ ¬ψ)) is by definition T(¬˙ ((λy. ¬φ ) ∧ (λy. ¬ψ ))),
˙
y ̸∈ FV(¬φ,¬ψ). So y does not occur in ¬φ and ¬ψ, such that both
˙
λ-terms are constant functions and we can apply axiom II.(9) which yields
˙ ˙ ˙ T(¬˙ (val (λy. ¬φ ))) ∨ T(¬˙ (val (λy. ¬ψ ))). This is equivalent to T(¬˙ ( ¬φ )) ∨
˙ ˙
T(¬˙ ( ¬ψ )) and axiom II.(7) yields T(φ˙ ) ∨ T(ψ). ⊣
Again, this Proposition allows to introduce a notion of abstraction t ∈ {x|φ} ↔ φ[t/x] for T-positive formulae φ in FPA using {x|φ} := λx.φ˙, and t ∈ s := T(s t).
Proposition 3.2.14. ID1 can be embedded within FPA + (F-IN) .
The proof is exactly the same like that for the embedding of ID1 within FON+(F-IN) in Proposition 3.1.9. As for FDA, the previous Lemma and Propo- sition guarantee that all steps of the proof can be translated into FPA + (F-IN).
Together with the equivalence of FPA + (Tot) and FON we get as a Corol- lary:
Proposition3.2.15. ID1 ≡FPA+(F-IN).
As for FDA for FPA, too, the question arises whether ∀x.P(x) is consis- tent. This question is still open, but we can prove that a recursion theoretical interpretation as presented for FDA will fail.
Proposition 3.2.16. For all closed terms t and s of LFp the theory FPA+(AllN)+ ∀x.T(x) ↔ t x = s is inconsistent.