Axiomatic Theories of Truth

First published Mon Dec 26, 2005; substantive revision Mon Nov 4, 2013

An axiomatic theory of truth is a deductive theory of truth as a primitive undefined predicate. Because of the liar and other paradoxes, the axioms and rules have to be chosen carefully in order to avoid inconsistency. Many axiom systems for the truth predicate have been discussed in the literature and their respective properties been analysed. Several philosophers, including Donald Davidson and many deflationists, have endorsed axiomatic theories of truth in their accounts of truth. The logical properties of the formal theories are relevant to various philosophical questions, such as questions about the ontological status of properties, Gödel's theorems, truth-theoretic deflationism, eliminability of semantic notions and the theory of meaning.

1. Motivations

There have been many attempts to define truth in terms of correspondence, coherence or other notions. However, it is far from clear that truth is a definable notion. In formal settings satisfying certain natural conditions, Tarski's theorem on the undefinability of the truth predicate shows that a definition of a truth predicate requires resources that go beyond those of the formal language for which truth is going to be defined and thus definitional approaches to truth have to fail. By contrast, the axiomatic approach does not presuppose that truth can be defined. Instead, a formal language is expanded by a new primitive predicate for truth, and axioms for that predicate are then laid down. This does not preclude the possibility that the truth predicate is definable, although in many cases it can be shown that the truth predicate is not definable.

In semantic theories of truth (e.g., Tarski 1935, Kripke 1975), in contrast, a truth predicate is defined for a language, the so-called object language. This definition is carried out in a metalanguage or metatheory, which is typically taken to include set theory or at least another strong theory or expressively rich interpreted language. Tarski's theorem on the undefinability of the truth predicate shows that, given certain general assumptions, the resources of the metalanguage or metatheory must go beyond the resources of the object-language. So semantic approaches usually necessitate the use of a metalanguage that is more powerful than the object-language for which it provides a semantics.

As with other formal deductive systems, axiomatic theories of truth can be presented within very weak logical frameworks. These frameworks require very few resources, and in particular, avoid the need for a strong metalanguage and metatheory.

Formal work on axiomatic theories of truth has helped to shed some light on semantic theories of truth. For instance, it has yielded information on what is required of a metalanguage that is sufficient for defining a truth predicate. Semantic theories of truth, in turn, provide one with the theoretical tools needed for investigating models of axiomatic theories of truth and with motivations for certain axiomatic theories. Thus axiomatic and semantic approaches to truth are intertwined.

This entry outlines the most popular axiomatic theories of truth and mentions some of the formal results that have been obtained concerning them. We give only hints as to their philosophical applications.

1.1 Truth, properties and sets

Theories of truth and predication are closely related to theories of properties and property attribution. To say that an open formula φ(x) is true of an individual a seems equivalent (in some sense) to the claim that a has the property of being such that φ (this property is signified by the open formula). For example, one might say that ‘x is a poor philosopher’ is true of Tom instead of saying that Tom has the property of being a poor philosopher. Quantification over definable properties can then be mimicked in a language with a truth predicate by quantifying over formulas. Instead of saying, for instance, that a and b have exactly the same properties, one says that exactly the same formulas are true of a and b. The reduction of properties to truth works also to some extent for sets of individuals.

