# Curious satisfaction classes

Ali Enayat  Department of Philosophy, Linguistics, and Theory of Science,
University of Gothenburg; email<EMAIL_ADDRESS>
###### Abstract.

We present two new constructions of satisfaction/truth classes over models of
$\mathsf{PA}$ (Peano Arithmetic) that provide a foil to the fact that the
existence of a disjunctively correct full truth class over a model
$\mathcal{M}$ of $\mathsf{PA}$ implies that $\mathcal{M}$ satisfies
$\mathsf{Con}(\mathsf{PA})$.

In the first construction, given an arbitrary countable recursively saturated
model $\mathcal{M}$ of the relational version of $\mathsf{PA}$, we build an
extensional satisfaction class $S$ over the family
$\mathsf{Form}_{\mathcal{M}}^{<\omega}$ of all arithmetical formulae coded in
$\mathcal{M}$ that have at most finitely-many free variables (from an external
point of view) with the property that the truth class naturally associated
with $S$ (using domain constants) is disjunctively correct for disjunctions in
$\mathsf{Form}_{\mathcal{M}}^{<\omega}$ (and $S$ has other ‘good’ properties).
This construction lends itself to a generalization in which
$\mathsf{Form}_{\mathcal{M}}^{<\omega}$ is replaced with
$\mathsf{Form}_{\mathcal{M}}^{<I}$, where $I$ is an arbitrarily large cut $I$
of $\mathcal{M}$ such that $I\prec\mathcal{M}$ and $I\cong\mathcal{M}$.

In the second construction, given an arbitrary countable recursively saturated
model $\mathcal{M}$ of the usual presentation of $\mathsf{PA}$ (with function
symbols for addition and multiplication, and constant symbols for 0 and 1), we
show that there are arbitrarily large cuts $I$ of $\mathcal{M}$ with the
property that $I\prec\mathcal{M}$, $I\cong\mathcal{M}$, and $\mathcal{M}$
carries a full truth class $T$ that is disjunctively correct for disjunctions
whose code is in $I$, and $T$ is also closed under first order proofs whose
code is in $I.$

The research presented in this paper was supported by the National Science
Centre, Poland (NCN), grant number 2019/34/A/HS1/00399.

1\. INTRODUCTION

By a theorem of Krajewski, Kotlarski, and Lachlan [KKL], every countable
recursively saturated model $\mathcal{M}$ of $\mathsf{PA}$ (Peano Arithmetic)
carries a ‘full satisfaction class’, i.e., there is a subset $S$ of the
universe $M$ of $\mathcal{M}$ that ‘decides’ the truth/falsity of each
sentence of arithmetic in the sense of $\mathcal{M}$ – even sentences of
nonstandard length – while obeying the usual recursive clauses guiding the
behavior of a Tarskian satisfaction predicate. This remarkable theorem implies
that theory $\mathsf{CT}^{-}\mathsf{[PA]}$ (compositional truth over
$\mathsf{PA}$ with induction only for the language $\mathcal{L}_{\mathsf{PA}}$
of arithmetic) is conservative over $\mathsf{PA}$, i.e., if an
$\mathcal{L}_{\mathsf{PA}}$-sentence $\varphi$ is provable in
$\mathsf{CT}^{-}\mathsf{[PA]}$, then $\varphi$ is already provable in
$\mathsf{PA}$. New proofs of this conservativity result were given by Visser
and Enayat [EV-2] using basic model theoretic ideas, and by Leigh [Lei] using
proof theoretic tools; these new proofs make it clear that in the Krajewski-
Kotlarski-Lachlan theorem the theory $\mathsf{PA}$ can be replaced by any
‘base’ theory that supports a modicum of coding machinery for handling
elementary syntax.

On the other hand, it is well-known that the consistency of $\mathsf{PA}$ (and
much more) is readily provable in the stronger theory $\mathsf{CT[PA]}$, which
is the result of strengthening $\mathsf{CT}^{-}\mathsf{[PA]}$ with the scheme
of induction over natural numbers for all
$\mathcal{L}_{\mathsf{PA+T}}$-formulae, where
$\mathcal{L}_{\mathsf{PA+T}}:=\mathcal{L}_{\mathsf{PA}}\cup\\{\mathsf{T}(x)\\}.$
Indeed, it is straightforward to demonstrate the consistency of $\mathsf{PA}$
within the subsystem $\mathsf{CT}_{1}\mathsf{[PA]}$ of $\mathsf{CT[PA]}$,
where $\mathsf{CT}_{n}\mathsf{[PA]}$ is the subtheory of $\mathsf{CT[PA]}$
with the scheme of induction over natural numbers limited to
$\mathcal{L}_{\mathsf{PA+T}}$-formulae that are at most of complexity
$\Sigma_{n}$ [WL, Thm. 2.8].

The case of $\mathsf{CT}_{0}\mathsf{[PA]}$ has taken a great deal of effort to
analyze. Kotlarski [Ko] established that $\mathsf{CT}_{0}\mathsf{[PA]}$ is a
subtheory of $\mathsf{CT}^{-}\mathsf{[PA]+Ref(PA)}$, where $\mathsf{Ref(PA)}$
is the $\mathcal{L}_{\mathsf{PA+T}}$-sentence stating that “every first order
consequence of $\mathsf{PA}$ is true”. Łełyk [Lel] demonstrated that the
converse also holds, which immediately implies that
$\mathsf{CT}_{0}\mathsf{[PA]}$ is not conservative over $\mathsf{PA}$ since
$\mathsf{Con(PA)}$ is readily provable in
$\mathsf{CT}^{-}\mathsf{[PA]+Ref(PA).}$111This result was first claimed by
Kotlarski [Ko], but his proof outline of $\mathsf{Ref(PA)}$ within
$\mathsf{CT}_{0}\mathsf{[PA]}$ was found to contain a serious gap in 2011 by
Heck and Visser; this gap cast doubt over the veracity of Kotlarski’s claim
until the issue was resolved by Łełyk in his doctoral dissertation [Lel].
Łełyk’s work was preceded by the discovery of an elegant proof of the
nonconservativity of $\mathsf{CT}_{0}\mathsf{[PA]}$ over $\mathsf{PA}$ by
Wcisło and Łełyk [WL]. Kotlarski’s aforementioned theorem was refined by
Cieśliński [C-1] who proved that $\mathsf{CT}^{-}\mathsf{[PA]+}$ “$\mathsf{T}$
is closed under propositional proofs” and
$\mathsf{CT}^{-}\mathsf{[PA]+Ref(PA)}$ axiomatize the same theory. Later
Enayat and Pakhomov [EP] refined Cieśliński’s result by demonstrating that
$\mathsf{CT}^{-}\mathsf{[I\Delta}_{0}+\mathsf{Exp]+DC}$ and
$\mathsf{CT}_{0}\mathsf{[PA]}$ axiomatize the same first order theory, a
result which was in turn refined by Cieśliński, Łełyk, and Wcisło [CLW], who
showed $\mathsf{CT}^{-}\mathsf{[I\Delta}_{0}+\mathsf{Exp]+DC}_{\mathrm{out}}$
is an axiomatization of $\mathsf{CT}_{0}\mathsf{[PA]}$, where
$\mathsf{DC}_{\mathrm{out}}$ is the ‘half’ of $\mathsf{DC}$ that says every
true disjunction has a true disjunct (the proof in [CLW] uses the version of
$\mathsf{CT}^{-}$ that includes the so-called regularity axiom; it is not
clear if the main result of [CLW] holds without the inclusion of the
regularity axiom. In contrast, the formulation in [EP] of $\mathsf{CT}^{-}$
does not include the regularity axiom).

In this paper we present two new constructions of satisfaction classes over
models of $\mathsf{PA}$ (Peano Arithmetic) that provide a foil to the
aforementioned nonconservativity results concerning disjunctive correctness,
as described below.

In the first construction (presented as Theorem 4.1), given an arbitrary
countable recursively saturated model $\mathcal{M}$ of the relational version
of $\mathsf{PA}$, we build an extensional satisfaction class $S$ over the
family $\mathsf{Form}_{\mathcal{M}}^{<\omega}$ of all arithmetical formulae
coded in $\mathcal{M}$ that have at most finitely-many free variables (from an
external point of view) with the property that $S$ is disjunctively correct
for disjunctions in $\mathsf{Form}_{\mathcal{M}}^{<\omega}$ ($S$ also has
other ‘good’ properties). In Theorem 4.3 we give a more general version of
Theorem 4.1, and in Theorem 4.4 we combine this construction with another
construction due to Fedor Pakhomov [P] to show that there are arbitrarily
large cuts $I$ in $\mathcal{M}$ such that there is full satisfaction class $S$
on $\mathcal{M}$ that is disjunctively correct for disjunctions whose code is
in $I$.

