CLASSICAL DETERMINATE TRUTH I

Abstract

We introduce and analyze a new axiomatic theory $\mathsf {CD}$ of truth. The primitive truth predicate can be applied to sentences containing the truth predicate. The theory is thoroughly classical in the sense that $\mathsf {CD}$ is not only formulated in classical logic, but that the axiomatized notion of truth itself is classical: The truth predicate commutes with all quantifiers and connectives, and thus the theory proves that there are no truth value gaps or gluts. To avoid inconsistency, the instances of the T-schema are restricted to determinate sentences. Determinateness is introduced as a further primitive predicate and axiomatized. The semantics and proof theory of $\mathsf {CD}$ are analyzed.

Ad veritatem autem copulativae requiritur quod utraque pars sit vera, et ideo si quaecumque pars copulativae sit falsa, ipsa copulativa est falsa.

William of Ockham, Summa Logicae II.32

Ad veritatem autem [propositionis] disiunctivae requiritur quod aliqua pars sit vera[.]

William of Ockham, Summa Logicae II.33

1 Classicality and compositional semantics

Philosophy abounds with general claims expressed with a truth predicate: Philosophers debate whether there are contingent or synthetic a priori truths, and whether there are unprovable or unverifiable truths; they mostly agree that what is known is true, but that some justified true beliefs are not known; they teach their students that the conclusion of a valid argument is true if its premisses are true and try to convince their students that the rules of natural deduction are truth-preserving. Specific instances of these claims can often be stated without a predicate for truth; but the quantified claims make essential use of the truth predicate.

In the arguments for this kind of claim, assumptions about the truth predicate are often used implicitly without further ado. In the present paper we strive to make these assumptions explicit by listing principles about the truth predicate that are jointly consistent with further plausible assumptions about the objects to which truth is ascribed. We presuppose that these objects share the structure of (types of) sentences without entering the debate about whether truth applies to propositions, beliefs, sentence tokens, or still other things. ¹

It is widely believed that truth serves its role as a device of generalization in virtue of its disquotational feature; and a large part of the literature on truth is devoted to the development of strong disquotational truth theories. However, in their zeal to devise theories of disquotational truth, some philosophers seem to have lost sight of how we reason with generalizations. When truth is used as a device of generalization, disquotation is not the only principle that is used in reasoning with generalizations. Compositional principles are just as important and used routinely without qualms. We give three examples.

Our first example comes from logic. When motivating axioms or rules for a logical calculus, compositional laws of truth are used. In the case of the elimination rule for conjunction or for the universal quantifier in natural deduction, students usually quickly accept the claim that the rule preserves truth. At this point in the course, students may not have seen the model-theoretic notions of satisfaction and truth or the object/metalanguage distinction at all; nevertheless they have no problems in seeing that a conjunct must be true if the conjunction is true and that a substitution instance is true if the universally quantified sentence is true. The point can also be made about the history of logic: Logicians chose sound logical calculi long before the arrival of the modern model-theoretic notion of truth in Tarski and Vaught [43] in 1956 (as far as we know; see Hodges [26]). Truth preservation of logical rules is often assumed to hold without any restriction. Any restriction to a specific sublanguage is at odds with the universality of logic.

The use of the compositional principles is by no means confined to the realm of logical theorizing. Our second example is from epistemology. Most epistemologists would be happy to endorse the following argument, which could form part of a Gettier example:

Smith believes a disjunction. He is justified in believing one disjunct, which happens to be false, while he does not believe the other disjunct, which happens to be true. Therefore Smith has a justified true belief.

In this argument we reason about the truth (and justification) of beliefs by analyzing and manipulating their logical structures without explicitly specifying exactly what these beliefs are. The validity of the argument depends on the assumption that a disjunction is true if one of its disjuncts is true, as stated by Ockham in the second quote above. Fujimoto [16, 17] called this kind of reasoning blind deduction, because we reason about the truth of beliefs or sentences without being able to specify these beliefs or sentences by means of a quotational name or a structural description. Disquotation axioms or T-sentences used as axioms permit only reasoning about the truth of sentences that are explicitly given by such a naming device.

The use of the compositional principles is so ubiquitous that their use often goes unnoticed as in our third example:

Alfred made a claim that was denied by Kurt (i.e., Kurt asserted the negation of the claim); and everything Kurt claimed is true. Therefore not everything Alfred claimed is true.

For the validity of this argument we require the principle that a claim is not true if its negation is true.

In the examples we quantify over all sentences, beliefs, or propositions. Blind deductions are not restricted to sentences that are safe, grounded, determinate, healthy, non-circular, or in some other way ‘unproblematic’. Moreover, the full compositional principles are consistent without any restrictions on the underlying logic or syntax theory.

The axioms for truth can and should be added to a base theory that yields at least a comprehensive theory of syntax (in a direct or coded form); the base theory may also go far beyond a theory of syntax. In [22, 23] the second author formulated the truth theory over set theory as the base. Here, however, we start from Peano arithmetic, which is traditionally used as base theory for axiomatic theories of truth; but we consider it only as a simple model case. Expressions are identified with their codes. As usual, we confine ourselves to a truth rather than a satisfaction predicate in the case of arithmetic, as names for all objects are available and satisfaction and variable assignments are not needed. All extensions of Peano arithmetic we consider are formulated in classical logic.

In what follows, $\mathcal {L}_0$ is the language of arithmetic. The axioms are formulated in an expansion of $\mathcal {L}_0$ with further predicate symbols $\mathrm {T}$ and $\mathrm {D}$ . Negation and conjunction are the only connectives, and the universal is the only quantifier in the language; other connectives and the existential quantifier are assumed to be defined. In the axioms below expresses that x is a sentence of $\mathcal {L}$ . The symbol expresses the function that, if it is applied to a sentence, returns its negation. If a suitable function symbol is not in $\mathcal {L}_0$ , this function needs to be expressed by a suitable formula; and are defined analogously. The quantifier $\forall t$ ranges over (codes of) closed terms and is defined using a suitable formula describing the set of closed terms; and $x(t/v)$ designates the result of formally substituting t for the variable v in x. The following axioms then express that a negated sentences is true iff the sentence is not, that a conjunct is true iff both conjuncts are, and that a universally quantified sentence is true iff all its substitution instances are:

1. T4

2. T5

3. T6

The axioms T4–T6 capture a thoroughly classical concept or truth: The truth theory is not only formulated in classical logic, but the notion of truth axiomatized by T4–T6 is itself classical. According to the axioms, truth commutes with quantifiers and connectives for all sentences, including those with the truth predicate. Theories such as the Kripke–Feferman theory [8, 37] or Cantini’s [6] VF are formulated in classical logic as well, but capture a non-classical notion of truth.

Axiom T4 disproves the existence of truth value gaps and gluts. We define falsity as the truth of the negation, that is, we stipulate: . If the truth predicate is classical and T4 is assumed, then falsity is equivalent to non-truth. Thus, every sentence is true or false; and no sentence is both true and false.

Disquotation axioms have been been thought to be more fundamental than the compositional axioms. Consequently, there have been various attempts to obtain compositional from disquotational principles. Tarski [42, p. 259] tried to derive restricted compositional principles from the T-sentences using what he called the rule of infinite induction, which is a generalization of the -rule. More recently, some authors, including Halbach [19] and Horsten and Leigh [27], have used reflection principles instead, which are of course finitized versions of infinitary rules. We are sceptical about the prospects of justifying compositional from disquotational axioms. There are general objections against the use of infinitary and reflection rules to this end. Another crucial objection is especially relevant when unrestricted compositional principles are employed. Usually, attempts to obtain compositional axioms for all sentences of a certain kind from disquotational principles rely on the disquotation principle for all sentences of this kind. For instance, we may try to derive the compositional axioms for all $\mathrm {T}$ -free (or $\mathrm {T}$ -positive) sentences from all equivalences $\mathrm {T}\ulcorner \phi \urcorner \leftrightarrow \phi $ , where $\phi $ is $\mathrm {T}$ -free (or $\mathrm {T}$ -positive). However, in the case of the completely unrestricted compositional axioms T4–T6, this strategy is not very promising. Of course, the unrestricted compositional axioms T4–T6 can be derived from all instances $\mathrm {T}\ulcorner \phi \urcorner \leftrightarrow \phi $ ; but this is because the unrestricted T-schema is inconsistent over arithmetic. Hence, we will not be able to derive all type-free compositional from disquotational principles, even if some kind of infinitary rule is assumed. ² Therefore we adopt the unproblematic, fully general compositional principles as axioms and do not attempt to derive them from a disquotation schema, which has to be restricted in some way.

2 Determinateness and disquotation

Our policy for restricting disquotation is inspired by disquotationalist and deflationist theories of truth. We expand the base language $\mathcal {L}_0$ by adding sentences that are needed for semantic ascent and generalization. The sentences of the base language together with those needed for semantic ascent and generalization form the set $\mathfrak {D}$ . Roughly, if we have a sentence $\phi $ in $\mathfrak {D}$ , we also add an equivalent new sentence $\mathrm {T}\ulcorner \phi \urcorner $ as a ‘copy’ of $\phi $ . These copies are required for semantic ascent. We close then under connectives and quantifiers in a way to be explained. This permits generalizations, because we can now express, for instance, that all provable sentences of $\mathcal {L}_0$ are true. This process is then iterated: We add copies $\mathrm {T}\ulcorner \phi \urcorner $ for semantic ascent and then close under connectives and quantifiers in order to be able to generalize. We add only sentences to $\mathfrak {D}$ that are required for semantic ascent and generalization, not all sentences of the full language $\mathcal {L}$ . In particular, not all sentences of the form $\mathrm {T}\ulcorner \phi \urcorner $ are in $\mathfrak {D}$ . The set $\mathfrak {D}$ fails to be decidable. In a general setting with ‘contingent’ vocabulary, whether a sentence belongs to $\mathfrak {D}$ may depend on empirical facts.

Our truth theory $\mathsf {CD}$ itself is formulated in the full language $\mathcal {L}$ ; but the disquotation schema is restricted to sentences of $\mathfrak {D}$ , that is, to the sentences of the base language and those needed for semantic ascent and generalization. Being a sentence of $\mathfrak {D}$ is expressed in $\mathsf {CD}$ by the primitive predicate symbol $\mathrm {D}$ , which is suitably axiomatized. As disquotation schema we can then use $\mathrm {D}\ulcorner \phi \urcorner \rightarrow (\mathrm {T}\ulcorner \phi \urcorner \leftrightarrow \phi )$ for all sentences of $\mathcal {L}$ , or rather a generalization thereof with parameters. We call the sentences in $\mathfrak {D}$ determinate. If it were not for the additional predicate $\mathrm {D}$ , they would be the sentences that are grounded in Kripke’s [28] sense (with some qualifications).

This approach ensures that truth can be used as a device of generalization over sentences in $\mathcal {L}_0$ and over generalizations of such generalizations, and so on. Hence this use of truth is fully available in $\mathsf {CD}$ . However, disquotation is not available for sentences that cannot be reached by semantic ascent and generalization.

2.1 Determinateness

We describe and axiomatize $\mathfrak {D}$ , the set of determinate sentences in more detail. First, we declare all atomic sentences of the base language $\mathcal {L}_0$ determinate:

1. D1

That is, all closed identity statements are determinate. If there were further predicate symbols in the base language, analogous axioms would be added. The axioms below will enable us to prove that all sentences of the base language $\mathcal {L}_0$ are determinate.

If and only if $\phi $ is determinate, that is, in $\mathfrak {D}$ , we add a copy $\mathrm {T}\ulcorner \phi \urcorner $ of $\phi $ to $\mathfrak {D}$ . This is stated for arbitrary closed terms t, not only numerals $\ulcorner \phi \urcorner $ :

1. D2

The expression ${t}^{\circ }$ stands for the value of the term t. We cannot have a function symbol ${}^{\circ }$ in our language, and thus this function needs to be expressed by a suitable formula.

A negated sentence is determinate iff the sentence is:

1. D4

Whether a conjunction is determinate depends on the determinateness of its conjuncts. Clearly, if both conjuncts are determinate, then so is their conjunction; and if both are indeterminate, so is their conjunction. But is a conjunction determinate if only one conjunct is?

Our choice here is motivated by the function of truth as a generalizing device. Typically, a universal generalization would have the form $\forall x\, (\phi (x)\rightarrow \mathrm {T} x)$ . The formula $\phi (x)$ could express that x is a provable sentence of Peano arithmetic or that x is sentence of the form $\mathrm {T}\ulcorner \mathrm {T}\cdots \ulcorner 0\! =\!0\urcorner \urcorner \cdots \urcorner $ . We consider the simple example $\forall x\, (x\! =\!\ulcorner 0\! =\! 0\urcorner \rightarrow \mathrm {T} x)$ whose antecedent is satisfied by a single sentence only; we ‘generalize’ via semantic ascent over all sentences of the form $0\! =\! 0$ . Of course, generalization via semantic ascent is not needed for a single sentence; but ‘generalizing’ over a single sentence demonstrates the principle. If $\mathfrak {D}$ contains the sentences required for generalizing via semantic ascent, then $\forall x\, (x=\ulcorner 0\! =\! 0\urcorner \rightarrow \mathrm {T} x)$ should be determinate. The determinateness of universal quantified sentences depends on their instances. Let $\lambda $ be an indeterminate sentence. Then the instance

(1) $$ \begin{align} \ulcorner \lambda\urcorner\! =\!\ulcorner 0\! =\! 0\urcorner\,\rightarrow\, \mathrm{T} \ulcorner \lambda\urcorner \end{align} $$

has a determinate antecedent and an indeterminate consequent, by axioms D1 and D2. If the instance (1) were indeterminate, so would be the universal generalization $\forall x\, (x\! =\!\ulcorner 0\! =\! 0\urcorner \rightarrow \mathrm {T} x)$ by any reasonably determinateness rules for quantification. Hence, our axioms for $\mathrm {D}$ should declare (1) determinate.

The determinateness of (1) should follow from the determinateness of the antecedent $\ulcorner \lambda \urcorner \! =\!\ulcorner 0\! =\! 0\urcorner $ . The falsity of the determinate antecedent renders the consequent irrelevant; and the truth value of (1) does not depend on the consequent. Thus, we stipulate that a sentence $\phi \rightarrow \psi $ can inherit its determinateness from a determinate and false antecedent. Equally, we also postulate that it is determinate if it has a true and determinate consequent.

This method of generalization applies equally if we do not only ‘generalize’ over a single sentence such as $0 = 0 $ , but, for instance, over all sentences provable in $\mathsf {PA}$ . Moreover, iterated semantic ascent permits generalization over all sentences $0\! =\! 0$ , $\mathrm {T}\ulcorner 0\! =\! 0\urcorner $ , $\mathrm {T}\ulcorner \mathrm {T}\ulcorner 0\! =\! 0\urcorner \urcorner $ , and so on.

In our official language negation and conjunction are our only connectives. $\phi \rightarrow \psi $ is conceived as an abbreviation of $\neg (\phi \wedge \neg \psi )$ . In the presence of D4 we can then state our determinateness axiom for binary connectives in the following way:

• $\phi \wedge \psi $ is determinate iff:

• $\phi $ and $\psi $ are both determinate, or

• one of the conjuncts is false and determinate.

This is expressed in the following axiom:

1. D5

By our conventions above, $\mathrm {F} x$ abbreviates , namely, falsehood of x; also note that $\mathrm {D} x$ and are equivalent by the axiom D4. By axiom T4, $\mathrm {F}$ can be replaced with $\neg \mathrm {T}$ .

Another way to argue for our treatment of binary connectives would be to argue that sentences such as $\forall x\, (x=\ulcorner 0\! =\! 0\urcorner \rightarrow \mathrm {T} x)$ and its instance (1) are only about the determinate sentence $0\! =\! 0$ and should be treated just like $\mathrm {T}\ulcorner 0\! =\! 0\urcorner $ . The latter is determinate by axiom D1. Thus, it may be argued, semantic ascent applies to (1) and the universally quantified sentence in the same way it applies to $\mathrm {T}\ulcorner 0\! =\! 0\urcorner $ . However, making precise the underlying notion of aboutness is notoriously challenging (see Picollo [33, 34]); we do not attempt to pursue this line here.

Universally quantified sentences are treated as conjunctions of their instances:

1. D6

Injecting the notion of determinateness into the object language makes it possible to apply the truth and determinateness predicates to sentences containing $\mathrm {D}$ . We treat both, truth and determinateness, as completely type-free: $\mathrm {D}$ and $\mathrm {T}$ can be applied meaningfully to any sentence of the language. This is in contrast to traditional conceptions of groundedness, which apply to sentences with truth, while truth cannot be applied to sentences containing groundedness claims. Therefore, in our setting, the question arises whether atomic sentences of the form $\mathrm {D} t$ are determinate.

Treating $\mathrm {D}$ like an elementary predicate of $\mathcal {L}_0$ , that is, a predicate from $\mathcal {L}_0$ would suggest the axiom . This would mean that we have $\mathrm {T}\ulcorner \mathrm {D} t\urcorner \leftrightarrow \mathrm {D} t$ for all terms t. However, when it comes to complex sentences, we axiomatize $\mathrm {D}$ in terms of $\mathrm {T}$ in D5 and D6. Hence, it looks unsafe to declare all sentence $\mathrm {D} t$ determinate; $\mathrm {D}$ should be treated with the same caution as $\mathrm {T}$ : If, and only if $\phi $ is determinate, we stipulate that $\mathrm {D}\ulcorner \phi \urcorner $ is determinate. Generalizing this to terms other than numerals gives the following axiom analogous to D2:

1. D3

This concludes the list of determinateness axioms.

2.2 Disquotation

We still need to add axioms stipulating that a sentence $\mathrm {T}\ulcorner \phi \urcorner $ in $\mathfrak {D}$ is always obtained by semantic ascent and thus a ‘copy’ of $\phi $ . Formally, we require that $\mathrm {D}\ulcorner \phi \urcorner \rightarrow (\mathrm {T}\ulcorner \phi \urcorner \leftrightarrow \phi )$ is a theorem of our theory $\mathsf {CD}$ for every sentence of $\mathcal {L}$ . We also require that our theory proves a more general, ‘uniform’ version of the disquotation schema; that is, we generalize it by quantifying over the closed terms and postulate for every formula $\phi (x_1,\ldots , x_n)$ with at most $x_1,\ldots ,x_n$ the following:

1. DDS

In this uniform determinate disquotation schema the expression stands for a complex term expressing that $t_1,\ldots ,t_n$ are formally substituted for the free variables in $\phi (x_1,\ldots ,x_n)$ . This permits us to bind the variables $t_1,\ldots ,t_n$ in . This concludes the list of axioms for our theory $\mathsf {CD}$ .

