# The two halves of disjunctive correctness

Cezary Cieśliński111Faculty of Philosophy, University of Warsaw., Mateusz
Łełyk222Faculty of Philosophy, University of Warsaw., Bartosz
Wcisło333Institute of Mathematics, Polish Academy of Sciences.

###### Abstract

Ali Enayat had asked whether two halves of Disjunctive Correctness (DC) for
the compositional truth predicate are conservative over Peano Arithmetic. In
this article, we show that the principle “every true disjunction has a true
disjunct” is equivalent to bounded induction for the compositional truth
predicate and thus it is not conservative. On the other hand, the converse
implication “any disjunction with a true disjunct is true” can be
conservatively added to PA. The methods introduced here allow us to give a
direct nonconservativeness proof for DC.

##  1 Introduction

The area of axiomatic truth theories analyses the concept of truth by studying
first-order theories which try to capture various properties of this notion.
These theories are formulated as follows: We choose a base theory strong
enough to represent syntax (this is typically Peano Arithmetic, PA). To this
theory, we add a fresh predicate $T(x)$ whose intended reading is “$x$ is (a
code of) a true sentence” together with axioms governing the behaviour of that
predicate. A notable example of such a theory is $\textnormal{CT}^{-}$ which
stipulates that the truth predicate satisfies Tarski’s compositional
conditions for arithmetical sentences. For instance, a conjunction
$\phi\wedge\psi$ is true iff both $\phi$ and $\psi$ are true.

If we add to $\textnormal{CT}^{-}$ full induction for the formulae containing
the truth predicate, the resulting theory, called CT, is not conservative over
PA, that is, it proves arithmetical theorems which cannot be demonstrated in
PA itself. More specifically, we can show by induction on the lengths of
proofs that every sentence provable in PA is true (a principle called global
reflection over PA) and, consequently, that PA is consistent.444This is one of
the basic results of truth theory. A comprehensive introduction to the area,
including this result, can be found in (Halbach, 2011). On the other hand, by
a theorem of Kotlarski, Krajewski, and Lachlan (see (Kotlarski et al., 1981))
$\textnormal{CT}^{-}$ itself does not prove any new arithmetical theorems.

In (Cieśliński, 2010), it was shown that already $\textnormal{CT}^{-}$
extended with a principle of propositional reflection “sentences derived in
propositional logic from true premises are true” suffices to prove global
reflection over PA. In other words, an overtly nonconservative principle can
be derived without explicitly assuming induction on a ground of a rather
innocuous principle of overtly truth-theoretic nature. Subsequently, it turned
out that a number of other truth-theoretic principles are not conservative
over PA and are all equivalent to $\Delta_{0}$-induction for the compositional
truth predicate ($\textnormal{CT}^{-}$ with $\Delta_{0}$-induction is called
$\textnormal{CT}_{0}$).555 For the proof of nonconservativity of
$\textnormal{CT}_{0}$, see (Łełyk and Wcisło, 2017). The picture that emerged
was that there seems to be a “minimal natural” nonconservative extension of
$\textnormal{CT}^{-}$.

The “dividing line” between conservative and nonconservative extensions of PA
has been named “Tarski boundary” by Ali Enayat.666One can find more
information on the Tarski boundary in (Cieśliński, 2017). A more concise
discussion is also contained in (Łełyk and Wcisło, 2016) and (Łełyk, 2019).
One of the most striking results on Tarski boundary was obtained by Enayat and
Pakhomov (2019). It was shown that among theories equivalent to
$\textnormal{CT}_{0}$ is $\textnormal{CT}^{-}$ together with the principle of
disjunctive correctness, DC, which states that any finite (but possibly
nostandard) disjunction is true iff one of the disjuncts is true. This axiom
appears to be a mild, natural, extension of the compositional clauses and yet
turns out to carry the full strength of $\Delta_{0}$-induction.

It was not clear whether this result can be pushed further in the following
manner: Disjunctive correctness can be naturally split into two halves. The
first half is a principle DC-in saying “a disjunction with true disjunct is
true” and the second is DC-out which says “a true disjunction has a true
disjunct”. It has been asked in (Enayat and Pakhomov, 2019) whether the second
of these principles can be added conservatively to PA.777See Question 5.3 in
(Enayat and Pakhomov, 2019). The conservativity of DC-in was settled in
December 2018 and stated in the formulation of that question, but the proof
was not published.

In this article, we analyse both of the above principles. We show that over
$\textnormal{CT}^{-}$, DC-in gives rise to a conservative extension of PA
while DC-out yields $\Delta_{0}$-induction. The methods used for the
nonconservativeness result yield a new, direct proof that DC is yet another
incarnation of $\Delta_{0}$-induction for the formulae containing the truth
predicate.

##  2 Preliminaries

We consider truth theories over Peano arithmetic, PA, as our base
theory.888The choice is motivated mostly by a certain tradition in the field.
However, the results make sense and still hold true over much weaker theories,
say $\textnormal{I}\Delta_{0}+\exp$. It is an axiomatic theory in a language
$\mathscr{L}_{\textnormal{PA}}=\\{S,+,\times,0\\}$ whose axioms consist of
inductive definitions of addition and multiplication in terms of the successor
function $S$ together with the full induction scheme. Although this theory
overtly speaks of natural numbers, in fact it is strong enough to capture
objects such as finite sets, finite sequences, or finite graphs. Crucially, PA
is capable of expressing syntactic notions such as “term”, “formula” or
“proof” and proving basic facts about these notions such as “a conjunction of
two formulae is a formula.” We assume that the reader is familiar with the
coding of syntax and the basic metamathematics. This is discussed in many
sources such as (Kaye, 1991), Chapter 9 or (Hájek and Pudlák, 1993), Chapter
I, Section 1(d), pp.50–61. Throughout the article, we will explain those bits
of notation that seem not to explain themselves. We provide a glossary of all
formalised notions we are using throughout the paper in the appendix.

######  Convention 1.

  * •

We will often conflate Gödel numbers of syntactic objects with those objects.
We will also use formulae denoting syntactic expressions as if they were sets.
For instance, we will write
$\phi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}$ rather than
$\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(\phi)$, where
$\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}$ expresses that $\phi$ is
(a Gödel code of) an arithmetical sentence.

  * •

Provably functional formulae will be used as if denoting actual functions. For
instance, we will write $\textnormal{FV}(\phi)$ for the set of free variables
of $\phi$.

  * •

In particular, we will often write the results of syntactic operations without
explicitly mentioning the operations themselves. For instance, if
$\phi,\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}$, we will
freely speak of the conjunction $\phi\wedge\psi$ rather than “the only $z$
such that $z$ is a conjunction of $\phi$, $\psi$.”

The research on Tarski boundary concerns extensions of the compositional truth
theory. Let us define it. By writing $\underline{n}$, we mean (the Gödel code
of) a numeral denoting the number $n$, that is,

$\ulcorner\underbrace{S(S\ldots S(0)\ldots)}_{\textnormal{``$S$'' repeated $n$
times}}\urcorner.$

If $t$ is (a Gödel code of) a closed arithmetical term, then by ${t}^{\circ}$
we mean the value of that term. Thus we have, for instance,

$\mathbb{N}\models{\ulcorner
S0+S(S(0))\urcorner}^{\circ}={\underline{3}}^{\circ}=3.$

Note that a value of an arithmetical term can be computed in a primitive
recursive way and the natural function computing it may be formalised in PA.
Now we can proceed to the actual definition.

######  Definition 2.

By $\textnormal{CT}^{-}$ (Compositional Truth) we mean a theory in the
arithmetical language with a fresh unary predicate $T$ extending PA with the
following axioms:

  * •

$\forall x\
\Big{(}T(x)\rightarrow\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(x)\Big{)}.$

  * •

$\forall
s,t\in\textnormal{ClTerm}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}T(s=t)\equiv{s}^{\circ}={t}^{\circ}\Big{)}.$

  * •

$\forall\phi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}T(\neg\phi)\equiv\neg
T\phi\Big{)}.$

  * •

$\forall\phi,\psi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}T(\phi\vee\psi)\equiv
T\phi\vee T\psi\Big{)}.$

  * •

$\forall\phi,\psi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}T(\phi\wedge\psi)\equiv
T\phi\wedge T\psi\Big{)}.$

  * •

$\forall\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}\forall
v\in\textnormal{Var}\Big{(}\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(\exists
v\phi)\rightarrow T(\exists v\phi)\equiv\exists x\
T\phi(\underline{x})\Big{)}.$

  * •

$\forall\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}\forall
v\in\textnormal{Var}\Big{(}\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(\forall
v\phi)\rightarrow T(\forall v\phi)\equiv\forall x\
T\phi(\underline{x})\Big{)}.$

  * •

$\forall\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}\forall\bar{s},\bar{t}\in\textnormal{ClTermSeq}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}{\bar{s}}^{\circ}={\bar{t}}^{\circ}\rightarrow
T\phi(\bar{s})=T\phi(\bar{t})\Big{)}.$

Above, $\textnormal{ClTermSeq}_{\mathscr{L}_{\textnormal{PA}}}(x)$ is a
formula expressing “$x$ is a sequence of closed arithmetical terms.” The rest
of the notation should be self-explanatory and, as we remarked earlier, it is
discussed in the appendix.

By CT, we mean $\textnormal{CT}^{-}$ with full induction for the extended
language. By $\textnormal{CT}_{0}$, we mean $\textnormal{CT}^{-}$ with
induction for $\Delta_{0}$ formulae containing the truth predicate. (Note that
already $\textnormal{CT}^{-}$ contains full arithmetical induction.)

The last clause in the above axioms for $\textnormal{CT}^{-}$ is called
Regularity Axiom, REG. It is not included among the basic axioms in the
standard presentations of this theory, like (Halbach, 2011) or (Cieśliński,
2017). The version of $\textnormal{CT}^{-}$ with REG appears, e.g., in (Enayat
et al., 2020) or (Łełyk and Wcisło, 2021). Admittedly, the regularity axiom
has a clearly different status than the rest of the axioms of
$\textnormal{CT}^{-}$. We add it mostly for two (admittedly technical) reasons
which we will explain in Section 6.

Although $\textnormal{CT}^{-}$ seems to express the crucial properties of the
truth predicate, it is not arithmetically stronger than PA. The result was
essentially proved by Kotlarski et al. (1981).999The original result concerns
satisfaction classes over a purely relational language. This work has been
extended in (Kaye, 1991) to languages with terms and in (Engström, 2002) to
truth classes over languages with terms. Subsequently, Enayat and Visser
(2015) introduced a new, elegant and flexible method of constructing
satisfaction classes which allowed them to strengthen the previous results in
a number of interesting ways. They worked again in purely relational
languages. A version for functional languages can be found in (Cieśliński,
2017). A version of Enayat–Visser construction covering languages with
functional symbols with the regularity axioms included is discussed in (Łełyk
and Wcisło, 2021). A reader may find a proof of a stronger result also in this
article in Section 4.

######  Theorem 3 (Kotlarski–Krajewski–Lachlan).

$\textnormal{CT}^{-}$ is conservative over PA, i.e., for any sentence
$\phi\in\mathscr{L}_{\textnormal{PA}}$ if $\textnormal{CT}^{-}\vdash\phi$,
then $\textnormal{PA}\vdash\phi$.

