Page 102 - Textos de Matemática Vol. 40

90 Chapter 3. Truth Theories
explicit mathematics, discussed in the previous Chapter. Flagg and Myhill have investigated Frege structures in a more general perspective. In particu- lar, they give up the primitive notion of proposition, but define it in terms of truth, [FM87a, FM87b]. The most comprehensive study of truth theories on an applicative basis may be found in Cantini’s monograph [Can96], see also [Can93].
Truth theories in the applicative context offer two distinguished features, namely “representation of formulae without G¨odelization” and “abstraction”. The first one refers to the possibility to formalize the truth theory without a G¨odelization of the language. Instead, we will use new constants to represent formulae on the term level. With “abstraction” we refer to the possibility to introduce a notion of classes (sets, types) in this theory—which, in fact, is still a first-order theory. It turns out that we optain theories of strong syntactic expressiveness, allowing, for example, the syntactical embedding of fixed point theories.
Due to a problem with strictness, it is complicated to formulate a (full) truth theory over partial applicative theories. Therefore, we will start with the presentation of truth theories for the total case. Afterwards, in Section 3.2 we will discuss in detail the partial case and present some possible solutions.
Finally we study two different possiblities to get stronger truth theories with respect to the proof-theoretic strength (again in the total case). On the one hand, we can define universes corresponding to levels of truth as they are known from ordinary truth theories. On the other hand, we can replace the truth axioms for Frege structures by truth axioms for supervaluation. This is a non compositional concept of truth, introduced by van Fraassen [vF68, vF70].
3.1 Truth theories in the total setting
In this Section we introduce a truth theory (Frege Structures) for total applica- tive theories and sketch the central results. There are several variant axiom- atizations. We will follow essentially the theory MF− of [Can96] (or NMT of [Can93]). The axiomatizations in [Bee85] and [HK95], for instance, presuppose a notion of proposition, which we, in contrast, define in terms of the truth pred- icate. The definition given here, is in some sense the most general one. The relation between the various variants, which may be found in the literature, is discussed below in Section 3.1.6.
3.1.1 The theory FON
The language LFt of FON is the language of TON extended by the new relation
symbol T (truth) and new individual constants =˙ , N˙ , ¬˙ , ∧˙ , and ∀˙ .1
1Cantini introduces for his theory MF− these constants as abbreviated terms, cf. [Can96, Def. 7.1].