2.3 Alternative axiomatizations

In the presence of the compositional axioms T4 –T6, we need to stipulate DDS only for atomic $\phi $ . Whatever our policy on disquotation is, we can always focus on the atomic instances; T4 –T6 will ensure that also all instances of $T\ulcorner \phi \urcorner \leftrightarrow \phi $ will be provable for all sentences $\phi $ built from those atomic formulae. Because we aim at an axiomatization that is as lean as possible for technical reasons, our official axiomatization does not feature schema DDS, but only disquotational axioms concerning atomic sentences. In particular, schema DDS can be replaced with the following three axioms:

1. T1

2. T2

3. T3

T2 can be derived from the following instance of DDS and axiom D3:

(2)

Thus the three axioms imply DDS in the presence of the other axioms as is established in Lemma 3.1.

The principles T3, (2), and T2 show that the truth and determinateness predicates interact in a serious manner. In particular, $\mathrm {D}$ is not only a formalization of a metatheoretic notion that has been injected into the object language; predicates of the object language—and especially the truth predicate—can be meaningfully applied to sentences with $\mathrm {D}$ .

From (2) we can prove one direction of the T-sentences $\phi \rightarrow \mathrm {T}\ulcorner \phi \urcorner $ for all sentences without $\mathrm {T}$ , including those with $\mathrm {D}$ . Some sentences without $\mathrm {T}$ but with $\mathrm {D}$ —such as $\mathrm {D}\ulcorner \lambda \urcorner $ for some indeterminate $\lambda $ —are not determinate, and thus DDS will not give us the T-schema for some sentences with $\mathrm {D}$ . Therefore, we consider the addition of the right-to-left direction to T2:

1. T2 ⁺ .

This sentence is not provable from the disquotation schema DDS, and is not covered by our policy about $\mathfrak {D}$ . With $\textsf {T2}^{+}$ we can derive all T-sentences $\mathrm {T}\ulcorner \phi \urcorner \leftrightarrow \phi $ as long as $\phi $ is $\mathrm {T}$ -free.

Determinateness is one of many predicates such as analyticity, knowledge, necessity, and logical validity that are deeply intertwined with truth. Having the T-sentences $\mathrm {T}\ulcorner \phi \urcorner \leftrightarrow \phi $ also for $\phi $ containing such predicates may be desirable; but we know already that this is not be possible for all such $\phi $ (see Halbach [20]), as axioms like $\textsf {T2}^{+}$ may engender inconsistency, depending on the axioms for the other predicates. We cannot think of a better strategy than to consider these axioms on a case-by-case basis and to endorse axioms like $\textsf {T2}^{+}$ , as long as they do not yield undesirable consequences. With $\textsf {T2}^{+}$ we leave the safety of disquotation for determinate sentences only. In the case of determinateness we show that axiom $\textsf {T2}^{+}$ does not affect the -soundness of our theory and thus $\textsf {T2}^{+}$ can be added as a further optional axiom.

The quantifier $\forall t$ in D2, D3, T2, T3, and $\textsf {T2}^{+}$ ranges over all closed terms, including those that do not denote a sentence. It may be desirable to restrict the quantifier in these axioms to terms denoting sentences. This would allow us to make any stipulations about sentences $\mathrm {T} t$ and $\mathrm {D} t$ where t fails to denote a sentence. We have chosen the version above for their simplicity.

2.4 Extensionality

In this section we discuss two additional axioms that are irrelevant to most of the metamathematical properties of our system. However, at least the first of these axioms is conceptually important. The issue goes beyond our specific system, and even beyond axiomatic theories, because semantic theories of truth are affected as well.

We expect truth to be an extensional notion unlike necessity, apriority, or being known. The compositional axioms prove the extensionality of truth for sentences in the following sense: Substituting a subformula in a sentence $\phi $ with another subformula with the same truth value does not affect truth or falsity of $\phi $ .

One would expect extensionality at the level of terms as well. That is, if the terms s and t have the same value, a sentence $\phi (t)$ ought to be true if, and only if $\phi (s)$ is true. However, this principle fails to be provable from the axioms we have listed so far. Only restricted versions can be proved, for instance, if the values of s and t are determinate or $\chi $ is purely arithmetical. Without axiom R1, we can refute $\mathrm {T}\ulcorner \mathrm {T} s\urcorner \wedge \neg \mathrm {T}\ulcorner \mathrm {T} t\urcorner $ under the assumption $s=t$ only for determinate s and t, but not for all terms. Here, we call a term determinate iff its value is. Thus, we state extensionality with respect to terms as an axiom:

1. R1

Axiom R1 is closely related to the question whether identity is a logical constant. Using R1, we can prove the truth of $\forall x\,\forall y\, (x\! =\! y\rightarrow (\phi (x)\rightarrow \phi (y)))$ for all formulae $\phi $ , which is a logical truth if identity is a logical constant. If identity is a logical constant and our theory is to prove all logically valid sentences, then we have to add R1 (or some other axiom). ³

So far we have focused on truth. For determinateness we also stipulate extensionality:

1. R2

Whether determinateness should also be extensional may be less clear. For our purposes the extensionality of determinateness is not decisive. Omitting R2 would not affect the results below.

3 Axioms for classical determinate truth

We now collect the stipulations in the previous sections. We start from the language $\mathcal {L}_0$ of arithmetic. It contains at least a constant for $0$ and a function symbol S for the successor function, a symbol $+$ for addition, and a symbol $\cdot $ for multiplication. For each number n we use the numeral , defined as the result of applying S to $0$ for n-many times, as the canonical name for n. $\mathcal {L}_0$ may feature further function and constant symbols, even those for all primitive recursive functions. The identity symbol $=$ is the only predicate symbol of $\mathcal {L}_0$ ; but further predicate symbols could easily be added. ⁴

The language $\mathcal {L}_{\mathrm {T}}$ is $\mathcal {L}_0$ augmented with $\mathrm {T}$ ; $\mathcal {L}_{\mathrm {D}}$ is $\mathcal {L}_0$ augmented with $\mathrm {D}$ . Adding both $\mathrm {T}$ and $\mathrm {D}$ to $\mathcal {L}_0$ yields the language $\mathcal {L}$ . Therefore, the following inclusions hold, if the languages are identified with the set of their formulae:

$$\begin{align*}\mathcal{L}_0 \subset \mathcal{L}_{\mathrm{T}}\ \mathrm{and}\ \mathcal{L}_{\mathrm{D}} \subset \mathcal{L.} \end{align*}$$

Our system is labelled $\mathsf {CD}$ for ‘Classical Determinate Truth’. It is formulated in the language $\mathcal {L}$ with $\mathrm {D}$ and $\mathrm {T}$ . The syntax of $\mathcal {L}$ is appropriately arithmetized within $\mathsf {PA}$ . We adopt the notation of Halbach [21] concerning arithmetization of syntax. However, for dealing with new predicate $\mathrm {D}$ and other technical reasons, we slightly supplement (and change) his notation as follows:

• • , ${{\mathrm {Sent}}_{\mathrm {T}}} ( x )$ , ${{\mathrm {Sent}}_{\mathrm {D}}} ( x )$ , and ${{\mathrm {Sent}}_{0}} ( x )$ represent the set of codes of $\mathcal {L}$ -, $\mathcal {L}_{\mathrm {T}}$ -, $\mathcal {L}_{\mathrm {D}}$ -, and $\mathcal {L}_0$ -sentences, respectively.

• • , ${\mathrm {Fml}_{\mathrm {T}}} ( x )$ , ${\mathrm {Fml}_{\mathrm {D}}} ( x )$ , and ${\mathrm {Fml}_{0}} ( x ),$ respectively, represent the set of codes of formula of these languages.

• • Similarly, we use , ${\mathrm {AtFml}_{\mathrm {T}}} ( x )$ , ${\mathrm {AtFml}_{\mathrm {D}}} ( x )$ , and ${\mathrm {AtFml}_{0}} ( x )$ for the codes of atomic formulae of these languages, and , ${\mathrm {AtSent}_{\mathrm {T}}} ( x )$ , ${\mathrm {AtSent}_{\mathrm {D}}} ( x )$ , and ${\mathrm {AtSent}_{0}} ( x )$ for the codes of atomic sentences of these languages, respectively.

• • and represent the sets of codes of variables and codes of $\mathcal {L}$ -terms (= the set of codes of $\mathcal {L}_0$ -terms), respectively; recall that is for the set of codes of closed $\mathcal {L}_0$ -terms, and note that every closed $\mathcal {L}$ -term is a closed $\mathcal {L}_0$ -term.

• • For each primitive predicate symbol R with arity k, is a k-ary function that represents the syntactic operation of applying R to k-many terms. For instance, is an arithmetical representation of the syntactic operation of applying $\mathrm {D}$ to a term.

• • $x ( y / z )$ represents the syntactic substitution of a term y for a variable z in an expression x.

Hence, it can be proved in $\mathsf {PA}$ that implies that v is the code of a variable (i.e., ) and that x codes some formula $\phi $ with at most one free variable. We use to express that x is a formula with at most the variable v free. Often we need to quantify over closed terms and abbreviate as $\forall t\, \psi (t)$ and also use s as a further variable ranging over closed terms.

The system $\mathsf {CD}$ is given by all axioms of $\mathsf {PA}$ with induction in the language $\mathcal {L}$ with $\mathrm {T}$ and $\mathrm {D}$ and the following axioms:

Truth axioms

1. T1

2. T2

3. T3

4. T4

5. T5

6. T6

Determinateness axioms

1. D1

2. D2

3. D3

4. D4

5. D5

6. D6

As explained above, $\mathrm {F} x$ abbreviates , which expresses the falsity of x.

Extensionality axioms

1. R1

2. R2

We now turn to some subsystems and supersystems of $\mathsf {CD}$ in order to assess the significance of axioms T2 and D3. It will be shown that removing one of these two axioms or both does not affect the proof-theoretic strength of $\mathsf {CD}$ . That is, the three systems

$$ \begin{align*} \mathsf{CD}_{\mathsf{0}}& := \mathsf{CD} - \mathsf{T2} - \mathsf{D3}\\ \mathsf{CD}_{\mathsf{1}} &:= \mathsf{CD} - \mathsf{T2} \\ \mathsf{CD}_{\mathsf{2}} &:= \mathsf{CD} - \mathsf{D3} \end{align*} $$

are proof-theoretically equivalent, although they are different theories.

The addition of axiom $\textsf {T2}^{+}$ boosts the proof-theoretic strength of $\mathsf {CD}$ , that is,

$$ \begin{align*} & \mathsf{CD}^{+} := \mathsf{CD} + \mathsf{T2}^{+} \\ & \mathsf{CD}_{\mathsf{2}}^{+} := \mathsf{CD}_{\mathsf{2}} + \mathsf{T2}^{+} \end{align*} $$

is properly stronger than $\mathsf {CD}$ . Further variants of $\mathsf {CD}$ will be studied in Part II of the paper.

We define disjunction $\vee $ , conditional $\rightarrow $ , and the existential quantifier $\exists $ in the standard manner in terms of negation $\neg $ , conjunction $\wedge $ , and universal quantifier $\forall $ : accordingly, their corresponding operations

,

, and

are defined as

It readily follows from T4 to T6 that $\mathrm {T}$ commutes with $\vee $ , $\rightarrow $ , and $\exists $ . In addition, the following compositional rules of determinateness for these connectives are provable in $\mathsf {CD}_{\mathsf {0}}$ :

(3)

(4)

(5)

Concluding this section, we mention some simple observations. First, we show that the uniform determinate disquotation schema is provable in $\mathsf {CD}$ , as mentioned above.

Lemma 3.1. For all $\mathcal {L}$ -formulae $\phi ( x_{1}, \ldots , x_{k} )$ with at most $x_{1}, \ldots , x_{k} $ free the theory $\mathsf {CD}$ proves the following:

1. DDS

In particular, $\mathrm {D} \ulcorner \phi \urcorner \rightarrow ( \mathrm {T}\hspace{1pt} \ulcorner \phi \urcorner \leftrightarrow \phi ) $ is provable for all sentences $\phi $ .

The lemma can be proved by a metatheoretic induction on the complexity of $\phi $ , where the complexity of a formula $\phi $ , $\mathit {cp}(\phi )$ for short, is standardly defined: every atomic formula has the complexity $0$ ; $\mathit {cp}(\neg \phi ) = \mathit {cp}(\forall x \phi ) = \mathit {cp}(\phi ) + 1$ ; $\mathit {cp}(\phi \wedge \psi ) = \max \{ \mathit {cp}(\phi ), \mathit {cp}(\psi ) \} + 1$ .

By an induction within $\mathsf {CD}$ all sentences of the base language can be shown to be determinate. expresses that x is a sentence of $\mathcal {L}_0$ .

Lemma 3.2. .

Using these two lemmata, we can establish the T-sentences for all sentences of the base language.

Lemma 3.3. For all $\mathcal {L}_0$ -formulae $\phi ( x_{1}, \ldots , x_{k} )$ with only $x_{1}, \ldots , x_{k}$ free, we have

Obviously, we cannot have the unrestricted T-schema in any axiomatic theory of truth. Some truth theories feature one direction of the T-schema without any restrictions. However, both directions are incompatible with $\mathsf {CD}$ .

Proposition 3.4. The axiom schemata ( $\mathrm {T}$ -Out) and ( $\mathrm {T}$ -In) are defined as follows:

1. (T-Out) $\mathrm {T}\hspace{1pt} \ulcorner \phi \urcorner \rightarrow \phi $ for all $\phi \in \mathcal {L}$ .

2. (T-In) $\phi \rightarrow \mathrm {T}\hspace{1pt} \ulcorner \phi \urcorner $ for all $\phi \in \mathcal {L}$ .

Then, each of $(\mathrm {T} \text{-}\mathrm {Out})$ and $(\mathrm {T} \text{-}\mathrm {In})$ is inconsistent with T4 over arithmetic, and thus with $\mathsf {CD}$ .

Proof We first derive a contradiction from $\mathsf {CD} + (\mathrm {T}\text{-} \mathrm {Out})$ . Let $\lambda $ be the liar sentence with $\lambda \leftrightarrow \neg \mathrm {T}\hspace{1pt} \ulcorner \lambda \urcorner $ as above. The liar sentence $\lambda $ implies $\mathrm {T}\hspace{1pt} \ulcorner \neg \lambda \urcorner $ by T4, from which $\neg \lambda $ follows by ( $\mathrm {T}$ -Out). Hence we have $\neg \lambda $ . However, $\neg \lambda $ is equivalent to $\mathrm {T}\hspace{1pt} \ulcorner \lambda \urcorner $ and thus implies $\lambda $ by ( $\mathrm {T}$ -Out).

The inconsistency of ( $\mathrm {T}$ -In) is shown in a similar way by using the other direction of T4.

A consequence of the compositional axioms is the thorough classicality of $\mathsf {CD}$ . $\mathsf {CD}$ proves that (classical) logic is truth-preserving for the entire language $\mathcal {L}$ .

Lemma 3.5. The following holds for all formulae $\phi (x)$ and canonical provability predicates constructed from $\phi (x)$ as defining the axioms:

Here, $\mathrm {Bew}_{\phi (x)}(y)$ expresses that y is provable from all sentences $\psi $ with $\phi (\ulcorner \psi \urcorner )$ .

Proof The claim is shown by induction on the length of a proof. Since $\mathrm {T}$ commutes with all logical connectives, quantifiers, and identity in $\mathsf {CD}$ , $\mathsf {CD}$ proves that every logical axiom is true; note that the extensionality axioms R1 and R2 are needed to show the logical axioms for identity. Every non-logical axiom is true by the assumption. The base step is thereby obtained. The induction step is straightforward, since commutativity ensures that every logical inference rule preserves truth.

Fischer et al. [12] criticized truth theories such as FS and variants of KF formulated in classical logic, because they are incompatible with reflection principles for logic. In $\mathsf {CD}$ the soundness of a calculus for predicate logic is provable. This is a trivial consequence of the lemma above if $\mathrm {Bew} (x)$ expresses provability in pure logic.

Corollary 3.6. $\mathsf {CD}$ proves that every logically valid sentence (in classical logic) is true: namely, .

4 Semantics

McGee [31] showed that certain theories of truth that are thoroughly classical are -inconsistent. In particular, the system FS that also features axioms T1 and T4 –T6 is -inconsistent. In order to defend $\mathsf {CD}$ and its variants we therefore do not only show that they are consistent, but also that they possess -models.

In this section, we will give an -model of $\mathsf {CD}^{+}$ , namely, a model of $\mathsf {CD}^{+}$ whose $\mathcal {L}_0$ -reduct is the standard model of arithmetic. The existence of an -model entails that $\mathsf {CD}^{+}$ and thus $\mathsf {CD}$ are -consistent. ⁵

4.1 The model

Let us define $\mathcal {L}$ -formulae $\mathcal {D}_{i} ( x )$ ( $1 \leq i \leq 6$ ) as follows:

We thereby define $\mathcal {D} ( x ) :\Leftrightarrow \bigvee _{1 \leq i \leq 6} \mathcal {D}_{i} ( x )$ . $\mathcal {D}$ describes the closure condition of a determinateness predicate $\mathrm {D}$ (relative to a fixed interpretation of the truth predicate $\mathrm {T}$ ).

By $( \mathbb {N}, X, Y )$ let us denote the $\mathcal {L}$ -structure with domain

, the set of natural numbers, in which $\mathrm {D}$ is interpreted by X, $\mathrm {T}$ is interpreted by Y, and all the other symbols receive the standard interpretations. Both $\mathrm {D}$ and $\mathrm {T}$ occur only positively in $\mathcal {D}$ . Hence, for each

, $\mathcal {D}$ induces the following monotone operator

so that

In general, given a monotone operator

, we say that

is $\Gamma $ -closed if $\Gamma ( X ) \subset X$ , and that

is a $\Gamma $ -fixed point if $\Gamma ( X ) = X$ .

Given an $\mathcal {L}_0$ -formula or $\mathcal {L}_0$ -term e, let us denote its standard interpretation by $e^{\mathbb {N}}$ and its Gödel number by $\# e$ . For instance, denote the set of the Gödel numbers of all $\mathcal {L}$ -sentences.

Lemma 4.1. For every , the following are equivalent. ⁶

1. 1. X is a $\Gamma _{\mathcal {D} [ Y ]}$ -fixed point.

2. 2. $( \mathbb {N}, X, Y )$ is a model of all the determinateness axioms D1–D6.

For each ordinal $\alpha $ , we define sets $D_{\alpha }$ and $T_{\alpha }$ as follows:

It is obvious from the definition that $T_{\lambda } = D_{\lambda } \cap T_{\lambda }$ for all limit ordinals $\lambda $ . We can also show by induction on ordinals that