The above result contrasts with the situation for CT. By induction on the
length of proofs, we can show that every proof in PA has true conclusion. In
other words, we can prove in CT the following principle of Global Reflection,
GRef:

$\forall\phi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}\textnormal{Pr}_{\textnormal{PA}}(\phi)\rightarrow
T\phi\Big{)}.$

Notice that $\textnormal{CT}^{-}+\textnormal{GRef}$ is clearly not
conservative over PA, since in particular $\neg T(0\neq 0)$ is provable in the
compositional theory $\textnormal{CT}^{-}$ and, by contraposition
$\neg\textnormal{Pr}_{\textnormal{PA}}(0\neq 0)$. The latter is not provable
in PA by Gödel’s second theorem.

As we have already mentioned, a number of seemingly unrelated principles
turned out to be equivalent to this canonical nonconservative axiom GRef. One
of them is $\Delta_{0}$-induction for the compositional truth predicate.
Another principle which will play an important role in this article is
Propositional Reflection, PropRef, defined as follows:

$\forall\phi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}\textnormal{Pr}^{T}_{\textnormal{Prop}}(\phi)\rightarrow
T\phi\Big{)},$

where $\textnormal{Pr}_{\textnormal{Prop}}^{T}(x)$ means that $x$ is derivable
in propositional logic from the set of premises $\Gamma$, such that $T(y)$
holds for each $y\in\Gamma$. As we have already noted, Cieśliński (2010)
showed that over $\textnormal{CT}^{-}$, PropRef is equivalent to $\Delta_{0}$
induction for the truth predicate. Subsequently, $\textnormal{CT}_{0}$ was
shown by Łełyk and Wcisło (2017) to be arithmetically equivalent to GRef and
then, in Łełyk (2017), to be exactly the same theory as
$\textnormal{CT}^{-}+\textnormal{GRef}$. Another presentation of the last
result can be also found in a recent preprint (Łełyk, 2021).

Related to propositional reflection is the following principle of
Propositional Soundness, PropSnd:

$\forall\phi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}\textnormal{Pr}_{\textnormal{Prop}}(\phi)\rightarrow
T\phi\Big{)}.$

In effect, this axiom expresses that any arithmetical sentence which is a
propositional tautology is true. It is still unknown whether
$\textnormal{CT}^{-}+\textnormal{PropSnd}$ is conservative over PA. In the
next section, we shall present a partial result towards this problem.

Now, let us turn to the main subject of our article. If
$M\models\textnormal{PA}$ and
$\bar{\phi}\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}(M)$ is a
coded sequence of sentences, we can form their disjunction
$\bigvee\bar{\phi}$, which we will also denote by $\bigvee_{i\leq c}\phi_{i}$
if the length of $\bar{\phi}$ is $c$. We always assume that in “big
disjunctions” parentheses are grouped to the left, so that the following
equality holds in $M$:

$\bigvee_{i\leq c+1}\phi_{i}=\bigvee_{i\leq c}\phi_{i}\vee\phi_{c+1}.$

In effect, $\bigvee_{i\leq c}\phi$ denotes the following formula:

$(((\phi_{0}\vee\phi_{1})\vee\ldots)\vee\phi_{c-1})\vee\phi_{c}.$

The precise definition of how disjunctions over multiple disjuncts are
parenthesised can actually matter in some cases. In the presence of
$\Delta_{0}$-induction for the extended language, one can show that any two
disjunctions with the same disjuncts are equivalent, no matter how the
disjuncts are ordered and grouped together. However, this is not the case in
pure $\textnormal{CT}^{-}$. The precise parenthesising can become relevant,
since it dictates the relations between disjunctions over arbitrarily many
disjuncts and the usual binary disjunctions. We will return to this issue in
Section 5.

By Disjunctive Correctness, DC, we mean the following axiom:

$\forall\bar{\phi}\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}\bigg{(}T\left(\bigvee\bar{\phi}\right)\equiv\exists
i\leq\textnormal{lh}(\bar{\phi})\ T\phi_{i}\bigg{)}.$

Therefore, DC states that a finite (but possibly nonstandard) disjunction is
true iff it has a true disjunct. Very surprisingly, DC is yet another
incarnation of $\textnormal{CT}_{0}$ as shown by Enayat and Pakhomov (2019).

######  Theorem 4 (Enayat–Pakhomov).

$\textnormal{CT}^{-}+\textnormal{DC}$ and $\textnormal{CT}_{0}$ are
equivalent.

As we mentioned, $\textnormal{CT}_{0}$ is not conservative over PA. Hence the
following fact easily follows:

######  Corollary 5 (Enayat–Pakhomov).

$\textnormal{CT}^{-}+\textnormal{DC}$ is not conservative over PA.

Disjunctive correctness can be naturally split into two principles. The first
is DC-out (“a true disjunction has a true disjunct”):

$\forall\bar{\phi}\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}T\bigvee\bar{\phi}\rightarrow\exists
i\leq\textnormal{lh}(\bar{\phi})\ T\phi_{i}\Big{)}.$

The second is DC-in (“a disjunction with a true disjunct is true”):

$\forall\bar{\phi}\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}\exists
i\leq\textnormal{lh}(\bar{\phi})\ T\phi_{i}\rightarrow
T\bigvee\bar{\phi}\Big{)}.$

As we have mentioned, the status of DC-out was not settled in (Enayat and
Pakhomov, 2019) and the claim that DC-in is conservative was stated without a
proof. The subsequent parts of this article will be devoted to the analysis of
both principles.

Let us finish this section by summing up the positive results on equivalences
of theories of truth relevant for this work:

######  Theorem 6.

The following theories are equivalent:

  1. 1.

$\textnormal{CT}_{0}$.

  2. 2.

$\textnormal{CT}^{-}+\textnormal{GRef}$.

  3. 3.

$\textnormal{CT}^{-}+\textnormal{PropRef}$.

  4. 4.

$\textnormal{CT}^{-}+\textnormal{DC}$.

##  3 Yablo sequences and disjunctive correctness

In this section, we prove that DC-out is equivalent to $\textnormal{CT}_{0}$.
The argument is indirectly inspired by the classical Visser–Yablo paradox:
101010See (Yablo, 1993). Consider the sequence of sentences
$Y_{n},n\in\mathbb{N}$, such that $Y_{n}$ says: “some sentence $Y_{k}$ for
$k>n$ is false.” If for some $k$, $Y_{k}$ is false, then every sentence
$Y_{l}$ for $l>k$ is true. However, if $Y_{l}$ is true, then there is some
$m>l$ such that $Y_{m}$ is false contradicting the assumption. Hence, every
sentence in the Yablo sequence is true. However, if some sequence in the Yablo
sequence is true, then some has to be false, so they cannot be all true. We
reach a contradiction.

Using a construction inspired by the Yablo sequence, we will show that DC-out
implies $\textnormal{CT}_{0}$. We will actually use two intermediate
principles which are overtly related to $\Delta_{0}$-induction. By sequential
induction, SInd, we mean the following axiom:111111A related principle of
Modus Ponens correctness was introduced earlier by Ali Enayat in an
unpublished note (Enayat, 2014). The principle states that if a conjunction of
the implications $\phi_{i}\rightarrow\phi_{i+1}$ is true for $i=0,1,\ldots,c$
and $\phi_{0}$ is true, then $\phi_{c+1}$ is true. However, as stated, this
principle is conservative over PA. Namely, it holds in any model in which all
conjunctions of nonstandard length are false and by a construction very
similar to that presented in Section 4, for any completion $U$ of PA, we can
find models with this property satisfying $U$.

$\forall s\in\textnormal{FinSeq}\ \Big{(}Ts_{0}\wedge\forall
i<\textnormal{lh}(s)-1\big{(}Ts_{i}\rightarrow
Ts_{i+1}\big{)}\rightarrow\forall j<\textnormal{lh}(s)\ Ts_{j}\Big{)}$

The sequential order induction, SOInd, is a natural variant of the above
principle:

$\forall s\in\textnormal{FinSeq}\ \Big{(}\forall
j<\textnormal{lh}(s)\big{(}(\forall i<jTs_{i})\rightarrow
Ts_{j}\big{)}\rightarrow\forall l<\textnormal{lh}(s)\ Ts_{l}\Big{)}.$

As we already mentioned, SInd and SOInd are clearly related to
$\Delta_{0}$-induction:

######  Proposition 7.

$\textnormal{CT}^{-}+\textnormal{SOInd}$ and $\textnormal{CT}_{0}$ are
equivalent.

###### Proof.

$\textnormal{CT}_{0}$ clearly entails SOInd. On the other hand, observe that
SOInd implies PropRef which by Theorem 6 is equivalent to
$\textnormal{CT}_{0}$. Working in $\textnormal{CT}^{-}+\textnormal{SOInd}$,
fix a proof $(\phi_{0},\ldots,\phi_{c})$ in propositional logic from true
premises. We can assume that the proof system is chosen so that for all $i$,
either $\phi_{i}$ is an assumption of the proof or $\phi_{i}$ is obtained by
modus ponens from two formulas appearing earlier in the proof. In particular,
for every $j$, if every formula $\phi_{j}$ for $j<i$ is true, then $\phi_{i}$
is true which, by SOInd, implies that the conclusion of the proof is true.
Thus PropRef holds. ∎

Now, we get to the core argument of the article:

######  Theorem 8.

Over $\textnormal{CT}^{-}$, DC-out implies SInd.

###### Proof.

Working in $\textnormal{CT}^{-}+\textnormal{DC-out}$, fix any sequence
$(\phi_{0},\ldots,\phi_{c})\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}$
such that $T\phi_{0}$ holds and for each $i$, $T\phi_{i}$ entails
$T\phi_{i+1}$. Let us define a sequence $\psi_{i},i\leq c$ as follows:

$\displaystyle\psi_{0}$ $\displaystyle:=$ $\displaystyle\phi_{0}$
$\displaystyle\psi_{j+1}$ $\displaystyle:=$
$\displaystyle\neg\phi_{j+1}\rightarrow\bigvee_{i<j+1}\neg\psi_{i}.$

We claim that for all $j\leq c$, the sentence $\psi_{j}$ is true. Suppose that
$\neg T\psi_{j}$ holds for some $j$. Then $j>0$, so we have:

$\neg T\phi_{j}\wedge\neg T\bigvee_{i<j}\neg\psi_{i}.$

By compositional conditions, this is equivalent to:

$\neg T\phi_{j}\wedge\neg T\left(\bigvee_{i<j-1}\neg\psi_{i}\right)\wedge
T\psi_{j-1}.$

Expanding the definition of $\psi_{j-1}$, we obtain:

$\neg T\phi_{j}\wedge\neg
T\left(\bigvee_{i<j-1}\neg\psi_{i}\right)\wedge\left(T\phi_{j-1}\vee
T\left(\bigvee_{i<j-1}\neg\psi_{i}\right)\right).$

However, $\neg T\phi_{j}$ implies $\neg T\phi_{j-1}$. Therefore, we have the
following:

$\neg T\phi_{j}\wedge\neg T\left(\bigvee_{i<j-1}\neg\psi_{i}\right)\wedge
T\left(\bigvee_{i<j-1}\neg\psi_{i}\right).$

This contradiction concludes the proof of the claim. Notice that the proof of
the claim only uses the fact that provably in $\textnormal{CT}^{-}$,

