Page 110 - Textos de Matemática Vol. 40

98 Chapter 3. Truth Theories 3.1.6 Discussion
Here we shortly discuss our definition of Frege structures in comparison with other approaches.
First, in contrast to Beeson, we have defined the truth theory over the total version of applicative theories, because of a subtle problem with strictness in the partial setting. This problem is discussed in detail in the next Section.
Secondly, Aczel’s original definition of Frege structures (and its formal- ization by Beeson) presupposed an (additionally axiomatized) notion of propo- sition [Acz77, Acz80, Bee85]. Then the truth axioms were applicable only for arguments which were propositions. We follow the more general axiomatization as given by Flagg and Myhill [FM87a, FM87b], whereby the notion of propo- sition is defined in terms of the truth predicate. In fact, this generalization is necessary to define fixed points in FON.
Based on the defined notion of sets, one can deal with (the total version of) EETJ together with the induction principles, cf. [Can93, Can96]. In contrast, an embedding of Frege structures within explicit mathematics is not known, as well as a direct definition of fixed points of arithmetical operator forms within EETJ.
Hayashi and Kobayashi gave in [HK95] a version of Frege structures which is exactly tuned to be equivalent to a version of explicit mathematics. This formalization also uses propositions.
The embedding of ID1 within FON + (LFt -IN) makes essential use of the Recursion, or Fixed Point Theorem, on the term level, cf. Proposition 1.2.2. Since there is no natural way to define least fixed points on the term level, we cannot expect to define a similar truth theory which allows an embedding of ID1. For an alternative approach to introduce a theory of the strength of ID1, see below Section 3.5.
Finally, we would like to mention the work of Smith who used a theory of Frege structures to give a semantics for Martin-Lo¨f’s type theory, [Smi78, Acz80, Smi84].
3.2 Truth theories in the partial setting
If we want to define Frege structures for partial applicative theories, problems arise with possibly undefined terms. The first attempt would be to introduce in FON (now formulated over BON) a further constant ↓˙ and to axiomatize truth for negated existence in the following way:
¬(x ↓) ↔ T(¬˙ (x ↓˙ )).
The Section on truth theories in the partial setting is based on [Kah99].