for all ordinals $\xi $ .

The next two propositions are obvious by definition.

Lemma 4.2. Let $\xi $ be any ordinal, a be a closed $\mathcal {L}_0$ -term, $\phi $ and $\psi $ be $\mathcal {L}$ -sentences, and $\theta ( x )$ be an $\mathcal {L}$ -formula with only a single variable x free.

1. 1. If $\xi> 0$ and $\phi $ is $\mathcal {L}_0$ -atomic, then $\# \phi \in D_{\xi }$ .

2. 2. $a^{\mathbb {N}} \in D_{\xi }$ iff $\# \mathrm {T} a \in D_{\xi + 1}$ .

3. 3. $a^{\mathbb {N}} \in D_{\xi }$ iff $\# \mathrm {D} a \in D_{\xi + 1}$ .

4. 4. $\# \phi \in D_{\xi }$ iff $\# \neg \phi \in D_{\xi + 1}$ .

5. 5. $\# ( \phi \wedge \psi ) \in D_{\xi + 1}$ , iff either $\# \phi , \# \psi \in D_{\xi }$ or $\# \neg \phi \in D_{\xi } \cap T_{\xi }$ or $\# \neg \psi \in D_{\xi } \cap T_{\xi }$ .

6. 6. $\# \forall x \theta ( x ) \in D_{\xi + 1}$ , iff either of the following holds:

   • • $\# \theta ( b ) \in D_{\xi }$ for all $\mathcal {L}_0$ -closed terms b;

   • • $\# \neg \theta ( b ) \in D_{\xi } \cap T_{\xi }$ for some $\mathcal {L}_0$ -closed term b.