$T\left(\bigvee_{i\leq j+1}\eta_{i}\right)\equiv T\left(\bigvee_{i\leq
j}\eta_{i}\right)\vee T\eta_{j+1}.$

Now, we show that for all $j<c$, $\phi_{j}$ is true. Suppose otherwise and fix
$j$ such that $\neg T\phi_{j}$. Since $T\psi_{j}$ holds, we have:

$T\bigvee_{i<j}\neg\psi_{i}$

By DC-out, we can fix $i<j$ such that $\neg T\psi_{i}$ holds. However, this
contradicts the previous claim. ∎

As an application of the above result, we show that DC-out is the same theory
as DC. In particular, $\textnormal{CT}^{-}+\textnormal{DC-out}$ is not
conservative over PA.

######  Theorem 9.

$\textnormal{CT}^{-}+\textnormal{SInd}$ implies DC-in. Consequently, DC-out
and DC are equivalent over $\textnormal{CT}^{-}$.

###### Proof.

Working in $\textnormal{CT}^{-}+\textnormal{SInd}$ fix any sequence
$(\alpha_{0},\ldots,\alpha_{c})$ such that
$\alpha_{i}\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}$ for all
$i\leq c$. Suppose that $\alpha_{j}$ is true for some $j\leq c$ and notice
that

$\bigvee_{i\leq j}\alpha_{i}=\bigvee_{i\leq j-1}\alpha_{i}\vee\alpha_{j},$

hence the disjunction of $\alpha_{i}$ up to and including $j$ has to be true
as well. Moreover, for any $k$, if $\bigvee_{i\leq k}\alpha_{i}$ is true, then
$\bigvee_{i\leq k+1}\alpha_{i}$ is true. Hence by sequential induction
(starting with $\bigvee_{i\leq j}\alpha_{i}$), $T\bigvee_{i\leq c}\alpha_{i}$
holds. ∎

Another application is a more perspicuous proof of nonconservativity of
$\textnormal{CT}^{-}+\textnormal{DC}$.

######  Theorem 10.

$\textnormal{CT}^{-}+\textnormal{DC}$ implies SOInd. Hence,
$\textnormal{CT}^{-}+\textnormal{DC}$ is equivalent to $\textnormal{CT}_{0}$.

###### Proof.

Working in $\textnormal{CT}^{-}+\textnormal{DC}$, fix any sequence
$(\phi_{0},\ldots,\phi_{c})$ and suppose that for any $j$, if $T\phi_{i}$
holds for all $i<j$, then $T\phi_{j}$ holds. By DC, the following implication
holds for all $j\leq c$:

$T\neg\bigvee_{i\leq j}\neg\phi_{i}\rightarrow T\neg\bigvee_{i\leq
j+1}\neg\phi_{i}.$

(Of course, these are essentially big conjunctions, but prima facie,
disjunctive correctness does not imply conjunctive correctness.) Then, by
SInd, we conclude that

$T\neg\bigvee_{i\leq j}\neg\phi_{i}$

holds for each $i$ which, again using DC implies that $T\phi_{j}$ holds for
each $j$.

By Proposition 7 it follows that
$\textnormal{CT}_{0}\subseteq\textnormal{CT}^{-}+\textnormal{DC}$. Since DC is
easily provable in $\textnormal{CT}_{0}$, we conclude that
$\textnormal{CT}^{-}+\textnormal{DC}$ is equivalent to $\textnormal{CT}_{0}$.
∎

######  Remark 11.

The main nonconservativeness proof for DC in (Enayat and Pakhomov, 2019)
consists of two parts: it is first shown that over $\textnormal{CT}^{-}$, DC
implies the axiom of internal induction INT, to be defined in the next
section, and then a much more direct proof that
$\textnormal{DC}+\textnormal{INT}$ implies $\textnormal{CT}_{0}$ follows. It
is easy to verify that $\textnormal{CT}^{-}+\textnormal{SInd}$ entails
internal induction and since we know that
$\textnormal{CT}^{-}+\textnormal{DC}$ implies SInd, we obtain a still
different proof that $\textnormal{CT}^{-}+\textnormal{DC}$ is equivalent to
$\textnormal{CT}_{0}$.

We can present the above results in a slightly more abstract manner. This will
allow us to obtain a significantly simpler proof of the result from (Wcisło,
2020) on the strength of certain extensions of Propositional Soundness.

######  Definition 12.

Let $U$ be a theory extending $\textnormal{CT}^{-}$. We say that $U$ has outer
disjunctions if there exists a provably functional formula $D(x,y)$ such that
for any
$\bar{\phi}=\langle\phi_{1},\ldots,\phi_{c}\rangle\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}$,
we have $D(\bar{\phi})\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}$
and the following two properties hold provably in $U$:

  * •

$\forall\bar{\phi}\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}\forall\psi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}\
\Big{(}TD(\bar{\phi}\frown\langle\psi\rangle)\equiv TD(\bar{\phi})\vee
T\psi\Big{)}.$

  * •

$\forall\bar{\phi}\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}TD(\bar{\phi})\rightarrow\exists
i\leq\textnormal{lh}(\bar{\phi})\ T\phi_{i}\Big{)}.$

We call $D$ as above an outer disjunction of $\phi_{1},\ldots,\phi_{c}$.

In other words, a theory of truth has outer disjunctions if it has some
uniform construction that behaves like disjunctions in
$\textnormal{CT}^{-}+\textnormal{DC-out}$.

######  Proposition 13.

Suppose that $U$ has outer disjunctions. Then it satisfies SOInd and in
particular, it contains $\textnormal{CT}_{0}$.

###### Sketch of the proof..

This is literally the same argument as in Theorems 8, 9, and 10. We only used
the fact that $\textnormal{CT}^{-}+\textnormal{DC-out}$ has outer
disjunctions. ∎

By quantifier-free correctness, QFC, we mean the following axiom:

$\forall\phi\in\textnormal{qfSent}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}\textnormal{Tr}_{0}(\phi)\rightarrow
T\phi\Big{)}.$

Let us pause for a moment and explain the notation. The formula
$\textnormal{qfSent}_{\mathscr{L}_{\textnormal{PA}}}(x)$ expresses that $x$ is
a quantifier-free sentence of $\mathscr{L}_{\textnormal{PA}}$, i.e., a Boolean
combination of closed term equations. Peano arithmetic has a canonical way of
deciding whether such (possibly nonstandard) sentences should be true or false
by applying partial arithmetical truth predicates. The formula
$\textnormal{Tr}_{0}$ is such a predicate for $\Delta_{0}$ formulae.121212For
a more detailed explanation of what partial arithmetical truth predicates are,
consult (Kaye, 1991), Section 9 or (Hájek and Pudlák, 1993), Chapter I,
Section 1(d). It can be checked that QFC does not bring any arithmetical
strength to $\textnormal{CT}^{-}$.

######  Proposition 14.

$\textnormal{CT}^{-}+\textnormal{QFC}$ is conservative over PA.

The above proposition follows by a routine application of the methods
introduced by Enayat and Visser, see e.g. (Enayat and Visser, 2015). A proof
of this result in the exact same setting in which we work (with regularity
axioms included in the definition of $\textnormal{CT}^{-}$) can be found in
(Wcisło, 2020). In the same article, it was shown with a different argument
using a propositional construction called disjunctions with stopping
conditions that QFC becomes significantly stronger when combined with PropSnd.
Now we can prove that result with a simpler argument:

######  Proposition 15.

$\textnormal{CT}^{-}+\textnormal{QFC}+\textnormal{PropSnd}$ has outer
disjunctions. In particular, it is equivalent to $\textnormal{CT}_{0}$.

###### Proof.

The “in particular” part follows by Proposition 13 and the fact that QFC and
PropSnd are clearly implied by $\Delta_{0}$-induction. So it is enough to show
that $\textnormal{CT}^{-}+\textnormal{QFC}+\textnormal{PropSnd}$ has outer
disjunctions.

For $\bar{\phi}=(\phi_{1},\ldots,\phi_{c})$, let

$D(\bar{\phi})=\exists x\leq c\bigvee_{i\leq c}\underline{i}=x\wedge\phi_{i}.$

Let us check that $D$ is an outer disjunction. First, consider the formula
$D(\bar{\phi}\frown\langle\phi_{c+1}\rangle)$, i.e.

$\exists x\leq c+1\bigvee_{i\leq c+1}\underline{i}=x\wedge\phi_{i}.$

We want to check that it is true iff either $D(\bar{\phi})$ is true or
$\phi_{c+1}$ is true. Suppose that

$T\exists x\leq c+1\ \bigvee_{i\leq c+1}\underline{i}=x\wedge\phi_{i}.$

By the compositional clauses and the definition of big disjunctions, this
implies:

$\exists x\leq c+1\ T\left(\bigvee_{i\leq
c}\underline{i}=\underline{x}\wedge\phi_{i}\right)\vee\exists x\leq c+1\
T\left(\underline{c+1}=\underline{x}\wedge\phi_{c+1}\right).$

It can be easily checked by compositional clauses that if the second clause
holds, then $T\phi_{c+1}$ holds. So it is enough to check that the first
clause in fact implies

$\exists x\leq c\ T\left(\bigvee_{i\leq
c}\underline{i}=\underline{x}\wedge\phi_{i}\right).$

To this end, we have to check that

$\neg T\left(\bigvee_{i\leq
c}\underline{i}=\underline{c+1}\wedge\phi_{i}\right).$

However, notice that the following implication is an instance of a
propositional tautology:

$\left(\bigwedge_{i\leq
c}\underline{i}\neq\underline{c+1}\right)\rightarrow\neg\left(\bigvee_{i\leq
c}\underline{i}=\underline{c+1}\wedge\phi_{i}\right).$

Hence, by PropRef, the whole implication is true and by QFC the antecedent is
true as well and the conclusion follows by compositionality. This ends the
proof of the implication.

The verification that $TD(\bar{\phi})\vee T\phi_{c+1}$ implies
$TD(\bar{\phi}\frown\langle\phi_{c+1}\rangle)$ is similar, but simpler, as it
only uses compositional clauses of $\textnormal{CT}^{-}$.

Now, suppose that the following holds:

$T\exists x\leq c\bigvee_{i\leq c}\underline{i}=x\wedge\phi_{i}.$

We want to check that for some $i\leq c$, $T\phi_{i}$ holds. By compositional
clauses, we know that there exists $a\leq c$ such that:

$T\bigvee_{i\leq c}\underline{i}=\underline{a}\wedge\phi_{i}.$

Again, using QFC and PropSnd, we check that the following holds:

$T\left(\neg\phi_{a}\rightarrow\neg\bigvee_{i\leq
c}\underline{i}=\underline{a}\wedge\phi_{i}\right).$

Thus we can conclude that $T\phi_{a}$ holds which ends the proof. ∎

######  Remark 16.

In the above proof, we could actually show that the formula $D(\bar{\phi})$
satisfies both directions of DC.

The principle SInd clearly looks very related to $\Delta_{0}$-induction for
the truth predicate. Indeed, it turns out that over $\textnormal{CT}^{-}$ the
two principles are equivalent.

######  Theorem 17.

$\textnormal{CT}^{-}+\textnormal{SInd}$ has outer disjunctions.

###### Proof.

For a coded sequence $(\phi_{1},\ldots,\phi_{k})$ of
$\mathscr{L}_{\textnormal{PA}}$-sentences, let $\bigwedge_{i\leq c}\phi_{i}$
be their conjunction with parentheses grouped to the left so that we have:

$\bigwedge_{i\leq c+1}\phi_{i}=\bigwedge_{i\leq c}\phi_{i}\wedge\phi_{c+1}.$

Using SInd, we can show that if $T\phi_{i}$ holds for every $i\leq c$, then
$T\bigwedge_{i\leq c}\phi_{i}$. We show this by considering an auxiliary
sequence

$\bigwedge_{i\leq 1}\phi_{i},\bigwedge_{i\leq
2}\phi_{i},\ldots,\bigwedge_{i\leq c}\phi_{i}.$

Now, we claim that the formula

$D(\bar{\phi}):=\neg\bigvee_{i\leq c}\neg\phi_{i}$

is an outer disjunction. It is easy to verify that over $\textnormal{CT}^{-}$:

$TD(\bar{\phi}\frown\langle\phi_{c+1}\rangle)\equiv TD(\bar{\phi})\vee
T\phi_{c+1}.$

We show that $D$ satisfies the second condition of outer disjunctions (DC-out)
by contraposition. If there is no $i\leq c$ such that $T\phi_{i}$, then
$T\neg\phi_{i}$ holds for every $i$. Consequently, the following conjunction
is true:

$\bigwedge_{i\leq c}\neg\phi_{i}$

which implies that $D\bar{\phi}$ cannot be true. This shows that $D$ is indeed
outer disjunction provably in $\textnormal{CT}^{-}+\textnormal{SInd}$. ∎

Let us summarise the above results:

######  Corollary 18.

The following theories are equivalent:

  * •

$\textnormal{CT}_{0}$

  * •

$\textnormal{CT}^{-}+\textnormal{SInd}$.

  * •

$\textnormal{CT}^{-}+\textnormal{SOInd}$.

  * •

$\textnormal{CT}^{-}+\textnormal{DC-out}$.

We conclude this section with some results that clarify the status of SInd and
SOInd. First of all, let us note that SInd and SOInd are really just some
forms of induction axioms and as such they do not require us to assume
$\textnormal{CT}^{-}$ to make sense. They both clearly follow from
$\textnormal{I}\Delta_{0}(T)$, the induction scheme for $\Delta_{0}$-formulae
containing the predicate $T$ (which is now treated just as some arbitrary
predicate). It turns out that these principles form a strict hierarchy.

######  Theorem 19.

Over PA,
$\textnormal{I}\Delta_{0}(T)\rightarrow\textnormal{SOInd}\rightarrow\textnormal{SInd}$.
Moreover, none of the implication reverses.

###### Proof.

Both implications are straightforward, so let us show that neither reverses.

$(\textnormal{SOInd}\nvdash\textnormal{I}\Delta_{0}(T))$. Let $M$ be a
countable nonstandard model of PA. Let $s_{i},i<\omega$ be an enumeration of
all coded sequences in $M$. We will inductively construct a sequence of finite
subsets of the standard cut $\omega^{M}$, $A_{i},B_{i},i<\omega$ such that for
all $i$, $A_{i}\cap B_{i}=\emptyset$. The sets $A$ are approximations to $T$,
the sets $B$ are approximations to the complement.

Let $A_{0}=B_{0}=\emptyset$. For an arbitrary $i<\omega$, we consider two
cases: if all the values of $s_{i}$ are elements of $A_{i}$, i.e.:

$\\{a\in M\ \mid\ \exists j<\textnormal{lh}(s_{i})\ a=s_{i}(j)\\}\subseteq
A_{i},$

then we set $A_{i+1}=A_{i},B_{i+1}=B_{i}$. Otherwise, let $j$ be the least
element such that $s_{i}(j)\notin A_{i}$ (this element exists, since $|A_{i}|$
is standard, and therefore, $A_{i}$ is arithmetically definable). Let
$b=s_{i}(j)$, let $a\neq b$ be an arbitrary element in
$\omega\setminus(A_{i}\cup B_{i})$ and set:

$\displaystyle A_{i+1}$ $\displaystyle=$ $\displaystyle A_{i}\cup\\{a\\}$
$\displaystyle B_{i+1}$ $\displaystyle=$ $\displaystyle B_{i}\cup\\{b\\}.$

Finally, we set $T=\bigcup_{i\in\omega}A_{i}$. We claim that
$(M,T)\models\textnormal{SOInd}$, but $(M,T)$ does not satisfy
$\textnormal{I}\Delta_{0}(T).$ The latter claim holds, since by construction
$T$ is an infinite (hence cofinal) subset of the standard cut $\omega$. To
check that the first claim holds, fix any coded sequence $s$. Pick $i<\omega$
such that $s=s_{i}$. By construction, either all values of $s_{i}$ are in
$A_{i}$, hence in $T$ or there exists an $l$ such that for all $j<l$,
$s_{i}(j)\in A_{i+1}$, but $s_{i}(l)\in B_{i+1}$ (which means that it is not
in $T$). This shows that $(M,T)\models\textnormal{SOInd}$.

($\textnormal{SInd}\nvdash\textnormal{SOInd}$) As before, fix an arbitrary
countable nonstandard model $M\models\textnormal{PA}$ and let $s_{i},i<\omega$
be an (external) enumeration of coded sequences from $M$. We inductively
construct two sequences of sets $A_{i},B_{i}$ such that for all $i$,
$A_{i}\cap B_{i}=\emptyset$, the sets $B_{i}$ are finite, and the sets $A_{i}$
contain only finitely many nonstandard elements of $M$.

We construct $A_{i},B_{i}$ as follows: let $A_{0}=\omega^{M}$ (the standard
initial cut of $M$) and $B_{0}=\emptyset$.

For an arbitrary $i$, if the set of values of $s_{i}$ is (standardly) finite,
we set $A_{i+1}=A_{i},B_{i+1}=B_{i}$. Otherwise, we consider two further
subcases. Suppose that the set of $j$ such that $s_{i}(j)\in B_{i}$ is an
initial segment in $M$ (possibly empty). Let $j_{0}$ be its supremum (it
exists by arithmetical induction, since $B_{i}$ is finite; if the considered
set is empty, then by definition, its supremum is $0$). On the other hand, the
set of values of $s_{i}$ is by assumption infinite, so by overspill there
exists $j>j_{0}$ such that $s_{i}(j)\notin A_{i}$. Let $a:=s_{i}(j-1)$ and let
$b:=s_{i}(j)$.

If the set $\\{j<\textnormal{lh}(s)\ \mid\ s_{i}(j)\in B_{i}\\}$ is not an
initial segment of $M$, then (again by arithmetical induction and finiteness
of $B_{i}$) there exists some $j$ such that $s_{i}(j)\notin B_{i}$ and
$s_{i}(j+1)\in B$. Let $a:=s_{i}(j),b:=s_{i}(j+1)$.

In both cases, set:

$\displaystyle A_{i+1}$ $\displaystyle=$ $\displaystyle A_{i}\cup\\{a\\}$
$\displaystyle B_{i+1}$ $\displaystyle=$ $\displaystyle B_{i}\cup\\{b\\}.$

Finally, let $T=\bigcup_{i\in\omega}A_{i}$. We claim that
$(M,T)\models\textnormal{SInd}$, but not SOInd.

To see that $(M,T)\models\textnormal{SInd}$, fix any coded sequence $s\in M$.
If the set of values of $s_{i}$ has (standard) finite number of elements, then
$T$ cannot violate the sequential induction axiom for $s$. So suppose that the
number of values of $s$ is nonstandard. Fix $i$ such that $s=s_{i}$ in our
enumeration. By construction, there exists $j\in M$ such that $s(j)\in
A_{i+1}\subset T$ and $s(j+1)\in B_{i+1}\subset M\setminus T$. So it is not
the case that for all $x$, $T(s(x))\rightarrow T(s(x+1))$ and thus the
sequential induction axiom for $s$ is satisfied.

On the other hand, $(M,T)$ does not satisfy SOInd. Indeed, fix any $c\in
M\setminus\omega$ and consider the identity sequence: $s(i)=i$ for
$i=0,1,\ldots,c$. We claim that the sequential order induction fails for this
sequence. Let us check that $s$ is progressive, i.e., if for any $j<i$
$s(j)\in T$, then $s(i)\in T$.

Fix any $i\leq c$. If $i\in\omega$, then $T(i)$ holds. On the other hand, if
$i$ is nonstandard, then consider the sequence $t:=s\upharpoonright i$. It has
nonstandardly many values, all of which are strictly below $i$. By
construction, there exists an element $b$ occurring in this sequence which is
not in $T$. This $b$ witnesses that not all $j<i$ are in $T$. Hence $s$ is
progressive. On the other hand, not all terms of $s$ are in $T$ which means
that SOInd fails.

∎

##  4 Conservativeness of DC-in

In the previous section, we have shown that
$\textnormal{CT}^{-}+\textnormal{DC-out}$ is not conservative over PA and
that, in fact, it is another incarnation of $\textnormal{CT}_{0}$. Now we will
use methods introduced by Enayat and Visser (2015) to show that the related
principle DC-in is actually conservative over PA. The Enayat–Visser technique
typically allows us to combine various results, so we can show joint
conservativity of several distinct principles. Here we will illustrate this
point by requiring that the constructed truth predicate additionally satisfies
internal induction. Let us recall that principle. If
$(M,T)\models\textnormal{CT}^{-}$, then each formula
$\phi\in\textnormal{Form}^{\leq 1}_{\mathscr{L}_{\textnormal{PA}}}(M)$
“defines” a set $\\{x\in M\ \mid\ \phi(\underline{x})\in T\\}$. Internal
induction $(\textnormal{INT})$ expresses that each such set satisfies the
induction principle:

$\forall\phi\in\textnormal{Form}^{\leq
1}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}T\phi(\underline{0})\wedge\forall
x\big{(}T\phi(\underline{x})\rightarrow
T\phi(\underline{x+1})\big{)}\rightarrow\forall x\
T\phi(\underline{x})\Big{)}.$

It was essentially observed already by Kotlarski et al. (1981) that
$\textnormal{CT}^{-}+\textnormal{INT}$ is conservative over PA. This result
can be also proved using cut elimination as in (Leigh, 2015) or the methods
invented by Enayat and Visser which we will use in this section in order to
show the following theorem:

######  Theorem 20.

$\textnormal{CT}^{-}+\textnormal{DC-in}+\textnormal{INT}$ is conservative over
PA.

The theorem is a direct corollary to the following model-theoretic result:

######  Theorem 21.

Let $M\models\textnormal{PA}$. Then there exists $M^{\prime}\succeq M$ and a
$T^{\prime}\subseteq M^{\prime}$ such that
$(M^{\prime},T^{\prime})\models\textnormal{CT}^{-}+\textnormal{INT}$ and for
all sequences
$\bar{\phi}\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}(M)$ of
nonstandard length, the disjunction $\bigvee\bar{\phi}$ is in $T^{\prime}$.

In other words, we will construct a model in which every disjunction with
infinitely many disjuncts is true. Such a model clearly satisfies DC-in: fix
any sequence of sentences $\bar{\phi}$ and suppose that there is
$i\leq\textnormal{lh}(\bar{\phi})$ such that $T^{\prime}\phi_{i}$. If
$\bar{\phi}$ has nonstandard length, then $\bigvee\bar{\phi}\in T^{\prime}$ by
assumption. On the other hand, if the length of $\bar{\phi}$ is standard, then
$\bigvee\bar{\phi}\in T^{\prime}$ directly by the compositional axioms. So it
is enough to prove Theorem 21.

