Page 101 - Textos de Matemática Vol. 40

Chapter 3
Truth Theories
In alternative to explicit mathematics we may introduce a notion of types (sets, classes) by use of truth theories over the applicative theories.
Ordinary truth theories are discussed at length, both from a philosophical point of view as well as from a mathematical one, following the seminal paper of Tarski [Tar36, Tar56]. In particular, Kripke’s general analysis of truth in [Kri75] was highly influential. A very good overview of the combination of different properties of formalized proof predicates over Peano Arithmetic and its proof-theoretic implications may be found in Friedman and Sheard [FS82]. In view of our later discussion of universes in truth theories of applicative theories, we also like to mention the studies of iteration of proof predicates, which allow to deal with negative truth on one level as positive truth on the next level, cf. [Tar36, Tar56, Fef91b, Hal96].
In [Bee85], Beeson introduces a truth theory for applicative theories by adding a truth predicate T and appropriate new constants. He shows that such a truth theory is an axiomatic counterpart of Aczel’s Frege structures. Going back to the prior work of Scott [Sco75], they are introduced as a semantical concept by Aczel to define a notion of set by means of a partial truth predicate, [Acz80].
Considering Frege’s well-known, inconsistent formal system Grundgesetze der Arithmetik [Fre93, Fre03], usually, the unrestricted comprehension scheme is held responsible for the inconsistency. Thus, in most of the later formal approaches, the comprehension scheme is restricted. In contrast, Aczel still allows unrestricted comprehension, but the element relation, which is defined in terms of the truth predicate, becomes partial. In the formal definition, he defines proposition and truth simultaneously as fixed points of appropriate operator forms.
By adding predicates for propositions and truth in the applicative frame- work, Beeson gives an axiomatization of Frege structures. He shows that the resulting theory has the proof-theoretic strength of the theory EETJ + (F-IN) of
89