Proof For example, we have and $( ( \# a )^{\circ } )^{\mathbb {N}} = a^{\mathbb {N}}$ , from which claim 2 follows, since we have

$$ \begin{align*} a^{\mathbb{N}} \in D_{\xi} \quad \Leftrightarrow \quad ( \mathbb{N}, D_{\xi}, T_{\xi} ) \models \mathcal{D}_{2} ( \# \mathrm{T} a ) \quad \Leftrightarrow \quad \# \mathrm{T} a \in D_{\xi + 1}.\\[-33pt] \end{align*} $$

Lemma 4.3. Let $\xi $ be any ordinal, a and b be closed $\mathcal {L}_0$ -terms, $\phi $ and $\psi $ be $\mathcal {L}$ -sentences, and $\theta ( x )$ be an $\mathcal {L}$ -formula only with some single variable x free.

1. 1. $\# ( a = b ) \in T_{\xi + 1}$ iff $a^{\mathbb {N}} = b^{\mathbb {N}}$ .

2. 2. $a^{\mathbb {N}} \in T_{\xi }$ iff $\# \mathrm {T} a \in T_{\xi + 1}$ .

3. 3. $a^{\mathbb {N}} \in D_{\xi }$ iff $\# \mathrm {D} a \in T_{\xi + 1}$ .

4. 4. $\# \neg \phi \in T_{\xi + 1}$ iff $\phi \not \in T_{\xi + 1}$ .

5. 5. $\# ( \phi \wedge \psi ) \in T_{\xi + 1}$ iff $\# \phi \in T_{\xi + 1}$ and $\# \psi \in T_{\xi + 1}$ .

6. 6. $\# \forall x \theta ( x ) \in T_{\xi + 1}$ iff $\# \theta ( c ) \in T_{\xi + 1}$ for all closed $\mathcal {L}_0$ -terms c.

Let us define a formula $x \approx y$ as follows:

Namely, for natural numbers $n, m \in \mathbb {N}$ , $n \approx ^{\mathbb {N}} \! m$ means that either $n = m$ or n and m code numerically equivalent $\mathcal {L}$ -sentences in the sense that they are substitution instances of the same $\mathcal {L}$ -formula with closed terms with the same values. Since all the existential quantifiers in the definition can actually be bounded by the values of some primitive recursive functions on x and y, the relation $\approx ^{\mathbb {N}}$ is primitive recursive in the value function (or the index function $[ \, \cdot \, ]$ of the primitive recursive functions) and thus provably recursive in $\mathsf {PA}$ . The extensionality axioms R1 and R2 say that truth and determinateness are invariant across numerically equivalent $\mathcal {L}$ -sentences, namely, sentences $\phi $ and $\psi $ with $\# \phi \approx ^{\mathbb {N}} \# \psi $ . ⁷ The following proposition is shown by a straightforward induction on ordinals.

Proposition 4.4. Let $\xi $ be any ordinal and $n \approx ^{\mathbb {N}}\! m$ .

1. 1. $n \in D_{\xi }$ iff $m \in D_{\xi }$ .

2. 2. $n \in T_{\xi }$ iff $m \in T_{\xi }$ ; note that if $\# \phi \approx ^{\mathbb {N}} \# \psi $ then $( \mathbb {N}, X, Y ) \models \phi \leftrightarrow \psi $ .

The next is the main lemma of this subsection.

Lemma 4.5. For all ordinals $\xi $ and $\eta $ with $\xi \leq \eta $ , the following hold:

1. 1. $D_{\xi } \cap T_{\xi } = D_{\xi } \cap T_{\eta }$ and

2. 2. $D_{\xi } \subset D_{\eta }$ .

Proof By simultaneous induction on $\xi $ . The base step is trivial. Let $\xi $ be a limit ordinal and $\eta \geq \xi $ . For each $n \in D_{\xi }$ , there is some $\zeta < \xi $ such that $n \in D_{\zeta }$ , for which we have $D_{\zeta } \cap T_{\xi } = D_{\zeta } \cap T_{\zeta } = D_{\zeta } \cap T_{\eta }$ and $D_{\zeta } \subset D_{\eta }$ by the induction hypothesis.

Let $\xi $ be a successor ordinal. Claim 1 is shown by sub-induction on $\eta $ ; we can assume $\eta> \xi $ . First, suppose $\eta $ is a limit. If $n \in D_{\xi } \cap T_{\xi }$ , then $n \in T_{\eta }$ by definition. Let $n \in D_{\xi } \cap T_{\eta }$ for the converse. By definition, there is some $\zeta < \eta $ such that $n \in D_{\zeta } \cap T_{\zeta }$ . If $\zeta < \xi $ , then $D_{\zeta } \cap T_{\zeta } \subset T_{\xi }$ by the induction hypothesis for 1; otherwise, $\xi \leq \zeta < \eta $ and thus $D_{\xi } \cap T_{\zeta } = D_{\xi } \cap T_{\xi }$ by the sub-induction hypothesis. Next, suppose $\eta $ is a successor, and take any $n = \# \phi \in D_{\xi }$ ( ) for an $\mathcal {L}$ -sentence $\phi $ . If $\phi $ is an $\mathcal {L}_0$ -atomic, then the claim follows from Lemmata 4.2.1 and 4.3.1. If $\phi = \mathrm {T} a$ for some closed $\mathcal {L}_0$ -term a, then we have $a^{\mathbb {N}} \in D_{\xi - 1}$ by Lemma 4.2.2, and thus we obtain

$$\begin{align*}n \in T_{\xi} \stackrel{ 4.3.2 }{ \quad \Leftrightarrow \quad } a^{\mathbb{N}} \in T_{\xi - 1} \stackrel{ \mathrm{IH} }{ \quad \Leftrightarrow \quad } a^{\mathbb{N}} \in T_{\eta - 1} \stackrel{ 4.3.2 }{ \quad \Leftrightarrow \quad } n \in T_{\eta}, \end{align*}$$

where ‘IH’ denotes the induction hypothesis. If $\phi = \mathrm {D} a$ , then we have $a^{\mathbb {N}} \in D_{\xi - 1}$ by Lemma 4.2.3, and thus $n \in T_{\xi }$ and $a^{\mathbb {N}} \in D_{\eta - 1}$ by Lemma 4.3.3 and the induction hypothesis for 2, respectively, the latter of which implies $n \in T_{\eta }$ again by Lemma 4.3.3; hence, both $n \in T_{\xi }$ and $n \in T_{\eta }$ hold. We move on to the cases for complex $\phi $ s. Let $\phi = \psi \wedge \theta $ . By Lemma 4.2.5, $n \in D_{\xi }$ implies

$$ \begin{align*} & \bigl( \# \psi, \# \theta \in D_{\xi - 1} \bigr) \vee \bigl( \# \neg \psi \in D_{\xi - 1} \cap T_{\xi - 1} \bigr) \vee \bigl( \# \neg \theta \in D_{\xi - 1} \cap T_{\xi - 1} \bigr). & \end{align*} $$

If the first disjunct holds, then we have

$$ \begin{align*} n \in T_{\xi} \stackrel{ 4.3.5 }{ \ \ \Leftrightarrow \ \ } \# \psi, \# \theta \in T_{\xi} \stackrel{\mathrm{IH}}{ \ \ \Leftrightarrow \ \ } \# \psi, \# \theta \in T_{\xi - 1} \stackrel{\mathrm{IH}}{ \ \ \Leftrightarrow \ \ } \# \psi, \# \theta \in T_{\eta} \stackrel{ 4.3.5 }{ \ \ \Leftrightarrow \ \ } n \in T_{\eta}. \end{align*} $$

If the second disjunct holds, then we have $\# \neg \psi \in T_{\xi } \cap T_{\eta }$ by the induction hypothesis for 1, from which we can infer

$$ \begin{align*} \# \neg \psi \in T_{\xi} \cap T_{\eta} \stackrel{4.3.4}{ \quad \Leftrightarrow \quad } \# \psi \not\in T_{\xi}\ \mathrm{and}\ \# \psi \not\in T_{\eta} \stackrel{4.3.5}{ \quad \Rightarrow \quad } \# \phi \not\in T_{\xi}\ \mathrm{and}\ \# \phi \not\in T_{\eta}. \end{align*} $$

The case where the third disjunct holds can be similarly treated. The claim for the remaining cases where $\phi $ is of the form $\neg \psi $ or $\forall x \psi ( x )$ can be shown similarly.

Claim 2 for a successor $\xi $ is also shown by sub-induction on $\eta $ . As before, we can assume $\eta> \xi $ , and the limit case is obvious. Let $\eta $ be a successor ordinal and take any $n = \# \phi \in D_{\xi }$ for an $\mathcal {L}$ -sentence $\phi $ . If $\phi $ is $\mathcal {L}_0$ -atomic, then the claim trivially obtains by Lemma 4.2.1. If either $\varphi = \mathrm {T} a$ or $\varphi = \mathrm {D} a$ , then we have

$$ \begin{align*} n \in D_{\xi} \stackrel{\mathrm{4.2.2\ or\ 3}}{ \ \ \quad \Leftrightarrow \quad \ \ } a^{\mathbb{N}} \in D_{\xi - 1} \stackrel{\mathrm{IH}}{ \ \ \quad \Rightarrow \quad \ \ } a^{\mathbb{N}} \in D_{\eta - 1} \stackrel{\mathrm{4.2.2\ or\ 3}}{ \ \ \quad \Leftrightarrow \quad \ \ } n \in D_{\eta}. \end{align*} $$

The claim for the other cases for complex $\phi $ s can be straightforwardly shown. For instance, if $\phi = \psi \wedge \theta $ , then we have

$$ \begin{align*} & n \in D_{\xi} & & \stackrel{\mathrm{4.2.5}}{ \ \Leftrightarrow \ } & & \bigl( \# \psi, \# \theta \in D_{\xi - 1} \bigr) \vee \bigl( \# \neg \psi \in D_{\xi - 1} \cap T_{\xi - 1} \bigr) \vee \bigl( \# \neg \theta \in D_{\xi - 1} \cap T_{\xi - 1} \bigr) &\\ & & & \stackrel{\mathrm{IH}}{ \ \Rightarrow \ } & & \bigl( \# \psi, \# \theta \in D_{\eta - 1} \bigr) \vee \bigl( \# \neg \psi \in D_{\eta - 1} \cap T_{\eta - 1} \bigr) \vee \bigl( \# \neg \theta \in D_{\eta - 1} \cap T_{\eta - 1} \bigr) &\\ & && \stackrel{\mathrm{4.2.5}}{ \ \Leftrightarrow \ } & & n \in D_{\eta}. & \end{align*} $$

The other cases can be treated in a similar way.

Lemma 4.6. Let $\phi $ be an $\mathcal {L}$ -sentence and $\xi $ an ordinal.

1. 1. If $\# \phi \in D_{\xi }$ , then $\# \phi \in T_{\xi }$ iff $( \mathbb {N}, D_{\xi }, T_{\xi } ) \models \phi $ .

2. 2. If $a^{\mathbb {N}} = \# \phi \in D_{\xi }$ , then $( \mathbb {N}, D_{\xi }, T_{\xi } ) \models \phi $ iff $( \mathbb {N}, D_{\xi }, T_{\xi } ) \models \mathrm {T} a$ .

Proof

1. 1. Let $\# \phi \in D_{\xi }$ . Then, we have

   $$ \begin{align*} \# \phi \in T_{\xi} \stackrel{4.5.1}{ \quad \Leftrightarrow \quad } \# \phi \in T_{\xi + 1} \stackrel{\mathrm{def}}{ \quad \Leftrightarrow \quad } \# ( \mathbb{N}, D_{\xi}, T_{\xi} ) \models \phi. \end{align*} $$

2. 2. Let $a^{\mathbb {N}} = \# \phi \in D_{\xi }$ . Then, we have

   $$ \begin{align*} ( \mathbb{N}, D_{\xi}, T_{\xi} ) \models \phi \stackrel{\mathrm{by\ 1}}{ \quad \Leftrightarrow \quad } \# \phi \in T_{\xi} \stackrel{\mathrm{def}}{ \quad \Leftrightarrow \quad } ( \mathbb{N}, D_{\xi}, T_{\xi} ) \models \mathrm{T} a.\\[-51pt] \end{align*} $$

Lemma 4.7.

1. 1. For each $\xi $ and $\mathcal {L}$ -sentence $\phi $ , either $\# \phi \not \in T_{\xi }$ or $\# \neg \phi \not \in T_{\xi }$ .

2. 2. For each $\xi $ and $\mathcal {L}$ -sentence $\phi $ , if $\# \phi \in D_{\xi }$ , then either $\# \phi \in T_{\xi }$ or $\# \neg \phi \in T_{\xi }$ .

Proof 1. By induction on $\xi $ . The claim for a non-limit $\xi $ immediately follows by definition. Let $\xi $ be a limit, and suppose for contradiction that $\# \phi \in T_{\xi }$ and $\# \neg \phi \in T_{\xi }$ . Then, there are some $\zeta , \eta < \xi $ such that $\# \phi \in T_{\zeta } \cap D_{\zeta }$ and $\# \neg \phi \in T_{\eta } \cap D_{\eta }$ , which is impossible by Lemma 4.5 and the induction hypothesis.

2. By induction on $\xi $ . If $\xi = 0$ , then and the claim trivially holds. If $\xi $ is a successor, then the claim immediately follows by Lemma 4.3.4. Finally, if $\xi $ is a limit and $\# \phi \in D_{\xi }$ , then $\# \phi \in D_{\zeta }$ for some $\zeta < \xi $ , and thus either $\# \phi \in T_{\zeta }$ or $\neg \phi \in T_{\zeta }$ by the induction hypothesis, from which the claim follows by Lemma 4.5.1.

Let denote the least uncountable ordinal. By Lemma 4.5, we have $D_{\xi } \subset D_{\eta }$ and $D_{\xi } \cap T_{\xi } \subset D_{\eta } \cap T_{\eta }$ for all $\xi \leq \eta $ . Hence, by the standard cardinality consideration, we have the following nice properties of and :

(6)

in particular, is a -fixed point. Let us denote and by $\mathit {D}_{\infty }$ and $\mathit {T}_{\infty }$ , respectively. We finally give an -model of $\mathsf {CD}$ .

Theorem 4.8. Let $\mathbb {T}_{\infty } := \{ \# \phi \mid ( \mathbb {N}, \mathit {D}_{\infty }, \mathit {T}_{\infty } ) \models \phi \}$ . Then, $( \mathbb {N}, \mathit {D}_{\infty }, \mathbb {T}_{\infty } ) \models \mathsf {CD}^{+}$ . Hence, in particular, $\mathsf {CD}^{+}$ and $\mathsf {CD}$ have an -model and thus are -consistent.

Proof By definition, it immediately follows that $( \mathbb {N}, \mathit {D}_{\infty }, \mathbb {T}_{\infty } )$ is a model of T1, $\textsf {T2}^{+}$ , and T4–T6. To see $( \mathbb {N}, \mathit {D}_{\infty }, \mathbb {T}_{\infty } ) \models \textsf {T3}$ , take any

and suppose $( {n}^{\circ } )^{\mathbb {N}} \in \mathit {D}_{\infty }$ . Then, there exist some closed $\mathcal {L}_0$ -term a and $\mathcal {L}$ -sentence $\phi $ such that $n = \# a$ and $( {n}^{\circ } )^{\mathbb {N}} = a^{\mathbb {N}} = \# \phi \in \mathit {D}_{\infty }$ (

). Hence, we have

Since $\mathit {D}_{\infty }$ is a $\Gamma _{\mathcal {D} [ \mathit {T}_{\infty } ]}$ -fixed point, $( \mathbb {N}, \mathit {D}_{\infty }, \mathbb {T}_{\infty } )$ satisfies D1–D4 (which does not depend on the interpretation of $\mathrm {T}$ ). To show $( \mathbb {N}, \mathit {D}_{\infty }, \mathbb {T}_{\infty } ) \models \textsf {D5}$ , take any $\mathcal {L}$ -sentences $\phi $ and $\psi $ . By Lemma 4.6.1, we have $\mathit {D}_{\infty } \cap \mathbb {T}_{\infty } = \mathit {D}_{\infty } \cap \mathit {T}_{\infty }$ and thus obtain

$$ \begin{align*} \# \phi \wedge \psi \in \mathit{D}_{\infty} & \stackrel{\mathrm{4.2.5}}{ \quad \Leftrightarrow \quad } ( \# \phi, \# \psi \in \mathit{D}_{\infty} ) \vee ( \# \neg \phi \in \mathit{D}_{\infty} \cap \mathit{T}_{\infty} ) \vee ( \# \neg \psi \in \mathit{D}_{\infty} \cap \mathit{T}_{\infty} )\\ & \stackrel{ \ }{ \quad \Leftrightarrow \quad } ( \# \phi, \# \psi \in \mathit{D}_{\infty} ) \vee ( \# \neg \phi \in \mathit{D}_{\infty} \cap \mathbb{T}_{\infty} ) \vee ( \# \neg \psi \in \mathit{D}_{\infty} \cap \mathbb{T}_{\infty} ). \end{align*} $$

We can similarly show $( \mathbb {N}, \mathit {D}_{\infty }, \mathbb {T}_{\infty } ) \models \textsf {D6}$ using $\mathit {D}_{\infty } \cap \mathit {T}_{\infty } = \mathit {D}_{\infty } \cap \mathbb {T}_{\infty }$ .

4.2 The minimality of D

In this section, we will show that $\mathit {D}_{\infty }$ ( ) has a certain ‘minimality’ property.

Let us define $\mathcal {L}$ -formulae $\mathcal {T}_{j} ( x )$ ( $1 \leq j \leq 6$ ) as follows:

We define $\mathcal {T} ( x ) :\Leftrightarrow \bigvee _{1 \leq j \leq 6} \mathcal {T}_{j} ( x )$ . Note that $\mathcal {T}$ says nothing about the Gödel numbers of $\mathcal {L}$ -sentences of the form $\neg \mathrm {D} a$ . Both $\mathrm {D}$ and $\mathrm {T}$ occur only positively in $\mathcal {T}$ . Hence, for each given

, it induces a monotone operator

such that

note that

for all

.

Lemma 4.9. Let . If $( \mathbb {N}, X, Y ) \models \mathsf {CD}$ , then Y is $\Gamma _{\mathcal {T} [ X ]}$ -closed.

Proof The proof is routine. Take any and let $n = \# \phi $ where $\phi $ is an $\mathcal {L}$ -sentence. If $\phi = \mathrm {D} a$ for a closed $\mathcal {L}_0$ -term a, then we have $a^{\mathbb {N}} \in X$ and thus $( \mathbb {N}, X, Y ) \models \mathrm {D} {a}^{\circ }$ , which implies , namely, $\# \phi \in Y$ , because $( \mathbb {N}, X, Y ) \models \textsf {T2}$ ; note that it is never the case that $\# \phi = \neg \mathrm {D} a$ for any closed $\mathcal {L}_0$ -term a. If $\phi = \neg \mathrm {T} a$ for a closed $\mathcal {L}_0$ -term a, then and thus $a^{\mathbb {N}} \in X \setminus Y$ by $( \mathbb {N}, X, Y ) \models \textsf {D4} \wedge \textsf {T4}$ , which implies $\# \phi \in Y$ because $( \mathbb {N}, X, Y ) \models \textsf {T3} \wedge \textsf {T4}$ . Next, let $\phi = \neg ( \psi \wedge \theta )$ . Then, either $\# \neg \psi \in Y$ or $\# \neg \theta \in Y$ . If the former is the case, then $\# \psi \not \in Y$ by $( \mathbb {N}, X, Y ) \models \textsf {T4}$ and thus $\# \phi \not \in Y$ by $( \mathbb {N}, X, Y ) \models \textsf {T5}$ , from which we get $\# \neg \phi \in Y$ by $( \mathbb {N}, X, Y ) \models \textsf {T4}$ . We leave the remaining cases to the reader.

Lemma 4.10. Let . Suppose the following:

1. (a) X is $\Gamma _{\mathcal {D} [ Y ]}$ -closed;

2. (b) Y is $\Gamma _{\mathcal {T} [ X ]}$ -closed.

Then we have $\mathit {D}_{\infty } \subset X$ and $\mathit {T}_{\infty } \subset Y$ and thus, by (6) above, $\mathit {T}_{\infty } \subset \mathit {D}_{\infty } \cap Y$ .

Proof It suffices to show the following under the supposition of (a) and (b): for all $\mathcal {L}$ -sentences $\phi $ and ordinals $\alpha $ ,

(7) $$ \begin{align} \# \phi &\in D_{\alpha} \rightarrow \# \phi \in X, \end{align} $$

(8) $$ \begin{align} \# \phi &\in D_{\alpha} \cap T_{\alpha} \rightarrow \# \phi \in Y, \end{align} $$

(9) $$ \begin{align} \# \phi &\in D_{\alpha} \setminus T_{\alpha} \rightarrow \# \neg \phi \in Y. \end{align} $$

They are shown by simultaneous induction on $\alpha $ . The base step is trivial. If $\alpha $ is a limit, the claim follows from the induction hypothesis using Lemma 4.5. Let $\alpha $ be a successor. The claim for the case where $\phi $ is an $\mathcal {L}_0$ -atomic is obvious. We will go through the remaining cases.

Let $\phi = \mathrm {T} a$ and suppose $\# \phi \in D_{\alpha }$ . We have $a^{\mathbb {N}} \in D_{\alpha - 1}$ (

) by Lemma 4.2.2. Then, we have $a^{\mathbb {N}} \in X$ by the induction hypothesis and thus $\# \phi \in X$ by (a); hence (7) holds for $\phi $ . The other claims (8) and (9) are obtained as follows:

Let $\phi = \mathrm {D} a$ and suppose $\# \phi \in D_{\alpha }$ . We have $a^{\mathbb {N}} \in D_{\alpha - 1}$ by Lemma 4.2.3. Then, we get $a^{\mathbb {N}} \in X$ by the induction hypothesis, which implies $\# \phi \in Y$ by (b); hence, (7) and (8) hold for $\phi $ . The other claim (9) trivially holds, since $\# \phi \not \in T_{\alpha }$ would imply $a^{\mathbb {N}} \not \in D_{\alpha - 1}$ by Lemma 4.3.3, which is absurd.

Let $\phi = \neg \psi $ and suppose $\# \phi \in D_{\alpha }$ . We have $\# \psi \in D_{\alpha - 1}$ by Lemma 4.2.4. Then, it follows that $\# \psi \in X$ by the induction hypothesis and thus $\# \phi \in X$ by (a). The other claims (8) and (9) are obtained as follows:

$$ \begin{align*} & \# \phi \in T_{\alpha} & & \stackrel{4.3.4}{ \Leftrightarrow } && \# \psi \not\in T_{\alpha} && \stackrel{4.5.1}{ \Leftrightarrow } && \# \psi \not\in T_{\alpha - 1} & & \stackrel{\mathrm{IH}}{ \Rightarrow } && \# \phi \in Y; & \\ & \# \phi \not\in T_{\alpha} && \stackrel{4.3.4}{ \Leftrightarrow } && \# \psi \in T_{\alpha} && \stackrel{4.5.1}{ \Leftrightarrow } & & \# \psi \in T_{\alpha - 1} && \stackrel{\mathrm{IH}}{ \Rightarrow } & & \# \psi \in Y && \stackrel{\mathrm{(b)}}{ \Rightarrow } & & \# \neg \phi \in Y. & \end{align*} $$

Let $\phi = \psi \wedge \theta $ and suppose $\# \phi \in D_{\alpha }$ . By Lemma 4.2.5, there are three cases to be separately considered. First assume $\# \psi , \# \theta \in D_{\alpha - 1}$ . Then, we get $\# \psi \in X$ and $\# \theta \in X$ by the induction hypothesis, and thus $\# \phi \in X$ by (a); hence, (7) holds for $\phi $ . We next obtain (8) as follows:

$$ \begin{align*} \# \phi \in T_{\alpha} \stackrel{4.3.5}{ \ \ \Leftrightarrow \ \ } \# \psi, \# \theta \in T_{\alpha} \stackrel{4.5.1}{ \ \ \Leftrightarrow \ \ } \# \psi, \# \theta \in T_{\alpha - 1} \stackrel{\mathrm{IH}}{ \ \ \Rightarrow \ \ } \# \psi, \# \theta \in Y \stackrel{\mathrm{(b)}}{ \ \ \Rightarrow \ \ } \# \phi \in Y. \end{align*} $$

For the remaining claim (9), we infer

$$ \begin{align*} \# \phi \not\in T_{\alpha} \stackrel{4.3.5}{ \ \ \ \Leftrightarrow \ \ \ } \# \psi \not\in T_{\alpha} \ \mathrm{or} \ \# \theta \not\in T_{\alpha} & \stackrel{4.5.1}{ \ \ \ \Leftrightarrow \ \ \ } \# \psi \not\in T_{\alpha - 1} \ \mathrm{or} \ \# \theta \not\in T_{\alpha - 1}\\ & \stackrel{\mathrm{IH}}{ \ \ \ \Rightarrow \ \ \ } \# \neg \psi \in Y \ \mathrm{or} \ \# \neg \theta \in Y \stackrel{\mathrm{(b)}}{ \ \ \ \Rightarrow \ \ \ } \# \neg \phi \in Y. \end{align*} $$

Second assume $\# \neg \psi \in D_{\alpha - 1} \cap T_{\alpha - 1}$ . We have $\# \neg \psi \in X \cap Y$ by the induction hypothesis, which implies $\# \phi \in X$ and $\# \neg \phi \in Y$ by (a) and (b); hence, (7) and (9) hold for $\phi $ . Note that $\# \phi \in T_{\alpha }$ can never be the case under the current assumption, since it would imply $\# \neg \psi \not \in T_{\alpha }$ by Lemmata 4.3.4 and 4.3.5 and thus $\# \neg \psi \not \in T_{\alpha - 1}$ by Lemma 4.5.1; hence, (8) trivially holds for $\phi $ . The case where $\# \neg \theta \in D_{\alpha - 1} \cap T_{\alpha - 1}$ can be similarly treated.

The remaining case where $\phi = \forall x \psi ( x )$ can be similarly treated to the last case, and we omit the details.

Remark 4.11. As we have remarked, $\mathit {D}_{\infty }$ is $\Gamma _{\mathcal {D} [ \mathit {T}_{\infty } ]}$ -closed. We can also show that $\mathit {T}_{\infty }$ is $\Gamma _{\mathcal {T} [ \mathit {D}_{\infty } ]}$ -closed; the proof is routine. Hence, it follows from Lemma 4.10 that $\mathit {D}_{\infty }$ and $\mathit {T}_{\infty }$ are simultaneously inductively defined by the following monotone operators from $\mathcal {P} ( \mathbb {N} ) \times \mathcal {P} ( \mathbb {N} )$ to $\mathcal {P} ( \mathbb {N} )$ :

$$ \begin{align*} & \Gamma_{\mathcal{D}} ( X, Y ) = \Gamma_{\mathcal{D} [ Y ]} ( X ) & & \mathrm{and} & & \Gamma_{\mathcal{T}} ( X, Y ) = \Gamma_{\mathcal{T} [ X ]} ( Y ). & \end{align*} $$

Lemma 4.12. Let . Suppose the same conditions (a) and (b) as in Lemma 4.10, as well as the following additional condition:

$$\begin{align*} \kern-28pt(\mathrm{c}) \qquad\qquad & \mathrm{for\ all }\ \mathcal{L}\text{-}\mathrm{sentences }\ \phi, \mathrm{ if }\ \# \phi \in X, \mathrm{ then\ either }\ \# \phi \not\in Y \mathrm{ or }\ \# \neg \phi \not\in Y. \end{align*}$$

Then the following holds.

1. 1. $\mathit {D}_{\infty } \cap Y = \mathit {T}_{\infty }$ .

2. 2. $\mathit {D}_{\infty }$ is the least $\Gamma _{\mathcal {D} [ Y ]}$ -closed set.

Proof We have $\mathit {T}_{\infty } \subset \mathit {D}_{\infty }$ by (6) and $\mathit {T}_{\infty } \subset Y$ by Lemma 4.10; hence, $\mathit {T}_{\infty } \subset \mathit {D}_{\infty } \cap Y$ . For the converse, take any $\# \phi \not \in \mathit {T}_{\infty }$ . If $\# \phi \in \mathit {D}_{\infty }$ , then we have $\# \neg \phi \in \mathit {T}_{\infty } \subset Y$ by Lemma 4.7.2 and thus $\# \phi \not \in Y$ by (c).

For claim 2, we first show that $\mathit {D}_{\infty }$ is $\Gamma _{\mathcal {D} [ Y ]}$ -closed. We observe that $\mathrm {T}$ only appears in the clauses $\mathcal {D}_{5}$ and $\mathcal {D}_{6}$ of $\mathcal {D}$ in the form . Hence, since $\mathit {D}_{\infty } \cap Y = \mathit {D}_{\infty } \cap \mathit {T}_{\infty }$ by claim 1, we have $\Gamma _{\mathcal {D} [ Y ]} ( \mathit {D}_{\infty } ) = \Gamma _{\mathcal {D} [ \mathit {T}_{\infty } ]} ( \mathit {D}_{\infty } ) \subset \mathit {D}_{\infty }$ . Now, take any $\Gamma _{\mathcal {D} [ Y ]}$ -closed set Z. Since the intersection of $\Gamma _{\mathcal {D} [ Y ]}$ -closed sets is also $\Gamma _{\mathcal {D} [ Y ]}$ -closed (by the monotonicity of $\Gamma _{\mathcal {D} [ Y ]}$ ), $\mathit {D}_{\infty } \cap Z$ is $\Gamma _{\mathcal {D} [ Y ]}$ -closed. Also, since $\mathrm {D}$ occurs in $\mathcal {T}$ only positively, it also follows that Y is $\Gamma _{\mathcal {T} [ \mathit {D}_{\infty } \cap Z ]}$ -closed; for, $\mathit {D}_{\infty } \subset X$ by Lemma 4.10 and thus $\Gamma _{\mathcal {T} [ \mathit {D}_{\infty } \cap Z ]} ( Y ) \subset \Gamma _{\mathcal {T} [ \mathit {D}_{\infty } ]} ( Y ) \subset \Gamma _{\mathcal {T} [ X ]} ( Y ) \subset Y$ . Hence, $\mathit {D}_{\infty } \cap Z$ and Y satisfy the conditions (a) and (b) of Lemma 4.10, and thus we obtain $\mathit {D}_{\infty } \subset Z$ .

The next theorem immediately follows from Lemmata 4.1, 4.9, and 4.12.

Theorem 4.13. Let $X, Y \subset \mathbb {N}$ . If $( \mathbb {N}, X, Y ) \models \mathsf {CD}$ , then the following hold:

1. 1. $\mathit {D}_{\infty } \subset X$ .

2. 2. $\mathit {D}_{\infty } \cap Y = \mathit {T}_{\infty }$ .

3. 3. $\mathit {D}_{\infty }$ is the least $\Gamma _{\mathcal {D} [ Y ]}$ -fixed point.

This theorem says that every sentence in $\mathit {D}_{\infty }$ is determinate in any -model of $\mathsf {CD}$ , the truth and the falsity are invariable on $\mathit {D}_{\infty }$ across all -models of $\mathsf {CD}$ , and $\mathit {D}_{\infty }$ is the least fixed point of $\Gamma _{\mathcal {D} [ Y ]}$ (and thus is the least set Z with $( \mathbb {N}, Z, Y ) \models \textsf {D1}-\textsf {D6}$ ) whenever $( \mathbb {N}, X, Y ) \models \mathsf {CD}$ for some X. This mathematical fact, as well as the philosophical story that motivated $\mathsf {CD}$ , suggests an axiom expressing such a minimality property of $\mathrm {D}$ , which yields a new theory $\mathsf {CD}_{\mu }$ . This axiom and the resulting system will be briefly explained in Section 9, but their full analysis is left for the Part II.

5 A lower bound of the strength of $\mathsf {CD}$

In this section, we will show that the system $\mathsf {RA}_{< \varepsilon _{0}}$ of ramified analysis up to $\varepsilon _{0}$ and the system $\mathsf {RT}_{< \varepsilon _{0}}$ of $\varepsilon _{0}$ -iterated truth (see [21] for its definition) are arithmetically conservative over $\mathsf {CD}$ , that is, every arithmetical theorem of the former system is provable in the latter system, and also that $\mathsf {RA}_{< \varepsilon _{\varepsilon _{0}}}$ and $\mathsf {RT}_{< \varepsilon _{\varepsilon _{0}}}$ are arithmetically conservative over $\mathsf {CD}^{+}$ . The reductions will be achieved by constructing a relative interpretation of intermediate systems $\mathsf {KF}$ and $\mathsf {CT} [ \! [ \mathsf {KF} ] \! ]$ in $\mathsf {CD}$ and $\mathsf {CD}^{+}$ , respectively.

5.1 The systems $\mathsf {KF}$ and $\mathsf {CT}$

For the sake of the reader’s convenience, we repeat the definition of the system $\mathsf {KF}$ of Feferman [8] (in our notation).

Definition 5.1. The $\mathcal {L}_{\mathrm {T}}$ -system $\mathsf {KF}$ is defined as $\mathsf {PA}$ with full induction in $\mathcal {L}_{\mathrm {T}}$ augmented with the following axioms:

1. K1

2. K2

3. K3

4. K4

5. K5

6. K6

7. K7

8. R3

Note that, while $\mathrm {F} x$ and $\neg \mathrm {T} x$ are equivalent in $\mathsf {CD}$ , they are not equivalent in $\mathsf {KF}$ , and we have to distinguish them when working in $\mathsf {KF}$ . It is easily shown that $\mathsf {R}3$ is redundant and provable from the other axioms (see [5, Lemma 3.1]). We will occasionally consider two extra axioms $\mathrm {Cons}$ and $\mathrm {Comp}$ , which are defined as follows:

$$ \begin{align*} \kern-90pt\mathrm{Cons}{:} \qquad\qquad\qquad\qquad\qquad\ & \forall x\, \bigl( {{\mathrm{Sent}}_{\mathrm{T}}}(x)\rightarrow\neg(\mathrm{T} x \wedge \mathrm{F} x ) \bigr), \end{align*} $$

$$ \begin{align*} \kern-96.5pt\mathrm{Comp}{:} \qquad\qquad\qquad\qquad\qquad & \!\forall x\, \bigl( {{\mathrm{Sent}}_{\mathrm{T}}} ( x ) \rightarrow ( \mathrm{T} x \vee \mathrm{F} x ) \bigr). \end{align*} $$

For each $\varphi \in \mathcal {L}_{\mathrm {T}}$ , let $\varphi ^{c}$ denote Cantini’s ‘dual’ translation of $\varphi $ : namely, $\mathrm {T}^{c} a := \neg \mathrm {F} a$ for each $\mathcal {L}_0$ -term a, and c preserves the $\mathcal {L}_0$ -vocabulary (as well as the logical connectives and quantifiers); see [5, Section 4]. c is a relative interpretation of $\mathsf {KF} + \mathrm {Cons}$ in $\mathsf {KF} + \mathrm {Comp}$ and vice versa. Cantini [5] showed that $\mathsf {KF} + \mathrm {Cons}$ and $\mathsf {KF} + \mathrm {Comp}$ are both proof-theoretically equivalent to $\mathsf {KF}$ .

Lemma 5.2. $\mathsf {KF}$ proves the following.

1. 1. .

2. 2. .

3. 3. .

Definition 5.3. Let $\mathcal {L}_{1}$ be a first-order language that extends $\mathcal {L}_0$ only with new predicate symbols. We set a new language $\mathcal {L}_{1}^{+}$ to be $\mathcal {L}_{1} \cup \{ \mathbb {T} \}$ where $\mathbb {T}$ is a fresh unary predicate symbol: the new predicate $\mathbb {T}$ will be interpreted as the Tarskian typed compositional truth for the language $\mathcal {L}_{1}$ . Let be a representation of the set of (codes of) $\mathcal {L}_{1}$ -sentences. Given any $\mathcal {L}_{1}$ -system $\mathsf {S}$ , the $\mathcal {L}_{1}^{+}$ -system $\mathsf {CT} [ \! [ \mathsf {S} ] \! ]$ is defined as $\mathsf {S}$ with all axiom schemata of $\mathsf {S}$ (possibly including other schemata than induction) extended for $\mathcal {L}_{1}^{+}$ together with the following axioms expressing Tarski’s ‘inductive clauses’ of truth.

1. 𝕋1 , for all $\mathcal {L}_{1}$ -atomic formulae $\mathrm {R} \vec {x.}$

2. 𝕋2

3. 𝕋3

4. 𝕋4

5. R4

Here we abbreviate a sequence of variables (or terms), $x_{0}, \ldots , x_{k}$ (or $a_{1}, \ldots , a_{k}$ ), by $\vec {x}$ (or $\vec {a}$ ) for saving space. If $\mathcal {L}_{1} \supset \mathcal {L}_{\mathrm {T}}$ , then $\mathbb {T}1$ contains . It can be shown in a parallel manner to the case of $\mathsf {R}3$ in $\mathsf {KF}$ that $\mathsf {R}4$ is derivable from the other axioms.

Lemma 5.4. Let $\mathsf {S}$ be as above. $\mathsf {CT} [ \! [ \mathsf {S} ] \! ]$ proves the following theorems:

1. 1.

2. 2.

3. 3.

5.2 Reduction of $\mathsf {KF}$ to $\mathsf {CD}_{\mathsf {0}}$

The translation $\natural $ of $\mathcal {L}_{\mathrm {T}}$ into $\mathcal {L}$ replaces every atomic formula $\mathrm {T}^{\natural } a $ (for a term a) with $\mathrm {T} a \wedge \mathrm {D} a $ ; $\natural $ does not change anything else.

In what follows, we will occasionally write instead of , instead of , and similarly for other formulae.

Lemma 5.5. $\natural $ is a relative interpretation of $\mathsf {KF}$ in $\mathsf {CD}_{\mathsf {0}}$ .

Proof We will only exhibit the proofs that $\natural $ preserves the axioms K2, K5, and K7. For K2, take any

. Then we have

The other conjunct can be shown similarly. For K5, take any $x, y \in {{\mathrm {Sent}}_{\mathrm {T}}}$ ; then we have

For K7, take any v and x such that

; then we have

The remaining cases are similarly and even more easily shown.

Because $\natural $ does not affect arithmetical sentences, the next corollary follows.

Corollary 5.6. $\mathsf {KF}$ is arithmetically conservative over $\mathsf {CD}_{\mathsf {0}}$ and thus $\mathsf {CD}$ .

Finally, since $\mathsf {KF}$ and $\mathsf {RA}_{< \varepsilon _{0}}$ are known to have the same arithmetical theorems by results due to Cantini [5] and Feferman [8], $\mathsf {RA}_{< \varepsilon _{0}}$ is arithmetically conservative over $\mathsf {CD}$ .

5.3 Reduction of $\mathsf {CT} [ \! [ \mathsf {KF} ] \! ]$ to $\mathsf {CD}_{\mathsf {2}}^{+}$

Let k be an $\mathcal {L}_0$ -definable function that represents the arithmetization of the translation $\natural $ of $\mathcal {L}_{\mathrm {T}}$ in $\mathcal {L}$ : that is, for all ,

(10)

With the standard coding, k is primitive recursive and thus definable in $\mathsf {PA}$ , and $\mathsf {PA}$ proves . Furthermore, with the notation of [5], $\mathsf {PA}$ also proves $\forall z \bigl ( \mathrm {Free} ( z, x ) \leftrightarrow \mathrm {Free} ( z, k x ) \bigr )$ , where $\mathrm {Free} ( a, b )$ says that a is a code of a variable that is free in the formula coded by b; in particular, we have .

We thereby extend $\natural $ to a translation of $\mathcal {L}_{\mathrm {T}}^{+}$ to $\mathcal {L}$ by stipulating the following:

$$\begin{align*}\mathbb{T}^{\natural} x \ := \ \mathrm{T} k x. \end{align*}$$

We will use the same symbol $\natural $ for the two translations for simplicity.

Lemma 5.7.

Proof By a routine induction on the complexity of x.

Lemma 5.8. The following claims are provable in $\mathsf {CD}_{\mathsf {2}}$ .

1. 1. ; by T4 and (10).

2. 2. ; by T5 and (10).

3. 3. ; by T6, (10), and Lemma 5.7.

Theorem 5.9. $\natural $ is a relative interpretation of $\mathsf {CT} [ \! [ \mathsf {KF} ] \! ]$ in $\mathsf {CD}_{\mathsf {2}}^{+}$ .

Proof It immediately follows from the definition of $\natural $ and the last lemma that the $\natural $ -translations of the axioms $\mathbb {T}1$ for all $\mathcal {L}_0$ -atomics and $\mathbb {T}2$ – $\mathbb {T}4$ are provable in $\mathsf {CD}_{\mathsf {2}}$ . $\mathsf {R}4^{\natural }$ readily follows from R1 and Lemma 5.7 (though this step is actually redundant because $\mathsf {R}4$ is derivable from the other axioms of $\mathsf {CT} [ \! [ \mathsf {KF} ] \! ]$ ). For the remaining case, i.e., the axiom $\mathbb {T}1$ for an atomic of the form $\mathrm {T} x$ , take any

. Then we have

note that the use of $\textsf {T2}^{+}$ in the third equivalence is crucial here.

Corollary 5.10. $\mathsf {CT} [ \! [ \mathsf {KF} ] \! ]$ is arithmetically conservative over $\mathsf {CD}_{\mathsf {2}}^{+}$ and thus $\mathsf {CD}^{+}\!\!\!$ .

Now, the following fact is essentially due to Cantini [5].

Fact 5.11. $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ ( $= \mathsf {CT} [ \! [ \mathsf {KF} ] \! ] + \mathrm {Cons}$ ) is arithmetically equivalent to $\mathsf {RA}_{< \varepsilon _{\varepsilon _{0}}}$ , that is, the two systems have the same arithmetical theorems.

Hence, $\mathsf {RT}_{< \varepsilon _{\varepsilon _{0}}}$ is arithmetically conservative over $\mathsf {CD}^{+}$ .

6 An upper bound of the strength of $\mathsf {CD}$

In this section, we will show that $\mathsf {CD}$ is proof-theoretically reducible to $\mathsf {KF}$ . This will be achieved via partial cut-elimination for a semi-formal system for $\mathsf {CD}$ .

6.1 Semi-formal system $\mathsf {CD}^{\infty }$

In this subsection, we will introduce a Tait-style semi-formal system $\mathsf {CD}^{\infty }$ .

Throughout this Section 6, capital Greek letters $\Gamma $ and will be used as variables ranging over finite sets of $\mathcal {L}$ -sentences, and we will only consider $\mathcal {L}$ -sentences in negation-normal form (or in what is sometimes called ‘Tait form’), which are constructed from closed $\mathcal {L}_0$ -literals by conjunction, disjunction, and universal and existential quantifiers; we will abuse the notation and denote the negation operation on negation-normal forms, which is often written as ‘ $\sim $ ’ in the literature, also by $\neg $ , e.g., $\neg ( \mathrm {T} a \wedge \mathrm {D} a ) = \neg \mathrm {T} a \vee \neg \mathrm {D} a$ . Following the convention, for a finite set $\Gamma $ of $\mathcal {L}$ -sentences and an $\mathcal {L}$ -sentence A, we will write $\Gamma , A$ for $\Gamma \cup \{ A \}$ .

The derivation relation in the semi-formal system $\mathsf {CD}^{\infty }$ for ordinals and and a set $\Gamma $ of $\mathcal {L}$ -sentences, which intuitively means that at least one $\phi \in \Gamma $ is verified by a derivation of length with cut-rank p, is defined as follows.

Axioms. Let a, b, and c be any closed $\mathcal {L}_0$ -terms, $\Gamma $ any set of $\mathcal {L}$ -sentences, any ordinal, and any finite ordinal.

1. (Ax1) If A is a true closed $\mathcal {L}_0$ -literal, then .

2. (Ax2) If $a^{\mathbb {N}} \approx ^{\mathbb {N}} b^{\mathbb {N}}$ (see p.13 for the definition of $\approx $ ), then .

3. (Ax3) If $a^{\mathbb {N}} \approx ^{\mathbb {N}} b^{\mathbb {N}}$ , then .

4. (D1) If and , then .

Logical Rules. Let A and B be $\mathcal {L}$ -sentences, $C ( x )$ an $\mathcal {L}$ -formula with at most one free variable, an ordinal, and .

1. (∨1) If for some ordinal , then .

2. (∨2) If for some ordinal , then .

3. (∧) If and for some ordinals , then .

4. (∃) If for some closed $\mathcal {L}_0$ -term a and ordinal , then .

5. (∀) If there exists some ordinal for each closed $\mathcal {L}_0$ -term a such that , then .

6. (cut) If and for some ordinals and $\mathcal {L}$ -sentence A with complexity $< p$ , then .

Rules for positive occurrences of $\mathrm {D}$ . For ordinals and and a closed term a, holds, if one of the following holds for some ordinal ⁸ :

• $( \textsf {D}{2}_{\infty }^{\mathit {pos}} )$ There is a closed term b such that and .

• $( \textsf {D}{3}_{\infty }^{\mathit {pos}} )$ There is a closed term b such that and .

• $( \textsf {D}{4}_{\infty }^{\mathit {pos}} )$ There is a closed term b such that and .

• $( \textsf {D}{5}_{\infty }^{\mathit {pos}} )$ There are some closed terms b and c such that and .

• $( \textsf {D}{6}_{\infty }^{\mathit {pos}} )$ There are some closed terms b and c such that and .

Rules for negative occurrences of $\mathrm {D}$ . For ordinals and and a closed term a, holds, if one of the following holds for some ordinal :

• $( \textsf {D}{2}_{\infty }^{\mathit {neg}}) $ There is a closed term b such that and .

• $( \textsf {D}{3}_{\infty }^{\mathit {neg}}) $ There is a closed term b such that and .

• $( \textsf {D}{4}_{\infty }^{\mathit {neg}}) $ There is a closed term b such that and .

• $( \textsf {D}{5}_{\infty }^{\mathit {neg}}) $ There are some closed terms b and c such that and .

• $( \textsf {D}{6}_{\infty }^{\mathit {neg}}) $ There are some closed terms b and c such that and .

Rules for positive occurrences of $\mathrm {T}$ . For ordinals and and a closed term a, holds, if one of the following holds for some ordinal :

• $(\textsf {T}{1}_{\infty }^{\mathit {pos}} )$ There are some closed terms b and c such that and .

• $(\textsf {T}{2}_{\infty }^{\mathit {pos}} )$ There is a closed term b such that and .

• $(\textsf {T}{3}_{\infty }^{\mathit {pos}} )$ There is a closed term b such that and .

• $(\textsf {T}{4}_{\infty }^{\mathit {pos}} )$ There is a closed term b such that and .

• $(\textsf {T}{5}_{\infty }^{\mathit {pos}} )$ There are some closed terms b and c such that and .

• $(\textsf {T}{6}_{\infty }^{\mathit {pos}} )$ There are some closed terms b and c such that and .

Rules for a negative occurrence of $\mathrm {T}$ . For ordinals and and a closed term a, holds, if one of the following holds for some ordinal :

• $( \textsf {T}{1}_{\infty }^{\mathit {neg}} )$ There are some closed terms b and c such that and .

• $( \textsf {T}{3}_{\infty }^{\mathit {neg}} )$ There is a closed term b such that and .

• $( \textsf {T}{4}_{\infty }^{\mathit {neg}} )$ There is a closed term b such that and .

• $( \textsf {T}{5}_{\infty }^{\mathit {neg}} )$ There are some closed terms b and c such that and .

• $( \textsf {T}{6}_{\infty }^{\mathit {neg}} )$ There are some closed terms b and c such that and .

Note that there is no rule for a negative occurrence of $\mathrm {T}$ corresponding to $(\textsf {T}{2}_{\infty }^{\mathit {pos}} )$ .

Lemma 6.1. The following basic properties of $\mathsf {CD}^{\infty }$ can be shown in the standard manner, and we omit their proofs.

1. 1. (Structural Lemma)

   For all , $q \leq p$ , and , if , then .

2. 2. (Numerical Equivalence Lemma)

   For all closed terms a and b, if $a^{\mathbb {N}} = b^{\mathbb {N}}$ and , then .

3. 3. (Tautology Lemma)

   ${\mathsf {CD}^{\infty } \, | \mspace {-5mu} \tfrac { \ {2 \cdot \mathit {cp}(A)} }{ \ {0} \ } \,} A, \neg A$ ; recall that $\mathit {cp}(A)$ denotes the complexity of A (see page 12).

4. 4. ( $\wedge $ -Inversion)

   If , then , and .

5. 5. ( $\vee $ -Exportation)

   If , then .

6. 6. ( $\forall $ -Inversion)

   If , then for all closed terms a.

The next lemma is nearly obvious from the design of $\mathsf {CD}^{\infty }$ , and the proof is routine.

Lemma 6.2. For every $\mathcal {L}$ -sentence $\psi $ , if $\mathsf {CD} \vdash \psi $ , then for some ; actually, we can primitive recursively calculate k and n from a given derivation of $\psi $ .

The following three lemmata can also be shown standardly.

Lemma 6.3 (Reduction Lemma).

If $\mathsf {CD}^{\infty } {\, | \mspace {-5mu} \tfrac { \ {\alpha } }{ \ {1 + n + 1} \ } \,} \Gamma $ , then $\mathsf {CD}^{\infty } {\, | \mspace {-5mu} \tfrac { \ {2^{\alpha }} }{ \ {1 + n} \ } \,} \Gamma $ .

Lemma 6.4 (Partial Cut-elimination Lemma).

If $\mathsf {CD}^{\infty } {\, | \mspace {-5mu} \tfrac { \ {\alpha } }{ \ {1 + n} \ } \,} \Gamma $ , then , where is recursively defined as follows: and .

Lemma 6.5. For every $\mathcal {L}$ -sentence $\psi $ , if $\mathsf {CD} \vdash \psi $ , then for some .

Note that means that there is a derivation of $\psi $ in $\mathsf {CD}^{\infty }$ in which $( \mathrm {cut} )$ is only applied to closed $\mathcal {L}$ -literals; such a derivation corresponds to what Cantini [5] calls a quasi-normal derivation in his semi-formal system $\mathrm {TKF}^{\infty }$ .

6.2 Reduction of $\mathsf {CD}$ to $\mathsf {KF}$

Let $\sigma $ , $\tau $ , and $\xi $ be ordinals. Recall that we only consider $\mathcal {L}$ -sentences in negation-normal form throughout the Section 6. Given an $\mathcal {L}$ -sentence $\phi $ , we write $\models \phi [ \sigma , \tau , \xi ]$ when $\phi $ is true under the following interpretation:

• • the quantifiers range over ;

• • the $\mathcal {L}_0$ -vocabulary receives the standard interpretations;

• • each negative occurrence of $\mathrm {D}$ in $\phi $ is interpreted by $D_{\sigma + 1}$ ;

• • each positive occurrence of $\mathrm {D}$ in $\phi $ is interpreted by $D_{\tau + 1}$ ;

• • each (either negative or positive) occurrence of $\mathrm {T}$ in $\phi $ is interpreted by $T_{\xi + 1}$ .

We extend this notation to finite sets $\Gamma $ of $\mathcal {L}$ -sentences and write $\models \Gamma [ \sigma , \tau , \xi ]$ when $\models \phi [ \sigma , \tau , \xi ]$ for some $\phi \in \Gamma $ . By Lemma 4.5.2, the sequence $\langle D_{\xi } \mid \xi \in On \rangle $ is a monotonically increasing, where $On$ denotes the class of ordinals, and thus the next lemma can be shown in the standard manner.

Lemma 6.6 (Persistence Lemma).

Let $\phi $ be an $\mathcal {L}$ -sentences and $\Gamma $ a finite set of $\mathcal {L}$ -sentences. For every ordinals $\sigma _{1} \leq \sigma _{0}$ , $\tau _{0} \leq \tau _{1}$ , and $\xi $ , the following hold.

1. 1. If $\models \varphi [ \sigma _{0}, \tau _{0}, \xi ]$ , then $\models \varphi [ \sigma _{1}, \tau _{1}, \xi ]$ .

2. 2. If $\models \Gamma [ \sigma _{0}, \tau _{0}, \xi ]$ , then $\models \Gamma [ \sigma _{1}, \tau _{1}, \xi ]$ .

The next is the main lemma of the present section.

Lemma 6.7. For all ordinals , if , then for all ordinals $\sigma $ and $\xi $ , if , then .

Proof The claim is shown by induction on derivation. Throughout this proof, a, b, c, and d always denote closed $\mathcal {L}_0$ -terms.

Suppose that the last inference is made by either of the following axioms:

where $\mathit {A}$ is a true closed $\mathcal {L}_0$ -literal, $a^{\mathbb {N}}\! \approx ^{\mathbb {N}} b^{\mathbb {N}}$ , and $c^{\mathbb {N}}$ is the Gödel number of a closed $\mathcal {L}_0$ -atomic. The claim for the first case is obvious; the claim for the second case follows from Proposition 4.4.2, and the claim for the third case follows from Proposition 4.2.1. Next, suppose the last inference is made by the axiom (Ax2):

where $a^{\mathbb {N}}\! \approx ^{\mathbb {N}} b^{\mathbb {N}}$ . Take any ordinal $\sigma $ and $\xi $ . Since

by Lemma 4.5.1,

implies $a^{\mathbb {N}} \not \in D_{\sigma + 1}$ and thus $b^{\mathbb {N}} \not \in D_{\sigma + 1}$ by Proposition 4.4.1. Hence, either

or $b^{\mathbb {N}} \not \in D_{\sigma + 1}$ holds, and thus

.

We move on to the induction step. The case where we use a logical rule in the last inference, except for cut, can be treated in the usual manner. For instance, suppose the last inference is made by $( \forall )$ , namely, (our variant of) the

-rule:

where

for each a. Take any $\sigma $ and $\xi $ with

. It follows from the induction hypothesis that for each closed term a, we have the following:

If

for any a, then we have

by Lemma 6.6. Otherwise, for all closed terms a, we have

and thus

by Lemma 6.6, which implies

.

Next, the claim for the cases where the last inference is made by one of the rules for determinateness can be straightforwardly shown using Lemmata 4.2 and 4.5. For example, suppose the last inference is of the following form:

where

and

. Take any $\sigma $ and $\xi $ with

. If we have $\models \Gamma \cup \{ \neg \mathrm {D} a \} [ \sigma , \sigma + 2^{\gamma }, \xi ]$ , then we get

by Lemma 6.6. Otherwise, we have the following by the induction hypothesis:

Since $D_{\sigma + 1} \supset D_{\sigma }$ and $D_{\sigma } \cap T_{\xi + 1} = D_{\sigma } \cap T_{\sigma }$ by Lemma 4.5, this implies

Hence, by Lemma 4.2.5, we obtain $a^{\mathbb {N}} \not \in D_{\sigma + 1}$ and thus

. Let us see one more example. Suppose the last inference is of the following form:

where

and

. Take any $\sigma $ and $\xi $ with

. As before, if $\models \Gamma \cup \{ \mathrm {D} a \} [ \sigma , \sigma + 2^{\gamma }, \xi ]$ , then the claim follows by Lemma 6.6. Otherwise, by the induction hypothesis, we have

Since

, it follows from Lemma 4.5 that

which implies

by Lemma 4.2.6 and thus

. We leave the other cases to the reader.

Now, let us assume that the last inference is made by a truth rule. Suppose the last inference is made by either $(\textsf {T}{4}_{\infty }^{\mathit {pos}} )$ or $( \textsf {T}{3}_{\infty }^{\mathit {neg}} )$ :

where

and

. Take any $\sigma $ and $\xi $ with

. We will prove the claim only for the former case; the latter case can be similarly shown. If ${\models \neg \mathrm {T} b [ \sigma , \sigma + 2^{\gamma }, \xi ]}$ , then $b^{\mathbb {N}} \not \in T_{\xi + 1}$ and thus $a^{\mathbb {N}} \in T_{\xi + 1}$ by Lemma 4.3.4, which implies

. Otherwise, we have $\models \Gamma \cup \{ \mathrm {T} a \} [ \sigma , \sigma + 2^{\gamma }, \xi ]$ by the induction hypothesis, and the claim follows by Lemma 6.6 as before. Next, suppose that we make either of the following inferences at the last step:

where

and

. Take any $\sigma $ and $\xi $ with

. For the former case, if $\models \mathrm {T} {b}^{\circ } \wedge \mathrm {D} {b}^{\circ } [ \sigma , \sigma + 2^{\gamma }, \xi ]$ , then, by Lemma 4.5, we have

and thus, by Lemmata 4.2.2, 4.3.2, and 4.5, we obtain

which implies

; otherwise, we have $\models \Gamma \cup \{ \mathrm {T} a \} [ \sigma , \sigma + 2^{\gamma }, \xi ]$ by the induction hypothesis, and the claim follows by Lemma 6.6 as before. Similarly, for the latter case, if $\models \neg \mathrm {T} {b}^{\circ } \wedge \mathrm {D} {b}^{\circ } [ \sigma , \sigma + 2^{\gamma }, \xi ]$ , then, by Lemma 4.5, we have

and thus, again by Lemmata 4.2.2, 4.3.2, and 4.5, we obtain

which implies

; otherwise, we have $\models \Gamma \cup \{ \neg \mathrm {T} a \} [ \sigma , \sigma + 2^{\gamma }, \xi ]$ by the induction hypothesis, and the claim follows by Lemma 6.6 as before. Thirdly, suppose that the last inference is made by the rule $(\textsf {T}{2}_{\infty }^{\mathit {pos}} )$ :

where

and

. Take any $\sigma $ and $\xi $ with

. Suppose $\models \mathrm {D} {b}^{\circ } [ \sigma , \sigma + 2^{\gamma }, \xi ]$ . We have $( {b}^{\circ } )^{\mathbb {N}} \in D_{\sigma + 2^{\gamma } + 1}$ and thus $( {b}^{\circ } )^{\mathbb {N}} \in D_{\xi }$ by Lemma 4.5.2. Hence, we get $a^{\mathbb {N}} \in T_{\xi + 1}$ by Lemma 4.3.3 and thus

. Otherwise, the claim follows by Lemma 6.6 as before. The remaining cases for the other truth rules can be dealt with similarly.

Finally, let us assume that the last inference is made by $( \mathrm {cut} )$ . We only consider the crucial case where the cut formulae are of the forms $\mathrm {D} a$ and $\neg \mathrm {D} a$ :

where

. Let $\gamma = \max \{ \gamma _{0}, \gamma _{1} \}$ and take any $\sigma $ and $\xi $ with

. Suppose

for contradiction. Since

, it would follow that

$$ \begin{align*} & \not\models \Gamma [ \sigma, \sigma + 2^{\gamma}, \xi ] & & \mathrm{and} & & \not\models \Gamma [ \sigma + 2^{\gamma}, \sigma + 2^{\gamma} + 2^{\gamma}, \xi ] & \end{align*} $$

by Lemma 6.6. Hence, by the induction hypothesis, we would have

$$ \begin{align*} & \models \mathrm{D} a [ \sigma, \sigma + 2^{\gamma}, \xi ] & & \mathrm{and} & & \models \neg \mathrm{D} a [ \sigma + 2^{\gamma}, \sigma + 2^{\gamma} + 2^{\gamma}, \xi ], & \end{align*} $$

which means $a^{\mathbb {N}} \!\in D_{\sigma + 2^{\gamma } + 1}$ and $a^{\mathbb {N}}\! \not \in D_{\sigma + 2^{\gamma } + 1}$ ; a contradiction. The remaining case in which the cut formulae are closed $\mathcal {L}_{\mathrm {T}}$ -literals can be straightforwardly treated.

Combining this with Lemma 6.5, we obtain the next corollary.

Corollary 6.8. For each $\mathcal {L}$ -sentence $\phi $ , if $\mathsf {CD} \vdash \phi $ , then there is some such that .

Now, the argument of this section can be adequately formalized within $\mathsf {KF}$ (or $\mathsf {RA}_{< \varepsilon _{0}}$ ), in which we can formalize the construction of $D_{\xi }$ s and $T_{\xi }$ s for sufficiently large ordinals ( $< \varepsilon _{0}$ ) and prove (the arithmetization of) Corollary 6.8 in terms of them. Hence, in particular, we obtain the following.

Corollary 6.9. $\mathsf {CD}$ is arithmetically conservative over $\mathsf {KF}$ .

Combining this corollary with Corollary 5.6, we obtain our main theorem.

Theorem 6.10. $\mathsf {CD}_{\mathsf {0}}$ , $\mathsf {CD}_{\mathsf {1}}$ , $\mathsf {CD}_{\mathsf {2}}$ , and $\mathsf {CD}$ are arithmetically equivalent to $\mathsf {KF}$ , $\mathsf {RA}_{< \varepsilon _{0}}$ , and $\mathsf {RT}_{< \varepsilon _{0}}$ , that is, they have exactly the same arithmetical theorems.

In fact, our proofs establish stronger results: All the systems are proof-theoretically reducible to each other in the sense of Feferman [7, 9].

7 Upper bound of the strength of $\mathsf {CD}^{+}$

We will show that $\mathsf {CD}^{+}$ is arithmetically conservative over $\mathsf {RT}_{< \varepsilon _{\varepsilon _{0}}}$ . This will be shown by constructing a relative interpretation of $\mathsf {CD}^{+}$ in $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ ( $= \mathsf {CT} [ \! [ \mathsf {KF} ] \! ] + \mathrm {Cons}$ ) that preserves the arithmetical part.

7.1 Total and consistent predicates

We begin with the following definition:

$$\begin{align*}D^{+} ( x ) \ :\Leftrightarrow \ ( \mathrm{F} x \leftrightarrow \neg \mathrm{T} x ). \end{align*}$$

Thus, $D^{+} ( x )$ is equivalent to $( \mathrm {T} x \vee \mathrm {F} x ) \wedge ( \neg \mathrm {T} x \vee \neg \mathrm {F} x )$ . We obviously have

(11) $$ \begin{align} \begin{aligned} & \mathsf{KF} + \mathrm{Cons} \vdash ( \forall x \in {{\mathrm{Sent}}_{\mathrm{T}}} ) \bigl( D^{+} ( x ) \leftrightarrow ( \mathrm{T} x \vee \mathrm{F} x ) \bigr),\\ & \mathsf{KF} + \mathrm{Comp} \vdash ( \forall x \in {{\mathrm{Sent}}_{\mathrm{T}}} ) \bigl( D^{+} ( x ) \leftrightarrow ( \neg \mathrm{T} x \vee \neg \mathrm{F} x ) \bigr). \end{aligned} \end{align} $$

Lemma 7.1. The following are provable in $\mathsf {KF}$ .

1. 1. ; use K2.

2. 2. ; use K3.

Lemma 7.2. The following are provable in $\mathsf {KF} + \mathrm {Cons}$ .

1. 1.

2. 2.

3. 3.

4. 4.

Proof We work within $\mathsf {KF} + \mathrm {Cons}$ ; recall that we have $D^{+} ( x ) \leftrightarrow ( \mathrm {T} x \vee \mathrm {F} x )$ for all $x \in {{\mathrm {Sent}}_{\mathrm {T}}}$ in $\mathsf {KF} + \mathrm {Cons}$ . For claim 1, take any $x, y \in {{\mathrm {Sent}}_{\mathrm {T}}}$ ; then we have

Claim 2 can be shown similarly to 1 using Lemma 7.1.2 and K3. For claim 3, take any v and x with

; then we have

Claim 4 can be shown similarly to 3 using Lemma 7.1.2 and K3.

Lemma 7.3. .

Proof Take any

. The following four equivalences are provable in $\mathsf {KF}$ :

The claim follows from these by logic.

7.2 Reduction of $\mathsf {CD}^{+}$ to $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$

In the present subsection, we give an interpretation of $\mathsf {CD}^{+}$ in $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ that preserves $\mathcal {L}_0$ . For this purpose, we need a few preliminary definitions.

By the recursion theorem we obtain a recursive function f that satisfies the following condition:

(12)

Here is an arithmetical representation of the syntactic operation of applying the function f to terms so that is provable in $\mathsf {PA}$ for each . ⁹ We can show that f is provably total in $\mathsf {PA}$ and thus f is a $\mathsf {PA}$ -definable function. Obviously we have $f x \in {\mathrm {Fml}_{\mathrm {T}}}$ for every (provably in $\mathsf {PA}$ ), and, as in the case for the function k, we have $\forall z \bigl ( \mathrm {Free} ( z, x ) \leftrightarrow \mathrm {Free} ( z, f x ) \bigr )$ ; hence, we have $f x \in {{\mathrm {Sent}}_{\mathrm {T}}}$ for every (provably in $\mathsf {PA}$ ).

The next is shown by routine induction on the complexity of x (cf. Lemma 5.7).

Lemma 7.4. .

Now, we define a translation $\sharp $ of $\mathcal {L}$ into $\mathcal {L}_{\mathrm {T}}^{+}$ as follows: for each term a,

$$ \begin{align*} & \mathrm{D}^{\sharp} a \ := \ \mathrm{T} f a \vee \mathrm{F} f a & & \mathrm{and} & & \mathrm{T}^{\sharp} a \ := \ \mathbb{T} f a; & \end{align*} $$

$\sharp $ preserves all the $\mathcal {L}_0$ -vocabulary. By (11), we have

(13)

We will show that $\sharp $ is a relative interpretation of $\mathsf {CD}$ in $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ .

Lemma 7.5. The following are provable in $\mathsf {KF} + \mathrm {Cons}$ .

1. 1. ; by (12) and K1.

2. 2. ; by (12), (13), and Lemma 7.1.1.

3. 3. ; by (12), (13), and Lemma 7.1.2.

Hence, the $\sharp $ -translations of D1, D2, and D4 are provable in $\mathsf {KF} + \mathrm {Cons}$ .

Lemma 7.6. . Hence, the $\sharp $ -translations of D3 is provable in $\mathsf {KF} + \mathrm {Cons}$ .

Proof The claim is readily observed from the following equivalences:

Lemma 7.7. The following are provable in $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ .

1. 1.

2. 2.

3. 3.

4. 4.

5. 5. .

Hence, the $\sharp $ -translation of T1 and T2 and T4–T6 are provable in $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ .

Proof We work within $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ . Claim 1 is obvious by $\mathbb {T}1$ . For claim 2, take any

, and then we infer

Claims 3 and 4 readily follow from $\mathbb {T}2$ and $\mathbb {T}3$ , respectively, together with the definition (12) of f. For claim 5, let v and x be such that

. Then, we have

Lemma 7.8. $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ] \vdash \forall x \bigl ( \mathrm {D}^{\sharp } ( x ) \rightarrow ( \mathbb {T} f ( x ) \leftrightarrow \mathrm {T} f ( x ) ) \bigr )$ .

Proof If

then $f ( x ) = \ulcorner 0 \!\neq \! 0\urcorner $ and thus $\mathbb {T} f ( x ) \wedge \mathrm {T} f ( x )$ . Let

. The claim is shown by induction on the complexity of x. For the base step, assume

. The case where $x \in {\mathrm {AtSent}_{0}}$ is obvious. Next, if

for some

, then we have

Lastly, let

for some

. Then, we have

For the induction step, we first let

and assume $\mathrm {D}^{\sharp } x$ . We have $\mathrm {D}^{\sharp } y$ by Lemma 7.5.3 and thus $D^{+} f ( y )$ by (13). Hence, we have

note that the assumption $\mathrm {D}^{\sharp } x$ is crucial here. The other cases can be shown similarly, but without the need to use the assumption $\mathrm {D}^{\sharp } x$ .

Lemma 7.9. . Hence, the $\sharp $ -translation of T3 is provable in $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ .

Proof Take any

and suppose $\mathrm {D}^{\sharp } ( {s}^{\circ } )$ . Then, we have

Lemma 7.10. $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ proves the following.

1. 1. .

2. 2. .

Hence, the $\sharp $ -translations of D5 and D6 are provable in $\mathsf {KF} + \mathrm {Cons}$ .

Proof 1. Let

. Then, we have

2. Let

. Then, we similarly obtain

By Lemmata 7.5–7.7, 7.9, and 7.10, we obtain the next theorem.

Theorem 7.11. The translation $\sharp $ is a relative interpretation of $\mathsf {CD}^{+}$ in $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ . Hence, in particular, $\mathsf {CD}^{+}$ is arithmetically conservative over $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ .

Combining this theorem with Corollary 5.10 and Fact 5.11, we obtain the next.

Theorem 7.12. $\mathsf {CD}_{\mathsf {2}}^{+}$ and $\mathsf {CD}^{+}$ are arithmetically equivalent to $\mathsf {RA}_{< \varepsilon _{\varepsilon _{0}}}$ and $\mathsf {RT}_{< \varepsilon _{\varepsilon _{0}}}$ .

As before, our proofs actually establish that all these systems are proof-theoretically reducible to each other in the sense of Feferman [7, 9].

8 Some supplementary results

8.1 An interpretation of $\mathsf {CD}^{+}$ in $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Comp} ] \! ]$