In the proof, we will construct an elementary sequence of models
$M_{i}\models\textnormal{PA}$ and a sequence of satisfaction classes
$S_{i}\subset M_{i}^{2},i<\omega$ such that $S_{i+1}$ will satisfy
compositional clauses for formulae in the model $M_{i}$. Let us first define
what a satisfaction class actually is. Below, if $s$ is (a code of) a term and
$\alpha$ is a function whose domain contains the free variables of $s$ (an
$s$-assignment), by $s^{\alpha}$ we mean the formally computed value of $s$
under the valuation $\alpha$. For instance, if $\alpha$ ascribes the value $2$
to $x$ and $5$ to $y$, then

$\mathbb{N}\models\ulcorner SSx\times Sy\urcorner^{\alpha}=24.$

If $\alpha,\beta$ are assignments and $v$ is a variable, then by
$\beta\sim_{v}\alpha$ we mean that
$\textnormal{dom}(\beta)\supseteq\textnormal{dom}(\alpha)\cup\\{v\\}$ and
$\beta(w)=\alpha(w)$ for every $w\in\textnormal{dom}(\alpha)\setminus\\{v\\}$.
In other words, $\beta$ is just like $\alpha$, possibly except for the value
$\beta(v)$ which is not even required to be defined for $\alpha$.

######  Definition 22.

Let $M\models\textnormal{PA}$ and let
$\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$. By the
compositional clauses for $\phi$, $\textnormal{Comp}(\phi)$, we mean the
disjunction of the following sentences:

  1. 1.

$\exists s,t\in\textnormal{Term}_{\mathscr{L}_{\textnormal{PA}}}\
\Big{(}\phi=(s=t)\wedge\forall\alpha\in\textnormal{Asn}(\phi)\
\Big{(}S(\phi,\alpha)\equiv s^{\alpha}=t^{\alpha}\Big{)}\Big{)}.$

  2. 2.

$\exists\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}\
\Big{(}\phi=(\neg\psi)\wedge\forall\alpha\in\textnormal{Asn}(\phi)\
\Big{(}S(\phi,\alpha)\equiv\neg S(\psi,\alpha)\Big{)}\Big{)}.$

  3. 3.

$\exists\psi,\eta\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)\
\Big{(}\phi=(\psi\vee\eta)\wedge\forall\alpha\in\textnormal{Asn}(\phi)\Big{(}S(\phi,\alpha)\equiv
S(\psi,\alpha)\vee S(\eta,\alpha)\Big{)}\Big{)}.$

  4. 4.

$\exists\psi,\eta\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)\
\Big{(}\phi=(\psi\wedge\eta)\wedge\forall\alpha\in\textnormal{Asn}(\phi)\Big{(}S(\phi,\alpha)\equiv
S(\psi,\alpha)\wedge S(\eta,\alpha)\Big{)}\Big{)}.$

  5. 5.

$\exists\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)\exists
v\in\textnormal{Var}\ \Big{(}\phi=(\exists
v\psi)\wedge\forall\alpha\in\textnormal{Asn}(\phi)\Big{(}S(\phi,\alpha)\equiv\exists\beta\sim_{v}\alpha
S(\psi,\beta)\Big{)}\Big{)}.$

  6. 6.

$\exists\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)\exists
v\in\textnormal{Var}\ \Big{(}\phi=(\forall
v\psi)\wedge\forall\alpha\in\textnormal{Asn}(\phi)\Big{(}S(\phi,\alpha)\equiv\forall\beta\sim_{v}\alpha\
S(\psi,\beta)\Big{)}\Big{)}.$

We say that $S\subset M^{2}$ is a satisfaction class if there exists a subset
$D\subseteq\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$ such that the
following holds:

  * •

If $(\phi,\alpha)\in S$, then
$\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$ and
$\alpha\in\textnormal{Asn}(\phi)$.

  * •

If $(\phi,\alpha)\in S$ for some $\alpha\in\textnormal{Asn}(\phi)$, then
$\textnormal{Comp}(\phi)$ holds.

  * •

If $(\phi,\alpha)\in S$, then $\phi\in D$ or $\phi=\neg\psi$ for some $\psi\in
D$.

  * •

If $\phi\in D$, then $\textnormal{Comp}(\phi)$ holds.

  * •

If $\phi\in D$ and $\psi$ is a direct subformula of $\phi$, then $\psi\in D$.

  * •

If $\phi\in D$, then for all $\alpha\in\textnormal{Asn}(\phi)$,
$(\phi,\alpha)\in S$ or $(\neg\phi,\alpha)\in S.$

By the domain of $S$, $\textnormal{dom}(S)$, we mean the maximal set $D$
satisfying the above conditions (the maximality requirement is needed, as
there is a slight ambiguity in how to count negations of formulae which are
not satisfied by any assignment). A satisfaction class is full iff its domain
is the whole set $\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$.

The definition of a satisfaction class presented above involves some technical
requirements which might seem to be slightly too restrictive, so let us
briefly explain our motivations. The definition of a satisfaction class
completely agrees with the usual one in the case of full satisfaction classes.
However, if $S$ is not a full satisfaction class, i.e., if it does not satisfy
compositional conditions for all formulae, it becomes ambiguous whether we
should interpret the fact that $(\phi,\alpha)\notin S$ as saying that $\phi$
is not satisfied under the valuation $\alpha$ or that $S$ simply does not
decide $\phi$ which might be a technical nuisance in some proofs or statements
of results. This includes results and arguments in this article, though the
specific difficulties we overcome with this definition will not be really
visible. Therefore, we essentially require that for every formula $\phi$ we
can unambiguously tell whether it is decided by $S$ or not. This requirement
is harmless: Define a pre-satisfaction class on $M$ as a set $S\subset M^{2}$
such that it satisfies compositional axioms on some set $D$ of formulae closed
under direct subformulae and does not contain any pair $(\phi,\alpha)$ for
$\phi\notin D$. Then for any pre-satisfaction class, we can canonically define
a satisfaction class extending it. Simply take the maximal set $D$ with the
two mentioned properties and extend $S$ with all pairs $(\neg\phi,\alpha)$
such that $\phi\in D$ and $(\phi,\alpha)\notin S.$ One can check that after
such a one-step extension, we obtain a satisfaction class in our sense.

Satisfaction classes and truth predicates satisfying $\textnormal{CT}^{-}$ are
very closely related objects. However, the link between them is not as direct
as one could hope (see (Wcisło, 2021) for a discussion of this connection). We
have to introduce a certain technical condition in order to switch between
them in a completely unproblematic manner.

Let $M\models\textnormal{PA}$,
$\phi,\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$,
$\alpha\in\textnormal{Asn}(\phi),\beta\in\textnormal{Asn}(\psi)$. We say that
the pairs $(\phi,\alpha),(\psi,\beta)$ are extensionally equivalent,
$(\phi,\alpha)\simeq(\psi,\beta)$ if there exists a formula $\eta$ and two
sequences of closed terms
$\bar{s},\bar{t}\in\textnormal{ClTermSeq}_{\mathscr{L}_{\textnormal{PA}}}$ of
the same length such that the sequences of their values are equal and

$\phi[\alpha]=\eta(\bar{s}),\psi[\beta]=\eta(\bar{t}),$

where $\phi[\alpha]$ is a sentence obtained by substituting in $\phi$ the
numeral $\underline{\alpha(v)}$ for each variable $v$. For instance, let
$\phi=\exists x(x+y=SS0)$, $\psi=\exists x(x+u\times v=w+S0)$, and let
$\alpha\in\textnormal{Asn}(\phi),\beta\in\textnormal{Asn}(\psi)$ be such that
$\alpha(y)=2,\beta(u)=2,\beta(v)=\beta(w)=1$. Then
$(\phi,\alpha)\simeq(\psi,\beta)$ as witnessed by the formula

$\eta=\exists x(x+v_{0}=v_{1})$

and the terms $(SS0,SS0),(SS0\times S0,S0+S0)$. Finally, we say that a
satisfaction class $S$ is regular iff for all pairs
$(\phi,\alpha)\simeq(\psi,\beta)$, $(\phi,\alpha)\in S$ iff $(\psi,\beta)\in
S$.

Before describing the relation between the interpretations of the truth
predicate and regular satisfaction classes, let us introduce one more
definition.

######  Definition 23.

  * •

If $M\models\textnormal{PA}$ and $S\subset M^{2}$ is a satisfaction class, we
say that internal induction holds for $\phi\in\textnormal{Form}^{\leq
1}_{\mathscr{L}_{\textnormal{PA}}}(M)$ if for every
$v\in\textnormal{FV}(\varphi)$ and every $\alpha\in\textnormal{Asn}(\phi)$,
the following holds:

$(\phi,\alpha[0/v])\in S\wedge\forall x\Big{(}(\phi,\alpha[x/v])\in
S\rightarrow(\phi,\alpha[x+1/v])\in S\Big{)}\rightarrow\forall x\
(\phi,\alpha[x/v])\in S.$

Above, $\alpha[y/v]$ denotes the assignment $\alpha^{\prime}$ which is
identical to $\alpha$, except for the fact that $\alpha^{\prime}(v)=y$.

  * •

We say that internal induction holds for $S$ if it holds for every
$\phi\in\textnormal{Form}^{\leq 1}_{\mathscr{L}_{\textnormal{PA}}}(M)$.

Notice that the formula $\phi$ need not be in the domain of $S$

The following proposition establishes the link between truth predicates
satisfying $\textnormal{CT}^{-}$ (possibly with INT) and regular satisfaction
classes (possibly with internal induction). It can be proved via a direct
verification.

######  Proposition 24.

  * (a)

Let $(M,T)\models\textnormal{CT}^{-}$ and let $S=\\{(\phi,\alpha)\in M^{2}\
\mid\
\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M),\alpha\in\textnormal{Asn}(\phi),\phi[\alpha]\in
T\\}.$ Then $S$ is a full regular satisfaction class.

  * (b)

Conversely, let $M\models\textnormal{PA}$, let $S\subset M^{2}$ be a full
regular satisfaction class in $M$ and let
$T=\\{\phi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(M)\ \mid\
(\phi,\emptyset)\in S\\}$. Then $(M,T)\models\textnormal{CT}^{-}$.

  * (c)

Let $(M,T)\models\textnormal{CT}^{-}+\textnormal{INT}$ and let $S$ be defined
as in (a). Then $S$ is a full regular satisfaction class and internal
induction holds for $S$.

  * (d)

Conversely, let $S$ be a full regular satisfaction class in $M$ such that
internal induction holds for $S$. Let $T$ be defined as in (b). Then
$(M,T)\models\textnormal{CT}^{-}+\textnormal{INT}$.

Now we are ready to prove Theorem 21.

###### Proof of Theorem 21, general idea..

Let $M\models\textnormal{PA}$. We will find an elementary extension $M\preceq
M^{\prime}$ and a full regular satisfaction class $S$ on $M^{\prime}$ with
internal induction such that for every disjunction
$\phi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(M)$ with
nonstandardly many disjuncts, $(\phi,\emptyset)\in S$. Then by Proposition 24,
there exists $T\subset M^{\prime}$ such that
$(M^{\prime},T)\models\textnormal{CT}^{-}+\textnormal{INT}$ and all
disjunctions with nonstandardly many disjuncts are in $T$.

