Page 118 - Textos de Matemática Vol. 40

106 Chapter 3. Truth Theories Proposition 3.2.10. There are interpretations ·∗ of LFp in LFt and ·+ of LFt in
LFp such that
1. FPA⊢φ⇒FON⊢φ∗,
2. FON⊢ψ⇒FPA+(Tot)⊢ψ+.
For the representation of the formulae in FPA we have to replace the sub- terms t and s of the prime formulae t ↓, N(t), and t = s, which may be undefined, by the corresponding pointer. That means, we “shift” t and s to the constant functions λy.t and λy.s, respectively (y ̸∈ FV(t, s)). In the same way we “shift” the subformulae of conjunctions to overcome the strictness problem for disjunc- tions.
Definition 3.2.11. Inductively we assign a term φ˙ to every formula φ of LFp (y ̸∈ FV(t, s, φ, ψ)):
˙
t↓ :=
˙
Nt :=
˙ t=s :=
˙ T(t) :=
˙
¬φ :=
˙ φ∧ψ :=
˙ ∀x.φ :=
˙ (λy.t)↓
˙ N(λy.t)
(λy.t)=˙(λy.s) ˙
Tt ¬˙φ˙
˙˙ (λy.φ˙)∧(λy.ψ)
˙
∀ (λx.φ˙ )
Like in FDA our definition of φ˙ makes substantial use of λ-abstraction and therefore it is not compatible with substitution. Still, we can prove that truth is preserved under substitutions of defined terms:
Lemma 3.2.12. For all closed terms t and formulae φ of LFp the following holds: ˙
FPA ⊢ t ↓ → (T(φ˙[t/x]) ↔ T(φ[t/x])).
Proof. The proof is analogous to the one of Lemma 3.1.3 and 3.2.4 by induction
on the build up of φ. Assuming that t is defined, we present the case of the
negated existence.9
˙ ˙
T((¬ s ↓)[t/x]) is by definition T(¬˙ ((λy.s)[t/x] ↓)), y ̸∈ FV(t, s). Because the substitution does not effect the fact that (λy.s)[t/x] is a constant function,
9The premiss t ↓ is mainly needed in the induction step for existential quantification, where we would have the same problem with undefined terms t like in the proof of Lemma 3.2.4.