Page 117 - Textos de Matemática Vol. 40

3.2. Truth theories in the partial setting 105 I. Closure under prime formulae of BON.
(1) Cf(x) → (valx ↓ ↔ T(x↓˙)),
(2) Cf(x) → (¬(valx ↓) ↔ T(¬˙ (x↓˙))),
(3) Cf(x)∧Cf(y)→(valx=valy↔T(x=˙ y)),
(4) Cf(x) ∧ Cf(y) → (¬val x = val y ↔ T(¬˙ (x =˙ y))), (5) Cf (x) → (N(val x) ↔ T(N˙ x)),
(6) Cf (x) → (¬N(val x) ↔ T(¬˙ (N˙ x))).
II. Closure under composed formulae.
(7) T(x) ↔ T(¬˙ (¬˙ x)),
(8) Cf(x) ∧ Cf(y) → (T(val x) ∧ T(val y) ↔ T(x ∧˙ y)),
(9) Cf(x) ∧ Cf(y) → (T(¬˙ (val x)) ∨ T(¬˙ (val y)) ↔ T(¬˙ (x ∧˙ y))),
(10) (∀x.T(f x)) ↔ T(∀˙ f),
(11) (∃x.T(¬˙ (f x))) ↔ T(¬˙ (∀˙ f)).
III. Consistency.
(12) ¬(T(x) ∧ T(¬˙ x)).
As for FON, by defining T˙ as λx.x we have as (trivial form of) self-reference the following two equivalence:
Self-reference.
T(x) ↔ T(T˙ x),
T(¬˙ x) ↔ T(¬˙ (T˙ x)),
It can be shown that our approach is compatible with the total version, in the sense that FPA + (Tot) is proof theoretically equivalent to FON. Although the theories are not as trivially equivalent as BON + (Tot) and TON, there are interpretations of each in the other. For the embedding of FPA within FON we havetoaddthefunctionvalinfrontoftheargumentsof=˙,N˙,and∧˙,i.e.,
=˙ ⋆ := λx, y.(val x) =˙ (val y), N˙ ⋆ := λx.N˙ (val x),
∧˙ ⋆ := λx, y.(val x) ∧˙ (val y),
and interpret definedness by an arbitrary true formula. For the interpretation ofFONinFPA+(Tot)we“shift”theargumentsof=˙,N˙,and∧˙toconstant functions by prefixing with k, i.e.,
=˙ + := λx,y.(kx)=˙ (ky), N˙ + := λx.N˙ (k x),
∧˙+ := λx,y.(kx)∧˙ (ky).