## 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.
In these cases 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 or satisfaction, and axioms for that predicate are then laid
down. This approach by itself 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 \(\phi(x)\)
is true of an individual \(a\) seems equivalent (in some sense)
to the claim that \(a\) has the property of
*being such that* \(\phi\) (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 Godel's incompleteness theorems,
 the statement that Peano Arithmetic (PA)
is consistent, in its guise as a number-theoretic statement (given the
technique of Godel 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 \(Bew\_{PA}(\ulcorner \phi \urcorner)
\rightarrow \phi\) where \(\phi\) is a formula of the language of
arithmetic, \(\ulcorner \phi \urcorner\) a name for \(\phi\)
and \(Bew\_{PA}(x)\) is the standard provability
predicate for PA ('\(Bew\)' was introduced by
Godel 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 Franzen 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
Levy 1968). The Global Reflection Principle for a formal system
S states that all sentences provable in S are true:



\[
\forall x(Bew\_{S} (x) \rightarrow Tx)
\]

\(Bew\_{S} (x)\) expresses here provability of
sentences in the system S (we omit discussion here of the problems of
defining \(Bew\_{S} (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.4 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\ulcorner \phi \urcorner \leftrightarrow \phi\), where \(T\) is the truth predicate, \(\phi\) is a sentence
and \(\ulcorner \phi \urcorner\) is a name for the
sentence \(\phi\). (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, 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.4 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 Godel 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. However, Fujimoto (2012)
 has shown that some axiomatic truth theories over set theory differ from their counterparts over Peano arithmetic in some aspects.


### 2.2 Notational conventions


For the sake of definiteness we assume that the language of
arithmetic has exactly \(\neg , \wedge\) and \(\vee\) as connectives and
\(\forall\) and \(\exists\) 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 \(\mathcal{L}\_T\) be the
language of arithmetic augmented by the new unary predicate
symbol \(T\) for truth. If \(\phi\) is a sentence
of \(\mathcal{L}\_T,
\ulcorner \phi \urcorner\) is a name for \(\phi\) in the
language \(\mathcal{L}\_T\);
formally speaking, it is the numeral of
the Godel number of
\(\phi\). In general, Greek letters like \(\phi\) and \(\psi\) 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). \(\phi\) and \(\psi\) range over
formulas of the formal
language \(\mathcal{L}\_T\).


In what follows, we use small, upper case italic letters
like \({\scriptsize A}, {\scriptsize B},\ldots\) as
variables in \(\mathcal{L}\_T\)
ranging over sentences (or their Godel numbers, to be
precise). Thus
\(\forall{\scriptsize A}(\ldots{\scriptsize A}\ldots)\)
stands for
\(\forall x(Sent\_T (x)
\rightarrow \ldots x\ldots)\),
where \(Sent\_T (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 \(\mathcal{L}\_T\)
that a negation of a sentence
of \(\mathcal{L}\_T\) is true if and
only if the sentence itself is not true. We would write this as 



\[
\forall{\scriptsize A}(T[\neg{\scriptsize A}] \leftrightarrow \neg T{\scriptsize A}).
\]

The square brackets indicate that the operation of forming the negation of
\({\scriptsize 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



\[
\forall{\scriptsize A}\forall{\scriptsize B}(T[{\scriptsize A} \wedge{\scriptsize B}] \leftrightarrow(T{\scriptsize A} \wedge T{\scriptsize B}))
\]

is a single sentence of the language \(\mathcal{L}\_T\) saying that a conjunction of
sentences of \(\mathcal{L}\_T\) is true if
and only if both sentences are true. In contrast, 



\[
T\ulcorner \phi \wedge \psi \urcorner \leftrightarrow 
 (T\ulcorner \phi \urcorner \wedge T\ulcorner \phi \urcorner)
\]

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 \(\mathcal{L}\_T\) for the Greek
letters \(\phi\) and \(\psi\). The single sentence
\(\forall{\scriptsize A}\forall{\scriptsize B}(T[{\scriptsize A} \wedge{\scriptsize B}] \leftrightarrow 
(T{\scriptsize A} \wedge T{\scriptsize B}))\) 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's 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 \(Tr\_0 (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,
Hajek 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\ulcorner \phi \urcorner \leftrightarrow \phi\), where \(\phi\) 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
\(\forall{\scriptsize A}(T{\scriptsize A}\vee T[\neg{\scriptsize A}\)])
where the quantifier \(\forall{\scriptsize 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\ulcorner \phi \urcorner \leftrightarrow \phi\) (where \(\phi\) 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 \(\neg 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.


In the form outlined above, T-sentences express the equivalence between \(T\ulcorner \phi \urcorner\) and \(\phi\) only when \(\phi\) is a sentence.
In order to capture the equivalence for properties \((x\) has property P iff 'P' is true of \(x)\) one must generalise the T-sentences. The result are usually referred to as the *uniform* T-senences and are formalised by the equivalences 
\(\forall x(T\ulcorner \phi(\underline{x})\urcorner \leftrightarrow \phi(x))\) for each open formula \(\phi(v)\) with at most \(v\) free in \(\phi\).
Underlining the variable indicates it is bound from the outside.
More precisely, \(\ulcorner \phi(\underline{x})\urcorner\) stands for the result of replacing the variable \(v\)
in \(\ulcorner \phi(v)\urcorner\) by the numeral
of \(x\).


### 3.3 Compositional truth


As was observed already by Tarski (1935), 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, \(AtomSent\_{PA}(\ulcorner{\scriptsize A}\urcorner)\)
expresses that \({\scriptsize A}\) is an atomic sentence of the
language of
arithmetic, \(Sent\_{PA}(\ulcorner{\scriptsize A}\urcorner)\)
expresses that \({\scriptsize A}\) is a sentence of the language
of arithmetic.


1. \(\forall{\scriptsize A}(AtomSent\_{PA}({\scriptsize A})
 \rightarrow(T{\scriptsize A} \leftrightarrow Tr\_0 ({\scriptsize A})))\)
2. \(\forall{\scriptsize A}(Sent\_{PA}({\scriptsize A})
 \rightarrow(T[\neg{\scriptsize A}] \leftrightarrow \neg T{\scriptsize A}))\)
3. \(\forall{\scriptsize A}\forall{\scriptsize B}(Sent\_{PA}({\scriptsize A}) \wedge Sent\_{PA}({\scriptsize B}) \rightarrow 
 (T[{\scriptsize A} \wedge{\scriptsize B}]
 \leftrightarrow(T{\scriptsize A}
 \wedge T{\scriptsize B})))\)
4. \(\forall{\scriptsize A}\forall{\scriptsize B}(Sent\_{PA}({\scriptsize A}) \wedge Sent\_{PA}({\scriptsize B}) \rightarrow 
 (T[{\scriptsize A} \vee{\scriptsize B}] \leftrightarrow 
 (T{\scriptsize A} \vee T{\scriptsize B})))\)
5. \(\forall{\scriptsize A}(v)(Sent\_{PA}(\forall v{\scriptsize A})
 \rightarrow(T[\forall v{\scriptsize A}(v)] \leftrightarrow \forall xT[{\scriptsize A}(\underline{x})\)]))
6. \(\forall{\scriptsize A}(v)(Sent\_{PA}(\forall v{\scriptsize A})
 \rightarrow(T[\exists v{\scriptsize A}(v)] \leftrightarrow \exists xT[{\scriptsize A}(\underline{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
\((Tr\_0\) 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.

\(Sent\_{PA}(\forall v{\scriptsize A})\)
says that \({\scriptsize A}(v)\) is a formula with at
most \(v\) free (because
\(\forall v{\scriptsize A}(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 claimed that this result is also finitarily provable, no such
proof was available until Enayat & Visser (2015) and Leigh
(2015). Moreover, the theory given by PA + axioms 1-6 is relatively interpretable in PA. However, this result is sensitive to the choice of the base theory: it fails for finitely axiomatized theories (Heck 2015, Nicolai 2016). These proof-theoretic results have been used extensively in the discussion of truth-theoretic deflationism (see Cieslinski 2017).



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), CT, 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
Godel'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:



\[
\exists X\forall y(y\in X \leftrightarrow \phi(x))
\]


where \(\phi(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. In T(PA), quantification
over sets can be defined as quantification over formulas with
one free variable and membership as the truth of the formula as
applied to a number. 



As the global reflection principle entails formal consistency, the conservativeness result for PA + axioms 1-6 implies that the global reflection principle for Peano arithmetic is not derivable in the typed compositional theory without expanding the induction axioms.
In fact, this theory proves neither the statement that all logical validities are true (global reflection for pure first-order logic) nor that all the Peano axioms of arithmetic are true.
Perhaps surprisingly, of these two unprovable statements it is the former that is the stronger.
The latter can be added as an axiom and the theory remains conservative over PA (Enayat and Visser 2015, Leigh 2015).
In contrast, over PA + axioms 1-6, the global reflection principle for first-order logic is equivalent to global reflection for Peano arithmetic (Cieslinski 2010), and these two theories have the same arithmetic consequences as adding the axiom of induction for bounded \((\Delta\_0)\) formulas containing the truth predicate (Wcislo and Lelyk 2017).



The transition from PA to T(PA) can be imagined as an act of reflection on the truth of \(\mathcal{L}\)-sentences in PA. Similarly, the step from the typed \(T\)-sentences to the compositional axioms is also tied to a reflection principle, specifically the *uniform reflection principle* over the typed uniform \(T\)-sentences.
This is the collection of sentences 
\(\forall x\, Bew\_{S} (\ulcorner \phi(\underline{x})\urcorner) \rightarrow \phi(x) \) where \(\phi\) ranges over formulas in \(\mathcal{L}\_T\) with one free variable and S is the theory of the uniform typed T-sentences.
Uniform reflection exactly captures the difference between the two theories: the reflection principle is both derivable in T(PA) and suffices to derive the six compositional axioms (Halbach 2001).
Moreover, the equivalence extends to iterations of uniform reflection, in that for any ordinal \(\alpha , 1 + \alpha\) iterations of uniform reflection over the typed \(T\)-sentences coincides with T(PA) extended by transfinite induction up to the ordinal \(\varepsilon\_{\alpha}\), namely the \(\alpha\)-th ordinal \(\kappa\) with the property that \(\omega^{\kappa} = \kappa \) (Leigh 2016).



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 \(\mathcal{L}\_T\) 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 \(T\_n\ulcorner \phi \urcorner \leftrightarrow \phi\) to the language of arithmetic where \(\phi\) contains only
truth predicates \(T\_k\)
with \(k\gt n\) to PA, a theory is
obtained that does not have a standard \((\omega\)-)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 (2015)
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\ulcorner \phi \urcorner \leftrightarrow \phi\), where \(\phi\) is any sentence of the
language \(\mathcal{L}\_T\), that
is, where \(\phi\) 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 \(\phi\)
in \(T\)-sentences \(T\ulcorner \phi \urcorner \leftrightarrow \phi\) 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 does not prove
certain generalizations but proves the same T-free sentences as the
strong type-free compositional Kripke-Feferman theory below (Halbach
2009). Schindler (2015) obtained a deductively very strong truth theory based on stratified disquotational principles.


### 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
\(\forall{\scriptsize A}(T[T{\scriptsize A}]
\leftrightarrow T{\scriptsize A})\) (where
\(\forall{\scriptsize A}\) ranges over all sentences). If the
type restriction of the typed compositional axiom for
negation is removed, the axiom
\(\forall{\scriptsize A}(T[\neg{\scriptsize A}]
\leftrightarrow \neg T{\scriptsize A})\) is obtained.


However, the axioms
\(\forall{\scriptsize A}(T[T{\scriptsize A}]
\leftrightarrow T{\scriptsize A})\) and
\(\forall{\scriptsize A}(T[\neg{\scriptsize A}]
\leftrightarrow \neg T{\scriptsize A})\) are inconsistent over
weak theories of syntax, so one of them has to be given up. If
\(\forall{\scriptsize A}(T[\neg{\scriptsize A}]
\leftrightarrow \neg T{\scriptsize A})\) is retained, one will
have to find weaker axioms or rules for truth iteration, but truth
remains a classical concept in the sense that
\(\forall{\scriptsize A}(T[\neg{\scriptsize A}]
\leftrightarrow \neg T{\scriptsize A})\) 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,
\(\forall{\scriptsize A}(T[\neg{\scriptsize A}]
\leftrightarrow \neg T{\scriptsize A})\) is rejected and
\(\forall{\scriptsize A}(T[T{\scriptsize A}]
\leftrightarrow T{\scriptsize A})\) 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
\(\forall{\scriptsize A}(T[\neg{\scriptsize A}]
\leftrightarrow \neg T{\scriptsize A})\). The further
compositional axioms are obtained by lifting the type restriction to
their untyped counterparts:


1. \(\forall{\scriptsize A}(AtomSent\_{PA}({\scriptsize A})
 \rightarrow(T{\scriptsize A} \leftrightarrow Tr\_0 ({\scriptsize A})))\)
2. \(\forall{\scriptsize A}(T[\neg{\scriptsize A}] \leftrightarrow \neg T{\scriptsize A})\)
3. \(\forall{\scriptsize A}\forall{\scriptsize B}(T[{\scriptsize A} \wedge{\scriptsize B}] \leftrightarrow(T{\scriptsize A} \wedge T{\scriptsize B}))\)
4. \(\forall{\scriptsize A}\forall{\scriptsize B}(T[{\scriptsize A} \vee{\scriptsize B}] \leftrightarrow(T{\scriptsize A} \vee T{\scriptsize B}))\)
5. \(\forall{\scriptsize A}(v)(Sent(\forall v{\scriptsize A})
 \rightarrow(T[\forall v{\scriptsize A}(v)] \leftrightarrow \forall xT[{\scriptsize A}(\underline{x})\)])
6. \(\forall{\scriptsize A}(v)(Sent(\forall v{\scriptsize A})
 \rightarrow(T[\exists v{\scriptsize A}(v)] \leftrightarrow \exists xT[{\scriptsize A}(\underline{x})\)]))



These axioms are added to PA formulated in the
language \(\mathcal{L}\_T\). As the
truth iteration axiom
\(\forall{\scriptsize A}(T[T{\scriptsize A}]
\leftrightarrow T{\scriptsize A})\) is inconsistent, only the
following two rules are added:


 If \(\phi\) is a theorem, one may infer
 \(T\ulcorner \phi \urcorner\), and conversely, if
 \(T\ulcorner \phi \urcorner\) is a theorem, one may
 infer \(\phi\). 


It follows from results due to McGee (1985) that FS is
\(\omega\)-inconsistent, that is, FS proves
\(\exists x\neg \phi(x)\), but proves also \(\phi\)(0),
\(\phi\)(1), \(\phi\)(2), ... for some formula \(\phi(x)\)
of \(\mathcal{L}\_T\). 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 \(\omega\)-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
\(\forall{\scriptsize A}(T[T{\scriptsize A}]
\leftrightarrow T{\scriptsize A})\), but the notion of truth
axiomatized is no longer classical because the negation axiom
\(\forall{\scriptsize A}(T[\neg{\scriptsize A}]
\leftrightarrow \neg T{\scriptsize A})\) is dropped. 


The semantical construction captured by this theory is a
generalization of the Tarskian typed inductive 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
\(\phi\) and \(\psi\) are true, their conjunction \(\phi \wedge \psi\) 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 \(\mathcal{L}\_T\) by
declaring a sentence of the
form \(T\ulcorner \phi \urcorner\) true
if \(\phi\) is already true. Moreover one will declare
\(\neg T\ulcorner \phi \urcorner\) true if
\(\neg \phi\) 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. \(\forall{\scriptsize A}(AtomSent\_{PA}({\scriptsize A})
 \rightarrow(T{\scriptsize A} \leftrightarrow Tr\_0 ({\scriptsize A})))\)
2. \(\forall{\scriptsize A}(AtomSent\_{PA}({\scriptsize A})
 \rightarrow(T[\neg{\scriptsize A}] \leftrightarrow \neg Tr\_0 ({\scriptsize A})))\)
3. \(\forall{\scriptsize A}(T[T{\scriptsize A}]
 \leftrightarrow T{\scriptsize A})\)
4. \(\forall{\scriptsize A}(T[\neg T{\scriptsize A}]
 \leftrightarrow T[\neg{\scriptsize A}\)])
5. \(\forall{\scriptsize A}(T[\neg \neg{\scriptsize A}]
 \leftrightarrow T{\scriptsize A})\)
6. \(\forall{\scriptsize A}\forall{\scriptsize B}(T[{\scriptsize A} \wedge{\scriptsize B}] \leftrightarrow(T{\scriptsize A} \wedge T{\scriptsize B}))\)
7. \(\forall{\scriptsize A}\forall{\scriptsize B}(T[\neg({\scriptsize A} \wedge{\scriptsize B})] \leftrightarrow 
 (T[\neg{\scriptsize A}] \vee T[\neg{\scriptsize B}\)]))
8. \(\forall{\scriptsize A}\forall{\scriptsize B}(T[{\scriptsize A} \vee{\scriptsize B}] \leftrightarrow(T{\scriptsize A} \vee T{\scriptsize B}))\)
9. \(\forall{\scriptsize A}\forall{\scriptsize B}(T[\neg({\scriptsize A} \vee{\scriptsize B})] \leftrightarrow 
 (T[\neg{\scriptsize A}] \wedge T[\neg{\scriptsize B}\)]))
10. \(\forall{\scriptsize A}(v)(Sent(\forall v{\scriptsize A})
 \rightarrow(T[\forall v{\scriptsize A}(v)] \leftrightarrow \forall xT[{\scriptsize A}(\underline{x})\)])
11. \(\forall{\scriptsize A}(v)(Sent(\forall v{\scriptsize A})
 \rightarrow(T[\neg \forall v{\scriptsize A}(v)] \leftrightarrow \exists xT[\neg{\scriptsize A}(\underline{x})\)])
12. \(\forall{\scriptsize A}(v)(Sent(\forall v{\scriptsize A})
 \rightarrow(T[\exists v{\scriptsize A}(v)] \leftrightarrow \exists xT[{\scriptsize A}(\underline{x})\)]))
13. \(\forall{\scriptsize A}(v)(Sent(\forall v{\scriptsize A})
 \rightarrow(T[\neg \exists v{\scriptsize A}(v)] \leftrightarrow \forall xT[\neg{\scriptsize A}(\underline{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\ulcorner L\urcorner \leftrightarrow T\ulcorner\neg L\urcorner\)
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
\(\varepsilon\_0\), the limit of the sequence \(\omega ,
\omega^{\omega},
\omega^{\omega^{ \omega} },\ldots\), or a theory of
ramified truth through the same ordinals. This result shows that in KF
exactly \(\varepsilon\_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
\(\Gamma\_0\).


Just as with the typed truth predicate, the theory KF (more precisely, a common variant of it) can be obtained via an act of reflection on a system of untyped \(T\)-sentences. The system of \(T\)-sentences in question is the extension of the uniform positive untyped \(T\)-sentences by a primitive falsity predicate, that is, the theory features two unary predicates \(T\) and \(F\) and axioms



\[\begin{align\*}
&\forall x(T\ulcorner \phi(\underline{x})\urcorner \leftrightarrow \phi(x)) \\
& \forall x(F\ulcorner \phi(\underline{x})\urcorner \leftrightarrow \phi '(x))
\end{align\*}\]


for every formula \(\phi(v)\) positive in both \(T\) and \(F\), where \(\phi '\) represents the De Morgan dual of \(\phi\) (exchanging \(T\) for \(F\) and vice versa).
From an application of uniform reflection over this disquotational theory, the truth axioms for the corresponding two predicate version of KF are derivable (Horsten and Leigh, 2016). The converse also holds, as does the generalisation to finite and transfinite iterations of reflection (Leigh, 2017).



### 4.5 Capturing the minimal fixed point


As remarked above, if KF
proves \(T\ulcorner \phi \urcorner\) for some
sentence \(\phi\) then \(\phi\) holds in all Kripke fixed point models. In
particular, there are \(2^{\aleph\_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 (2014) provides an
expansion of KF, named \(\mu\)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 \(\phi\), 



 If \(\phi\) satisfies the same axioms of KF as the predicate \(T\)
 then \(\phi\) holds of every true sentence.




From a proof-theoretic perspective \(\mu\)KF is significantly stronger
than KF. The single axiom schema expressing the minimality of the
truth predicate allows one to embed into \(\mu\)KF the system
ID\(\_1\) of one arithmetical inductive definition, an
impredicative theory. While intuitively plausible, \(\mu\)KF suffers the
same expressive incompleteness as KF: Since the minimal Kripkean fixed
point forms a complete \(\Pi^{1}\_1\) set and the
internal theory of \(\mu\)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 \(\mu\)KF.



### 4.6 Axiomatisations 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 \(\phi \vee \neg \phi\) is a theorem; in particular, this
disjunction is not true if \(\phi\) lacks a truth
value. Consequently \(T\ulcorner L\vee \neg L\urcorner\)
(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\ulcorner L \vee \neg L\urcorner\), for instance, is a theorem of
VF. VF can be formulated
in \(\mathcal{L}\_T\) and uses
classical logic. It is no longer a *compositional* theory of
truth, for the following is not a theorem of VF:



\[
\forall{\scriptsize A}\forall{\scriptsize B}(T[{\scriptsize A} \vee{\scriptsize B}] \leftrightarrow(T{\scriptsize A} \vee T{\scriptsize B})).
\]

Not only is this principle inconsistent with the other axioms of
VF, it does not fit the supervaluationist model for it
implies \(T\ulcorner L\urcorner \vee T\ulcorner \neg L\urcorner\),
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 ID\(\_1\) 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.



There is also a large number of approaches that employ paraconsistent or substructural logics. In most cases these approaches do not employ an axiomatic base theory such as Peano arithmetic and therefore deviate form the setting considered here, although there is no technical obstacle in applying paraconsistent or substructural logics to truth theories over such base theories. Here we cover only accounts that are close to the setting considered above. For further information on the application of substructural and paraconsistent logics to the truth-theoretic paradoxes see the relevant section in the entry on the liar paradox.

### 5.1 The truth predicate in intuitionistic logic


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, the compositional axiom for
implication \((\rightarrow)\) is equivalent to the principle of completeness,
\(\forall{\scriptsize A}(T[{\scriptsize A}] \vee T[\neg{\scriptsize A}\)]). If the logic under
the truth predicate is classical, completeness is equivalent to 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 & 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
\(\forall{\scriptsize A}(T[{\scriptsize A}]
\rightarrow T[T{\scriptsize A}])\).
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, and the two theories share the same \(\Pi^{0}\_2\) consequences (Leigh & Rathjen 2012; Leigh, 2013). 
This result should be contrasted with KF which, if formulated
without the law of excluded middle, remains maximally consistent with
respect to its choice of truth axioms but is 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 \(\phi\) is a theorem of KF, so is
 \(T\ulcorner \phi \urcorner\).




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 \(\neg , \vee\) and
\(\wedge\). 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.