Preliminarily, we give an interpretation of $\mathsf {CD}^{+}$ in $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Comp} ] \! ]$ . ¹⁰

Similarly to the function f, introduced in (12) above, we define a recursive function h by the recursion theorem so that the following condition obtains:

(14)

Using h, the translation $\flat $ of $\mathcal {L}$ into $\mathcal {L}_{\mathrm {T}}$ is defined as follows: for each term a,

$$ \begin{align*} & \mathrm{D}^{\flat} a \ = \ \neg \mathrm{T} h a \vee \neg \mathrm{F} h a & & \mathrm{and} & & \mathrm{T}^{\flat} a \ = \ \mathbb{T} h ( a ); & \end{align*} $$

all the $\mathcal {L}_0$ -vocabulary, logical connectives, and quantifiers are preserved by $\flat $ . By (11), we have $\mathsf {KF} + \mathrm {Comp} \vdash \forall x \bigl ( \mathrm {D}^{\flat } x \leftrightarrow D^{+} ( h x ) \bigr )$ .

The proof of the next theorem is completely dual to that of Theorem 7.11, and we omit the details.

Theorem 8.1. $\flat $ is a relative interpretation of $\mathsf {CD}$ in $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Comp} ] \! ]$ .

8.2 Liars and truth tellers

In previous section we compared $\mathsf {CD}$ and its variants with other truth theories with respect to their strength. Truth theories are often compared by the way liar and truth teller sentences behave. In the present section we establish a few results about their behaviour in $\mathsf {CD}$ and its variants.