There are also reductions in the other direction: Tarski (1935) has shown that certain second-order existence assumptions (e.g., comprehension axioms) may be utilized to define truth (see the entry on Tarski's definition of truth). The mathematical analysis of axiomatic theories of truth and second-order systems has exhibited many equivalences between these second-order existence assumptions and truth-theoretic assumptions.

These results show exactly what is required for defining a truth predicate that satisfies certain axioms, thereby sharpening Tarski's insights into definability of truth. In particular, proof-theoretic equivalences described in Section 3.3 below make explicit to what extent a metalanguage (or rather metatheory) has to be richer than the object language in order to be able to define a truth predicate.

The equivalence between second-order theories and truth theories also has bearing on traditional metaphysical topics. The reductions of second-order theories (i.e., theories of properties or sets) to axiomatic theories of truth may be conceived as forms of reductive nominalism, for they replace existence assumptions for sets or properties (e.g., comprehension axioms) by ontologically innocuous assumptions, in the present case by assumptions on the behaviour of the truth predicate.

1.2 Truth and reflection

According to Gödel's incompleteness theorems, the statement that Peano Arithmetic (PA) is consistent, in its guise as a number-theoretic statement (given the technique of Gödel numbering), cannot be derived in PA itself. But PA can be strengthened by adding this consistency statement or by stronger axioms. In particular, axioms partially expressing the soundness of PA can be added. These are known as reflection principles. An example of a reflection principle for PA would be the set of sentences BewPA(⌈φ⌉) → φ where φ is a formula of the language of arithmetic, ⌈φ⌉ a name for φ and BewPA(x) is the standard provability predicate for PA (‘Bew’ was introduced by Gödel and is short for the German word ‘beweisbar’, that is, ‘provable’).

The process of adding reflection principles can be iterated: one can add, for example, a reflection principle R for PA to PA; this results in a new theory PA+R. Then one adds the reflection principle for the system PA+R to the theory PA+R. This process can be continued into the transfinite (see Feferman 1962 and Franzén 2004).

The reflection principles express—at least partially—the soundness of the system. The most natural and full expression of the soundness of a system involves the truth predicate and is known as the Global Reflection Principle (see Kreisel and Lévy 1968). The Global Reflection Principle for a formal system S states that all sentences provable in S are true:

∀x(BewS(x) → Tx)

BewS(x) expresses here provability of sentences in the system S (we omit discussion here of the problems of defining BewS(x)). The truth predicate has to satisfy certain principles; otherwise the global reflection principle would be vacuous. Thus not only the global reflection principle has to be added, but also axioms for truth. If a natural theory of truth like T(PA) below is added, however, it is no longer necessary to postulate the global reflection principle explicitly, as theories like T(PA) prove already the global reflection principle for PA. One may therefore view truth theories as reflection principles as they prove soundness statements and add the resources to express these statements.

Thus instead of iterating reflection principles that are formulated entirely in the language of arithmetic, one can add by iteration new truth predicates and correspondingly new axioms for the new truth predicates. Thereby one might hope to make explicit all the assumptions that are implicit in the acceptance of a theory like PA. The resulting theory is called the reflective closure of the initial theory. Feferman (1991) has proposed the use of a single truth predicate and a single theory (KF), rather than a hierarchy of predicates and theories, in order to explicate the reflective closure of PA and other theories. (KF is discussed further in Section 4.3 below.)

The relation of truth theories and (iterated) reflection principles also became prominent in the discussion of truth-theoretic deflationism (see Tennant 2002 and the follow-up discussion).

1.3 Truth-theoretic deflationism

Many proponents of deflationist theories of truth have chosen to treat truth as a primitive notion and to axiomatize it, often using some version of the T-sentences as axioms. T-sentences are equivalences of the form T ⌈φ⌉ ↔ φ, where T is the truth predicate, φ is a sentence and ⌈φ⌉ is a name for the sentence φ. (More refined axioms have also been discussed by deflationists.) At first glance at least, the axiomatic approach seems much less ‘deflationary’ than those more traditional theories which rely on a definition of truth in terms of correspondence or the like. If truth can be explicitly defined, it can be eliminated, whereas an axiomatized notion of truth may and often does come with commitments that go beyond that of the base theory.

If truth does not have any explanatory force, as some deflationists claim, the axioms for truth should not allow us to prove any new theorems that do not involve the truth predicate. Accordingly, by Horsten (1995), Shapiro (1998) and Ketland (1999) have suggested that a deflationary axiomatization of truth should be at least conservative. The new axioms for truth are conservative if they do not imply any additional sentences (free of occurrences of the truth-predicate) that aren't already provable without the truth axioms. Thus a non-conservative theory of truth adds new non-semantic content to a theory and has genuine explanatory power, contrary to many deflationist views. Certain natural theories of truth, however, fail to be conservative (see Section 3.3 below, Field 1999 and Shapiro 2002 for further discussion).

According to many deflationists, truth serves merely the purpose of expressing infinite conjunctions. It is plain that not all infinite conjunctions can be expressed because there are uncountably many (non-equivalent) infinite conjunctions over a countable language. Since the language with an added truth predicate has only countably many formulas, not every infinite conjunction can be expressed by a different finite formula. The formal work on axiomatic theories of truth has helped to specify exactly which infinite conjunctions can be expressed with a truth predicate. Feferman (1991) provides a proof-theoretic analysis of a fairly strong system. (Again, this will be explained in the discussion about KF in Section 4.3 below.)

2. The base theory

2.1 The choice of the base theory

In most axiomatic theories, truth is conceived as a predicate of objects. There is an extensive philosophical discussion on the category of objects to which truth applies: propositions conceived as objects that are independent of any language, types and tokens of sentences and utterances, thoughts, and many other objects have been proposed. Since the structure of sentences considered as types is relatively clear, sentence types have often been used as the objects that can be true. In many cases there is no need to make very specific metaphysical commitments, because only certain modest assumptions on the structure of these objects are required, independently from whether they are finally taken to be syntactic objects, propositions or still something else. The theory that describes the properties of the objects to which truth can be attributed is called the base theory. The formulation of the base theory does not involve the truth predicate or any specific truth-theoretic assumptions. The base theory could describe the structure of sentences, propositions and the like, so that notions like the negation of such an object can then be used in the formulation of the truth-theoretic axioms.

In many axiomatic truth theories, truth is taken as a predicate applying to the Gödel numbers of sentences. Peano arithmetic has proved to be a versatile theory of objects to which truth is applied, mainly because adding truth-theoretic axioms to Peano arithmetic yields interesting systems and because Peano arithmetic is equivalent to many straightforward theories of syntax and even theories of propositions. However, other base theories have been considered as well, including formal syntax theories and set theories.

Of course, we can also investigate theories which result by adding the truth-theoretic axioms to much stronger theories like set theory. Usually there is no chance of proving the consistency of set theory plus further truth-theoretic axioms because the consistency of set theory itself cannot be established without assumptions transcending set theory. In many cases not even relative consistency proofs are feasible. However, if adding certain truth-theoretic axioms to PA yields a consistent theory, it seems at least plausible that adding analogous axioms to set theory will not lead to an inconsistency. Therefore, the hope is that research on theories of truth over PA will give an some indication of what will happen when we extend stronger theories with axioms for the truth predicate.

2.2 Notational conventions

For the sake of definiteness we assume that the language of arithmetic has exactly ¬, ∧ and ∨ as connectives and ∀ and ∃ as quantifiers. It has as individual constants only the symbol 0 for zero; its only function symbol is the unary successor symbol S; addition and multiplication are expressed by predicate symbols. Therefore the only closed terms of the language of arithmetic are the numerals 0, S(0), S(S(0)), S(S(S(0))), ….

The language of arithmetic does not contain the unary predicate symbol T, so let LT be the language of arithmetic augmented by the new unary predicate symbol T for truth. If φ is a sentence of LT, ⌈φ⌉ is a name for φ in the language LT; formally speaking, it is the numeral of the Gödel number of φ. In general, Greek letters like φ and ψ are variables of the metalanguage, that is, the language used for talking about theories of truth and the language in which this entry is written (i.e., English enriched by some symbols). φ and ψ range over formulas of the formal language LT.

In what follows, we use small, upper case italic letters like A, B,… as variables in LT ranging over sentences (or their Gödel numbers, to be precise). Thus ∀A(…A…) stands for ∀x(SentT(x) → …x…), where SentT(x) expresses in the language of arithmetic that x is a sentence of the language of arithmetic extended by the predicate symbol T. The syntactical operations of forming a conjunction of two sentences and similar operations can be expressed in the language of arithmetic. Since the language of arithmetic does not contain any function symbol apart from the symbol for successor, these operations must be expressed by sutiable predicate expressions. Thus one can say in the language LT that a negation of a sentence of LT is true if and only if the sentence itself is not true. We would write this as

∀A(T[¬A] ↔ ¬TA).

The square brackets indicate that the operation of forming the negation of A is expressed in the language of arithmetic. Since the language of arithmetic does not contain a function symbol representing the function that sends sentences to their negations, appropriate paraphrases involving predicates must be given.

Thus, for instance, the expression

∀A∀B(T[A ∧ B] ↔ (TA ∧ TB))

is a single sentence of the language LT saying that a conjunction of sentences of LT is true if and only if both sentences are true. In contrast,

T ⌈φ ∧ ψ⌉ ↔ (T ⌈φ⌉ ∧ T ⌈φ⌉)

is only a schema. That is, it stands for the set of all sentences that are obtained from the above expression by substituting sentences of LT for the Greek letters φ and ψ. The single sentence ∀A∀B(T[A ∧ B] ↔ (TA ∧ TB)) implies all sentences which are instances of the schema, but the instances of the schema do not imply the single universally quantified sentence. In general, the quantified versions are stronger than the corresponding schemata.

3. Typed theories of truth

In typed theories of truth, only the truth of sentences not containing the same truth predicate is provable, thus avoiding the paradoxes by observing Tarski distinction between object and metalanguage.

3.1 Definable truth predicates

Certain truth predicates can be defined within the language of arithmetic. Predicates suitable as truth predicates for sublanguages of the language of arithmetic can be defined within the language of arithmetic, as long as the quantificational complexity of the formulas in the sublanguage is restricted. In particular, there is a formula Tr0(x) that expresses that x is a true atomic sentence of the language of arithmetic, that is, a sentence of the form n=k, where k and n are identical numerals. For further information on partial truth predicates see, for instance, Hájek and Pudlak (1993), Kaye (1991) and Takeuti (1987).

The definable truth predicates are truly redundant, because they are expressible in PA; therefore there is no need to introduce them axiomatically. All truth predicates in the following are not definable in the language of arithmetic, and therefore not redundant at least in the sense that they are not definable.

3.2 The T-sentences

The typed T-sentences are all equivalences of the form T ⌈φ⌉ ↔ φ, where φ is a sentence not containing the truth predicate. Tarski (1935) called any theory proving these equivalences ‘materially adequate’. Tarski (1935) criticised an axiomatization of truth relying only on the T-sentences, not because he aimed at a definition rather than an axiomatization of truth, but because such a theory seemed too weak. Thus although the theory is materially adequate, Tarski thought that the T-sentences are deductively too weak. He observed, in particular, that the T-sentences do not prove the principle of completeness, that is, the sentence ∀A(TA ∨ T[¬A]) where the quantifier ∀A is restricted to sentences not containing T.

Theories of truth based on the T-sentences, and their formal properties, have also recently been a focus of interest in the context of so-called deflationary theories of truth. The T-sentences T ⌈φ⌉ ↔ φ (where φ does not contain T) are not conservative over first-order logic with identity, that is, they prove a sentence not containing T that is not logically valid. For the T-sentences prove that the sentences 0=0 and ¬0=0 are different and that therefore at least two objects exist. In other words, the T-sentences are not conservative over the empty base theory. If the T-sentences are added to PA, the resulting theory is conservative over PA. This means that the theory does not prove T-free sentences that are not already provable in PA. This result even holds if in addition to the T-sentences also all induction axioms containing the truth predicate are added. This may be shown by appealing to the Compactness Theorem again.

3.3 Compositional truth

As was observed already by Tarski (1935), the certain desirable generalizations don't follow from the T-sentences. For instance, together with reasonable base theories they don't imply that a conjunction is true if both conjuncts are true.

In order to obtain systems that also prove universally quantified truth-theoretic principles, one can turn the inductive clauses of Tarski's definition of truth into axioms. In the following axioms, AtomSentPA(⌈A⌉) expresses that A is an atomic sentence of the language of arithmetic, SentPA(⌈A⌉) expresses that A is a sentence of the language of arithmetic.

  1. ∀A(AtomSentPA(A) → (TA ↔ Tr0(A)))
  2. ∀A(SentPA(A) → (T[¬A] ↔ ¬TA))
  3. ∀A∀B(SentPA(A)  ∧ SentPA(B) → (T[A  ∧ B] ↔ (TA  ∧ TB)))
  4. ∀A∀B(SentPA(A)  ∧ SentPA(B) → (T[A ∨ B] ↔ (TA ∨ TB)))
  5. ∀A(v)(SentPA(∀vA) → (T[∀vA(v)] ↔ ∀xT[A(x)]))
  6. ∀A(v)(SentPA(∀vA) → (T[∃vA(v)] ↔ ∃xT[A(x)]))

Axiom 1 says that an atomic sentence of the language of Peano arithmetic is true if and only if it is true according to the arithmetical truth predicate for this language (Tr0 was defined in Section 3.1). Axioms 2–6 claim that truth commutes with all connectives and quantifiers. Axiom 5 says that a universally quantified sentence of the language of arithmetic is true if and only if all its numerical instances are true. Underlining the variable in square brackets indicates it is bound from the outside. More precisely, [A(x)] stands for the result of replacing the variable v in A(v) by the numeral of x. SentPA(∀vA) says that A(v) is a formula with at most v free (because ∀vA(v) is a sentence).

If these axioms are to be formulated for a language like set theory that lacks names for all objects, then axioms 5 and 6 require the use of a satisfaction relation rather than a unary truth predicate.

Axioms in the style of 1–6 above played a central role in Donald Davidson‘s theory of meaning and in several deflationist approaches to truth.

The theory given by all axioms of PA and Axioms 1–6 but with induction only for T-free formulae is conservative over PA, that is, it doesn't prove any new T-free theorems that not already provable in PA. However, not all models of PA can be expanded to models of PA + axioms 1–6. This follows from a result due to Lachlan (1981). Kotlarski, Krajewski, and Lachlan (1981) proved the conservativeness very similar to PA + axioms 1–6 by model-theoretic means. Although several authors, including Halbach (1999), claimed that this result is also finitarily provable, no such proof was available until Enayat & Visser (2013) and Leigh (2013).

Of course PA + axioms 1–6 is restrictive insofar as it does not contain the induction axioms in the language with the truth predicate. There are various labels for the system that is obtained by adding all induction axioms involving the truth predicate to the system PA + axioms 1–6: T(PA), PA(S) or PA + ‘there is a full inductive satisfaction class’. This theory is no longer conservative over its base theory PA. For instance one can formalise the soundness theorem or global reflection principle for PA, that is, the claim that all sentences provable in PA are true. The global reflection principle for PA in turn implies the consistency of PA, which is not provable in pure PA by Gödel's Second Incompleteness Theorem. Thus T(PA) is not conservative over PA. T(PA) is much stronger than the mere consistency statement for PA: T(PA) is equivalent to the second-order system ACA of arithmetical comprehension (see Takeuti 1987 and Feferman 1991). More precisely, T(PA) and ACA are intertranslatable in a way that preserves all arithmetical sentences. ACA is given by the axioms of PA with full induction in the second-order language and the following comprehension principle:

∃X∀y(y∈X ↔ φ(x))

where φ(x) is any formula (in which x may or may not be free) that does not contain any second-order quantifiers, but possibly free second-order variables. More precisely, quantification over sets can be defined in T(PA) as quantification over formulas with one free variable and membership as the truth of the formula as applied to a number.

Much stronger fragments of second-order arithmetic can be interpreted by type-free truth systems, that is, by theories of truth that prove not only the truth of arithmetical sentences but also the truth of sentences of the language LT with the truth predicate; see Section 4 below.

3.4 Hierarchical theories

The above mentioned theories of truth can be iterated by introducing indexed truth predicates. One adds to the language of PA truth predicates indexed by ordinals (or ordinal notations) or one adds a binary truth predicate that applies to ordinal notations and sentences. In this respect the hierarchical approach does not fit the framework outlined in Section 2, because the language does not feature a single unary truth predicate applying to sentences but rather many unary truth predicates or a single binary truth predicate (or even a single unary truth predicate applying to pairs of ordinal notations and sentences).

In such a language an axiomatization of Tarski's hierarchy of truth predicates can be formulated. On the proof-theoretic side iterating truth theories in the style of T(PA) corresponds to iterating elementary comprehension, that is, to iterating ACA. The system of iterated truth theories corresponds to the system of ramified analysis (see Feferman 1991).

Visser (1989) has studied non-wellfounded hierarchies of languages and axiomatizations thereof. If one adds the T-sentences Tn⌈φ⌉ ↔ φ to the language of arithmetic where φ contains only truth predicates Tk with k > n to PA, a theory is obtained that does not have a standard (ω-)model.

4. Type-free truth

The truth predicates in natural languages do not come with any ouvert type restriction. Therefore typed theories of truth (axiomatic as well as semantic theories) have been thought to be inadequate for analysing the truth predicate of natural language, although recently hierarchical theories have been advocated by Glanzberg (forthcoming) and others. This is one motive for investigating type-free theories of truth, that is, systems of truth that allow one to prove the truth of sentences involving the truth predicate. Some type-free theories of truth have much higher expressive power than the typed theories that have been surveyed in the previous section (at least as long as indexed truth predicates are avoided). Therefore type-free theories of truth are much more powerful tools in the reduction of other theories (for instance, second-order ones).

4.1 Type-free T-sentences

The set of all T-sentences T ⌈φ⌉ ↔ φ, where φ is any sentence of the language LT, that is, where φ may contain T, is inconsistent with PA (or any theory that proves the diagonal lemma) because of the Liar paradox. Therefore one might try to drop from the set of all T-sentences only those that lead to an inconsistency. In other words, one may consider maximal consistent sets of T-sentences. McGee (1992) showed that there are uncountably many maximal sets of T-sentences that are consistent with PA. So the strategy does not lead to a single theory. Even worse, given an arithmetical sentence (i.e., a sentence not containing T) that can neither be proved nor disproved in PA, one can find a consistent T-sentence that decides this sentence (McGee 1992). This implies that many consistent sets of T-sentences prove false arithmetical statements. Thus the strategy to drop just the T-sentences that yield an inconsistency is doomed.

A set of T-sentences that does not imply any false arithmetical statement may be obtained by allowing only those φ in T-sentences T ⌈φ⌉ ↔ φ that contain T only positively, that is, in the scope of an even number of negation symbols. Like the typed theory in Section 3.2 this theory is does not prove certain generalizations but proves the same T-free sentences as the strong type-free compositional Kripke-Feferman theory below (Halbach 2009).

4.2 Compositionality

Besides the disquotational feature of truth, one would also like to capture the compositional features of truth and generalize the axioms of typed compositional truth to the type-free case. To this end, axioms or rules concerning the truth of atomic sentences with the truth predicate will have to be added and the restriction to T-free sentences in the compositional axioms will have to be lifted. In order to treat truth like other predicates, one will add the axiom ∀A(T[TA] ↔ TA) (where ∀A ranges over all sentences). If the type restriction of the typed compositional axiom for negation is removed, the axiom ∀A(T[¬A] ↔ ¬TA) is obtained.

However, the axioms ∀A(T[TA] ↔ TA) and ∀A(T[¬A] ↔ ¬TA) are inconsistent over weak theories of syntax, so one of them has to be given up. If ∀A(T[¬A] ↔ ¬TA) is retained, one will have to find weaker axioms or rules for truth iteration, but truth remains a classical concept in the sense that ∀A(T[¬A] ↔ ¬TA) implies the law of excluded middle (for any sentence either the sentence itself or its negation is true) and the law of noncontradiction (for no sentence the sentence itself and its negation are true). If, in contrast, ∀A(T[¬A] ↔ ¬TA) is rejected and ∀A(T[TA] ↔ TA) retained, then it will become provable that either some sentences are true together with their negations or that for some sentences neither they nor their negations are true, and thus systems of non-classical truth are obtained, although the systems themselves are still formulated in classical logic. In the next two sections we overview the most prominent system of each kind.

4.3 The Friedman–Sheard theory and revision semantics

The system FS, named after Friedman and Sheard (1987), retains the negation axiom ∀A(T[¬A] ↔ ¬TA). The further compositional axioms are obtained by lifting the type restriction to their untyped counterparts:

  1. ∀A(AtomSentPA(A) → (TA ↔ Tr0(A)))
  2. ∀A(T[¬A] ↔ ¬TA)
  3. ∀A∀B(T[A ∧ B] ↔ (TA ∧ TB))
  4. ∀A∀B(T[A ∨ B] ↔ (TA ∨ TB))
  5. ∀A(v)(Sent(∀vA) → (T[∀vA(v)] ↔ ∀xT[A(x)])
  6. ∀A(v)(Sent(∀vA) → (T[∃vA(v)] ↔ ∃xT[A(x)]))
These axioms are added to PA formulated in the language LT. As the truth iteration axiom ∀A(T[TA] ↔ TA) is inconsistent, only the following two rules are added:
If φ is a theorem, one may infer T ⌈φ⌉, and conversely, if T ⌈φ⌉ is a theorem, one may infer φ.

It follows from results due to McGee (1985) that FS is ω-inconsistent, that is, FS proves ∃x¬φ(x), but proves also φ(0), φ(1), φ(2), … for some formula φ(x) of LT. The arithmetical theorems of FS, however, are all correct.

In FS one can define all finite levels of the classical Tarskian hierarchy, but FS isn't strong enough to allow one to recover any of its transfinite levels. Indeed, Halbach (1994) determined its proof-theoretic strength to be precisely that of the theory of ramified truth for all finite levels (i.e., finitely iterated T(PA); see Section 3.4) or, equivalently, the theory of ramified analysis for all finite levels. If either direction of the rule is dropped but the other kept, FS retains its proof-theoretic strength (Sheard 2001).

It is a virtue of FS that it is thoroughly classical: It is formulated in classical logic; if a sentence is provably true in FS, then the sentence itself is provable in FS; and conversely if a sentence is provable, then it is also provably true. Its drawback is its ω-inconsistency. FS may be seen as an axiomatization of rule-of-revision semantics for all finite levels (see the entry on the revision theory of truth).

4.4 The Kripke–Feferman theory

The Kripke–Feferman theory retains the truth iteration axiom ∀A(T[TA] ↔ TA), but the notion of truth axiomatized is no longer classical because the negation axiom ∀A(T[¬A] ↔ ¬TA) is dropped.

The semantical construction captured by this theory is a generalization of the Tarskian typed induction definition of truth captured by T(PA). In the generalized definition one starts with the true atomic sentence of the arithmetical language and then one declares true the complex sentences depending on whether its components are true or not. For instance, as in the typed case, if φ and ψ are true, their conjunction φ∧ψ will be true as well. In the case of the quantified sentences their truth value is determined by the truth values of their instances (one could render the quantifier clauses purely compositional by using a satisfaction predicate); for instance, a universally quantified sentence will be declared true if and only if all its instances are true. One can now extend this inductive definition of truth to the language LT by declaring a sentence of the form T ⌈φ⌉ true if φ is already true. Moreover one will declare ¬T⌈φ⌉ true if ¬φ is true. By making this idea precise, one obtains a variant of Kripke's (1975) theory of truth with the so called Strong Kleene valuation scheme (see the entry on many-valued logic). If axiomatized it leads to the following system, which is known as KF (‘Kripke–Feferman’), of which several variants appear in the literature:

  1. ∀A(AtomSentPA(A) → (TA ↔ Tr0(A)))
  2. ∀A(AtomSentPA(A) → (T[¬A] ↔ ¬Tr0(A)))
  3. ∀A(T[TA] ↔ TA)
  4. ∀A(T[¬TA] ↔ T[¬A])
  5. ∀A(T[¬¬A] ↔ TA)
  6. ∀A∀B(T[A ∧ B] ↔ (TA ∧ TB))
  7. ∀A∀B(T[¬(A ∧ B)] ↔ (T[¬A] ∨ T[¬B]))
  8. ∀A∀B(T[A ∨ B] ↔ (TA ∨ TB))
  9. ∀A∀B(T[¬(A ∨ B)] ↔ (T[¬A] ∧ T[¬B]))
  10. ∀A(v)(Sent(∀vA) → (T[∀vA(v)] ↔ ∀xT[A(x)])
  11. ∀A(v)(Sent(∀vA) → (T[¬∀vA(v)] ↔ ∃xT[¬A(x)])
  12. ∀A(v)(Sent(∀vA) → (T[∃vA(v)] ↔ ∃xT[A(x)]))
  13. ∀A(v)(Sent(∀vA) → (T[¬∃vA(v)] ↔ ∀xT[¬A(x)]))

Apart from the truth-theoretic axioms, KF comprises all axioms of PA and all induction axioms involving the truth predicate. The system is credited to Feferman on the basis of two lectures for the Association of Symbolic Logic, one in 1979 and the second in 1983, as well as in subsequent manuscripts. Feferman published his version of the system under the label Ref(PA) (‘weak reflective closure of PA’) only in 1991, after several other versions of KF had already appeared in print (e.g., Reinhardt 1986, Cantini 1989, who both refer to this unpublished work by Feferman).

KF itself is formulated in classical logic, but it describes a non-classical notion of truth. For instance, one can prove T⌈L⌉ ↔ T⌈¬L⌉ if L is the Liar sentence. Thus KF proves that either both the liar sentence and its negation are true or that neither is true. So either is the notion of truth paraconsistent (a sentence is true together with its negation) or paracomplete (neither is true). Some authors have augmented KF with an axiom ruling out truth-value gluts, which makes KF sound for Kripke's model construction, because Kripke had ruled out truth-value gluts.

Feferman (1991) showed that KF is proof-theoretically equivalent to the theory of ramified analysis through all levels below ε0, the limit of the sequence ω, ωω, ωωω, …, or a theory of ramified truth through the same ordinals. This result shows that in KF exactly ε0 many levels of the classical Tarskian hierarchy in its axiomatized form can be recovered. Thus KF is far stronger than FS, let alone T(PA). Feferman (1991) devised also a strengthening of KF that is as strong as full predicative analysis, that is ramified analysis or truth up to the ordinal Γ0.

4.5 Capturing the minimal fixed point

As remarked above, if KF proves T⌈φ⌉ for some sentence φ then φ holds in all Kripke fixed point models. In particular, there are 2ℵ‎0 fixed points that form a model of the internal theory of KF. Thus from the perspective of KF, the least fixed point (from which Kripke's theory is defined) is not singled out. Burgess (forthcoming) provides an expansion of KF, named μKF, that attempts to capture the minimal Kripkean fixed point. KF is expanded by additional axioms that express that the internal theory of KF is the smallest class closed under the defining axioms for Kripkean truth. This can be formulated as a single axiom schema that states, for each open formula φ,

If φ satisfies the same axioms of KF as the predicate T then φ holds of every true sentence.

From a proof-theoretic perspective μKF is significantly stronger than KF. The single axiom schema expressing the minimality of the truth predicate allows one to embed into μKF the system ID1 of one arithmetical inductive definition, an impredicative theory. While intuitively plausible, μKF suffers the same expressive incompleteness as KF: Since the minimal Kripkean fixed point forms a complete Π11 set and the internal theory of μKF remains recursively enumerable, there are standard models of the theory in which the interpretation of the truth predicate is not actually the minimal fixed point. At present there lacks a thorough analysis of the models of μKF.

4.6 Axiomatizations of Kripke's theory with supervaluations

KF is intended to be an axiomatization of Kripke's (1975) semantical theory. This theory is based on partial logic with the Strong Kleene evaluation scheme. In Strong Kleene logic not every sentence φ ∨ ¬φ is a theorem; in particular, this disjunction is not true if φ lacks a truth value. Consequently T ⌈L ∨ ¬L⌉ (where L is the Liar sentence) is not a theorem of KF and its negation is even provable. Cantini (1990) has proposed a system VF that is inspired by the supervaluations scheme. In VF all classical tautologies are provably true and T ⌈L  ∨ ¬L⌉, for instance, is a theorem of VF. VF can be formulated in LT and uses classical logic. It is no longer a compositional theory of truth, for the following is not a theorem of VF:

∀A∀B(T[A ∨ B] ↔ (TA ∨ TB)).

Not only is this principle inconsistent with the other axioms of VF, it does not fit the supervaluationist model for it implies T⌈L⌉ ∨ T⌈¬L⌉, which of course is not correct because according to the intended semantics neither the liar sentence nor its negation is true: both lack a truth value.

Extending a result due to Friedman and Sheard (1987), Cantini showed that VF is much stronger than KF: VF is proof-theoretically equivalent to the theory ID1 of non-iterated inductive definitions, which is not predicative.

5. Non-classical approaches to self-reference

The theories of truth discussed thus far are all axiomatized in classical logic. Some authors have also looked into axiomatic theories of truth based on non-classical logic (see, for example, Field 2008, Halbach and Horsten 2006, Leigh and Rathjen 2012). There are a number of reasons why a logic weaker than classical logic may be preferred. The most obvious is that by weakening the logic, some collections of axioms of truth that were previously inconsistent become consistent. Another common reason is that the axiomatic theory in question intends to capture a particular non-classical semantics of truth, for which a classical background theory may prove unsound.

5.1 The role of logic in axiomatising truth

The inconsistency of the T-sentences does not rely on classical reasoning. It is also inconsistent over much weaker logics such as minimal logic and partial logic. However, classical logic does play a role in restricting the free use of principles of truth. For instance, over a classical base theory, compositionality for implication is equivalent to the principle of completeness, ∀A(T[A] ∨ T[¬A]). If the logic under the truth predicate is classical, completeness becomes equivalent to stating the compositional axiom for disjunction. Without the law of excluded middle, FS can be formulated as a fully compositional theory while not proving the truth-completeness principle (Leigh and Rathjen 2012). In addition, classical logic has an effect on attempts to combine compositional and self-applicable axioms of truth. If, for example, one drops the axiom of truth-consistency from FS (the left-to-right direction of axiom 2 in Section 4.3) as well as the law of excluded middle for the truth predicate, it is possible to add consistently the truth-iteration axiom ∀A(T[A] → T[TA]). The resulting theory still bears a strong resemblance to FS in that the constructive version of the rule-of-revision semantics for all finite levels provides a natural model of the theory (Leigh & Rathjen 2012). In Leigh (2012) it is shown that the theory proves the same Π02 arithmetical statements as classical FS. This result should be contrasted with KF which, if formulated without the law of excluded middle, remains maximally consistent with respect to its axiomatisation but becomes a conservative extension of Heyting arithmetic.

5.2 Axiomatising Kripke's theory

Kripke's (1975) theory in its different guises is based on partial logic. In order to obtain models for a theory in classical logic, the extension of the truth predicate in the partial model is used again as the extension of truth in the classical model. In the classical model false sentences and those without a truth value in the partial model are declared not true. KF is sound with respect to these classical models and thus incorporates two distinct logics. The first is the ‘internal’ logic of statements under the truth predicate and is formulated with the Strong Kleene valuation schema. The second is the ‘external’ logic which is full classical logic. An effect of formulating KF in classical logic is that the theory cannot be consistently closed under the truth-introduction rule

If φ is a theorem of KF, so is T⌈φ⌉.

A second effect of classical logic is the statement of the excluded middle for the liar sentence. Neither the Liar sentence nor its negation obtains a truth value in Kripke's theory, so the disjunction of the two is not valid. The upshot is that KF, if viewed as an axiomatisation of Kripke's theory, is not sound with respect to its intended semantics. For this reason Halbach and Horsten (2006) and Horsten (2011) explore an axiomatization of Kripke's theory with partial logic as inner and outer logic. Their suggestion, a theory labelled PKF (‘partial KF’), can be axiomatised as a Gentzen-style two-sided sequent calculus based on Strong Kleene logic (see the entry on many-valued logic). PKF is formed by adding to this calculus the Peano–Dedekind axioms of arithmetic including full induction and the compositional and truth-iteration rules for the truth predicate as proscribed by Kripke's theory. The result is a theory of truth that is sound with respect to Kripke's theory.

Halbach and Horsten show that this axiomatization of Kripke's theory is significantly weaker than it's classical cousin KF. The result demonstrates that restricting logic only for sentences with the truth predicate can hamper also the derivation of truth-free theorems.

5.3 Adding a conditional

Field (2008) and others criticised theories based on partial logic for the absence of a ‘proper’ conditional and bi-conditional. Various authors have proposed conditionals and bi-conditionals that are not definable in terms of ¬, ∨ and ∧. Field (2008) aims at an axiomatic theory of truth not dissimilar to PKF but with a new conditional. Feferman (1984) also introduced a bi-conditional to a theory in non-classical logic. Unlike Field's and his own 1984 theory, Feferman's (2008) theory DT is formulated in classical logic, but it's internal logic is again a partial logic with a strong conditional.

Bibliography

  • Aczel, Peter, 1980, “Frege structures and the notion of proposition, truth and set”, The Kleene Symposium, Jon Barwise et al. (editors), Amsterdam: North-Holland, 31–59.
  • Bealer, George, 1982, Quality and Concept, Oxford: Clarendon Press.
  • Burgess, John P., forthcoming, “Friedman and the axiomatization of Kripke's theory of truth”, in Foundational Adventures: Essays in Honor of Harvey M. Friedman, edited by Neil Tennant, London: College Publications and Templeton Press (online).
  • Cantini, Andrea, 1989,“Notes on Formal Theories of Truth”, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 35: 97–130.
  • Cantini, Andrea, 1990, “A Theory of Formal Truth Arithmetically Equivalent to ID1”,Journal of Symbolic Logic, 55: 244–59.
  • Cantini, Andrea, 1996, Logical Frameworks for Truth and Abstraction: An Axiomatic Study, Studies in Logic and the Foundations of Mathematics (No. 135), Amsterdam: Elsevier.
  • Cieśliński, Cezary, 2007, “Deflationism, Conservativeness and Maximality”, Journal of Philosophical Logic, 36: 695–705.
  • Enayat, Ali and Albert Visser, 2013, “New Constructions of satisfaction classes.” In (Achourioti, T., Galinon, H., Fujimoto, K. and Martínez-Fernández, J. eds.) Unifying the philosophy of truth, Springer, to appear.
  • Feferman, Solomon, 1962, Transfinite recursive progressions of axiomatic theories, Journal of Symbolic Logic, 27: 259–316.
  • Feferman, Solomon, 1984, “Towards Useful Type-free Theories. I.” Journal of Symbolic Logic, 49: 75–111.
  • Feferman, Solomon, 1991, “Reflecting on Incompleteness”, Journal of Symbolic Logic, 56: 1–49.
  • Feferman, Solomon, 2008, “Axioms for Determinateness and Truth”, Review of Symbolic Logic, 1: 204–217.
  • Field, Hartry, 1999, “Deflating the Conservativeness Argument”, Journal of Philosophy, 96: 533–40.
  • Field, Hartry, 2003, “A Revenge-Immune Solution to the Semantic Paradoxes”, Journal of Philosophical Logic, 32: 139–177.
  • Field, Hartry, 2008, Saving Truth from Paradox, Oxford: Oxford University Press.
  • Franzén, Torkel, 2004, Inexhaustibility: a non-exhaustive treatment, Association for Symbolic Logic.
  • Friedman, Harvey and Michael Sheard, 1987, “An Axiomatic Approach to Self-Referential Truth”, Annals of Pure and Applied Logic, 33: 1–21.
  • Friedman, Harvey and Michael Sheard, 1988, “The Disjunction and Existence Properties for Axiomatic Systems of Truth”, Annals of Pure and Applied Logic, 40: 1–10.
  • Glanzberg, Michael, forthcoming, “Complexity and Hierarchy in Truth Predicates”, forthcoming in Unifying the Philosophy of Truth, ed. T. Achourioti, H. Galinon, K. Fujimoto, and J. Martínez-Fernández, Dordrecth: Springer.
  • Halbach, Volker, 1994, “A System of Complete and Consistent Truth”, Notre Dame Journal of Formal Logic, 35: 311–27.
  • Halbach, Volker, 1999, “Conservative Theories of Classical Truth”, Studia Logica, 62: 353–70.
  • Halbach, Volker, 2001, “Disquotational Truth and Analyticity”, Journal of Symbolic Logic, 66: 1959–1973.
  • Halbach, Volker and Leon Horsten, 2006, “Axiomatizing Kripke's Theory of Truth”, Journal of Symbolic Logic, 71: 677–712.
  • Halbach, Volker, 2009, “Reducing Compositional to Disquotational Truth”, Review of Symbolic Logic 2 (2009), 786–798.
  • Halbach, Volker, 2011, Axiomatic Theories of Truth, Cambridge University.
  • Hájek, Petr and Pavel Pudlak, 1993, Metamathematics of First-Order Arithmetic, Berlin: Springer.
  • Heck, Richard, 2001, “Truth and Disquotation”, Synthese, 142: 317–352.
  • Horsten, Leon, 1995, “The Semantical Paradoxes, the Neutrality of Truth and the Neutrality of the Minimalist Theory of Truth”, in The Many Problems of Realism (Studies in the General Philosophy of Science: Volume 3), P. Cortois (ed.), Tilburg: Tilburg University Press, 173–87.
  • Horsten, Leon, 2011, The Tarskian Turn. Deflationism and Axiomatic Truth, MIT Press
  • Kahle, Reinhard, 2001, “Truth in applicative theories”, Studia Logica, 68: 103–128.
  • Kaye, Richard, 1991, Models of Peano Arithmetic, Oxford Logic Guides, Oxford: Oxford University Press.
  • Ketland, Jeffrey, 1999, “Deflationism and Tarski's Paradise” Mind, 108 (429): 69–94.
  • Kotlarski, Henryk and Zygmunt Ratajczyk, 1990a, “Inductive Full Satisfaction Classes”, Annals of Pure and Applied Logic, 47: 199–223.
  • Kotlarski, Henryk and Zygmunt Ratajczyk, 1990b, “More on Induction in the Language with a Satisfaction Class”, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 36: 441–54.
  • Kotlarski, Henryk, Stanislav Krajewski, and Alistair H. Lachlan, 1981, “Construction of Satisfaction Classes for Nonstandard Models”, Canadian Mathematical Bulletin, 24: 283–93.
  • Kreisel, Georg and Azriel Lévy, 1968, “Reflection Principles and Their Use for Establishing the Complexity of Axiomatic Systems”, Zeitschrift für mathematische Logic und Grundlagen der Mathematik, 14: 97–142.
  • Kremer, Michael, 1988, “Kripke and the logic of truth”, Journal of Philosophical Logic, 17: 225–278.
  • Kripke, Saul, 1975, “Outline of a Theory of Truth”, Journal of Philosophy, 72: 690–716.
  • Lachlan, Alistair H., 1981, “Full Satisfaction Classes and Recursive Saturation”, Canadian Mathematical Bulletin, 24: 295–97.
  • Leigh, Graham E., 2013, “Conservativity for theories of compositional truth via cut elimination.” arXiv:1308.0168 [math.LO]
  • Leigh, Graham E., 2013, “A proof-theoretic account of classical principles of truth.” Annals of Pure and Applied Logic, 164: 1009–1024.
  • Leigh, Graham E., and Rathjen, Michael, 2012, “The Friedman-Sheard Programme in Intuitionistic Logic”, Journal of Symbolic Logic, 77: 777–806.
  • Leigh, Graham E., and Rathjen, Michael 2010, “An ordinal analysis for theories of self-referential truth”, Archive for Mathematical Logic, 49: 213–247.
  • Leitgeb, Hannes, 2001, “Theories of truth which have no standard models”, Studia Logica, 68: 69–87.
  • Maudlin, Tim, 2004, Truth and paradox. Solving the riddles, Oxford: Clarendon Press.
  • McGee, Vann, 1985, “How Truthlike Can a Predicate Be? A Negative Result,” Journal of Philosophical Logic, 14: 399–410.
  • McGee, Vann, 1991, Truth, Vagueness, and Paradox: An Essay on the Logic of Truth, Indianapolis and Cambridge: Hackett Publishing.
  • McGee, Vann, 1992, “Maximal consistent sets of instances of Tarski's schema (T)”, Journal of Philosophical Logic, 21: 235–241.
  • Myhill, John, 1950, “A system which can define its own truth”, Fundamenta Mathematicae, 37: 190–92.
  • Reinhardt, William N., 1986, “Some Remarks on Extending and Interpreting Theories,with a Partial Predicate for Truth”, Journal of Philosophical Logic, 15: 219–51.
  • Scott, Dana, 1975, “Combinators and classes”, in λ-calculus and Computer Science Theory (Lecture Notes in Computer Science: Volume 37), C. Böhm (ed.), Berlin: Springer, 1–26.
  • Shapiro, Stewart, 1998, “Proof and Truth: Through Thick and Thin”, Journal of Philosophy, 95 (10): 493–521.
  • Shapiro, Stewart, 2002, “Deflation and Conservation”, Principles of truth, Volker Halbach and Leon Horsten (eds.), Frankfurt a.M.: Dr. Hänsel-Hohenhausen, 103-128
  • Sheard, Michael, 1994, “A Guide to truth Predicates in the Modern Era”, Journal of Symbolic Logic, 59: 1032–54.
  • Sheard, Michael, 2001, “Weak and strong theories of truth”, Studia Logica , 68: 89–101.
  • Sheard, Michael, 2002, “Truth, probability, and naive criteria”, Principles of truth, Volker Halbach and Leon Horsten (eds.), Frankfurt a.M.: Dr. Hänsel-Hohenhausen, 169–181.
  • Takeuti, Gaisi, 1987, Proof Theory (Studies in Logic and the Foundations of Mathematics: No. 81), Amsterdam: North-Holland, second edition.
  • Tarski, Alfred, 1935, “The Concept of Truth in Formalized Languages”, in Logic, Semantics, Metamathematics, Indianapolis: Hackett 1983, 2d edition, 152–278.
  • Tennant, Neil, 2002, “Deflationism and the Gödel-Phenomena”, Mind, 111: 551–582.
  • Turner, Raymond, 1990,Truth and modality, London: Pitman.
  • Visser, Albert, 1989, “Semantics and the liar paradox,” Handbook of Philosophical Logic, 4: 617–706.
  • Yablo, Stephen, 1993, “Paradox without self-reference,” Analysis, 53: 251–252.

Other Internet Resources

[Please contact the author with suggestions.]

Copyright © 2013 by
Volker Halbach <volker.halbach@philosophy.ox.ac.uk>
Graham E. Leigh <graham.leigh@philosophy.ox.ac.uk>

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.