We will construct $(M^{\prime},S)$ in stages. We will produce a sequence
$(M_{n},S_{n})$ of models such that:

  * •

$M_{0}:=M,S_{0}=\emptyset$.

  * •

The models $M_{i}\models\textnormal{PA}$ form an elementary chain.

  * •

$S_{n+1}\subset M_{n+1}^{2}$ is a regular satisfaction class whose domain
contains $\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M_{n})$.

  * •

For every $n$, $S_{n}\subset S_{n+1}$.

  * •

For every $n$, the model $M_{n}$ expanded with all the predicates
$S_{\phi},\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M_{n})$
defined by $S_{\phi}(x)\equiv S_{n}(\phi,x)$ satisfies the full induction
scheme.

  * •

If $\phi:=\bigvee\phi_{i}$ is a disjunction with nonstandardly many disjuncts
and $\phi$ is in the domain of $S_{n+1}$, then $(\phi,\alpha)\in S_{n+1}$ for
every $\alpha\in\textnormal{Asn}(\phi)$.

Finally, we set $M^{\prime}=\bigcup M_{n}$ and $S=\bigcup S_{n}$. By a
straightforward verification, we check that $S$ is indeed a full regular
satisfaction class and it clearly makes all disjunctions with infinitely many
disjuncts true and satisfies internal induction.

To complete the proof, it is enough to check that a sequence $(M_{n},S_{n})$
as above can be produced. This will be demonstrated in Lemma 26 which takes
care of the induction step for $n>1$ (the existence of $(M_{1},S_{1})$ can be
proved with a very similar, slightly simpler argument). ∎

Some care is needed in order to make sure that the satisfaction classes which
we will construct are indeed regular. Before we state and prove the induction
step lemma, we will introduce one more technical notion. (It appeared in the
same context earlier, e.g. in (Łełyk and Wcisło, 2021).)

######  Definition 25.

Let $\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}$. By a syntactic
template of $\phi$, we mean the smallest formula $\widehat{\phi}$ such that
the following conditions are satisfied:

  1. 1.

There exists a sequence of arithmetical terms $\bar{s}$ (not necessarily
closed) such that $\phi=\widehat{\phi}(\bar{s})$.

  2. 2.

No variable occurs in $\widehat{\phi}$ both free and bound.

  3. 3.

No free variable occurs in $\widehat{\phi}$ more than once.

  4. 4.

No closed term occurs in $\widehat{\phi}$.

  5. 5.

No complex term containing only free variables occurs in $\widehat{\phi}$.

For instance, if $\phi=\exists x(SSx+Sy=(z\times(y+S0))\times x)$, then

$\widehat{\phi}=\exists x(SSx+v_{0}=v_{1}\times x),$

where $v_{0},v_{1}$ are chosen so as to minimise the formula.

We say that $\phi$ and $\psi$ are syntactically similar if they have the same
syntactic template. We denote it with $\phi\sim\psi$. Notice that if
$(\phi,\alpha)\simeq(\psi,\beta)$ for some $\alpha,\beta$, then
$\phi\sim\psi$.

######  Lemma 26.

Let $M\models\textnormal{PA}$, let $S\subset M^{2}$ be a regular satisfaction
class such that:

  * •

The model $(M,S_{\phi})_{\phi\in M}$ satisfies full induction, where
$S_{\phi}(x)\equiv S(\phi,x)$.

  * •

If $\phi$ is a disjunction with nonstandardly many disjuncts in the domain of
$S$, then $(\phi,\alpha)\in S$ for all $\alpha\in\textnormal{Asn}(\phi)$.

Then there exists an elementary extension $M\preceq M^{\prime}$ and a regular
satisfaction class $S^{\prime}\supseteq S$ such that $(M^{\prime},S^{\prime})$
satisfies the above conditions and
$\textnormal{dom}(S^{\prime})\supseteq\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$.

###### Proof.

Let $M,S$ be as in the assumptions of the lemma. Let us consider a theory
$\Theta$ in a language $\mathscr{L}_{\textnormal{PA}}$ extended with an
additional predicate $S^{\prime}$ and a family of auxiliary predicates
$S^{\prime}_{\phi},\phi\in M$ which comprises the following axioms:

  * •

$\textnormal{ElDiag}(M)$, the elementary diagram of $M$.

  * •

$\forall x\ S^{\prime}_{\phi}(x)\equiv S^{\prime}(\phi,x)$ where
$\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$. (The definition
of $S^{\prime}_{\phi}$).

  * •

$\textnormal{Comp}(\phi)$ for $S^{\prime}$, where
$\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$.
(Compositionality Scheme).

  * •

$S^{\prime}(\phi,\alpha)$, where $(\phi,\alpha)\in S$. (Preservation Scheme).

  * •

$\forall\phi,\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}\forall\alpha\in\textnormal{Asn}(\phi),\beta\in\textnormal{Asn}(\psi)\
\Big{(}(\phi,\alpha)\simeq(\psi,\beta)\rightarrow
S^{\prime}(\phi,\alpha)\equiv S^{\prime}(\psi,\beta)\Big{)}.$ (Regularity
Axiom)

  * •

The full induction scheme for formulae in the language
$\mathscr{L}_{\textnormal{PA}}+S^{\prime}_{\phi},\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$.
(Internal Induction).

  * •

$\forall\alpha\in\textnormal{Asn}(\phi)\ S^{\prime}(\phi,\alpha)$, where
$\phi=\bigvee_{i\leq c}\phi_{i}$ for some $(\phi_{i})_{i\leq
c}\in\textnormal{FormSeq}_{\mathscr{L}_{\textnormal{PA}}}(M)$ and a
nonstandard $c$. (Disjunction Scheme).

The predicates $S^{\prime}_{\phi}$ are introduced to concisely express what
form of internal induction we accept. Note that in the Internal induction
scheme, we do not allow formulae containing the predicate $S^{\prime}$.
Crucially, we are not allowed to treat $\phi$ like a variable. On the other
hand, the form of induction we accept is prima facie stronger than the
internal induction condition introduced in Definition 23.

If $(M^{\prime},S^{\prime},S^{\prime}_{\phi})_{\phi\in M}\models\Theta$, then
by restricting $S^{\prime}$ to $(\phi,\alpha)$ such that
$\phi\sim\phi^{\prime}$ for some $\phi^{\prime}\in M$ and ignoring the
predicates $S^{\prime}_{\phi}$, we obtain a model satisfying the conclusion of
the lemma (note that $S^{\prime}$ itself need not be a satisfaction class, as
the compositional conditions may possibly fail badly for formulae in
$M^{\prime}\setminus M$). Therefore, it is enough to check that $\Theta$ is
consistent. We will prove it by compactness. Let $\Theta_{0}\subset\Theta$ be
a finite subtheory. It is enough to check the consistency of $\Theta_{0}$.

Let
$\phi_{1},\ldots,\phi_{n}\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$
be all formulae such that the instances of their compositionality,
preservation, and disjunction schemes are in $\Theta_{0}$. We will define
$S^{\prime}\subset M^{2}$ which satisfies these instances of schemes, as well
as all the other axioms in $\Theta$. Note that $\textnormal{ElDiag}(M)$ will
be automatically satisfied, since the interpretation of the relation
$S^{\prime}$ will be defined in $M$.

Let us consider the classes $[\phi_{i}]_{\sim}$, where $\sim$ is the syntactic
similarity relation (see Definition 25 and the remark below the definition).
Let $\lhd$ be a relation defined on the classes as follows: $[\phi]\lhd[\psi]$
iff there exist $\phi^{\prime}\in[\phi],\psi^{\prime}\in[\psi]$ such that
$\phi^{\prime}$ is a direct subformula of $\psi^{\prime}$. We define a
sequence of relations $S_{0},S_{1},\ldots,S_{k}\subset M^{2}$ by induction on
the rank of classes in the relation $\lhd$. We let $(\phi,\alpha)\in S_{0}$ if
$[\phi]$ is minimal in the relation $\lhd$ and one of the following holds:

  * •

There exist $s,t\in\textnormal{Term}_{\mathscr{L}_{\textnormal{PA}}}(M)$ such
that $\phi=(s=t)$ and $s^{\alpha}=t^{\alpha}$.

  * •

$(\phi,\alpha)\in S$.

  * •

$\phi$ is a disjunction with nonstandardly many disjuncts.

Above, we want to define $S_{0}$ on all classes minimal with respect to the
relation $\lhd$. If $S$ already holds of $\phi$ and $\alpha$, then we preserve
it in $S_{0}$. If $\phi$ happens to be a disjunction with infinitely many
disjuncts, then we make it true under all valuations. Otherwise, we set
$(\phi,\alpha)\notin S_{0}$ for all $\alpha$, but we do not have to mention it
explicitly.

We define $S_{i+1}$ as the union of $S_{i}$ and the pairs $(\phi,\alpha)$ such
that $[\phi]$ has rank $i+1$ and one of the following holds:

  * •

There exists $\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$
such that $\phi=\neg\psi$ and $(\psi,\alpha)\notin S_{i}$.

  * •

There exist $\psi,\eta\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$
such that $\phi=\psi\vee\eta$ and $(\psi,\alpha)\in S_{i}$ or
$(\eta,\alpha)\in S_{i}$.

  * •

There exist $\psi,\eta\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$
such that $\phi=\psi\wedge\eta$ and $(\psi,\alpha)\in S_{i}$ and
$(\eta,\alpha)\in S_{i}$.

  * •

There exists
$\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M),v\in\textnormal{Var}(M)$
such that $\phi=\exists v\psi$ and $(\psi,\beta)\in S_{i}$ for some
$\beta\sim_{v}\alpha$.

  * •

There exists
$\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M),v\in\textnormal{Var}(M)$
such that $\phi=\forall v\psi$ and $(\psi,\beta)\in S_{i}$ for all
$\beta\sim_{v}\alpha$.

In other words, we extend $S_{i}$ to $S_{i+1}$ so as to satisfy the
compositional clauses. Finally, since we consider only finitely many classes,
they can only attain some finite rank $k$. Let $S^{\prime}=S_{k}$. Let
$S^{\prime}_{\phi},\phi\in M$ be defined so that the definition-axiom of
$S^{\prime}_{\phi}$ is satisfied. We claim that
$(M,S^{\prime},S^{\prime}_{\phi})_{\phi\in M}\models\Theta.$

It is obvious that $(M,S^{\prime})$ satisfies $\textnormal{ElDiag}(M)$. It
follows directly by construction that it satisfies the compositional clauses
for the formulae $\phi_{1},\ldots,\phi_{n}$. It satisfies the instances of the
preservation scheme for these formulae: for the formulae of minimal rank it
follows by the definition of $S_{0}$, since if a disjunction with infinitely
many disjuncts is in the domain of $S$, then it is satisfied under all
assignments. For formulae of higher rank, this follows by construction, since
$S$ is compositional on its domain and the compositional clauses uniquely
determine the extension of a satisfaction predicate on a formula, given its
extension on the direct subformulae.

Let us verify that $S^{\prime}$ satisfies the regularity axiom. For formulae
in the $\lhd$-minimal classes, this follows by construction and the assumption
that $S$ is regular. For formulae in the classes of rank $>0$, we can directly
check that compositional clauses preserve regularity and thus show by
induction that all the predicates $S_{i}$ satisfy the regularity axiom.