Let $\mathfrak {l}$ and $\mathfrak {t}$ be closed $\mathcal {L}_0$ -terms with the following properties:

(15) $$ \begin{align} \mathsf{PA} \vdash \mathfrak{l} = \ulcorner \!\neg \mathrm{T} \mathfrak{l}\urcorner \quad \mathrm{and} \quad \mathsf{PA} \vdash \mathfrak{t} = \ulcorner \mathrm{T} \mathfrak{t}\urcorner. \end{align} $$

Hence, we have

(16) $$ \begin{align} \mathsf{CD} \vdash \mathrm{T} \mathfrak{l} \leftrightarrow \neg \mathrm{T}\hspace{1pt} \ulcorner \mathrm{T} \mathfrak{l}\urcorner \quad \mathrm{and} \quad \mathsf{CD} \vdash \mathrm{T} \mathfrak{t} \leftrightarrow \mathrm{T}\hspace{1pt} \ulcorner \mathrm{T} \mathfrak{t} \urcorner\!\!. \end{align} $$

Therefore, $\neg \mathrm {T} \mathfrak {l}$ and $\mathrm {T} \mathfrak {t}$ are a liar and a truth-teller sentence, respectively. ¹¹

Proposition 8.2.

1. 1. $\mathsf {CD} \vdash \neg \mathrm {D} \mathfrak {l}$ .

2. 2. $\mathsf {CD}^{+} \not \vdash \mathrm {D} \mathfrak {t}$ .

3. 3. $\mathsf {CD}^{+} \not \vdash \mathrm {T} \mathfrak {t}$ and $\mathsf {CD}^{+} \not \vdash \neg \mathrm {T} \mathfrak {t}$ .

