Page 116 - Textos de Matemática Vol. 40

104 Chapter 3. Truth Theories
More general, we may ask which conditions hold for the existence of terms representing formulae in FDA. By classical logic we get that =˙ and N˙ are total in the sense that ∀x,y.(x=˙ y) ↓∧(N˙ x) ↓ holds. If we add ∀x.P(x) we have also ∀x,y.(T˙ x) ↓∧(x∧˙ y) ↓∧(¬˙ x) ↓. The existence of x∧˙ y follows by case- distinction on T(¬˙ x) ∨ T(¬˙ y) ∨ (T(x) ∧ T(y)). In the first two cases we have T(¬˙ (x ∧˙ y)), in the last one T(x ∧˙ y). Now strictness implies (x ∧˙ y) ↓.
However, for the universal quantification we can prove:
Proposition3.2.9. FDA+∀x.P(x)+∀f.(∀˙f)↓isinconsistent.
Proof. Consider the function λx.t, with t := rec (λf, x.¬˙ (f x)) 0. In the presence of ∀x.P(x) we get ∀x.¬ (λx.t) x ↓. Since we have (∀˙ (λx.t)) ↓, ∀x.P(x) implies T(∀˙ (λx.t)) ∨ T(¬˙ (∀˙ (λx.t)). The axioms for ∀˙ yield (∀x.T(t)) ∨ ∃x.T(¬˙ t) which contradicts by strictness the fact that t is not defined. ⊣
3.2.2 Using pointers
In a second approach we will solve the problems of strictness by use of pointers. Therefore we associate with each (possibly undefined) term t an object t¯ which is always defined and allows to reconstruct t itself. So t¯ plays the role of a pointer to t. It is easy to find a proper candidate for t¯ in BON: the constant function λy.t (with y ̸∈ FV(t)) is always defined and we can reconstruct t trivially by applying it to 0. In contrast to the total case, where a map t → t¯ is definable within the theory as λf.kf, in the partial setting, the definition uses induction on the formation of terms. Thus the map t → t¯ becomes a meta theoretical operation. Fortunately we do not need the operation at the object level. Instead of “shifting” the terms t to the pointer t¯ in the formalization, we start with the pointers as constant functions and re-evaluate the value by applying 0. Then the truth condition for negated existence, which is directly expressible by the schema ¬(t ↓) ↔ T(¬˙ (t¯↓˙)), can be written as the axiom Cf (x) → (¬((val x) ↓) ↔ T(¬˙ (x ↓˙ ))) using the abbreviations
Cf(t) := ∀x,y.tx ≃ ty and val := λx.x0.
We define the theory FPA of Frege structures for BON as follows.
The language LFp of FPA is the language Lp of BON extended by the new relation symbol T and new individual constants ↓˙ , =˙ , N˙ , ¬˙ , ∧˙ and ∀˙ .
The axioms of FPA are the axioms of BON extended to the new language; the axioms about truth differ from those of FON by the use of pointers for the prime formulae of BON and the closure under conjunction and disjunction:8
8In [Kah97a, Section 2.2.2] we already introduced a theory called FPA; however, the ax- iomatization given there, which does not include the use of pointers in the closure under conjunction, causes problems in the treatment of disjunction.