The model $(M,S^{\prime}_{\phi})_{\phi\in M}$ satisfies the full induction
scheme, since we can verify by an easy induction on $i$ that $S_{i}$ is
arithmetically definable in terms of $S_{\phi_{i}}$, $i\leq n$, such that the
class $[\phi_{i}]$ is $\lhd$-minimal and $\phi_{i}\in\textnormal{dom}S$. By
assumption, $(M,S_{\phi})_{\phi\in M}$ satisfies the full induction scheme and
since $S^{\prime}$ is definable in that structure, it satisfies induction. The
conclusion follows.

The predicate $S^{\prime}$ satisfies the disjunction scheme for formulae
$\phi_{1},\ldots,\phi_{n}$. Indeed, if $\phi$ is a disjunction with a
nonstandard number of disjuncts and $[\phi]$ is minimal in the relation
$\lhd$, then $(\phi,\alpha)\in S^{\prime}$ by construction. Let us check by
induction that the disjunction scheme is satisfied for formulae whose classes
have higher rank. If the rank of $[\phi]$ is $i+1$, then there exist formulae
$\psi,\eta$ such that $\psi$ is a disjunction with a nonstandard number of
disjuncts and $\phi=\psi\vee\eta$, where the rank of $[\psi]$ is $\leq i$. By
induction hypothesis, $(\psi,\alpha)\in S^{\prime}$ for all
$\alpha\in\textnormal{Asn}(\psi)$, hence by the compositional clauses
$(\psi\vee\eta,\beta)\in S^{\prime}$ for all
$\beta\in\textnormal{Asn}(\psi\vee\eta)$. This concludes the proof. ∎

######  Remark 27.

As we have already pointed out, Enayat–Visser methods of building satisfaction
classes typically allow us to combine various conservativeness results. For
instance, in Theorem 21, we could additionally require that the constructed
predicate is correct with respect to blocks of existential or universal
quantifiers.

It might appear that since a class we build in the proof of this theorem is
somewhat pathological, there are certain obvious limits to what truth-
theoretic principles can be additionally satisfied. For instance, if the
constructed truth predicate makes true all infinite disjunctions, then it
cannot agree with $\Sigma_{n}$ arithmetical truth predicates on sentences from
the respective syntactic classes. However, as pointed out by Ali Enayat, we
could still construct a model in which the truth predicate $T$ agrees with all
the usual partial arithmetical $\Sigma_{n}$-truth predicates and DC-in is
satisfied. It is enough that in the proof of Lemma 26 we change the definition
of $S_{0}$ so that for a minimal class $[\phi]$, where $\phi$ is a
$\Sigma_{n}$-formula for some standard $n$ which is not in the domain of $S$,
$S_{0}$ agrees with the partial arithmetical satisfaction predicates. An
alternative approach, mixing an Enayat–Visser approach and resplendence (by
building a satisfaction class from recursively saturated partial classes) was
proposed in an unpublished note by Enayat (2018).

##  5 Alternative versions of DC

In our paper, we defined $\bigvee_{i\leq c}\phi_{i}$ as
$((\ldots(\phi_{0}\vee\phi_{1})\vee\ldots)\vee\phi_{c-1})\vee\phi_{c}$. This
is not the only possible definition of disjunction (and admittedly not the
most natural one) and one could wonder whether modifying that definition has
some impact on the presented results.

This point has been partially addressed in the definition of outer
disjunctions: our proof of nonconservativity of
$\textnormal{CT}^{-}+\textnormal{DC-out}$ used the clause

$TD(\phi_{1},\ldots,\phi_{c},\phi_{c+1})\equiv
TD(\phi_{1},\ldots,\phi_{c})\vee T\phi_{c+1}.$ (*)

It turns out that this assumption cannot be weakened much further. Let us
define balanced disjunctions of a sequence of formulae
$\phi_{1},\ldots,\phi_{c}$, $B(\phi_{1},\ldots,\phi_{c})$ by recursion in the
following way:

$\displaystyle B(\emptyset)$ $\displaystyle:=$ $\displaystyle 0\neq 0$
$\displaystyle B(\phi_{1})$ $\displaystyle:=$ $\displaystyle\phi_{1}$
$\displaystyle B(\phi_{1},\ldots,\phi_{c})$ $\displaystyle:=$ $\displaystyle
B(\phi_{1},\ldots,\phi_{\llcorner c/2\lrcorner})\vee B(\phi_{\llcorner
c/2\lrcorner+1},\ldots,\phi_{c}).$

In other words, we are grouping disjunctions of $\phi_{1},\ldots,\phi_{k}$ so
that the parentheses form a binary tree. Over $\textnormal{CT}^{-}$, balanced
disjunctions do not satisfy the condition * ‣ 5 and in fact, if we add an
analogue of DC-out for that kind of disjunctions, we do not gain any
arithmetical strength.

######  Theorem 28.

$\textnormal{CT}^{-}$ together with the axiom
$\forall\bar{\phi}\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}\Big{(}TB(\bar{\phi})\rightarrow\exists
i\leq\textnormal{lh}(\bar{\phi})\ T\phi_{i}\Big{)}$ is a conservative
extension of PA.

###### Sketch of a proof..

Analogously to the proof of Theorem 20, we fix a model
$M\models\textnormal{PA}$ and we construct an elementary extension
$M^{\prime}\succeq M$ and $T\subset M^{\prime}$ such that any balanced
disjunction of a sequence
$(\phi_{1},\ldots,\phi_{c})\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}(M^{\prime})$
of nonstandard length is false.

It is enough to observe that if $\phi$ is a balanced disjunction of
nonstandardly many sentences, then there exist $\phi_{1},\phi_{2}$ such that
$\phi=\phi_{1}\vee\phi_{2}$ and $\phi_{i}$ are themselves such balanced
disjunctions, so we can maintain the requirement that all sentences of this
form are false throughout the whole construction. ∎

Notice that in the model produced in the proof of Theorem 20, all balanced
disjunctions with nonstandardly many disjuncts are in fact true. This shows
that both the analogues of DC-in and DC-out for the balanced formulae are
conservative over PA and that in general DC-out is sensitive to the specific
kind of forming disjunctions for which they are formulated. This leads to a
natural question whether some natural forms of disjunction, say, balanced
disjunctions, can satisfy full DC while remaining conservative. It turns out
that DC behaves stably under such varying implementations.

######  Theorem 29.

Suppose that $U$ is a theory extending $\textnormal{CT}^{-}$. Suppose that
there exists a provably functional formula $D(x)$ such that provably in $U$
for any
$\bar{\phi}=(\phi_{1},\ldots,\phi_{c})\in\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}$,
$D(\bar{\phi})$ is in $\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}$ and
the following holds:

$TD(\bar{\phi})\equiv\exists i\leq c\ T\phi_{i}.$

Then $U$ extends $\textnormal{CT}_{0}$.

###### Proof.

Under the assumptions of the theorem, $D$ is an outer disjunction provably in
$U$. The conclusion follows by Proposition 13. ∎

######  Remark 30.

As we have noted above, the results on DC-out are sensitive to how we exactly
define disjunctions over finite sets of sentences. One way to express
abstractly what properties of disjunctions are used is the notion of outer
disjunction. Ali Enayat has proposed a further generalisation of this concept.

Let $U$ be a theory extending $\textnormal{CT}^{-}$. We say that a provably
functional formula $D$ is a selective disjunction if there exists a formula
$F$ which provably in $U$ defines a choice function for finite sets and the
following conditions hold provably in $U$:

  * •

For any $\Phi\in\textnormal{SentSet}_{\mathscr{L}_{\textnormal{PA}}}$,
$D(\Phi)\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}$.

  * •

$TD(\Phi)\equiv TF(\Phi)\vee TD(\Phi\setminus\\{F(\phi)\\}).$

One can check that if a theory $U$ has selective disjunctions satisfying the
analogue of DC-out, namely:

$TD(\Phi)\rightarrow\exists\phi\in\Phi\ T\phi,$

then $U$ is again equivalent to $\textnormal{CT}_{0}$.

##  6 The role of the regularity axiom

In Section 2, we briefly mentioned that we have certain technical reasons to
include Regularity, REG among the axioms for the compositional truth. Let us
now explain why we adopt this principle and how this choice affects our
results.

First of all, without REG, we have to be careful about the exact formulation
of the compositional axioms for quantifiers. Our basic choice is between two
options. We can require that, say, an existential statement $\exists v\phi(v)$
is true iff some sentence obtained by substituting a numeral in $\phi(v)$ is
true. This amounts to adopting quantifier axioms in the form which we have
chosen in this article:

$T\exists v\phi(v)\equiv\exists x\ T\phi(\underline{x}).$

The second option is to require that an existential statement is true iff a
sentence obtained by substituting some closed arithmetical term for the
quantified variable is true. Then, the quantifier axioms would have a form:

$T\exists v\phi(v)\equiv\exists
t\in\textnormal{ClTerm}_{\mathscr{L}_{\textnormal{PA}}}\ T\phi(t).$

Note that these two versions of the quantifier axiom are not immediately
comparable with respect to their strength. The left-to-right implication is
stronger in the numeral version:

$T\exists v\phi(v)\rightarrow\exists xT\phi(\underline{x})$

whereas the reverse implication is formally stronger for the term version:

$\exists t\in\textnormal{ClTerm}_{\mathscr{L}_{\textnormal{PA}}}\
T\phi(t)\rightarrow T\exists v\phi(v).$

The term version was chosen, for instance, by Halbach (2011). The numeral
version appears, e.g., in (Friedman and Sheard, 1987) or (Horsten and Leigh,
2017). This choice, in turn, may have a significant bearing on our results.
Most importantly, we do not know whether adding $\Delta_{0}$-induction to a
version of $\textnormal{CT}^{-}$ whose compositional axioms for quantifiers
involve terms results in a non-conservative extension of PA. So, when
regularity is missing, some of the main results in this article will depend on
a technical choice in the formulation of compositional axioms which may lead
to some further confusions.

Another issue is that without regularity, there is a mismatch between the
notion of a truth predicate as discussed in the philosophical literature and
the notion of satisfaction classes, as discussed in the literature on models
of PA (e.g., as in (Kaye, 1991)). There is a direct link between the
compositional truth and satisfaction classes assuming that we include some
form of extensionality conditions in both these cases. (A more comprehensive
discussion of why these kind of assumptions are relevant can be found in
(Wcisło, 2021).) This link is important, as some techniques used in our proofs
are designed to work specifically in the context of satisfaction classes. Most
importantly, the conservativity arguments using the Enayat–Visser technique
which we employ in Section 4 do not really work when directly applied to truth
classes. Therefore, we would most likely need to add regularity assumptions to
statements of some technical lemmas which could make for a potentially awkward
reading.

Finally, let us discuss the impact of REG on the results in this article. The
main results in Section 4, namely Theorems 20 and 21 are also true for
$\textnormal{CT}^{-}$ without the regularity axiom, as the latter versions are
formally weaker. The same applies to Remark 27, Proposition 14, and Theorem
28.

The situation of the results in Section 3 is slightly more complicated. As we
have already mentioned, Theorem 6 is only known to hold if we consider a
version of $\textnormal{CT}^{-}$ in which the numeral variant of the
compositional quantifier axioms is assumed. In this case, all results from
Section 3, still hold. Unfortunately, this is not necessarily true for the
term variant. Let us discuss in some detail what can be salvaged in this
scenario.

