Page 115 - Textos de Matemática Vol. 40

3.2. Truth theories in the partial setting 103
In contrast to FON, the truth predicate can be total in FDA. That is, the assumption ∀x.P(x) is consistent with FDA. This can be shown by an embedding of FDA + ∀x.P(x) + (AllN) within the theory BON + (AllN) extended by the recursion theoretic functional E#0 , cf. Section 1.6.
Proposition 3.2.7. FDA + ∀x.P(x) + (AllN) can be embedded within BON(E#0 ) + (AllN).
Proof. We translate T(t) by t⋆ ̸= 0, choose for the dotted constants the following interpretations
=˙⋆ := λx,y.dN10xy, N˙⋆ := λx.1,
¬˙⋆ := λx.dN10x0, ∧˙⋆ := λx,y.dN0yx0,
∀˙⋆ := λf.E#0 f, T˙⋆ := λx.x,
and extend ·⋆ in the straightforward way to all formulae. The verification of the axioms of FDA is˙done by a simple calculation, in which the use of E#0 in the interpretation of ∀ is crucial. As an example we present the axiom II.(9) for the existential quantification:
(∃x.T(¬˙ (f x)))⋆
↔ ∃x.(¬˙ (f x))⋆ ̸= 0
↔ ∃x.dN 10(f x)0 ̸= 0
↔ ∃x.fx=0
↔ E #0 f = 0
↔ (∀˙f)⋆=0
↔ dN10(∀˙f)⋆0̸=0
↔ ¬˙⋆(∀˙f)⋆̸=0
↔ T(¬˙(∀˙f))⋆ ⊣
With Theorem 1.7.24 about the proof-theoretic strength of BON(E#0 ) + (F-IN), which holds also in the presence of (AllN), we get:
Proposition 3.2.8. ID1 ≡ FDA + (AllN) + (F-IN) ≡ FDA + (AllN) + ∀x.P(x) + (F-IN) .
The usual paradoxes in truth theories, like the liar, are avoided by the logic of partial terms. So it is possible to define terms t such that FDA proves ¬T(t) ∧ ¬T(¬˙ t), for instance t := rec (λf, x.¬˙ (f x)) 0. But by ∀x.P(x) we get immediately ¬ t ↓.