In the second construction (presented as Theorem 5.1), given an arbitrary
countable recursively saturated model $\mathcal{M}$ of the usual presentation
of $\mathsf{PA}$ (with function symbols for addition and multiplication, and
constant symbols for 0 and 1), we show that there are arbitrarily large cuts
$I$ in $\mathcal{M}$ such that there is a full truth class $T$ on
$\mathcal{M}$ that is disjunctively correct for disjunctions coded in $I$ (and
also $T$ is closed under first order proofs whose code is in $I).$ This is the
analogue of Theorem 4.4 for the usual presentation of $\mathsf{PA}$.

The main idea of the construction in Section 4 was discovered by the author in
2009 (two years later, I found out that a similar construction was proposed by
Smoryński in unpublished work; see Section 6 for more detail). The protoforms
of the results in Sections 3 and 5 appeared in a privately circulated
manuscript [EV-1] written in collaboration with Albert Visser, and appear here
with his kind permission.

2\. PRELIMINARIES

2.1. Definition. In this paper we will use two versions of Peano arithmetic,
namely $\mathsf{PA}_{\text{{Rel}}}$ and $\mathsf{PA}_{\text{{Func}}}$; the
former is employed in the first construction, and the latter in the second
one. $\mathsf{PA}_{\text{{Rel}}}$ refers to Peano arithmetic formulated in a
relational language $\mathcal{L}_{\mathsf{PA}}$ using the logical constants
$\left\\{\lnot,\vee,\exists,=\right\\}$. Note that in this formulation
$\mathsf{PA}$ has no constant symbols; the arithmetical operations of addition
and multiplication are construed as ternary relations; and conjunction,
universal quantification, and other logical constants are taken as defined
notions in the usual way. $\mathsf{PA}_{\text{{Func}}}$ is the usual
formulation of Peano arithmetic in a language that has function symbols for
addition and multiplication, constant symbols for 0 and 1, and the logical
constants $\left\\{\lnot,\vee,\exists,=\right\\}.$ Of course
$\mathsf{PA}_{\text{{Rel}}}$ and $\mathsf{PA}_{\text{{Func}}}$ are
definitionally equivalent, but the difference between them is manifested in
the way in which a compositional truth theory is built upon them (see
Definitions 2.2 and 2.4 below).

It is well known that Peano Arithmetic has more than sufficient expressive
machinery to handle syntactic notions. The following list of
$\mathcal{L}_{\mathsf{PA}}$-formulae will be useful here. Each of the formulae
defined in the following bullet items has two versions, depending on whether
one is using $\mathsf{PA}_{\text{{Rel}}}$ or $\mathsf{PA}_{\text{{Func}}}$ (in
the paper the context will make it clear which one is intended, hence in the
interest of keeping notation to a minimum we will not subscript them with Rel
and Func).

  * •

$\mathsf{Form}(x)$ is the formula expressing “$x$ is the code of an
$\mathcal{L}_{\mathsf{PA}}$-formula using variables
$\\{v_{i}:i\in\mathbb{N}\\},$ and the non-logical symbols available in
$\mathcal{L}_{\mathsf{PA}}$”.

  * •

$\mathsf{Sent}(x)$ is the conjunction of $\mathsf{Form}(x)$ and the sentence
expressing “$x$ has no free variables”.

  * •

$\mathsf{Asn}(x)$ is the formula expressing “$x$ is the code of an
assignment”, where an assignment here simply refers to a function whose domain
consists of a (finite) set of variables. We use $\alpha$ and its variants
($\alpha^{\prime}$, $\alpha_{0}$, etc.) to range over assignments.

  * •

$y\in\mathsf{FV}(x)$ is the formula expressing “$\mathsf{Form}(x)$ and $y$ is
a free variable of $x$”.

  * •

$y\in\mathsf{Dom}(\alpha)$ is the formula expressing “the domain of $\alpha$
includes $y$”.

  * •

$\mathsf{Asn}(\alpha,x)$ is the following formula expressing “$\alpha$ is an
assignment for $x$”:

$\left(\mathsf{Form}(x)\wedge\mathsf{Asn}(\alpha)\wedge\forall
y(y\in\mathsf{Dom}(\alpha)\leftrightarrow y\in\mathsf{FV}(x)\right).$

The theory $\mathsf{CS}^{-}[\mathsf{PA}_{\text{{Rel}}}]$ defined below is
formulated in an expansion of the language $\mathcal{L}_{\mathsf{PA}}$ by
adding a new binary predicate $\mathsf{S}(x,y)$. The binary/unary distinction
is of course not an essential one since $\mathsf{PA}$ has access to a
definable pairing function. However, the binary/unary distinction at the
conceptual level marks the key difference between satisfaction classes and
truth classes.

When reading the definition below it is helpful to bear in mind that
$\mathsf{Tarski}(\mathsf{S,F})$ expresses:

> F is a subset of Form that is closed under immediate subformulae; each
> member of $\mathsf{S}$ is an ordered pair of the form $(x,\alpha)$, where
> $x\in\mathsf{F}$ and $\alpha$ is an assignment for $x;$ and $\mathsf{S}$
> satisfies Tarski’s compositional clauses.

2.2. Definition. $\mathsf{CS}^{-}[\mathsf{PA}_{\text{{Rel}}}]:=$
$\mathsf{PA}_{\text{{Rel}}}\cup\mathsf{Tarski}\left(\mathsf{S},\mathsf{Form}\right)$,
where $\mathsf{Tarski}(\mathsf{S,F})$ is the conjunction of the universal
generalizations of the formulae $\mathsf{tarski}_{0}(\mathsf{S},\mathsf{F})$
through $\mathsf{tarski}_{4}(\mathsf{S},\mathsf{F})$ described below, all of
which are formulated in
$\mathcal{L}_{\mathsf{PA}}\cup\\{\mathsf{F}(\cdot),\mathsf{S}(\cdot,\cdot)\\}$,
where $\mathsf{S}$ and $\mathsf{F}$ are fresh predicates added to
$\mathcal{L}_{\mathsf{PA}}$.

> In the following formulae $R$ ranges over the relations in
> $\mathcal{L}_{\mathsf{PA}}$; $t,t_{0},t_{1},\cdot\cdot\cdot$ are
> metavariables, e.g., we write $R\left(t_{0},\cdot\cdot\cdot,t_{n-1}\right)$
> instead of $R\left(v_{i_{0}},\cdot\cdot\cdot,v_{i_{n-1}}\right);$
> $\vartriangleleft$ is the direct subformula relation, and
> $\alpha^{\prime}\supseteq\alpha$ abbreviates

$\left(\mathsf{Dom}(\alpha^{\prime})\supseteq\mathsf{Dom}(\alpha)\right)\wedge\forall
t\in\mathsf{Dom}(\alpha)$ $\alpha(t)=\alpha^{\prime}(t).$

  * •

tarski${}_{0}(\mathsf{S},\mathsf{F}):=\left(\mathsf{F}(x)\rightarrow\mathsf{Form}(x)\right)\wedge\left(\mathsf{S}(x,\alpha)\rightarrow\left(\mathsf{F}(x)\wedge\mathsf{Asn}(\alpha,x)\right)\right)\wedge$

$\left(y\vartriangleleft
x\wedge\mathsf{F}(x)\rightarrow\mathsf{F}(y)\right).\vskip 6.0pt plus 2.0pt
minus 2.0pt$

  * •

tarski${}_{1,R}(\mathsf{S,F}):=$

$\left(\mathsf{F}(x)\wedge\left(x=\ulcorner
R\left(t_{0},\cdot\cdot\cdot,t_{n-1}\right)\urcorner\right)\wedge\mathsf{Asn}(\alpha,x)\wedge\bigwedge\limits_{i<n}\alpha(t_{i})=a_{i}\right)\rightarrow$

$\left(\mathsf{S}(x,\alpha)\leftrightarrow
R\left(a_{0},\cdot\cdot\cdot,a_{n-1}\right)\right).$

  * •

tarski${}_{2}(\mathsf{S},\mathsf{F}):=\left(\mathsf{F}(x)\wedge(x=\lnot
y)\wedge\mathsf{Asn}(\alpha,x)\right)\rightarrow$

$\left(\mathsf{S}(x,\alpha)\leftrightarrow\lnot\mathsf{S}(y,\alpha)\right).$

  * •

tarski${}_{3}(\mathsf{S},\mathsf{F}):=\left(\mathsf{F}(x)\wedge\left(x=y_{1}\vee
y_{2}\right)\wedge\mathsf{Asn}(\alpha,x)\right)\rightarrow$

$\left(\mathsf{S}(x,\alpha)\leftrightarrow\left(\mathsf{S}\left(y_{1},\alpha\upharpoonright\mathsf{FV}(y_{1})\right)\vee\mathsf{S}\left(y_{2},\alpha\upharpoonright\mathsf{FV}(y_{2})\right)\right)\right).$

  * •

tarski${}_{4}(\mathsf{S},\mathsf{F}):=\left(\mathsf{F}(x)\wedge(x=\exists t\
y)\wedge\mathsf{Asn}(\alpha,x)\right)\rightarrow$

$\left(\mathsf{S}(x,\alpha)\leftrightarrow\exists\alpha^{\prime}\supseteq\alpha\
\mathsf{S}(y,\alpha^{\prime})\right).\vskip 6.0pt plus 2.0pt minus 2.0pt$

2.3. Definition. Suppose $\mathcal{M}\models\mathcal{L}_{\mathsf{PA}}$,
$F\subseteq M$, and $S$ is a binary relation on $M$.222Throughout the paper we
use the convention of using $M$, $M_{0},$ $N$, etc. to denote the universes of
discourse of structures $\mathcal{M}$, $\mathcal{M}_{0},$ $\mathcal{N},$ etc.

(a) $S$ is an $F$-satisfaction class if
$(\mathcal{M},S,F)\models\mathsf{Tarski}(\mathsf{S,F})$.333Note that the
closure of $F$ under direct subformulae does not guarantee that $F$ should
also contain ‘infinitely deep’ subformulae of a nonstandard formula in $F.$

(b) $S$ is a full satisfaction class on $\mathcal{M}$ if $S$ is an
$F$-satisfaction class for $F:=\mathsf{Form}_{\mathcal{M}}.$ This is
equivalent to
$(\mathcal{M},S)\models\mathsf{CS}^{-}[\mathsf{PA}_{\text{{Rel}}}].$

2.4. Definition. $\mathsf{CT}^{-}[\mathsf{PA}_{\text{{Func}}}]$ is the theory
obtained by strengthening $\mathsf{PA}_{\text{{Func}}}$ by adding the
sentences $\mathsf{CT}_{1}$ through $\mathsf{CT}_{5}$ described below. We
follow the additional notational conventions:
$x\in\mathnormal{\mathsf{ClTerm}}_{\mathcal{L}_{\mathnormal{\mathsf{PA}}}}$ is
the arithmetical formula that expresses ”$x$ is (the code of) a closed term of
$\mathcal{L_{\mathsf{PA}}}$”;
$x\in\mathnormal{\mathsf{ClTermSeq}}_{\mathcal{L}_{\mathnormal{\mathsf{PA}}}}$
is the arithmetical formula that expresses ”$x$ is (the code of) a sequence of
closed terms of $\mathcal{L_{\mathsf{PA}}}$”; $\underline{x}$ is (the code of)
the numeral representing $x$; $\varphi[\underline{x}/v]$ is (the code of) the
formula obtained by substituting the variable $v$ with the numeral
representing $x$ and $\varphi[\bar{s}/\bar{v}]$ has an analogous meaning for
simultaneous substitution of terms from the sequence $\bar{s}$ for variables
from the sequence $\bar{v}$; ${s}^{\circ}$ denotes the value of the term $s$,
and ${\bar{s}}^{\circ}$ denotes the sequence of numbers that correspond to
values of terms from the sequence of terms $\bar{s}$.

  1. $\mathnormal{\mathsf{CT}}1$

$\forall
s,t\in\mathnormal{\mathsf{ClTerm}}_{\mathcal{L}_{\mathnormal{\mathsf{PA}}}}\ \
T(s=t)\leftrightarrow{s}^{\circ}={t}^{\circ}$.

  2. $\mathnormal{\mathsf{CT}}2$

$\forall\varphi,\psi\in\mathnormal{\mathsf{Sent}}_{\mathcal{L}_{\mathnormal{\mathsf{PA}}}}\
\ T(\varphi\vee\psi)\leftrightarrow T(\varphi)\vee T(\psi)$.

  3. $\mathnormal{\mathsf{CT}}3$

$\forall\varphi\in\mathnormal{\mathsf{Sent}}_{\mathcal{L}_{\mathnormal{\mathsf{PA}}}}\
\ T(\neg\varphi)\leftrightarrow\neg T(\varphi)$.

  4. $\mathnormal{\mathsf{CT}}4$

$\forall v\in\mathsf{Var\
}\forall\varphi\in{\mathnormal{\mathsf{Form}}}_{\mathcal{L}_{\mathnormal{\mathsf{PA}}}}^{\leq
1}\ \ T(\exists v\varphi)\leftrightarrow\exists
x~{}T(\varphi[\underline{x}/v])$.

  5. $\mathnormal{\mathsf{CT}}5$

$\forall\varphi(\bar{v})\in\mathnormal{\mathsf{Form}}_{\mathcal{L}_{\mathnormal{\mathsf{PA}}}}\
\
\forall\bar{s},\bar{t}\in\mathnormal{\mathsf{ClTermSeq}}_{\mathcal{L}_{\mathnormal{\mathsf{PA}}}}\
\ \left(\bar{{s}^{\circ}}=\bar{{t}^{\circ}}\rightarrow
T\left(\varphi[\bar{s}/\bar{v}]\right)\leftrightarrow
T\left(\varphi[\bar{t}/\bar{v}]\right)\right).$

The axiom $\mathnormal{\mathsf{CT}}5$ is sometimes called generalized
regularity, or generalized term-extensionality, and is not included in the
accounts of $\mathnormal{\mathsf{CT}}^{-}$ provided in the monographs of [H]
and [C-2]. The conservativity of this particular version of
$\mathnormal{\mathsf{CT}}^{-}[\mathnormal{\mathsf{PA}}],$ which is due to
Łełyk, and Wcisło, is verified by a refinement of the model-theoretic method
introduced in [EV-2]; see [ELW] or [KW] .

Both constructions presented in this paper employ known isomorphism results
about countable recursively saturated models of arithmetic. The following
classical result can be found in Kaye’s monograph [Ka].

2.5. Theorem. Suppose $\mathcal{M}$ and $\mathcal{N}$ are countable
recursively saturated models of $\mathsf{PA.}$ $\mathcal{M}$ and $\mathcal{N}$
are isomorphic iff $\mathrm{SSy}(\mathcal{M})=\mathrm{SSy}(\mathcal{N})$ and
$\mathrm{Th}(\mathcal{M})=\mathrm{Th}(\mathcal{M})$.

In order to state the next isomorphism theorem we need to recall the following
definitions:

2.6. Definition. Suppose $I$ is a proper cut of $\mathcal{M}\mathfrak{.}$ $I$
is $\mathbb{N}$-coded from below (above) in $\mathcal{M}$ iff for some $c\in
M,$ $\\{(c)_{n}:n\in\mathbb{N}\\}$ is cofinal in $I$ (downward cofinal in
$M\backslash I)$; here $(c)_{n}$ is the exponent of the $n$-th prime in the
prime factorization of $c$ within $\mathcal{M}$.

2.7. Definition. Suppose $I$ is a cut of a model $\mathcal{M}$ of
$\mathsf{PA}$. $\mathrm{SSy}_{I}(\mathcal{M})$ is the collection of subsets of
$I$ that are coded in $\mathcal{M}$. More precisely,
$\mathrm{SSy}_{I}(\mathcal{M})$ consists of sets of the form $c_{E}\cap I,$ as
c ranges in $\mathcal{M}$, where $c_{E}=\\{x\in M:\mathcal{M}\models
x\in_{\mathrm{Ack}}c\\}$ and $\in_{\mathrm{Ack}}$ is the Ackermann membership
defined by: $x\in_{\mathrm{Ack}}c$ iff the $x$-th digit of the binary
expansion of $c$ is $1$.

2.8. Theorem. (Kossak-Kotlarski [KK, Theorem 2.1, Corollary 2.3]) Suppose
$\mathcal{M}$ and $\mathcal{N}$ are countable recursively saturated models of
$\mathsf{PA}$, and $I$ is a cut shared by both $\mathcal{M}$ and $\mathcal{N}$
that satisfies the following two properties:

(a) $I$ is $\mathbb{N}$-coded from above in neither $\mathcal{M}$ nor
$\mathcal{N}$, and

(b) $\mathrm{SSy}_{I}(\mathcal{M})=\mathrm{SSy}_{I}(\mathcal{N}).$

Then $\mathcal{M}$ and $\mathcal{N}$ are isomorphic over $I$, i.e., there is
an isomorphism between $\mathcal{M}$ and $\mathcal{N}$ that is the identity on
$I.$

2.9. Remark.

(a) Thanks to Overspill, a cut $I$ cannot be both $\mathbb{N}$-coded from
above and $\mathbb{N}$-coded from below in a nonstandard model $\mathcal{M}$.
In particular, if $c$ is nonstandard element of $\mathcal{M}$, then the cut
determined by finite powers of $c$ is not coded from above in $\mathcal{M}$.

(b) It is easy to see that if $I$ is a strong cut of $\mathcal{M}$, then $I$
is not $\mathbb{N}$-coded from above.

(c) It is well-known that given a countable recursively saturated model
$\mathcal{M}$ of $\mathsf{PA}$, there are arbitrarily large strong cuts $I$ of
$\mathcal{M}$ such that $I\prec\mathcal{M}$ and $I\cong\mathcal{M}$. One way
of seeing this is as follows: by the resplendence property of $\mathcal{M}$,
$\mathcal{M}$ carries an inductive satisfaction class $S$. Next, use the
Phillips-Gaifman refinement of the MacDowell-Specker theorem to build a
countable conservative elementary end extension
$(\mathcal{M}^{\ast},S^{\ast})$ of $\left(\mathcal{M},S\right)$. Clearly
$\mathcal{M}$ is strong in $\mathcal{M}^{\ast}$ since
$\mathrm{SSy}_{M}(\mathcal{M})$ satisfies $\mathsf{ACA}_{0}$, and
$\mathcal{M}^{\ast}\cong\mathcal{M}$ by Theorem 2.5 (since
$\mathcal{M}^{\ast}$ is recursively saturated). Finally, the resplendence of
$\mathcal{M}$ allows us to finish the argument.

3\. AN ARITHMETIZATION

The second construction in this paper employs an arithmetized form of the main
construction in [EV-2] as in Theorem 3.2 below. In this section PA denotes the
usual formulation of $\mathsf{PA}$, i.e., $\mathsf{PA}_{\mathsf{Func}}.$Our
method of proof of Theorem 3.2 is through an arithmetization of the so-called
Enayat-Visser construction for this particular version of
$\mathnormal{\mathsf{CT}}^{-}[\mathnormal{\mathsf{PA}}],$ presented both in
[ELW] and [KW], which refine the model-theoretic construction given in [EV-2]
for $\mathsf{PA}$ formulated in a relational language. As we shall see, the
compactness and elementary chain argument used in the model-theoretic
conservativity proof of $\mathsf{CT}^{-}[\mathsf{PA}]$ over $\mathsf{PA}$ can
be implemented in the fragment $\mathrm{I}\Sigma_{2}$ of $\mathsf{PA}$ with
the help of the so-called Low Basis Theorem of Recursion Theory444Indeed,
using the technology of $\mathrm{LL}_{1}$-sets of [HP, Theorem 4.2.7.1, p.
104], the main argument presented in this section can be implemented in
$\mathrm{I}\Sigma_{1}.$. Note that the results of this section can be also
established by the arithmetization method presented in [ELW], or by taking
advantage of the main proof-theoretic result of [Lei].

Definition 3.1. Suppose $\mathcal{M}$ is a model of $\mathsf{PA}$, and
$\mathcal{N}$ is a structure in a finite language $\mathcal{L}$. $\mathcal{N}$
is strongly interpretable in $\mathcal{M}$ if $\mathcal{M}$ can interpret an
isomorphic copy $\mathcal{N}_{0}$ of $\mathcal{N}$; and moreover there is an
$\mathcal{M}$-definable $F$-satisfaction class $S$ on $\mathcal{N}_{0}$, where
$F$ is the collection of all $\mathcal{L}$-formulas in the sense of
$\mathcal{M}$.

Theorem 3.2. (joint with Albert Visser) Suppose
$\mathsf{PA}\vdash\mathsf{Con}(\mathsf{B}),$ where $\mathsf{B}$ is some
recursively axiomatizable theory extending $\mathrm{I}\Delta_{0}+\
\mathsf{Exp}$. Then $\mathsf{PA}$ strongly interprets
$\mathsf{CT}^{-}[\mathsf{B}],$ i.e., every model
$\mathcal{M}\models\mathsf{PA}$ strongly interprets a structure
$(\mathcal{N},T)\models\mathsf{CT}^{-}[\mathsf{B}]$ in a uniform manner.

Proof. Before starting the proof, we need to review some key definitions and
ideas from Recursion Theory. In what follows $X$ and $Y$ are subsets of
$\omega.$

  * •

$X$ is low-$\Delta_{2}^{0}$, if $X$ is $\Delta_{2}^{0}$, and
$X^{\prime}\leq_{T}0^{\prime}$ (where $\leq_{T}$ denotes Turing reducibility,
and $Z^{\prime}$ is the Turing-jump of $Z$).

  * •

More generally, $Y$ is low-$\Delta_{2}^{0}$ in the oracle $X$, if $Y$ is
$\Delta_{2}^{0}$ in the oracle $X$, and $Y^{\prime}\leq_{T}X^{\prime}$.

By classical recursion theory, we have:

(1) $X\leq_{T}Y^{\prime}$ iff $X$ is $\Delta_{2}^{0}$ in the oracle $Y$.

Next, observe that if $X^{\prime}\leq_{T}0^{\prime}$ and
$Y^{\prime}\leq_{T}X^{\prime}$, then $Y^{\prime}\leq_{T}0^{\prime}$, hence $Y$
is low-$\Delta_{2}^{0}$ by (1). Therefore:

(2) If $X$ is low-$\Delta_{2}^{0}$, and $Y$ is low-$\Delta_{2}^{0}$ in the
oracle $X$, then $Y$ is low-$\Delta_{2}^{0}.$

The classical ‘Low Basis Theorem’ of Jockusch and Soare [JS] asserts that
every infinite finitely branching recursive tree has an infinite branch $B$
such that $B$ is low-$\Delta_{2}^{0}$. Moreover, it is known that the Low
Basis Theorem is implementable in $\mathrm{I}\Delta_{0}+\mathrm{B}\Sigma_{2}$
(this is due to Clote, whose argument is presented in [HP, Chapter I, Section
3(c)]). In particular, $\mathrm{I}\Delta_{0}+\mathrm{B}\Sigma_{2}$ can verify
that every countable consistent $\Delta_{1}^{0}$-set of first order sentences
has a low-$\Delta_{2}$ completion. Since the Henkin construction of a model of
a prescribed complete theory is already implementable in
$\mathrm{I}\Sigma_{1}$, this shows that

(3) $\mathrm{I}\Delta_{0}+\mathrm{B}\Sigma_{2}$ can verify that every
consistent $\Delta_{1}^{0}$ set of first order sentences has a model
$\mathcal{M}$ such that the satisfaction predicate
$\mathsf{Sat}_{\mathcal{M}}$ of $\mathcal{M}$ is low-$\Delta_{2}.$

We are now ready to establish Theorem 3.2. We argue model-theoretically for
ease of exposition, and we will work with satisfaction classes instead of
truth classes.

Let $\mathcal{M}\models\mathsf{PA}$, and $\mathsf{B}$ be as in the assumption
of the theorem. By (3) there is an internal model $\mathcal{N}$ of
$\mathsf{B}$ such that $\mathsf{Sat}_{\mathcal{N}}$ is low-$\Delta_{2}$. Using
a truth-predicate for $\Delta_{2}^{0}$-predicates we can execute the
construction of Lemma 3.1 of [EV-2] (the same idea can be applied to the
counterpart of Lemma 3.1 in the proof of the conservativity of [ELW] and
[KW]); the key idea is that if $\mathsf{Sat}_{\left(\mathcal{N},S\right)}$ is
low-$\Delta_{2}$, then so is $\mathsf{Th}^{+}(\mathcal{N})$, and therefore
there is some elementary extension $\mathcal{N}_{1}$ of $\mathcal{N}$, and
some $\mathsf{Form}_{\mathcal{N}}$-satisfaction class $S_{1}\supseteq S$ such
that $\mathsf{Sat}_{\left(\mathcal{N}_{1},S_{1}\right)}$ is also
low-$\Delta_{2}$, thanks to (2) and the Low Basis Theorem. This shows that the
construction

$\left(\mathcal{N},S\right)\mapsto\left(\mathcal{N}_{1},S_{1}\right)$

can be uniformly described in $\mathrm{I}\Sigma_{2}+\mathsf{Con}(\mathsf{B})$,
so as to obtain an $\mathcal{M}$-definable increasing sequence of structures
$\left\langle\left(\mathcal{M}_{i},S_{i}\right):i\in M\right\rangle$ (as in
the proof of Theorem 3.3 of [EV-2]) with the additional feature that each
$\left(\mathcal{M}_{i},S_{i}\right)$ is strongly interpretable in
$\mathcal{M}$. Consider the limit model
$\left(\mathcal{N},S\right)=\bigcup\limits_{i\in
M}\left(\mathcal{M}_{i},S_{i}\right).$ $\left(\mathcal{N},S\right)$ is clearly
interpretable in $\mathcal{M}$, and additionally (thanks to the elementary
chains theorem applied within $\mathcal{M}$) the reduct $\mathcal{N}$ of
$\left(\mathcal{N},S\right)$ is strongly interpretable in $\mathcal{M}$, thus
$\mathcal{M}$ “knows” that $\mathcal{N}$ is a model of $\mathsf{B}$.

However, there is no reason to expect that the expansion
$\left(\mathcal{N},S\right)$ is strongly interpretable in $\mathcal{M}$. To
circumvent this problem, we appeal to a trick found by Mateusz Łełyk (first
introduced in [ELW]) to take advantage of $\left(\mathcal{N},S\right)$ in
order to show that $\mathcal{M}$ satisfies
$\mathsf{Con}(\mathsf{CT}^{-}[\mathsf{B}])$, thereby concluding the existence
of a model of $\mathsf{CT}^{-}[\mathsf{B}]$ is strongly interpretable in
$\mathcal{M}$. The key idea is to take advantage of (1) the classical fact of
proof theory that any deduction in first order logic can be replaced by
another deduction which has the same conclusion but which has the subformula
property555This fact is provable in PA, indeed it is well-known that it is
already provable in the fragment $\mathrm{I}\Delta_{0}+\mathsf{Supexp}$ of
Primitive Recursive Arithmetic., (2) the fact that
$\mathsf{CT}^{-}[\mathsf{B}]$ is the result of augmenting $\mathsf{B}$ with
only finitely many truth axioms, and (3) the fact that $\mathcal{M}$ has full
access to the elementary diagram of $\mathcal{N}.$ The veracity of
$\mathsf{Con}(\mathsf{CT}^{-}[\mathsf{B}])$ within $\mathcal{M}$ then allows
us to invoke the completeness theorem of first order logic within
$\mathcal{M}$ to get hold of model of $\mathsf{CT}^{-}[\mathsf{B}]$ that is
strongly interpretable in $\mathcal{M}$. $\square\vskip 6.0pt plus 2.0pt minus
2.0pt$

3.3. Corollary. $\mathsf{PA}$ strongly interprets
$\mathsf{CT}^{-}[\mathsf{PA}];$ indeed there is a uniform definition within
$\mathsf{PA}$, that yields a model
$\left(\mathcal{M}^{\ast},T\right)\models\mathsf{CT}^{-}[\mathsf{PA}]$ when
applied within any model of $\mathsf{PA}$ with the additional feature that
$\left(\mathcal{M}^{\ast},T\right)$ is strongly interpreted in
$\mathcal{M}.\vskip 6.0pt plus 2.0pt minus 2.0pt$

Proof. Let $\mathcal{M}$ be an arbitrary model of $\mathsf{PA}$. Within
$\mathcal{M}$, if $\mathsf{PA}$ is inconsistent let $\mathsf{B}$ be the first
$n$ such that $\mathrm{I}\Sigma_{n}$ is inconsistent, otherwise let
$\mathsf{B}=\mathsf{PA}$. Thus $\mathsf{Con}(\mathsf{B})$ holds in
$\mathcal{M}$. By Mostowski’s Reflection Theorem, $\mathsf{B}$ extends
$\mathrm{I}\Sigma_{n}$ for each $n\in\omega$ (recall that
$\mathrm{I}\Sigma_{n}$ is finitely axiomatizable for $n\geq 1)$ and thus
$\mathsf{B}$ extends $\mathsf{PA}$ (from an external point of view). Thus
Theorem 3.2 applies.666By using the proof strategy of the first stage of the
proof of Theorem 4.1 one can strengthen the conclusion of Corollary 3.3 by
arranging for $\mathcal{M}^{\ast}$ to be an elementary extension of
$\mathcal{M}$ provided $\mathcal{M}$ is recursively saturated. $\square$

3.4. Corollary. $\mathsf{PA}\vdash\mathsf{Con}(\mathsf{CT}^{-}[\mathsf{B}])$
for every finitely axiomatized subtheory $\mathsf{B}$ of $\mathsf{PA}$ that
extends $\mathrm{I}\Delta_{0}+\mathsf{Exp}.\vskip 6.0pt plus 2.0pt minus
2.0pt$

Proof. Let $\mathsf{B}$ be a finitely axiomatizable subtheory of
$\mathsf{PA}$. The formal consistency of $\mathsf{B}_{0}$ is verifiable in
$\mathsf{PA}$ by Mostowski’s Reflection Theorem. Therefore by Theorem 3.2
$\mathsf{PA}$ can produce an internal model of $\mathsf{CT}^{-}[\mathsf{B}]$
for which it has a satisfaction predicate; which in turn immediately implies
that $\mathsf{Con}(\mathsf{CT}^{-}[\mathsf{B}])$ is provable in $\mathsf{PA}$.
$\square$

3.5. Corollary. $\mathsf{CT}^{-}[\mathsf{PA}]$ is not finitely axiomatizable.

Proof. Put Corollary 3.4 together with Gödel’s second incompleteness theorem.
$\square$

4\. THE FIRST CONSTRUCTION

In this section $\mathsf{PA}:=\mathsf{PA}_{\text{Rel}}$, and $F$-satisfaction
classes are as in Definition 2.3(a)
---

4.1. Theorem. Let $\mathcal{M}$ be a countable recursively saturated model of
$\mathsf{PA}$. Let $\mathsf{Form}_{\mathcal{M}}^{<\omega}$ be the collection
of arithmetical formulae in the sense of $\mathcal{M}$ with at most finitely
many free variables, i.e.,

$\mathsf{Form}_{\mathcal{M}}^{<\omega}=\bigcup\limits_{n\in\omega}\mathsf{Form}_{\mathcal{M}}^{\leq
n},$

where $\mathsf{Form}_{\mathcal{M}}^{\leq n}$ is the collection of (codes of)
arithmetical formulae in $\mathcal{M}$ that have at most $n$ free variables.
Then there is an extensional, alphabetically correct777Alphabetically correct
satisfaction classes are those that well-behaved under the renaming of bound
variables. $\mathsf{Form}_{<\omega}^{\mathcal{M}}$-satisfaction class
$S_{\mathcal{M}}$ on $\mathcal{M}$ that whose associated truth class888More
explicitly, $\mathrm{Sent}_{\mathcal{M}}^{<\omega}$ is the result of
substituting domain constants from $\mathcal{M}$ into formulae in
$\mathrm{Form}_{\mathcal{M}}^{<\omega}$ so as to obtain a truth class
$T_{\mathcal{M}}$ from the extensional satisfaction class $S_{\mathcal{M}}$,
as in [EV-2, Proposition 4.3]. $T_{M}$ is
$\mathsf{Sent}_{\mathcal{M}}^{<\omega}$ -disjunctively correct, i.e., given
any disjunction
$\delta(x_{1},...,x_{n})=\bigvee\limits_{i<m}\varphi_{i}\in\mathsf{Form}_{\mathcal{M}}^{<\omega}$
[where $m$ is allowed to be nonstandard] and any $(a_{1},...,a_{n})\in M^{n},$
we have:

$T_{\mathcal{M}}(\delta(a_{1},...,a_{n}))\text{ {iff there is some} }i<m\text{
{such that} }T_{\mathcal{M}}(\varphi_{i}(a_{1},...,a_{n})).$

Moreover, $T_{\mathcal{M}}$ satisfies the following additional properties:

(a) $T_{\mathcal{M}}$ is closed under proofs of Propositional Logic (in a
Hilbert-style system where the only rule of inference is Modus Ponens, and the
axioms consist of finitely many axiom templates) in the following sense:

If $\pi=\left\langle\varphi_{i}:i\leq m\right\rangle$ is (the code of) an
$\mathcal{M}$-finite sequence of sentences in
$\mathsf{Sent}_{\mathcal{M}}^{<\omega}$ such that for each $i\leq m$,

$\varphi_{i}$ is either a substitution instance of an axiom template of
Propositional Logic by sentences in $\mathsf{Sent}_{\mathcal{M}}^{<\omega},$

or $\varphi_{i}$ is a member of $T_{\mathcal{M}}$,

or $\varphi_{i}$ is derivable from earlier components of $\pi$ via Modus
Ponens,

then $\varphi_{m}\in T_{\mathcal{M}}.$

(b) $T_{\mathcal{M}}$ deems all the axioms of one-parameter version of
$\mathsf{PA}$ to be true (indeed the same goes for the version of
$\mathsf{PA}$ with finitely many parameters, from an external point of view).

Proof. Let $\mathcal{M}$ be a countable recursively saturated model of
$\mathsf{PA.}$ In the first stage of the proof we shall build an appropriate
elementary extension $\mathcal{N}$ of $\mathcal{M}$ with two key properties:
$\mathcal{M}$ and $\mathcal{N}$ are isomorphic, and yet $\mathcal{N}$ is
strongly interpretable in $\mathcal{M}$ (the latter property does not
contradict Tarski’s Undefinability of Truth).

To build such an $\mathcal{N}$, we first observe that by recursive saturation
we can find an element $c$ in $\mathcal{M}$ that codes
$\mathsf{Th}(\mathcal{M})$ by realizing the recursive type $\Sigma(v)$, where

$\Sigma(v):=\\{\varphi\leftrightarrow\ulcorner\varphi\urcorner\in_{\mathsf{Ack}}v:\varphi\in\mathsf{Sent}_{\mathsf{PA}}\\},$

where $\ulcorner\varphi\urcorner$ is the Gödel number for $\varphi$,
$\in_{\mathsf{Ack}}$ is “Ackermann’s $\in$”, i.e., $a\in_{\mathsf{Ack}}b$
holds iff the $a$-th bit of the binary expansion of $b$ is $1;$ and
$\mathsf{Sent}_{\mathsf{PA}}$ is the (recursive) set of sentences in the usual
language of arithmetic. Next, let
$\left\langle\varphi_{n}:n\in\omega\right\rangle$ be a recursive enumeration
of arithmetical sentences, and consider the arithmetical formula $\gamma(i)$
defined below:

$\gamma(i):=\mathrm{Con}\left(\left\\{\varphi_{j}:j<i\wedge\varphi_{j}\in_{\mathsf{Ack}}c\right\\}\right)$

It is easy to see, using Mostowski’s Reflection Theorem999Mostowski’s
Reflection Theorem is the statement that for each arithmetical formula
$\varphi(x)$, the following statement is provable in $\mathsf{PA}$:  $\forall
x(\varphi(x)\rightarrow\mathrm{Con}(\varphi(\overset{\cdot}{x})).$ and our
choice of $c$ that $\mathcal{M}\models\gamma(n)$ for each $n<\omega.$ Hence by
Overspill $\mathcal{A}\models\gamma(d)$ for some nonstandard element $d$ of
$\mathcal{M}$. By invoking the Arithmetized Completeness Theorem (as in [Ka])
within $\mathcal{M}$, we can conclude that there is a model $\mathcal{M}$ of
$T$ with the following three properties:

(1) $\mathrm{Th}(\mathcal{M})=\mathrm{Th}(\mathcal{N}).$

(2) $\mathcal{N}$ is recursively saturated.

(3) $\mathrm{SSy}(\mathcal{M})=\mathrm{SSy}(\mathcal{N}).\vskip 6.0pt plus
2.0pt minus 2.0pt$

Note that (1) holds by design and (2) holds by a routine argument using
Overspill and the definability of the elementary diagram of $\mathcal{N}$
within $\mathcal{M}$. The definability of $\mathcal{N}$ within $\mathcal{M}$
combined with an internal recursion within $\mathcal{M}$, implies that there
is an $\mathcal{M}$-definable embedding from $\mathcal{M}$ into an initial
segment of $\mathcal{N},$ which in turn shows that (3) is true since standard
systems of models of arithmetic are invariant under end extensions. By Theorem
2.5. we may conclude that there is a function $f:M\rightarrow N$ that
witnesses that $\mathcal{M}$ and $\mathcal{N}$ are isomorphic.

The second stage of the proof involves the definition of the desired
satisfaction class $S$ on $\mathcal{M}$. Let $S_{\mathcal{N}}$ be the
$\mathcal{M}$-definable satisfaction
$\mathsf{Form}_{\mathcal{M}}$-satisfaction class for $\mathcal{N}.$ Since
$S_{\mathcal{N}}$ is extensional, we will treat it as a truth predicate, i.e.,
we will write $S_{\mathcal{N}}(\varphi(a_{1},\cdot\cdot\cdot,a_{n}))$ instead
of
$S_{\mathcal{N}}(\left\langle\varphi(x_{1},...,x_{n}),\alpha\right\rangle),$
where $\alpha$ is the assignment $x_{i}\mapsto a_{i}$ for $1\leq i\leq n$.

Given any
$\varphi=\varphi(x_{1},x_{2},...,x_{n})\in\left(\mathsf{Form}_{\mathsf{PA}}^{n}\right)^{\mathcal{M}}$
(where $n\in\omega)$, and any assignment $\alpha=(a_{1},a_{2},...,a_{n})$ in
$\mathcal{M}$ for $\varphi,$ let $S=S_{\mathcal{M}}$ where $S_{\mathcal{M}}$
is defined via:

$S_{\mathcal{M}}(\varphi(a_{1},a_{2},...,a_{n}))$ iff
$S_{\mathcal{N}}(\varphi(f(a_{1}),f(a_{2}),...,f(a_{n}))).$

We first verify that $S_{\mathcal{M}}$ is an
$\mathsf{Form}_{\mathcal{M}}^{<\omega}$-satisfaction class.

Atomic case: We only check the condition for + ( the other atomic formulae are
handled similarly).

$S_{\mathcal{M}}(a+b=c)$ iff $S_{\mathcal{N}}(f(a)+f(b)=f(c))$

[by the definition of $S_{\mathcal{M}}$],

$S_{\mathcal{N}}(f(a)+f(b)=f(c))$ iff $f(a)+_{\mathcal{N}}f(b)=f(c)$

[since $S_{\mathcal{N}}$ is an $\mathsf{Form}_{\mathcal{M}}$-satisfaction
class for $\mathcal{N}$], and

$f(a)+_{\mathcal{N}}f(b)=f(c)$ iff $a+_{\mathcal{M}}b=c$

[since $f$ is an isomorphism].

Negation case: Suppose $\varphi(a_{1},...,a_{n})=\lnot\psi(a_{1},...,a_{n}).$

$S_{\mathcal{M}}(\lnot\psi(a_{1},...,a_{n}))$ iff
$S_{\mathcal{N}}(\lnot\psi(f(a_{1}),...,f(a_{n})))$,

[by the definition of $S_{\mathcal{M}}$],

$S_{\mathcal{N}}(\lnot\psi(f(a_{1}),...,f(a_{n})))$ iff $\lnot
S_{\mathcal{N}}(\psi(f(a_{1}),...,f(a_{n})))$,

[since $S_{\mathcal{N}}$ is an $\mathsf{Form}_{\mathcal{M}}$-satisfaction
class for $\mathcal{N}$ and $\lnot\psi\in\mathsf{Form}_{\mathcal{M}}$], and

$\lnot S_{\mathcal{N}}(\psi(f(a_{1}),...,f(a_{n})))$ iff $\lnot
S_{\mathcal{M}}(\psi(a_{1},...,a_{n}))$,

[by the definition of $S_{\mathcal{M}}$].

The disjunction case is handled similarly to the negation case, so we omit it.

Existential case. Suppose $\varphi(a_{1},...,a_{n})=\exists x\
\psi(x,a_{1},...,a_{n}).$

$S_{\mathcal{M}}(\exists x\ \psi(x,a_{1},...,a_{n}))$ iff
$S_{\mathcal{N}}(\exists x\ \psi(x,f(a_{1}),...,f(a_{n})))$

[by the definition of $S_{\mathcal{M}}],$

$S_{\mathcal{N}}(\exists x\ \psi(x,f(a_{1}),...,f(a_{n})))$ iff $\exists b\in
N$ $S_{\mathcal{N}}(\psi(b,f(a_{1}),...,f(a_{n})))$,

[since $S_{\mathcal{N}}$ is an $\mathsf{Form}_{\mathcal{M}}$-satisfaction
class for $\mathcal{N}$ and $\exists x\ \psi\in\mathsf{Form}_{\mathcal{M}}$],

$\exists b\in N$ $S_{\mathcal{N}}(\psi(b,f(a_{1}),...,f(a_{n})))$ iff $\
\exists c\in M\ S_{\mathcal{M}}(\psi(f(c),f(a_{1}),...,f(a_{n})))$

[by the surjectivity of $f$ and definition of $S_{\mathcal{M}}]\vskip 6.0pt
plus 2.0pt minus 2.0pt,$ and

$\exists c\in M\ S_{\mathcal{M}}(\psi(f(c),f(a_{1}),...,f(a_{n}))$ iff
$\exists c\in M\ S_{\mathcal{M}}(\psi(c,a_{1},...,a_{n})).$

[by the definition of $S_{\mathcal{M}}].$

Extensionality of $S_{\mathcal{M}}$ and alphabetical correctness of
$S_{\mathcal{M}}$ can also be readily checked with similar arguments as above,
using the fact $\mathcal{M}$ is strongly interpreted in $\mathcal{M}$, and
thus $S_{\mathcal{N}}$ satisfies the usual properties (such as extensionality
and alphabetic correctness) of the classical Tarskian satisfaction predicates
for structures since such properties are readily verifiable in $\mathsf{PA}$.

  * •

Note that the extensionality property of $S_{\mathcal{M}}$ allows us to write
$T_{\mathcal{M}}$ for the truth class naturally associated with
$S_{\mathcal{M}}$ (with the help of domain constants).

Next we verify the disjunctive correctness of $S_{\mathcal{M}}$. Suppose we
have disjunction
$\bigvee\limits_{i<m}\varphi_{i}\in\mathsf{Sent}_{\mathcal{M}}^{<\omega}$
(where $m$ is a possibly nonstandard element of $\mathcal{M}$), and let
$\varphi_{i}=\varphi_{i}(a_{1},...,a_{n})$. Then we have:.

$T_{\mathcal{M}}(\bigvee\limits_{i<m}\varphi_{i}(a_{1},...,a_{n}))$ iff
$T_{\mathcal{N}}(\bigvee\limits_{i<m}\varphi_{i}(f(a_{1}),...,f(a_{n})))$,

[by the definition of $S_{\mathcal{M}}],$

$T_{\mathcal{N}}(\bigvee\limits_{i<m}\varphi_{i}(f(a_{1}),...,f(a_{n})))$ iff
$\exists k<m$ $T_{\mathcal{N}}(\varphi_{k}(f(a_{1}),...,f(a_{n})))$

[since $T_{\mathcal{N}}$ is disjunctively correct], and

$T_{\mathcal{N}}(\varphi_{k}(f(a_{1}),...,f(a_{n})))$ iff
$T_{\mathcal{M}}(\varphi_{k}(f(a_{1}),...,f(a_{n}))).$

[by the definition of $T_{\mathcal{M}}].$

Next we verify that $T_{\mathcal{M}}$ is closed under Propositional Logic
(where the only rule of inference is Modus Ponens, and the axioms consist of
finitely many axiom finite templates). Suppose
$\pi=\left\langle\varphi_{i}:i\leq m\right\rangle$ is (the code of) an
$\mathcal{M}$-finite sequence of arithmetical sentences in the sense of $M$
such that for each $i\leq m$, $\varphi_{i}$ is either a substitution instance
of an axiom scheme of Propositional Logic by sentences in
$\mathsf{Sent}_{\mathcal{M}}^{<\omega},$ or is a member of $T_{\mathcal{M}}$,
or is derivable from earlier components of $\pi$ via Modus Ponens. Let
$\pi=\left\langle\varphi_{i}(a_{1},...,a_{n}):i\leq m\right\rangle$, and
consider $\pi^{f}=\left\langle\varphi_{i}(f(a_{1}),...,f(a_{n})):i\leq
m\right\rangle.$ Then it can be readily checked that $\pi^{f}$ is a proof in
Propositional Logic from hypotheses in the truth class $T_{\mathcal{N}}$, and
therefore by the closure of $T_{\mathcal{N}}$ under propositional proofs
(which is an immediate consequence of definability of $S_{\mathcal{N}}$ in
$\mathcal{M}$, and the fact that $\mathcal{M}\models\mathsf{PA}$), we can
conclude that $\varphi_{m}(f(a_{1}),...,f(a_{n}))$ is a member of
$T_{\mathcal{N}}$, and therefore $\varphi_{m}(a_{1},...,a_{n})$ is in
$T_{\mathcal{M}},$ as desired.

Finally, it is easy to see that all the axioms of the parameter-free version
of $\mathsf{PA}$ are deemed true by $S_{\mathcal{M}}$ using the fact that
$T_{\mathcal{M}}$ is closed under Propositional Logic by a standard argument
that derives each instance of the induction scheme from repeated applications
of Modus Ponens. $\square$

4.2. Question. Suppose $\mathcal{M}$ is a model of $\mathsf{PA}$ that has an
expansion to an $\mathsf{Form}_{\mathcal{M}}^{<\omega}$-satisfaction class.
Does $\mathcal{M}$ have to be recursively saturated? More generally, in light
of Wcisło’s theorem concerning $\omega$-interpretability of $\mathsf{UTB}$ in
$\mathsf{CT}^{-}$ (see, e.g., Theorem 3 of [KW]), does $\mathcal{M}$
necessarily have an expansion to $\mathsf{UTB}$?

4.3. Theorem. Suppose $\mathcal{M}$ is a countable recursively saturated
model. In part (a) below $\mathsf{Form}_{\mathcal{M}}^{<I}$ is the collection
of arithmetical formulae in $\mathcal{M}$ with at most $i$ free variables for
some $i\in I;$ and in part (b) $\mathsf{Form}_{\mathcal{M}}\upharpoonright I$
is the collection of arithmetical formulae in $\mathcal{M}$ whose code is in
$I$.

(a) There are arbitrarily large cuts $I\prec\mathcal{M}$ such that
$I\cong\mathcal{M}$ and $\mathcal{M}$ carries an extensional, alphabetically
correct $\mathsf{Form}_{\mathcal{M}}^{<I}$-satisfaction class whose associated
truth class is $\mathsf{Sent}_{\mathcal{M}}^{<\omega}$ -disjunctively correct
(and also satisfies the analogues of (a) and (b) of Theorem 4.1).

(b) There are arbitrarily large cuts $I\prec\mathcal{M}$ such that
$I\cong\mathcal{M}$ and $\mathcal{M}$ carries an extensional, alphabetically
correct $\mathsf{Form}_{\mathcal{M}}\upharpoonright I$-satisfaction class
whose associated truth class is $\mathsf{Sent}_{\mathcal{M}}\upharpoonright I$
-disjunctively correct (and also satisfies the analogues of (a) and (b) of
Theorem 4.1).

Proof Outline. Use the strategy of the proof of Theorem 4.1, but use Theorem
2.5 instead of Theorem 2.8, and invoke Remark 2.9(c).

4.4. Theorem. Suppose $\mathcal{M}$ is a countable recursively saturated
model. There are arbitrary large cuts $I$ in $\mathcal{M}$ such that
$\mathcal{M}$ carries a full truth class that is disjunctively correct for
disjunctions resulting from substituting domain constants that are in $I$ in
$\mathsf{Form}_{\mathcal{M}}\upharpoonright I$.

Proof Outline. This is an immediate consequence of putting Remark 2.9(c) and
Theorem 4.3(b) (for strong cuts $I$ in $\mathcal{M}$) together with the main
theorem of Pakhomov’s manuscript [P] that gives a sufficient condition (which
is satisfied by $\mathsf{Form}_{\mathcal{M}}\upharpoonright I$-satisfaction
classes) to be extendible to full satisfaction classes on a countable
recursively saturated model of $\mathsf{PA}$. $\square$

4.5. Question. Suppose $\mathcal{M}$ is a countable recursively saturated
model. Is there a full satisfaction class on $\mathcal{M}$ that is
disjunctively correct for disjunctions resulting from substituting domain
constants in $\mathsf{Form}_{\mathcal{M}}^{<\omega}$?

5\. THE SECOND CONSTRUCTION

In this section $\mathsf{PA}:=\mathsf{PA}_{\mathrm{Func}},$ and
$\mathsf{CT}^{-}[\mathsf{PA}]$ is as in Definition 2.4.
---

5.1. Theorem. (joint with Albert Visser) Let $\mathcal{M}$ be a countable
recursively saturated model of $\mathsf{PA.}$ There are arbitrarily large cuts
$I$ of $\mathcal{M}$ for which the following properties hold:

$\mathbf{(a)}$ $I\prec\mathcal{M}$ and $I\cong\mathcal{M}.$

$\mathbf{(b)\ }\mathcal{M}$ carries a full truth class T that is
$I$-deductively correct (i.e., $T\ $is closed under first order proofs coded
in $I)$ and is $I$-disjunctively correct (i.e., a disjunction whose code is in
$I$ is deemed true by $T$ iff one if its disjuncts is true).

Proof. Let $\mathcal{M}$ be a countable recursively saturated model of
$\mathsf{PA}$. Let $\mathcal{N}$ be as in the proof of the first construction;
thus $\mathcal{N}$ is an elementary extension of $\mathcal{M}$ that is
strongly interpreted in $\mathcal{M}$ and
$\mathrm{SSy}(\mathcal{M})=\mathrm{SSy}(\mathcal{N}).$ Thanks to Corollary 3.3
there is an elementary extension $\mathcal{N}^{\ast}$ of $\mathcal{N}$ that
carries a truth class $T$ such that
$(\mathcal{N},T_{N})\models\mathsf{CT}^{-}[\mathsf{PA}],$ and
$(\mathcal{N},T_{N})$ is strongly interpretable in $\mathcal{M}$, which in
turn will allow us to conclude that $\mathcal{N}^{\ast}$ satisfies the
following four properties:

$(1)$ $T_{N}$ is $\mathcal{M}$-deductively correct (i.e., the conclusion of
any from hypotheses in $T_{N}$ is also in $T_{N}$; this is handled the usual
argument that shows that the classical Tarskian truth predicate is deductively
correct) and $\mathcal{M}$-disjunctively correct (i.e., any disjunction in
$\mathcal{M}$ that is deemed true by $T_{N}$ has a true disjunct).

$(2)$ There is an $\mathcal{M}$-definable embedding of $\mathcal{M}$ as an
initial segment of $\mathcal{N}^{\ast}.$

$(3)$ $\mathrm{SSy}(\mathcal{M})=\mathrm{SSy}(\mathcal{N}^{\ast}).$

$(4)$ $\mathcal{N}^{\ast}$ is recursively saturated.

Thanks to (2), (3), (4), and Theorem 2.5,
$\mathcal{M}\cong\mathcal{N}^{\ast}$, which implies that we ‘copy over’
$T_{N}$ on $\mathcal{M}$, thus $\mathcal{M}$ carries a full truth $T$ class
that is $I$-correct for some cut $I$ of $\mathcal{M}$. By using Theorem 2.8
and Remark 2.9 we can readily conclude that such cuts can be arranged to be
arbitrarily large cuts $I$ in $\mathcal{M}$ (more specifically, if $I$ is a
strong cut of $\mathcal{M}$, then by Theorem 2.8 there is an isomorphism
$f:\mathcal{M}\rightarrow\mathcal{N}^{\ast}$ with $f(i)=i$ for all $i$ in $I$.
This makes it clear that $T:=f(T_{N})$ is the desired full truth class).
$\square$

5.2. Remark. If $\mathcal{M}\models\mathsf{PA}+\mathsf{\lnot Con(PA)}$ and
$\mathcal{M}$ carries an inductive satisfaction class (in other words,
$\mathcal{M}$ is expandable to $\mathsf{UTB}$), then there is a topped
nonstandard initial segment $I$ of $\mathbb{N}^{\mathcal{M}}$ such that $S$
satisfies the Tarski conditions for all formulas in $I$. If $\mathcal{M}$, and
$\pi\in\mathbb{N}^{\mathcal{M}}$ codes up a proof of inconsistency of
$\mathsf{PA}$ in $\mathcal{M}$, then $\pi\notin I$. This is in contrast to
Theorem 5.1 that shows that a full satisfaction class that is $I$-deductively
correct can be always arranged for arbitrarily high cuts $I$ in $\mathcal{M}$.

6\. Historical Note

The main idea of the first construction was found by the author in 2009; it
was written up in a short note that was privately circulated among a few
colleagues. In 2011, I received an email from Jim Schmerl that shows that over
three decades earlier Craig Smoryński had come up with the same idea, as
indicated below. The email, as well as my response, are copied below.

From James Schmerl to Ali Enayat

July 5, 2011

I moved out of my office over the weekend. I’m sure you’re not interested in
that tidbit, but what you might be interested in is that, in the process, I
uncovered the Smoryński letter that I had told you about a while ago. I
transcribed the relevant portion to the attached file [see below]. What do you
think of his proof?

The following is an exact transcription of a portion of a handwritten letter
dated 10 June ’80 sent to me by Craig Smoryński:

**************

Kotlarski-Krajewski-Lachlan. If $M$ is countable rec. sat., $M$ has a full
satisfaction class.

Pf: Let $M$ define truth for $N\models\mathrm{Th}$($M$) by Orey’s Compactness
Theorem. Since $M\equiv N$ and $\mathrm{SSy}(M)=\mathrm{SSy}(N)$ we have
$M\cong N$. Now truth for $N$ is defined for all nonstandard formulae in $M$
with parameters in $N$. Using isomorphism $F$ define

$S(\left\langle a_{0},...,a_{e-1}\right\rangle,\ulcorner\varphi
v_{0},...,v_{e-1}\urcorner)\leftrightarrow\mathsf{Tr}_{N}(\ulcorner\varphi
Fa_{0},...,Fa_{e-1}\urcorner)$

[$e$ possibly ns.].

**************

From Ali Enayat to James Schmerl

July 5, 2011

Thank you very much for sending me the note, it is VERY interesting for me,
because a couple of years ago I came up with an identical construction (and
even talked about it in a seminar in Sweden).

Later, when I tried to write a careful proof that the construction works, I
found a subtle serious obstacle, having to do with the case when $\varphi$ has
nonstandardly-many free variables. I recall spending a great deal of effort
dealing with this obstacle, and was finally convinced that this “cheap way”
cannot produce a full satisfaction class. However, using the automorphism
trick, one *can* obtain the nontrivial result that when $M$ is countable rec.
sat., then for any prescribed m in $M$, there is a satisfaction class on $M$
that decides all the formulas at least up to $m$.

## References

  * [C-1] C. Cieśliński, Deflationary truth and pathologies, The Journal of Philosophical Logic, vol. 39, (2010), pp. 325–337.
  * [C-2] ———–, The Epistemic Lightness of Truth. Deflationism and its Logic, Cambridge University Press, 2017.
  * [CLW] C. Cieśliński, M. Łełyk and B. Wcisło, The two halves of disjunctive correctness, Journal of Mathematical Logic (2023), no.2, Paper No. 2250026, 28 pp
  * [ELW] A. Enayat, M. Łełyk and B. Wcisło, Truth and feasible reducibility, Journal of Symbolic Logic, vol. 85 (2020), pp. 367–421.
  * [EP] A. Enayat and F. Pakhomov, Truth, disjunction, and induction, Archive for Mathematical Logic, vol. 58 (2019), pp. 753–766.
  * [EV-1] A. Enayat and A. Visser, Full satisfaction classes in a general setting, privately circulated manuscript (2012).
  * [EV-2] ______________________________, New constructions of full satisfaction classes, in Unifying the Philosophy of Truth, (ed. T. Achourioti, H. Galinon, K. Fujimoto, and J. Martínez-Fernández), Springer, 2015, pp. 321–325.
  * [HP] P. Hájek and P. Pudlák, Metamathematics of First-Order Arithmetic, Springer, 1993.
  * [H] V. Halbach, Axiomatic Theories of Truth, Cambridge University Press, Cambridge, 2011.
  * [JS] C. G. Jockusch and R. I. Soare, $\Pi_{1}^{0}$ classes and degrees of theories, Trans. Amer. Math. Soc. vol. 173 (1972), 33-56.
  * [Ka] R. Kaye, Models of Peano Arithmetic, Oxford Logic Guides, Oxford University Press, Oxford, 1991.
  * [KK] R. Kossak and H. Kotlarski, Results on automorphisms of recursively saturated models of PA, Fundamenta Mathematicae, vol. 129 (1988), pp. 9–15.
  * [KS] R. Kossak and J. Schmerl, The Structure of Models of Arithmetic, Oxford Logic Guides, Oxford University Press, 2006.
  * [KW] R. Kossak and B. Wcisło, Disjunctions with stopping conditions, Bulletin of Symbolic Logic, vol. 27 (2021), pp. 231–253.
  * [KKL] H. Kotlarski, S. Krajewski, and A. H. Lachlan, Construction of satisfaction classes for nonstandard models, Canadian Mathematical Bulletin, vol. 24 (1981), pp. 283–293.
  * [Ko] H. Kotlarski, Bounded induction and satisfaction classes. Zeitschrift für matematische Logik und Grundlagen der Mathematik, vol. 32, (1986), pp. 531–544.
  * [La] A. H. Lachlan, Full satisfaction classes and recursive saturation, Canadian Mathematical Bulletin, vol. 24 (1981), pp. 295-297.
  * [Lei] G. Leigh, Conservativity for theories of compositional truth via cut elimination, The Journal of Symbolic Logic, vol. 80, (2015), pp. 845–865.
  * [Lel] M. Łełyk, Axiomatic Theories of Truth, Bounded Induction and Reflection Principles, Ph.D. disseration, University of Warsaw, 2017.
  * [P] F. Pakhomov, One more construction of a full satisfaction class, privately circulated manuscript, June 2020.
  * [WL] B. Wcisło and M. Łełyk, Notes on bounded induction for the compositional truth predicate, The Review of Symbolic Logic, vol. 10, 2017, pp. 455–480.