4. 4. $\mathsf {CD}^{+} \not \vdash \neg \mathrm {T} \mathfrak {l}$ and $\mathsf {CD}^{+} \not \vdash \mathrm {T} \mathfrak {l}$ .

Proof 1. Provably in $\mathsf {CD}$ , if $\mathrm {D} \mathfrak {l}$ were the case, then we would have $\mathrm {T} \mathfrak {l} \leftrightarrow \mathrm {T}\hspace{1pt} \ulcorner \mathrm {T} \mathfrak {l} \urcorner $ by T3, which contradicts (16).

2. Using (15), we can show that $\mathfrak {t} \not \in D_{\xi }$ for all $\xi $ by straightforward induction on $\xi $ .

3. For the function f defined in Section 7.2, we observe that $\mathsf {PA}$ proves the following:

(17) $$ \begin{align} f ( \mathfrak{t} ) = f ( \ulcorner \mathrm{T} \mathfrak{t}\urcorner ) = \ulcorner \mathrm{T} f ( \mathfrak{t} )\urcorner \quad \mathrm{and} \quad h ( \mathfrak{t} ) = h ( \ulcorner \mathrm{T} \mathfrak{t}\urcorner ) = \ulcorner \mathrm{T} h ( \mathfrak{t} )\urcorner; \end{align} $$

hence, both $f ( \mathfrak {t} )$ and $h ( \mathfrak {t} )$ are also truth-tellers. Let I be the least Kripkean fixed point, namely, the least set such that $( \mathbb {N}, I ) \models \mathsf {KF}$ , where I interprets the truth predicate $\mathrm {T}$ . It is known that $( \mathbb {N}, I ) \models \mathrm {Cons}$ . By the standard argument, we can show that $f ( \mathfrak {t} ) \not \in I$ and . Let $J := \{ \# \neg \phi \mid \# \phi \not \in I \}$ ; hence, $( \mathbb {N}, J )$ is the $\mathcal {L}_{\mathrm {T}}$ -structure induced from $( \mathbb {N}, I )$ by Cantini’s dual interpretation, and thus $( \mathbb {N}, J ) \models \mathsf {KF} + \mathrm {Comp}$ . Then, we have

(18) $$ \begin{align} ( \mathbb{N}, I ) \not\models \mathrm{T} f ( \mathfrak{t} ) \quad \mathrm{and} \quad ( \mathbb{N}, J ) \models \mathrm{T} h ( \mathfrak{t} ). \end{align} $$

Now, by (17), we have the following:

(19) $$ \begin{align} \mathsf{CT} [ \! [ \mathsf{KF} ] \! ] \vdash \mathbb{T} f ( \mathfrak{t} ) \leftrightarrow \mathrm{T} f ( \mathfrak{t} ) \quad \mathrm{and} \quad \mathsf{CT} [ \! [ \mathsf{KF} ] \! ] \vdash \mathbb{T} h ( \mathfrak{t} ) \leftrightarrow \mathrm{T} h ( \mathfrak{t} ). \end{align} $$

Let $I^{+} := \{ \# \phi \mid ( \mathbb {N}, I ) \models \phi \}$ and $J^{+} := \{ \# \phi \mid ( \mathbb {N}, J ) \models \phi \}$ ; then, the $\mathcal {L}_{\mathrm {T}}^{+}$ -structures $( \mathbb {N}, I, I^{+} )$ and $( \mathbb {N}, J, J^{+} )$ , in which $\mathbb {T}$ is interpreted by $I^{+}$ and $J^{+}$ respectively, are models of $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ and $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Comp} ] \! ]$ , respectively. It follows from (18) and (19) that

$$\begin{align*}( \mathbb{N}, I, I^{+} ) \not\models \mathbb{T} f ( \mathfrak{t} ) \quad \mathrm{and} \quad ( \mathbb{N}, J, J^{+} ) \not\models \neg \mathbb{T} h ( \mathfrak{t} ). \end{align*}$$

Hence, $\mathsf {CD}^{+} \not \vdash \mathrm {T} \mathfrak {t}$ and $\mathsf {CD}^{+} \not \vdash \neg \mathrm {T} \mathfrak {t}$ by Theorems 7.11 and 8.1.

4. Observe that $\mathsf {PA}$ proves the following:

(20) $$ \begin{align} f ( \mathfrak{l} ) = f ( \ulcorner \neg \mathrm{T} \mathfrak{l}\urcorner ) = \ulcorner \neg \mathrm{T} f ( \mathfrak{l} )\urcorner \quad \mathrm{and} \quad h ( \mathfrak{l} ) = h ( \ulcorner \neg \mathrm{T} \mathfrak{l}\urcorner ) = \ulcorner \neg \mathrm{T} h ( \mathfrak{l} )\urcorner; \end{align} $$

namely, $f ( \mathfrak {l} )$ and $h ( \mathfrak {l} )$ are also liar sentences. Hence, we obtain

(21) $$ \begin{align} \mathsf{KF} \vdash \mathrm{T} f ( \mathfrak{l} ) \leftrightarrow \mathrm{F} f ( \mathfrak{l} )\qquad\qquad \mathrm{and}\qquad\qquad \mathsf{KF} \vdash \mathrm{T} h ( \mathfrak{l} ) \leftrightarrow \mathrm{F} h ( \mathfrak{l} ), \end{align} $$

which implies $\mathsf {KF} + \mathrm {Cons} \vdash \neg \mathrm {T} f ( \mathfrak {l} )$ and $\mathsf {KF} + \mathrm {Comp} \vdash \mathrm {T} h ( \mathfrak {l} )$ . Finally, it follows from (20) that $\mathsf {CT} [ \! [ \mathsf {KF} ] \! ]$ proves

$$ \begin{align*} \mathbb{T} f ( \mathfrak{l} ) \leftrightarrow \mathbb{T}\hspace{1pt} \ulcorner \neg \mathrm{T} f ( \mathfrak{l} )\urcorner \leftrightarrow \neg \mathrm{T} f ( \mathfrak{l} ) \quad \mathrm{and} \quad \mathbb{T} h ( \mathfrak{l} ) \leftrightarrow \mathbb{T} ( \ulcorner \neg \mathrm{T} h \mathfrak{l}\urcorner ) \ \Leftrightarrow \ \neg \mathrm{T} h ( \mathfrak{l} ). \end{align*} $$

Hence, we have $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ] \vdash \mathbb {T} f ( \mathfrak {l} )$ and $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Comp} ] \! ] \vdash \neg \mathbb {T} h ( \mathfrak {l} )$ , which implies $\mathsf {CD}^{+} \not \vdash \neg \mathrm {T} \mathfrak {l}$ and $\mathsf {CD}^{+} \not \vdash \mathrm {T} \mathfrak {l}$ by Theorems 7.11 and 8.1.

Proposition 8.3. Let us write $\lambda $ for $\neg \mathrm {T} \mathfrak {l}$ . We have the following:

1. 1. $\mathsf {CD}^{+} \not \vdash \mathrm {T}\ulcorner \mathrm {T}\ulcorner \lambda \vee \neg \lambda \urcorner \urcorner $ and $\mathsf {CD}^{+} \not \vdash \neg \mathrm {T}\ulcorner \mathrm {T}\ulcorner \lambda \vee \neg \lambda \urcorner \urcorner $ ; hence, the truth of some logical truth is neither provable nor refutable in $\mathsf {CD}$ .

2. 2. $\mathsf {CD}^{+} \nvdash \mathrm {T}\,\ulcorner \,(\,\mathrm {T}\,\ulcorner \neg \lambda \urcorner \leftrightarrow \neg \mathrm {T}\,\ulcorner \lambda \urcorner )\,\urcorner $ ; hence, not all $\mathsf {CD}$ -axioms are provably true in $\mathsf {CD}$ .

3. 3. $\mathsf {CD}^{+} \vdash \neg \mathrm {D}\,\ulcorner \,(\,\mathrm {T}\,\ulcorner \neg \lambda \urcorner \leftrightarrow \neg \mathrm {T}\,\ulcorner \lambda \urcorner )\,\urcorner $ ; hence, not all $\mathsf {CD}$ -axioms are provably determinate in $\mathsf {CD}$ .

Proof 1. $\mathsf {CT} [ \! [ \mathsf {KF} ] \! ]$ proves the following equivalences:

$$ \begin{align*} & \mathrm{T}^{\sharp} \ulcorner \mathrm{T}\ulcorner \lambda \vee \neg \lambda\urcorner\urcorner \ \Leftrightarrow \ \mathbb{T}\hspace{1pt} \ulcorner \mathrm{T} f ( \ulcorner \lambda\vee \neg \lambda\urcorner )\urcorner \ \Leftrightarrow \ \mathrm{T} f ( \ulcorner \lambda\vee \neg \lambda\urcorner ) \ \Leftrightarrow \ \mathrm{T} f ( \lambda ) \vee \mathrm{F} f ( \lambda ), \\ & \mathrm{T}^{\flat} \ulcorner \mathrm{T}\ulcorner \lambda \vee \neg \lambda\urcorner\urcorner \ \Leftrightarrow \ \mathbb{T}\hspace{1pt} \ulcorner \mathrm{T} h ( \ulcorner \lambda\vee \neg \lambda\urcorner )\urcorner \ \Leftrightarrow \ \mathrm{T} h ( \ulcorner \lambda\vee \neg \lambda\urcorner ) \ \Leftrightarrow \ \mathrm{T} h ( \lambda ) \vee \mathrm{F} h ( \lambda ). \end{align*} $$

By (15) and (21), $\mathsf {KF} + \mathrm {Cons} \vdash \neg ( \mathrm {T} f ( \lambda ) \vee \mathrm {F} f ( \lambda ) )$ and $\mathsf {KF} + \mathrm {Comp} \vdash \mathrm {T} h ( \lambda ) \vee \mathrm {F} h ( \lambda )$ . Hence, $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ] \vdash \neg \mathrm {T}^{\sharp } \ulcorner \mathrm {T}\ulcorner \lambda \vee \neg \lambda \urcorner \urcorner $ and $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Comp} ] \! ] \vdash \mathrm {T}^{\flat } \ulcorner \mathrm {T}\ulcorner \lambda \vee \neg \lambda \urcorner \urcorner $ ; thus, $\mathsf {CD}^{+} \not \vdash \mathrm {T}\hspace{1pt} \ulcorner \mathrm {T}\ulcorner \lambda \vee \neg \lambda \urcorner \urcorner $ and $\mathsf {CD}^{+} \not \vdash \neg \mathrm {T}\hspace{1pt} \ulcorner \mathrm {T}\ulcorner \lambda \vee \neg \lambda \urcorner \urcorner $ by Theorems 7.11 and 8.1.

2. $\mathsf {CT} [ \! [ \mathsf {KF} ] \! ]$ derives the following:

$$ \begin{align*} \mathrm{T}^{\sharp} \ulcorner \,(\,\mathrm{T}\,\ulcorner \neg \lambda \urcorner\leftrightarrow \neg \mathrm{T}\,\ulcorner \lambda \urcorner)\urcorner & \ \quad \Leftrightarrow \quad \ \mathbb{T} f ( \ulcorner \,\mathrm{T}\,\ulcorner \neg \lambda\urcorner\urcorner ) \leftrightarrow \neg \mathbb{T} f ( \ulcorner \mathrm{T}\,\ulcorner \lambda \urcorner\urcorner ) \\ & \ \quad \Leftrightarrow \quad \ \mathrm{F} f ( \lambda ) \leftrightarrow \neg \mathrm{T} f ( \lambda ) \\ & \stackrel{(15) \, \& \, (21)}{ \ \quad \Leftrightarrow \quad \ } \mathrm{T} f ( \lambda ) \leftrightarrow \neg \mathrm{T} f ( \lambda ). \end{align*} $$

Hence, we have $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ] \vdash \neg \mathrm {T}^{\sharp } \ulcorner \,(\,\mathrm {T}\,\ulcorner \neg \lambda \urcorner \leftrightarrow \neg \mathrm {T}\,\ulcorner \lambda \urcorner )\urcorner $ , from which the claim follows by Theorems 7.11.

3. Provably in $\mathsf {CD}$ , if $\mathrm {D}\,\ulcorner \,(\,\mathrm {T}\,\ulcorner \neg \lambda \urcorner \leftrightarrow \neg \mathrm {T}\,\ulcorner \lambda \urcorner )\,\urcorner $ , then $\mathrm {D} \ulcorner \neg \mathrm {T}\hspace{1pt} \ulcorner \lambda \urcorner \urcorner $ and thus $\mathrm {D} \mathfrak {l}$ by (15), which contradicts Proposition 8.2.1.

8.3 Additional axioms

In this subsection, we will consider a few conservative extensions of $\mathsf {CD}^{+}$ with additional axioms about iterations of truth.

Lemma 8.4.

1. 1. .

2. 2. .

Proof We work within $\mathsf {CT} [ \! [ \mathsf {KF} + \mathrm {Cons} ] \! ]$ . Take any

. We have

recall that $\mathrm {T}^{\sharp } a := \mathbb {T} f a$ and $\mathrm {D}^{\sharp } a := D^{+} f a$ . Similarly, for each

, we have

This completes the proof.

By the dual argument, we can also show the following.

Lemma 8.5.

1. 1. .

2. 2. .

Let $\mathsf {num} ( n )$ represent the function and thus it is the code of the numeral for n. Following the notation of [21], given a formula $\phi ( x )$ with a distinguished free variable x, denotes $\ulcorner \phi ( x )\urcorner ( \mathsf {num} ( z ) / \ulcorner x\urcorner )$ and also denotes $\ulcorner \phi ( x )\urcorner ( s / \ulcorner x\urcorner )$ for . We will occasionally write or without specifying the distinguished free variable of $\phi $ , but in doing so we always assume that $\phi $ contains some free variable to be substituted for.

Lemma 8.6. .

Proof Take any

. The first conjunct is shown as follows:

The second conjunct can be shown similarly by just replacing f above with h.

We conclude with the next theorem, which immediately follows from the last three lemmata and Theorems 7.11 and 8.1.

Theorem 8.7. The following two systems are both conservative over $\mathsf {CD}^{+}$ :

1. 1.

2. 2.

Hence, either set of the new axioms can be consistently added to $\mathsf {CD}$ .

9 The minimality axiom

The axioms for determinateness postulate that certain sentences are determinate; but $\mathsf {CD}$ lacks axioms that tell us that no other sentences are determinate. For instance, our axioms for determinateness do not rule out that truth teller sentences or similar sentences are determinate. Only in the case of sentences, such as liar sentences, where the assumption of determinateness leads to inconsistency, can we prove in $\mathsf {CD}$ that they are not determinate.

Theorem 4.13 says that no matter what model $( \mathbb {N}, X, Y )$ of $\mathsf {CD}$ we choose, $\mathit {D}_{\infty }$ is the least fixed point of $\Gamma _{\mathcal {D} [ Y ]}$ and can be inductively defined ‘from the bottom up’ in Y. Hence, $\mathit {D}_{\infty }$ seems to be a natural candidate for the ‘intended’ interpretation of the determinateness predicate $\mathrm {D}$ . In this section, we present an axiomatization of this conception of determinateness, which allows us to refute the determinateness of truth tellers, and state the proof-theoretic strength of the resulting system; however, the full analysis of the system goes beyond limited space of the present paper and is left for the Part II.

The system $\mathsf {ID}_{1}$ of (positive arithmetical) inductive definitions contains an axiom schema expressing that each fixed point expressed by a predicate of $\mathsf {ID}_{1}$ is the least, inductively defined, one. We use the same strategy for expressing the leastness of $\mathrm {D}$ . We remind the reader of the definition of $\mathsf {ID}_{1}$ . The language $\mathcal {L}_{\mathrm {fix}}$ of $\mathsf {ID}_{1}$ has a predicate symbol $J_{\mathcal {A}}$ for each second-order arithmetical formula $\mathcal {A} ( x, X )$ with only the displayed variables free in which X occurs only positively. $\mathsf {ID}_{1}$ comprises the following axioms for each predicate $J_{\mathcal {A}}$ together with the axioms of $\mathsf {PA}$ and full induction for $\mathcal {L}_{\mathrm {fix}}$ :

1. ID1 $\forall x \bigl ( \mathcal {A} ( x, \mathit {J}_{\mathcal {A}} ) \rightarrow \mathit {J}_{\mathcal {A}} x \bigr ),$

2. ID2 $\forall x \bigl ( \mathcal {A} ( x, \Phi ) \rightarrow \Phi ( x ) \bigr ) \rightarrow \forall x \bigl ( \mathit {J}_{\mathcal {A}} x \rightarrow \Phi ( x ) \bigr )$ , for all $\Phi \in \mathcal {L}_{\mathrm {fix}},$

where $\mathcal {A} ( x, \Phi )$ for an $\mathcal {L}_{\mathrm {fix}}$ -formula $\Phi ( u )$ with a designated variable u is the result of substituting $\Phi ( a )$ for each occurrence of $a \in X$ in $\mathcal {A} ( x, X )$ for each term a (with renaming of bound variables as necessary to avoid collision). Inspired by ID2, Burgess [4] proposes the following axiom schema as an axiomatic characterization of the groundedness of the truth predicate $\mathrm {T}$ in Kripke’s [28] sense:

$$ \begin{align*} \forall x \bigl( \mathcal{B} ( x, \Phi ) \rightarrow \Phi ( x ) \bigr) \rightarrow \forall x \bigl( \mathrm{T} x \rightarrow \Phi ( x ) \bigr), \ \mathrm{for\ all }\ \Phi \in \mathcal{L}_{\mathrm{T}}, \end{align*} $$

where $\mathcal {B} ( x, X )$ is taken so that $\forall x \bigl ( \mathcal {B} ( x, X ) \rightarrow X \bigr )$ expresses that X is closed under the strong Kleene evaluation schema of truth values. Burgess’s schema expresses that the extension of $\mathrm {T}$ is the least Kripkean fixed point under the strong Kleene evaluation schema; the system obtained by augmenting $\mathsf {KF}$ with this schema is called $\mathsf {KFB}$ . We follow the lead of Burgess’s idea toward an axiomatic characterization of $\mathrm {D}$ as the least set that satisfies the closure conditions of determinateness relative to the truth predicate $\mathrm {T}$ (but recall that the least such set is invariant across the choice of $\mathrm {T}$ ).

For each $\mathcal {L}$ -formula $\Phi ( u )$ with a designated variable u, we write $\mathcal {D} ( x, \Phi )$ for the result of substituting $\Phi ( a )$ for each occurrence of $\mathrm {D} a$ in $\mathcal {D} ( x )$ for each term a (with renaming of bound variables as necessary to avoid collision). For the uniformity of notation, we will write $\mathcal {D} ( x, \mathrm {D} )$ for $\mathcal {D} ( x )$ in (and only in) the present section. Thereby we introduce two new axioms.