Theorem 8 does not depend at all on quantifier axioms and thus it holds
without assuming regularity in either version of $\textnormal{CT}^{-}$;
similarly for Theorem 9. The first part of Theorem 10 and Theorem 17 also hold
true. It is clear that SOInd implies PropRef for $\textnormal{CT}^{-}$ in the
term version as well. Moreover, PropRef clearly implies DC using just
compositional axioms for boolean connectives. However, it is unclear whether
PropRef and $\textnormal{CT}_{0}$ are equivalent without assuming REG and with
the quantifier axioms in the term version. Similarly, the first part of
Proposition 13 does not depend of regularity or the quantifier axioms, but we
do not know whether such theories contain $\textnormal{CT}_{0}$. Proposition
15 may be entirely false if we do not assume the numeral version of the
quantifier axioms, as the proof relies significantly on that assumption.

To sum it up: by the results of Section 3, $\textnormal{DC-
out},\textnormal{DC},\textnormal{SInd}$, SOInd, and PropRef are pairwise
equivalent over any version of $\textnormal{CT}^{-}$ without assuming
regularity. They are equivalent to $\textnormal{CT}_{0}$ and not conservative
over PA if we consider $\textnormal{CT}^{-}$ with quantifier axioms for
numerals. If we consider $\textnormal{CT}^{-}$ with the term variant of the
quantifier axioms, we do not know either whether DC or PropRef are equivalent
to $\textnormal{CT}_{0}$, or whether the latter theory is arithmetically
stronger than PA.

## Appendix: a glossary of formalised notions

Throughout the article, we referred to a number of formalised notions and used
some rather technical notation. Let us now gather it in a glossary for the
convenience of the reader.

  * •

$\alpha\sim_{v}\beta$ means that
$\textnormal{dom}(\beta)\supseteq\textnormal{dom}(\alpha)\cup\\{v\\}$ and
$\beta(w)=\alpha(w)$ for every $w\in\textnormal{dom}(\alpha)\setminus\\{v\\}$.

  * •

${t}^{\circ}$. If $t$ is (a Gödel code of) a closed arithmetical term, then
${t}^{\circ}$ is the value of a term (whose Gödel code is) $t$. We use the
same expression to denote the formalised version of this function.

  * •

$t^{\alpha}$. If $t$ is (a Gödel code of) an arithmetical term, and $\alpha$
is a $t$-assignment, then $t^{\alpha}$ is the value of term $t$ under the
assignment $\alpha$. We use the same expression to denote the formalised
version of this function.

  * •

${\bar{t}}^{\circ}$. If $\bar{t}$ is a sequence of (Gödel codes of) closed
arithmetical terms, then ${\bar{t}}^{\circ}$ is the sequence of their values.
We also use this expression to denote the formalised version of this function.

  * •

$\underline{x}$ is (a Gödel code of) a canonical numeral denoting the number
$x$. We also use this expression to denote the formalised version of this
function.

  * •

$\phi[\alpha]$. If $\phi$ is a formula and $\alpha\in\textnormal{Asn}(\phi)$,
then by $\phi[\alpha]$ we mean a sentence obtained by substituting in $\phi$
the numeral $\underline{\alpha(v)}$ for each variable $v$. We also use this
expression to denote the corresponding formalised notion.

  * •

$\textnormal{Asn}(x)$ is a set of $x$-assignments, that is, functions whose
domain contains the set of free variables of $x$, where $x$ is a term, a
formula, or a sequence thereof. We also use this expression to denote the
corresponding formalised notion.

  * •

$\textnormal{ClTerm}_{\mathscr{L}_{\textnormal{PA}}}(x)$ is a formula
expressing “$x$ is (a Gödel code of) a closed arithmetical term.” (That is, a
term with no free variables.)

  * •

$\textnormal{ClTermSeq}_{\mathscr{L}_{\textnormal{PA}}}(x)$ is a formula
expressing “$x$ is a sequence of (Gödel codes of) closed arithmetical terms.”

  * •

$\textnormal{FinSeq}(x)$ is a formula expressing “$x$ is a finite sequence of
numbers.”

  * •

$\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(x)$ is a formula expressing
“$x$ is (a Gödel code of) an arithmetical formula.”

  * •

$\textnormal{Form}^{\leq 1}_{\mathscr{L}_{\textnormal{PA}}}$ is a formula
expressing “$x$ is (a Gödel code of) an arithmetical formula with at most one
free variable.”

  * •

$\textnormal{FormSeq}_{\mathscr{L}_{\textnormal{PA}}}(x)$ is a formula
expressing “$x$ is a sequence of (Gödel codes of) arithmetical formulae.”

  * •

$\textnormal{lh}(s)=x$ is a formula expressing “$s$ is a sequence and its
length is $x$.”

  * •

$\textnormal{Pr}_{\textnormal{PA}}(x)$ is a formula expressing “$x$ is (a
Gödel code of) an arithmetical sentence provable in PA.”

  * •

$\textnormal{Pr}_{\textnormal{Prop}}(x)$ is a formula expressing “$x$ is (a
Gödel code of) an arithmetical sentence which is provable in pure
propositional logic.”

  * •

$\textnormal{Pr}^{T}_{\textnormal{Prop}}(x)$ is a formula expressing “$x$ is
(a Gödel code of) an arithmetical sentence which is provable in propositional
logic from the set of premises $\Gamma$ such that $T(y)$ holds for all
$y\in\Gamma$.”

  * •

$\textnormal{qfSent}_{\mathscr{L}_{\textnormal{PA}}}(x)$ is a formula
expressing “$x$ is (a Gödel code of) a quantifier-free arithmetical sentence.”

  * •

$\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(x)$ is a formula expressing
“$x$ is (a Gödel code of) an arithmetical sentence.”

  * •

$\textnormal{SentSeq}_{\mathscr{L}_{\textnormal{PA}}}(x)$ is a formula
expressing “$x$ is a sequence of (Gödel codes of) arithmetical sentences.”

  * •

$\textnormal{SentSet}_{\mathscr{L}_{\textnormal{PA}}}(x)$ is a formula
expressing “$x$ is a finite set of (Gödel codes of) arithmetical sentences.”

  * •

$\textnormal{Term}_{\mathscr{L}_{\textnormal{PA}}}(x)$ is a formula expressing
“$x$ is (a Gödel code of) an arithmetical term.”

  * •

$\textnormal{Tr}_{0}$ is the arithmetical truth predicate for
$\Delta_{0}$-formulae.

  * •

$\textnormal{Var}(x)$ is a formula expressing “$x$ is (a Gödel code of) a
first-order variable.”

## Acknowledgements

We are very grateful to Ali Enayat for a number of helpful comments and
suggestions which allowed us to improve this article.

This research was supported by an NCN MAESTRO grant 2019/34/A/HS1/00399
“Epistemic and Semantic Commitments of Foundational Theories.”

## References

  * Cieśliński (2010) Cezary Cieśliński.  Truth, conservativeness and provability.  _Mind_ , 119:409–422, 2010.
  * Cieśliński (2017) Cezary Cieśliński.  _The Epistemic Lightness of Truth. Deflationism and its Logic_.  Cambridge University Press, 2017.
  * Enayat (2014) Ali Enayat.  Fine-tuning Kotlarski, 2014.  An unpublished note.
  * Enayat (2018) Ali Enayat.  On $\textnormal{DC}_{\textnormal{intro}}$, 2018.  An upublished note.
  * Enayat and Pakhomov (2019) Ali Enayat and Fedor Pakhomov.  Truth, disjunction, and induction.  _The Archive for Mathematical Logic_ , 58:753–766, 2019\.
  * Enayat and Visser (2015) Ali Enayat and Albert Visser.  New constructions of satisfaction classes.  In Theodora Achourioti, Henri Galinon, José Martínez Fernández, and Kentaro Fujimoto, editors, _Unifying the Philosophy of Truth_ , pages 321–325. Springer-Verlag, 2015.
  * Enayat et al. (2020) Ali Enayat, Mateusz Łełyk, and Bartosz Wcisło.  Truth and feasible reducibility.  _The Journal of Symbolic Logic_ , 85:367–421, 2020.
  * Engström (2002) Fredrik Engström.  _Satisfaction Classes in Nonstandard Models of First-order Arithmetic_.  Licentiate thesis, Chalmers University of Technology and Göteborg University, 2002.
  * Friedman and Sheard (1987) Harvey Friedman and Michael Sheard.  An axiomatic approach to self-referential truth.  _Annals of Pure and Applied Logic_ , 33:1–21, 1987.
  * Hájek and Pudlák (1993) Petr Hájek and Pavel Pudlák.  _Metamathematics of First-Order Arithmetic_.  Springer-Verlag, 1993.
  * Halbach (2011) Volker Halbach.  _Axiomatic Theories of Truth_.  Cambridge University Press, 2011.
  * Horsten and Leigh (2017) Leon Horsten and Graham Leigh.  Truth is simple.  _Mind_ , 126:195–232, 2017.
  * Kaye (1991) Richard Kaye.  _Models of Peano Arithmetic_.  Oxford: Clarendon Press, 1991.
  * Kotlarski et al. (1981) Henryk Kotlarski, Stanisaw Krajewski, and Alistair Lachlan.  Construction of satisfaction classes for nonstandard models.  _Canadian Mathematical Bulletin_ , 24:283–93, 1981.
  * Leigh (2015) Graham Leigh.  Conservativity for theories of compositional truth via cut elimination.  _The Journal of Symbolic Logic_ , 80(3):845–865, 2015.
  * Łełyk (2017) Mateusz Łełyk.  _Axiomatic Theories of Truth, Bounded Induction and Reflection Principles_.  PhD thesis, University of Warsaw, 2017.
  * Łełyk (2019) Mateusz Łełyk.  Comparing axiomatic theories of truth.  _Studia Semiotyczne_ , 33(2):255–286, 2019.
  * Łełyk (2021) Mateusz Łełyk.  Model theory and proof theory of the Global Reflection principle, 2021\.  An unpublished work. Preprint Available at sites.google.com/uw.edu.pl/lelyk/research.
  * Łełyk and Wcisło (2016) Mateusz Łełyk and Bartosz Wcisło.  Strong and weak truth principles.  _Studia Semiotyczne_ , 30(2):107–126, 2016.
  * Łełyk and Wcisło (2017) Mateusz Łełyk and Bartosz Wcisło.  Notes on bounded induction for the compositional truth predicate.  _The Review of Symbolic Logic_ , 10:455–480, 2017.
  * Łełyk and Wcisło (2021) Mateusz Łełyk and Bartosz Wcisło.  Local collection and end-extenstions of models of compositional truth.  _Annals of Pure and Applied Logic_ , 172, 2021.
  * Wcisło (2020) Bartosz Wcisło.  Compositional truth with propositional tautologies and quantifier-free correctness, 2020.  An unpublished work. Preprint Available at arxiv.org/abs/2011.06940.
  * Wcisło (2021) Bartosz Wcisło.  Satisfaction classes, definability, and automorphisms, 2021.  An unpublished work. Preprint Availabe at arxiv.org/abs/2104.09969.
  * Yablo (1993) Stephen Yablo.  Paradox without self-reference.  _Analysis_ , 53:251–252, 1993.