Page 111 - Textos de Matemática Vol. 40

3.2. Truth theories in the partial setting 99 But this axiom would be meaningless, since in the logic of partial terms variables
are always defined. The corresponding axiom scheme: ¬(t ↓) ↔ T(¬˙ (t↓˙))
violates the strictness axiom (S1) if there is an undefined term t, or in other words, it proves (Tot).
This problem was overlooked by Beeson in [Bee85] where he worked in a partial framework. It is not clear how one can prove his Proposition XVII.9.1, claiming the embedding of elementary comprehension within Frege structures, for the case of prime formulae containing possibly undefined terms.
If we try to preserve the embedding of ID1 within Frege structures we have also another problem concerning disjunctions. Consider the T-positive formula 0 = 0∨T(uv). If we use the representation 0=˙ 0∨˙ T˙ (uv), i.e., ¬˙ (¬˙ (0=˙ 0)∧˙ ¬˙ (T˙ (u v))), we could use an axiom like II.(7) only if T˙ (u v) is defined. In general we cannot prove this for the interpretation of the fixed point constants.
In the following we will give two different approaches to define Frege struc- tures in a partial setting. In the first one we simply ignore undefinedness in the truth definition yielding a theory with total truth. For the second one we in- troduce a certain notion of pointer to avoid strictness problems. This approach turns out to be closely related to the concept of promises in scheme which is used to introduce streams in strict functional programming languages.
3.2.1 Ignoring undefined terms
For the first approach we just use the axioms of truth of FON but now over BON. Since the variables used in these axioms can be substituted by defined terms only, we do not obtain a theory of truth for the whole theory BON, we do, however, for its “defined” part. To prove the embedding of ID1 within this theory we have to add the axiom (AllN) which allows to define a representation of disjunctions avoiding the problem described above. This theory allows the truth predicate to be total, i.e., ∀x.P(x) is consistent. In the second approach we introduce a notion of pointer to replace possibly undefined terms by defined ones. Axiomatizing truth by use of these pointers we get a truth theory for the whole theory BON and, again, we can embed the theory ID1.
For FDA (Frege structures for the defined part of partial applicative theo- ries) we extend BON in the same way as TON for FON.
The language LFd of FDA is the language Lp of BON extended by the new relation symbol T and new individual constants =˙ , N˙ , ¬˙ , ∧˙ , ∀˙ and T˙ .3
The axioms of FDA are the axioms of BON extended to the new language plus the additional ones of FON (see above).
3For the following embedding of ID1, the constant ∧˙ and the axioms II.(6) and II.(7) are superfluous, since we will represent conjunctions by use of ∀˙ (see below). For uniformity reasons, however, and to state the following remark without complications, we keep ∧˙ in FDA.