$$\begin{align*} \kern-131pt D_{\mu}1 \kern40pt & \forall x ( \mathcal{D} ( x, \mathrm{D} ) \rightarrow \mathrm{D} x ). \end{align*}$$

$$\begin{align*} \kern-50pt D_{\mu}2 \kern40pt & \forall x \bigl( \mathcal{D} ( x, \Phi ) \rightarrow \Phi ( x ) \bigr) \rightarrow \forall x ( \mathrm{D} x \rightarrow \Phi ( x ) ), \ \mathrm{for\ all}\ \Phi \in \mathcal{L}. \end{align*}$$

Note that D_μ2 is not a single axiom but an axioms schema.

Definition 9.1. We define the system $\mathsf {CD}_{\mu }$ as $\mathsf {CD} + \mathrm {D}_{\mu }1 + \mathrm {D}_{\mu }2$ . We can easily show that Dμ1 is derivable from $\mathsf {CD}$ and thus $\mathsf {CD}_{\mu }$ is identical with $\mathsf {CD} + \mathrm {D}_{\mu }2$ . The system $\mathsf {CD}^{+}_{\mu }$ is defined as $\mathsf {CD}^{+} + \mathrm {D}_{\mu }2$ .

The next follows from Theorems 4.8 and 4.13.

Corollary 9.2. $( \mathbb {N}, D_{\infty }, \mathbb {T} ) \models \mathsf {CD}^{+}_{\mu }$ .

The system $\mathsf {CD}_{\mu }$ has some desirable properties. For example, we have the following.

Proposition 9.3. $\mathsf {CD}_{\mu } \vdash \neg \mathrm {D} \mathfrak {t}$ ; see Section 8.2 for the definition of $\mathfrak {t}$ .

Proof Suppose $\mathrm {D} \mathfrak {t}$ for contradiction. Let $\Phi ( x ) := \mathrm {D} x \wedge x \neq \mathfrak {t}$ . Since $\mathcal {D} ( \mathfrak {t}, \Phi )$ implies $\Phi ( \mathfrak {t} )$ by (15), we have $\neg \mathcal {D} ( \mathfrak {t}, \Phi )$ and thus $\forall x ( \mathcal {D} ( x, \Phi ) \rightarrow \Phi ( x ) )$ by D_μ1, which would imply $\forall x ( \mathrm {D} x \rightarrow \Phi ( x ) )$ ; a contradiction.

In fact, all the underivability results proved in Section 8.2 still hold in $\mathsf {CD}_{\mu }$ and $\mathsf {CD}^{+}_{\mu }$ , and the additional axioms considered in Section 8.3 are also consistent with $\mathsf {CD}_{\mu }$ and $\mathsf {CD}^{+}_{\mu }$ .

The full proof-theoretic analyses of these new systems are left for the Part II. We state the main results below without giving their proofs.

Theorem 9.4.

1. 1. $\mathsf {CD}_{\mu }$ is proof-theoretically equivalent to $\mathsf {ID}_1$ .

2. 2. $\mathsf {CD}^{+}_{\mu }$ is proof-theoretically equivalent to $\mathsf {BID}_{1}^{2}$ (see [36] for its definition and Fujimoto [15] for its proof-theoretic analysis), and thus its proof-theoretic ordinal (if appropriately defined) is .

10 Comparison with other axiomatizations of truth

We think that $\mathsf {CD}$ is more promising than many other systems found in the literature. This section contains brief comparisons with such systems. We leave a more thorough discussion of the philosophical aspects for another paper.

10.1 Comparison with the Friedman–Sheard system

The Friedman–Sheard system $\mathsf {FS}$ features all the truth axioms of $\mathsf {CD}$ , except for the truth iteration axiom T3 and all axioms involving $\mathrm {D}$ , which is not in the language of ${\mathsf {FS}}$ . Axiom T3 is replaced with two rules called Necessitation NEC and Conecessitation CONEC:

Adding these two rules for all sentences to T1 and T4 – T6 yields the Friedman–Sheard system ${\mathsf {FS}}$ , which was analyzed by Friedman and Sheard [13] with a different axiomatization. McGee [31] showed that a subsystem of ${\mathsf {FS}}$ is

-inconsistent and thus does not have a standard model, that is, the standard model of arithmetic cannot be expanded to a model of ${\mathsf {FS}}$ by specifying a suitable extension for the truth predicate. Halbach [18] determined the proof-theoretic strength of ${\mathsf {FS}}$ as ramified analysis

up to

or

-times iterated typed truth (see Halbach [21, Section 14.2]).

A neat feature of ${\mathsf {FS}}$ is its symmetry: What is provable in ${\mathsf {FS}}$ and what is provably true in ${\mathsf {FS}}$ coincide. Moreover, if $\phi $ is a classical tautology such as $\lambda \vee \neg \lambda $ (for a liar sentence $\lambda $ ), the sentence

$$\begin{align*}\underbrace{\mathrm{T}\ulcorner\mathrm{T}\ulcorner\ldots \mathrm{T}}_{n\ \mathrm{ iterations\ of\ }\mathrm{T}}\ulcorner{\phi }\urcorner\ldots\urcorner\urcorner \end{align*}$$

is provable in ${\mathsf {FS}}$ . In $\mathsf {CD}$ $\mathrm {T}\ulcorner \phi \urcorner $ is provable for every classical tautology, but $\mathrm {T}\ulcorner \mathrm {T}\ulcorner \lambda \vee \neg \lambda \urcorner \urcorner $ and further iterations are not, as was shown in Proposition 8.3. In ${\mathsf {FS}}$ no transfinite iterations of truth can be proved. Hence neither is ${\mathsf {FS}}$ a subsystem of $\mathsf {CD}$ nor is $\mathsf {CD}$ a subsystem of ${\mathsf {FS}}$ . Moreover, neither can the truth predicate of ${\mathsf {FS}}$ be defined in $\mathsf {CD}$ nor can the truth predicate of $\mathsf {CD}$ be defined in ${\mathsf {FS}}$ . This follows from general arguments by Fujimoto [14] (see also Halbach [21]). We will show in Part II that $\mathsf {CD}$ can be consistently closed under NEC and CONEC. The result is a system that properly contains ${\mathsf {FS}}$ and is consequently -inconsistent.

The system ${\mathsf {FS}}$ has rightly been criticized by various authors. Barrio and Picollo [2] list some of the problematic features of ${\mathsf {FS}}$ caused by the -inconsistency. In particular, the rule NEC can naturally be replaced with an -times iterated reflection axiom. If the reflection axiom is iterated into the transfinite, an inconsistency ensues (Halbach and Horsten [3] and Halbach [21, Corollary 14.39]). These shortcomings of ${\mathsf {FS}}$ prompted our search for an alternative to ${\mathsf {FS}}$ without giving up the thorough classicality of ${\mathsf {FS}}$ and endorsing the internal non-classicality of systems such as ${\mathsf {KF}}$ .

Some alternative systems have been developed that prove the truth of classical tautologies, but are -consistent such as Cantini’s [6] $\mathsf {VF}$ and Stern’s [41] $\mathsf {IT}$ and their variants. For these systems -models can be obtained via constructions involving supervaluations.

10.2 Comparison with Kripke–Feferman

Feferman [8] defined a determinateness predicate D in terms of a truth and a falsity predicate within the Kripke–Feferman system ${\mathsf {KF}}$ . ¹² Understanding the falsity of a sentence as the truth of its negation, Feferman defined D as the formula we called $D^{+}$ above:

The schema $D\ulcorner \phi \urcorner \rightarrow (\mathrm {T}\ulcorner \phi \urcorner \leftrightarrow \phi )$ becomes provable in ${\mathsf {KF}}$ with this definition. The schema had been mentioned by Kripke [28] already.

Reinhardt [37, 38] takes the determinateness predicate to express meaningful applicability or significance; and truth is only meaningfully applicable to determinate sentences. ¹³ In particular, the liar sentence is not in the range of significance of the truth predicate. Reinhardt concludes that the system ${\mathsf {KF}}$ , which is formulated in classical logic, is not sound in the sense that it proves only true theorems, where truth is understood in the sense of the truth predicate $\mathrm {T}$ of ${\mathsf {KF}}$ . According to Reinhardt, one might hope that the sentences $\phi $ with $\mathsf {KF}\vdash \mathrm {T}\ulcorner \phi \urcorner $ are true and significant. The set of these sentences is not closed under classical logic. The theorems of ${\mathsf {KF}}$ itself need not be significant or trustworthy; only those whose truth can be proved are. Generally, it is very hard to avoid the provability of sentences that are not ‘significant’ or not ‘healthy’, as Reinhardt [37] and Bacon [1] have argued.

In contrast to Reinhardt, we do not think that the range of significance of the truth predicate is restricted in any way; the determinateness predicate cannot be seen as indicating the range of significance of $\mathrm {T}$ . For instance, truth should commute with connectives for all sentences, not just with those in some range of significance. However, some sentences, including liar sentences, are sensitive to the addition of another layer of truth. Stacking an additional layer of truth onto the liar sentence will change its semantic status; but that does not mean that the truth predicate cannot meaningfully applied to it. We would only run into the Reinhardt–Bacon problem by postulating that only insensitive sentences ought to be provable. We reject this kind of soundness condition. We endorse sensitive sentences such as the compositional axioms or classical tautologies as theorems. However, we may not be able to ascend semantically from such sentences and add a further level of truth. It is not possible to ascend semantically from the compositional axiom; they are already at the highest level of generality and further semantic ascend and generalization is not possible.

10.3 Comparison with Feferman’s DT

Feferman [10, p. 205] originally introduced $\mathsf {KF}$ as an instrument to explain ‘what notions and principles one ought to accept if one accepts the basic notions and principles of the theory’, the foundational question which had long been one of the central themes of Feferman’s work. ¹⁴

As a theory of truth per se, Feferman later proposed another system $\mathsf {DT}$ . Again, each predicate is assumed to have a domain of significance and to be meaningfully applicable only to objects in that domain. In the case of the truth predicate $\mathrm {T}$ , its domain $\mathfrak {D}$ of significance is taken to consist of the sentences that are meaningful and determinate, and all the principles of truth are only applicable to the sentences in the domain $\mathfrak {D}$ . Accordingly, the system $\mathsf {DT}$ comprises two groups of axioms: the axioms characterizing the domain $\mathfrak {D}$ and the axioms expressing the $\mathrm {T}$ -schema and the compositional axioms for all sentences in $\mathfrak {D}$ .

Feferman’s axioms for determinateness differ from ours in particular with respect to the determinateness of sentences formed with binary connectives. In his system a disjunction is determinate if, and only if both disjuncts are; and a conjunction is determinate if, and only if both conjuncts are. We discussed our choice of axiom D5 on page 6 and justified its endorsement with the generalizing function of truth. Many harmless generalizations would become indeterminate (and consequently the system proof-theoretically weak) if generalization were expressed with conjunction and disjunction and Feferman’s concept of determinateness. To overcome the problem, he introduced a special conditional $\rightarrow $ as a primitive logical connective so that the truth and determinateness of a conditional sentence $\phi \rightarrow \psi $ is characterized independently and differently from its usual definition $\neg ( \phi \wedge \neg \psi )$ in terms of negation and conjunction (or $\neg \phi \vee \psi $ in terms of negation and disjunction) by the following axioms:

Feferman’s approach diverges from ours in two crucial respects: First, he took $\mathfrak {D}$ as the range of all the principles of truth comprehensively and restricted every principle of truth to the class of determinate sentences $\mathfrak {D}$ , whereas we take the class of determinate sentences only as the range of the disquotation schema and postulate the compositional axioms unrestrictedly for every sentence. Secondly, he took $\mathfrak {D}$ as definable in terms of truth by stipulating $D x\leftrightarrow \mathrm {T} x \vee \mathrm {F} x$ ; but this definition does not yield the desired properties of $\mathrm {D}$ in our theory and we consequently introduce determinateness as a primitive notion.

Fujimoto [14] observed that $\mathsf {DT}$ is identical with the system $\mathsf {FKF} + \mathrm {Cons}$ of non-classical partial truth whose evaluation rule is given by the Aczel–Feferman evaluation schema. The Aczel–Feferman evaluation schema is the same as the weak Kleene evaluation schema, with the exception of the evaluation rule of the conditional. $\mathsf {FKF}$ is a variant of $\mathsf {KF}$ with the Aczel–Feferman evaluation schema: $\mathsf {FKF}$ is to the Aczel–Feferman evaluation schema is what $\mathsf {KF}$ is to the strong Kleene evaluation schema.

10.4 Comparison with the Leitgeb–Schindler system

Schindler [40] defined a group of systems that resemble ours. They differ from $\mathsf {CD}$ in restricting the compositional principles T4 –T6 to grounded sentences. The predicate symbol G for groundedness plays a role comparable to that of $\mathrm {D}$ in $\mathsf {CD}$ . The full system is called $\mathsf {CG}$ . All the unrestricted compositional axioms T4–T6 are provable except for the right-to-left direction of the negation axiom T4. That is, is not provable in $\mathsf {CG}$ . In this sense Schindler’s system fails to be thoroughly classical.

One of the axioms of $\mathsf {CG}$ is a ‘definitional’ axiom of groundedness [40, p. 77]:

This axiom of $\mathsf {CG}$ is not a theorem (with $\mathrm {D}$ for G) of our theory $\mathsf {CD}$ , because the full negation axiom T4 and thus

are theorems of $\mathsf {CD}$ and therefore Schindler’s definitional axiom would imply

. Consequently, Schindler’s system does not really require a primitive predicate for groundedness, while the definition of determinateness as truth or falsity fails in our system.

On Schindler’s approach, $\mathrm {T}$ applies provably only to sentences without G, because it lacks an axiom analogous to our T2. This is in line with the intended interpretation of G as Leitgeb’s [30] notion of groundedness. Also G cannot be iterated, and axiom D3 is absent from Schindler’s list of axioms. However, contrary to Schindler’s official formulation of the system, we could view $G x$ as a metalinguistic abbreviation for . Then $\mathrm {T}$ provably applies to sentences containing G.

10.5 Comparison with Halbach’s system PUTB

The truth-theoretic axioms of the system $\mathsf {PUTB}$ are given by all instances $\mathrm {T}\ulcorner \phi \urcorner \leftrightarrow \phi $ of the T-schema where the truth predicate occurs only positively in $\phi $ and parameters are allowed in $\phi $ .

Positiveness has the advantage over determinateness that it is a very simple syntactic decidable property that is definable in the language of arithmetic. If in the schema

1. DDS

the symbol $\mathrm {D}$ expresses that $\mathrm {T}$ occurs only positively, no primitive predicate $\mathrm {D}$ is needed, as positiveness can be expressed by an arithmetical formula. Consequently, because $\mathrm {D}$ is arithmetical, our axiom $\textsf {T2}^{+}$ , that is, becomes provable.

The theory $\mathsf {PUTB}$ does not prove the compositional axiom T4 –T6. To obtain a system closer to $\mathsf {CD}$ , one could add the compositional axioms to $\mathsf {PUTB}$ or derive them from reflection principles, as Horsten and Leigh [27] suggest.

However, T-positiveness and determinateness differ significantly: In particular, truth-teller sentences are provably T-positive, while they are not provably determinate in our sense; in fact we can refute their determinateness in $\mathsf {CD}_{\mu }$ as was shown in proposition 9.3. The proof-theoretic strength of $\mathsf {PUTB}$ relies crucially on indeterminate instances that allow one to mimick positive inductive definitions. Overall the restriction to determinate instead of positive sentences is better motivated.

10.6 Comparison with Picollo’s system WFUTB

Picollo [34, 35] defines a notion of referential well-foundedness, which is related to determinateness in our sense. Here we do not go into the details of its definition and only highlight some differences to our approach. First, the notion of well-foundedness is defined in such a way that it becomes arithmetically definable. Thus only a truth predicate needs to be added and no separate predicate for referential well-foundedness as our primitive predicate $\mathrm {D}$ . Roughly, the main axiom schema of her system $\mathsf {WFUTB}$ then states the T-sentences for sentences that are referentially well-founded in her sense (or $\mathsf {PA}$ - provably equivalent to such a sentence). ¹⁵ $\mathsf {WFUTB}$ does not feature any compositional axioms, and it can be shown that they are not provable in it, although the system was shown by Picollo to be proof-theoretically at least as strong as ramified analysis $\mathsf {RA}_{<\Gamma _0}$ up to $\Gamma _0$ and thus much stronger than PUTB and compositional theories such as $\mathsf {KF}$ .

10.7 Comparison with Field’s systems Int

The most fundamental decision for the truth theorist is whether to sacrifice classical logic for transparency or transparency for classical logic. By transparency we mean here some equivalence of $\phi $ with $\mathrm {T}\ulcorner \phi \urcorner $ for all $\phi $ . Field [11] sacrifices classical logic; we sacrifice transparency. Field saves truth from paradox; we save logic from paradox. We regain transparency for determinate sentences; Field regains classical logic for what he calls strongly classical sentences.

Field employs a new primitive predicate $Scl$ for strongly classical truth. Although Field’s and our approach are pulling in exactly opposite directions, Field’s axioms for $Scl$ and ours for $\mathrm {D}$ have a striking resemblance. As Field in footnote 6 mentions, he and we arrived at our axiomatizations independently. Of course, a serious comparison of Int and $\mathsf {CD}$ leads back to the most fundamental decision that truth theorists face, and we do not enter the discussion here.

11 Further perspectives

In the part II of this paper, we will give proof-theoretic analysis of variants of $\mathsf {CD}$ . In particular, among many others, we will give a proof of Theorem 9.4. We conclude the paper by listing two open problems.

1. (I) We may consider $\mathsf {CD}$ and its variants with the schema of induction restricted to the arithmetical sentences. In many cases, the restriction of induction to the arithmetical sentences results in a proof-theoretically conservative theory (over $\mathsf {PA}$ ). We conjecture that the same holds for $\mathsf {CD}$ . Conservativeness proofs in the analogous case of $\mathsf {KF}$ can be given in a model-theoretic way by showing how to extend a given model of $\mathsf {PA}$ to a model of ${\mathsf {KF}}$ with arithmetical induction only. This is not possible in the case of $\mathsf {CD}$ because Lachlan’s theorem [29] applies and nonstandard models that can be expanded to $\mathsf {CD}$ with restricted induction have to be recursively saturated.

2. (II) It may be of interest to replace the axiom D3 of $\mathsf {CD}$ with an alternative axiom . Together with DDS this would yield our additional axiom $\textsf {T2}^{+}$ . Thus, adding may be more natural than adding $\textsf {T2}^{+}$ . We do not know how strong $\mathsf {CD}$ becomes if is added.