# Full satisfaction classes, definability, and automorphisms

Bartosz Wcisło111Institute of Mathematics, Polish Academy of Sciences.

###### Abstract

We show that for every countable recursively saturated model $M$ of Peano
Arithmetic and every subset $A\subseteq M$, there exists a full satisfaction
class $S_{A}\subset M^{2}$ such that $A$ is definable in $(M,S_{A})$ without
parametres. It follows that in every such model, there exists a full
satisfaction class which makes every element definable and thus the expanded
model is minimal and rigid. On the other hand, we show that for every full
satisfaction class $S$ there are two elements which have the same arithmetical
type, but exactly one of them is in $S$. In particular, the automorphism group
of a model expanded with a satisfaction class is never equal to the
automorphism group of the original model. The analogue of many of the results
proved here for full satisfaction classes were obtained by Roman Kossak for
partial inductive satisfaction classes. However, most of the proofs relied
heavily on the induction scheme in a crucial way, so recapturing the results
in the setting of full satisfaction classes requires quite different
arguments.

##  1 Introduction

Satisfaction classes are a classical topic in the study of models of Peano
Arithmetic. A full satisfaction class is essentially a function which assigns
to each formula in the sense of a model a set of elements which "satisfy" that
formula. We require that this assignment is compositional in that, for
instance, the set of elements satisfying a conjunction $\phi\wedge\psi$ is the
intersection of the sets of elements satisfying $\phi$ and $\psi$. In that way
we endow nonstandard arithmetical formulae with certain "semantics." We can
also weaken the requirement that the relation of satisfaction is defined for
all formulae, thus obtaining a notion of a partial satisfaction class, or
strengthen it in a number of interesting ways. For instance, we may require
that the expansion of a model $M$ with a satisfaction class $S$ satisfies full
induction, obtaining a notion of an inductive satisfaction class.

A systematic study of satisfaction classes was initiated by Krajewski,
preceded by a study of "nonstandard semantics" by Robinson, [15]. Probably the
most important result of the whole area was obtained by Kotlarski, Krajewski,
and Lachlan in [13], where it was proved that in every countable recursively
saturated model of PA there exists a full satisfaction class. The saturation
assumption turned out to be essential, since it was subsequently shown by
Lachlan in [14] that indeed every model with a full satisfaction class is
recursively saturated. Later, it was shown that the presence of a full
satisfaction class in a model is a strictly stronger requirement than
recursive saturation. In [17] it was proved by Smith that every model
$M\models\textnormal{PA}$ with a full satisfaction class has an undefinable
subset whose all bounded initial segments are coded in the model. On the other
hand, by the previous work of Kaufmann, [8], we know that there are
uncountable recursively saturated models in which no such subset can be found
(so called rather classless models).

Model-theoretic properties of the satisfaction classes themselves were also a
subject of study. In [10], a number of results typical for models of PA were
proved by Kossak for the models expanded with satisfaction classes. For
instance, it was shown that in every countable recursively saturated model $M$
of PA, there exists a class $S\subset M$ such that $(M,S)$ is minimal, i.e.,
it does not have a proper elementary submodel. It was also proved that in any
countable model $M\models\textnormal{PA}$, there exists a family of continuum
many pairwise non-elementary-equivalent satisfaction classes. The work of
Kossak was later used by him in a joint paper with Schmerl, [11], to obtain
new results on models of pure PA.

The findings from [10] mostly applied to inductive satisfaction classes, so
most of them do not typically generalise when we require that the constructed
class is also full, since the presence of a full inductive satisfaction class
has nontrivial implications for the theory of the underlying model (e.g., it
can be verified that such a model satisfies
$\textnormal{Con}_{\textnormal{PA}}$). The proofs in [10] mostly relied on the
induction scheme in a crucial way, so recapturing the results in the setting
of full satisfaction classes requires quite different arguments.222This paper
actually answers some questions of Roman Kossak, who asked during his visit in
Warsaw whether certain results from that previous work also hold for full
satisfaction classes.

In this article, we investigate such full satisfaction classes with special
model-theoretic properties. Among other things, we show that in a countable
model of PA, every set is definable (without parametres) from a full
satisfaction class. This has a number of model-theoretic corollaries. For
instance, we can require that every element in the model is definable from $S$
without parametres, so that all elements of $M$ become distinguishable in the
presence of a full satisfaction class. On the other hand, we show that if $S$
is a full satisfaction class on $M$, we can always find a pair of sentences
$\phi,\psi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(M)$ with the
same arithmetical types such that $\phi$ is rendered true and $\psi$ is
rendered false, so it cannot happen that all elements indistinguishable by
arithmetical formulae are also indistinguishable from the perspective of a
given satisfaction class.

The study of satisfaction classes closely parallels the study of truth
predicates which is an active research area in philosophical logic.333A
classical textbook on axiomatic truth predicates is [6]. See also [1] for an
overview of some more recent results in that field. Although the results in
both terminological traditions seem to go hand-in-hand, they are typically not
formulated in a way that allows for a direct translation. In this article, we
try to close this small gap and propose certain additional technical
assumptions both on satisfaction and on truth classes that makes the
correspondence completely direct. In particular, all our results apply,
mutatis mutandis, both to satisfaction classes and to truth predicates.

##  2 Preliminaries

###  2.1 Arithmetic

In this article, we will consider satisfaction classes over Peano Arithmetic,
PA. We will assume that the reader has some previous knowledge of PA and its
models. Crucially for our purposes, Peano Arithmetic can define Ackermann’s
elementhood notion $x\in_{\textnormal{Ack}}y$ defined as "$x$-th bit of the
binary expansion of $y$ is one." This notion, provably in PA, satisfies the
axioms of the Zermelo–Fränkel set theory, except for the Axiom of Infinity.
This allows us to treat PA as a theory of finite sets (consequently, we will
denote the relation $\in_{\textnormal{Ack}}$ simply with "$\in$"). In
particular, PA is capable of handling syntactic notions such as formulae,
sentences of proofs. All the relevant background facts including formalisation
of syntax can be found e.g. in [9], especially Chapters 1–9 or [5], especially
Chapter I.

Let us introduce some notation for the formalised syntactic objects.

######  Definition 1.

Let $\mathscr{L}$ be a primitive recursive langauge containing
$\mathscr{L}_{\textnormal{PA}}$ (i.e, $\mathscr{L}$ is countable and the
function which given a Gödel number returns the type of symbol it represents
and its arity is primitive recursive).

  * •

The formula $\textnormal{Var}(x)$ expresses that $x$ is (a code of) a first-
oder variable.

  * •

The formula $\textnormal{VarSeq}(x)$ expresses that $x$ is (a code of) a
sequence of first-order variables.

  * •

The formula $\textnormal{Term}_{\mathscr{L}}(x)$ expresses that $x$ is (a code
of) a term over the language $\mathscr{L}$.

  * •

The formula $\textnormal{ClTerm}_{\mathscr{L}}(x)$ expresses that $x$ is (a
code of) a closed term over the language $\mathscr{L}$.

  * •

The formula $\textnormal{ClTermSeq}_{\mathscr{L}}(x)$ expresses that $x$ is (a
code of) a sequence of closed terms over the language $\mathscr{L}$.

  * •

The formula $\textnormal{Form}_{\mathscr{L}}(x)$ expresses that $x$ is (a code
of) a formula over the language $\mathscr{L}$.

  * •

The formula $\textnormal{Sent}_{\mathscr{L}}(x)$ expresses that $x$ is (a code
of) a sentence over the language $\mathscr{L}$.

  * •

The formula $\textnormal{FV}_{\mathscr{L}}(x,y)$ expresses that $y$ is (a code
of) a set of free variables of $x$, where $x$ is a term or a formula in
$\mathscr{L}$. In what follows, we will omit the subscript $\mathscr{L}$ and
assume that we have one formula FV which works uniformly for all the relevant
languages.

  * •

The formula $\textnormal{Asn}_{\mathscr{L}}(x,y)$ expresses that $y$ is an
$x$-assignment, i.e. $x$ is (a code of) a term or a formula and $y$ is a
function whose domain contains $\textnormal{FV}_{\mathscr{L}}(x)$. As in the
case of FV, we will omit the mention of the language in the formula Asn.

  * •

If $\alpha,\beta$ are two assignments and $\bar{v}=\langle
v_{1},\ldots,v_{c}\rangle\in\textnormal{VarSeq}$, by
$\beta\sim_{\bar{v}}\alpha$, we mean that
$\textnormal{dom}\beta\supseteq\textnormal{dom}\alpha\cup\\{v_{1},\ldots,v_{c}\\}$
and $\beta(v)=\alpha(v)$ for every
$v\in\textnormal{dom}(\alpha)\setminus\\{v_{1},\ldots,v_{c}\\}.$ If $\bar{v}$
is a sequence of length one of the form $\langle v\rangle$, we will write
$\beta\sim_{v}\alpha$.

  * •

If $t\in\textnormal{Term}_{\mathscr{L}_{\textnormal{PA}}}$ and
$\alpha\in\textnormal{Asn}(t)$, the formula $\textnormal{Val}(t,\alpha,x)$
expresses that $x$ is a formally computed value of $t$ under the assignment
$\alpha$. For instance, if $t=\ulcorner 0+v\times(S0+S0)\urcorner$ and
$\alpha$ is an assignment which sends the variable $v$ to $5$, then
$\textnormal{Val}(t,\alpha,10)$ holds. We will also denote it with
$t^{\alpha}=x$. In the special case when $t$ is a closed term and $\alpha$ is
the empty valuation, we will use the notation $t^{\circ}=x$.

  * •

By $\textnormal{Num}(x,y)$ we mean that $y$ is (a code of) the formal numeral
$S\ldots S0$ of $\mathscr{L}_{\textnormal{PA}}$, where $S$ is iterated $x$
times. We will also denote it with $\underline{x}=y$.

  * •

If $\phi\in\textnormal{Form}_{\mathscr{L}}$ and
$\alpha\in\textnormal{Asn}(\phi)$, then the formula
$\textnormal{SubAsn}(\phi,\alpha,x)$ expresses that $x$ is (a code of) the
sentence resulting by substituting the numeral $\underline{\alpha(v)}$ for
each free variable $v$ in $\phi$. We will also denote it with
$\phi[\alpha]=x$.

  * •

If $\phi\in\textnormal{Form}_{\mathscr{L}}$, then the formula
$\textnormal{dp}(\phi,x)$ expresses that the syntactic depth of $\phi$ is
equal to $x$, where the syntactic depth is the depth of nesting of quantifiers
and connectives in $\phi$ (thus counting the depth of all atomic formulae,
possibly featuring very complex terms, as $0$). We will also denote it with
$\textnormal{dp}(\phi)=x$.

In the article, we will make use of a number of notational conventions.

######  Convention 2.

  * •

We will often suppress formal notation referring to syntactic operations and
write the results of these operations instead. For instance, we will write
$S(\phi\wedge\psi,\alpha)$ rather than "For all $z$, if $z$ is the unique
formula which is a conjunction of $\phi$ and $\psi$, then $S(z,\alpha)$."

  * •

We will use the notions defined with functional expressions such as
$\underline{x},{t}^{\circ},\textnormal{FV}(\phi)$ as if they had a stand-alone
meaning (as if they were terms).

  * •

We will use the expressions such as
$\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}$ or Asn as if they were
denoting sets, e.g., writing
$\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}$ or
$\alpha\in\textnormal{Asn}(\phi)$ (note that in the latter case, we also make
use of the previous convention).

  * •

If
$M\models\textnormal{PA},\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M),\bar{v}\in\textnormal{VarSeq}(M),Q\in\\{\forall,\exists\\}$,
then by $Q\bar{v}\phi$, we mean $Qv_{1}\ldots Qv_{c}\phi$, where
$\bar{v}=\langle v_{1},\ldots,v_{c}\rangle$.

Let us recall some basic definitions and facts about models of PA.

######  Definition 3.

We say that a model $M$ is recursively saturated if every recursive type with
finitely many parametres and variables is satisfied.444Recursive type is the
same thing as a computable type, i.e., a consistent set of formulae which is
computable as a set of Gödel codes. In this article, we stick to the
”recursive” terminology, since it is prevalent in the area of models of
arithmetic. We say that a model $M$ is resplendent if for every recursive
theory Th consistent with $\textnormal{ElDiag}(M)$, $M$ can be expanded to a
model of Th.

The notion of resplendence is clearly very rich in consequences. Thanks to its
link with the recursive saturation, it is also rather easy to meet in nature
(see [9], Theorems 15.7 and 15.8):

######  Theorem 4 (Barwise–Schlipf, Ressayre).

Every countable recursively saturated model in a countable recursive language
is resplendent. Moreover, if $M$ is a countable recursively saturated model
and Th is a countable recursive theory, then we can find an expansion of $M$
to a model of Th which is itself recursively saturated.

Another important feature of recursively saturated models is that they allow
very powerful back-and-forth constructions which are very rich in structural
consequences.

######  Definition 5.

Let $M\models\textnormal{PA}$. By the standard system of $M$, we mean the
family of $X\subseteq\omega$ such that there exists $c\in M$ for which
$X=\\{n\in\omega\ \mid\ M\models n\in_{\textnormal{Ack}}c\\}.$

######  Theorem 6 (Wilmers).

Suppose that $M,N\models\textnormal{PA}$ are recursively saturated models.
Then $M\simeq N$ iff $M\equiv N$ and $M,N$ have the same standard systems.

The result was first obtained by Wilmers in his PhD thesis [18]. The proof may
be found in [9], Theorem 15.2.3, where it is stated in greater generality (for
so called rich theories). For us, the following corollary will be
relevant.555Strictly speaking, the corollary does not follow from Theorem 6 as
stated. However, it readily follows from its proof or from a more general
statement, like Theorem 15.2.3 from [9].

######  Theorem 7.

Let $M\models\textnormal{PA}$ be a recursively saturated model. Suppose that
$a,b\in M$ have the same types. Then there exists an automorphism
$f\in\textnormal{Aut}(M)$ such that $f(a)=b$.

###  2.2 Satisfaction classes

In the literature, there are two concurrent terminological traditions. One of
them speaks of satisfaction classes and is more widespread in the study of
models of arithmetic. The other tradition, which stems from philosophical
logic, tends to formulate results in terms of truth predicates. In deference
to [10], we will follow the former tradition. However, to make our results
easily translatable to the language of truth predicates, we will make sure
that all satisfaction classes which we construct satisfy certain additional
regularity properties.

######  Definition 8.

Let $M\models\textnormal{PA}$ and let
$\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$. Let $S\subset
M^{2}$. We say that $S$ satisfies compositional conditions for $\phi$,
$\textnormal{Comp}(\phi)$ if the disjunction of the following clauses holds in
$(M,S)$:

  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{)}.$

######  Definition 9.

Let $M\models\textnormal{PA}$. We say that a set $S\subset M^{2}$ is a
satisfaction class if there exists
$D\subset\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$ such that:

  * •

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

  * •

If there exists $\alpha$ such that $(\phi,\alpha)\in S$, then
$(M,S)\models\textnormal{Comp}(\phi)$.

  * •

If there exists $\alpha$ such that $(\phi,\alpha)\in S$, then either $\phi\in
D$ or there exists $\psi$ such that $\phi=\neg\psi$ and $\psi\in D$.

  * •

$(M,S)$ satisfies $\textnormal{Comp}(\phi)$ for every $\phi\in D$.

  * •

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

  * •

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

By a domain of $S$, $\textnormal{dom}(S)$, we mean the minimal set
$D\subset\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$ satisfying the
above conditions.666Without the minimality requirement the domain is ”almost”
unique, since it not determined how to treat the formulae which are negations
satisfied under all assignments. If $(\neg\phi,\alpha)\in S$ for all $\alpha$
and $(\neg\neg\neg\phi,\alpha)\notin S$ for any $\alpha$, then we stipulate
that $\phi$ is in the domain of $S$, but $\neg\phi$ is not. We say that a
satisfaction class $S$ decides a formula $\phi$ if for every
$\alpha\in\textnormal{Val}(\phi)$ either $(\phi,\alpha)\in S$ or
$(\neg\phi,\alpha)\in S$. We say that $S$ is a full satisfaction class if
$\textnormal{dom}(S)=M$, i.e., $(M,S)$ satisfies $\textnormal{Comp}(\phi)$ for
every $\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$. We call a
satisfaction class partial if it is not full. A (full or partial) satisfaction
class $S$ is inductive iff $(M,S)$ satisfies the full induction scheme.

######  Remark 10.

Our definition of a satisfaction class agrees with the usual one for full
satisfaction classes and essentially agrees with the usual one for
satisfaction classes defined on the formulae in some initial segment of a
model.

According to the definition proposed above, a satisfaction class is required
to be completely determined about any formula to which it ascribes any
assignments. If $(\phi,\alpha)\in S$, then we fully know for any
$\beta\in\textnormal{Asn}(\phi)$ whether $(\phi,\beta)$ holds or not and the
same holds for the direct subformulae of $\phi$.

Notice that our definition is not very restrictive. Let us introduce a notion
of a pre-satisfaction class: $S$ is a pre-satisfaction class if it satisfies
compositional conditions on a set of formulae $D$ closed under direct
subformulae. Then given such an $S$, we can define a satisfaction class
$S^{\prime}$ such that $S^{\prime}\cap(D\times M)=S\cap(D\times M)$. Indeed,
let $(\phi,\alpha)\in S^{\prime}$ if either $\phi\in D$ and $(\phi,\alpha)\in
S$ or $\phi=\neg\psi$, $\psi\in D$ and $(\psi,\alpha)\notin S$. One can verify
that $S^{\prime}$ defined in such a way is a satisfaction class in our sense,
so we do not lose very much by imposing the "definiteness" conditions.

######  Remark 11.

In Definition 9, we required that satisfaction classes are defined over the
arithmetical language. Of course, nothing prevents us from defining them over
an arbitrary (say, primitive recursive) language $\mathscr{L}$. In such a
case, we have to add the atomic clauses for the new atomic formulae of
$\mathscr{L}$ to the condition $\textnormal{Comp}(\phi)$ and replace every
mention of $\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}$ with
$\textnormal{Form}_{\mathscr{L}}$.

As we have already remarked, there are two concurrent terminological
traditions which speak of essentially the same objects: satisfaction classes
and truth predicates. Unfortunately, these two notions do not translate
directly into each other. Indeed, suppose that $M\models\textnormal{PA}$ and
$S$ is a full satisfaction class on $M$. Then we would like to define a truth
predicate $T$ as follows:

$T=\\{\phi[\alpha]\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(M)\
\mid\ (\phi,\alpha)\in S\\}.$

However, defined in such a way, $T$ is not necessarily a truth predicate.777We
will shortly define what we actually mean by a truth predicate. For the time
being, the reader should think of it as a set of sentences in the sense of a
model which satisfies compositional conditions similar to that of a
satisfaction class, where we require that true quantified statements are
witnessed by (certain) terms. Indeed, take a formula
$\phi(v)\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$ with only one
free variable $v$ and suppose that $(\phi,\alpha)\in S$, where $\alpha$ sends
$v$ to $0$. Then, by definition $T(\phi(0))$ holds. However, notice that
nothing in the definition of the satisfaction class guarantees that
$(\phi(0),\emptyset)\in S$. In fact, one can construct full satisfaction
classes such that both $(\phi,\alpha)$ and $(\neg\phi(0),\emptyset)$ belong to
$S$. Such a class would yield $T(\neg\phi(0))$, contradicting
compositionality.888Such a construction could be performed by an application
of the Enayat–Visser technique which we discuss in this article.

A familiar definition which says that a sentence is true iff it is satisfied
under any assignment works even worse. Again, we can construct models of PA
with full satisfaction classes, $(M,S)$, where for some sentence
$\phi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(M)$ neither
$(\phi,\alpha)\in S$ nor $(\neg\phi,\alpha)\in S$ holds for all $\alpha$ (that
is, the satisfaction predicate may depend nontrivially on the assignments,
even though a formula in question has no free variables). A truth predicate
obtained from such a model with this classical definition would not even
satisfy the compositional condition for the negation.

The question of defining a satisfaction class out of a truth class is slightly
subtler and depends on what exact compositional conditions for the quantifiers
are accepted. One of the common choices requires that quantified sentences are
true if they are witnessed by some term. Thus the compositional axiom for the
existential quantifier looks as follows:

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

If we accept this kind of axioms and set, for instance,

$S=\\{(\phi,\alpha)\in M^{2}\ \mid\ \phi[\alpha]\in T\\}.$

then in general we cannot show that quantifier axioms for the satisfaction
class will hold, since it could happen for a nonstandard
$\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$ that $\exists
v\phi\in T,\phi(0+0)\in T$ and for all $x\in M$, $\phi(\underline{x})\notin
T$. Then the quantifier axiom for $S$ would break down as well. (Recall that
in $\phi[\alpha]$ we substitute for any free variable $v$ the _numeral_ whose
value is $\alpha(v)$.) Whether a satisfaction class can define a truth
predicate with some other, possibly much more complex definition (or vice
versa), seems to be a rather subtle question, but we will not pursue it any
further in this article.

In order to make the statements about truth predicates and satisfaction
classes directly translatable between the two settings, we will impose some
additional technical conditions on the constructed classes. This will not be
important for any results in this article (i.e., they still hold if we do not
make any of these regularity assumptions).

######  Definition 12.

Suppose that $\phi,\psi$ are arithmetical formulae. Let
$\alpha\in\textnormal{Asn}(\phi),\beta\in\textnormal{Asn}(\psi)$. We say that
the pairs $(\phi,\alpha),(\psi,\beta)$ are extensionally equivalent if there
exist two sequences of closed terms $\bar{s},\bar{t}$ such that for each $i$,
${t_{i}}^{\circ}={s_{i}}^{\circ}$, and a formula $\eta$ such that
$\phi[\alpha]=\eta(\bar{s}),\psi[\beta]=\eta(\bar{t})$. If
$(\phi,\alpha),(\psi,\beta)$ are extensionally equivalent, we denote it with
$(\phi,\alpha)\simeq(\psi,\beta)$.

######  Definition 13.

Let $M\models\textnormal{PA}$ and let $S\subset M^{2}$ be a (full or partial)
satisfaction class. We say that $M$ is regular if for any extensionally
equivalent pairs $(\phi,\alpha)\simeq(\psi,\beta)$, $(\phi,\alpha)\in S$ iff
$(\psi,\beta)\in S$.

Regular satisfaction classes are in one-to-one correspondence with
compositional truth predicates satisfying regularity assumptions, so our
results extend to that setting. Let us state this in a more precise manner.

######  Definition 14.

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

  1. 1.

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

  2. 2.

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

  3. 3.

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

  4. 4.

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

  5. 5.

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

  6. 6.

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

  7. 7.

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

  8. 8.

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

Essentially, in our definitions we stipulate that both satisfaction classes
and truth predicates are not sensitive to specific terms, but only see their
values. The following claim can be now easily verified.

######  Proposition 15.

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

We can define a number of other natural regularity properties of satisfaction
or truth classes. Let us introduce one of them which will play a prominent
role in our paper.

######  Definition 16.

Let $M\models\textnormal{PA}$, let $S$ be a satisfaction class, and let
$\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$. We say that the
quantifier correctness property holds for $\phi$ if for all $c\in M$ and all
$\bar{v}\in\textnormal{VarSeq}(M)$ such that $\exists\bar{v}\phi$ is in the
domain of $S$,

$S(\exists\bar{v}\phi,\alpha)\equiv\exists\beta\sim_{\bar{v}}\alpha\
S(\phi,\beta);$

and for all $\bar{v}\in\textnormal{VarSeq}(M)$ such that $\forall\bar{v}\phi$
is in the domain of $S$,

$S(\forall\bar{v}\phi,\alpha)\equiv\forall\beta\sim_{\bar{v}}\alpha\
S(\phi,\beta).$

We say that the quantifier correctness fails for $\phi$ if one of the above
equivalences does not hold for a pair of formulae $\phi,\exists\bar{v}\phi$ or
$\phi,\forall\bar{v}\phi$ which are both in $\textnormal{dom}(S)$.

In other words, quantifier correctness means that $\phi$ satisfies
compositional clauses with respect to blocks of quantifiers. If $S$ is a full
satisfaction class, then the quantifier correctness fails for $\phi$ iff it
does not hold for $\phi$. In the case of partial satisfaction classes the
distinction is nontrivial. For instance, suppose that
$M\models\textnormal{PA}$ is a nonstandard model and $S\subset M^{2}$ contains
only standard arithmetical formulae (on which all satisfaction classes agree).
Then the quantifier correctness will not hold in general, since $S$ does not
contain e.g. $\exists v_{1}\ldots\exists v_{c}0=0$ for nonstandardly long
blocs of quantifiers. On the other hand, this is not yet a failure of the
quantifier correctness for which we require that for some $\alpha$,
$S(\neg\exists v_{1}\ldots\exists v_{c}0=0,\alpha)$ holds.

##  3 Enayat–Visser Lemma

In the article [4] (see also [3]), a method for constructing satisfaction
classes was introduced which proved to be extremely handy, as it allows us to
guarantee that the constructed classes enjoy a number of additional
properties.

However, these applications typically require slight modifications of the
original proof in a way which prevents us from simply quoting the result. One
attempt to present Enayat–Visser construction in a form of a more general
statement has been made by James Schmerl in [16]. Unfortunately, his
formulation, while very elegant, seems (at least to us) rather unsuitable for
the typical applications of the discussed technique. In this section, we try
to present the core of Enayat–Visser argument in a way that allows us to use
it as a (simple) black box.

######  Definition 17.

By an Enayat–Visser class (or EV class) we mean a class $\mathscr{C}$ of pairs
$(M,S)$, where $M$ is a model of some theory $T$ in a language extending
$\mathscr{L}$ and $S\subset M^{2}$ is an $\mathscr{L}$-satisfaction class such
that the following conditions are satisfied:

  1. 1.

For every $(M,S)\in\mathscr{C}$, there exists
$(M^{\prime},S^{\prime})\in\mathscr{C}$ such that $M^{\prime}\succeq M$,
$S^{\prime}\supseteq S$, and the the domain of $S^{\prime}$ contains
$\textnormal{Form}_{\mathscr{L}}(M)$. (Unboundedness.)

  2. 2.

If $(M_{i},S_{i})\in\mathscr{C}$ for $i<\omega$ and for each $i$,
$M_{i}\preceq M_{i+1},S_{i}\subset S_{i+1}$, then
$(M^{\prime},S^{\prime})\in\mathscr{C}$, where
$M^{\prime}=\bigcup_{i<\omega}M_{i},S^{\prime}=\bigcup_{i<\omega}S_{i}$.
(Closure.)

In the paper, we will only focus on the case where
$\mathscr{L}=\mathscr{L}_{\textnormal{PA}}$ is the arithmetical language. Note
that in the definition we do not assume that $\mathscr{C}$ is nonempty.
However, it will be implied by the assumptions of the following theorem, which
encapsulates the core of the Enayat–Visser argument.

######  Theorem 18 (Enayat–Visser Lemma).

Let $\mathscr{C}$ be an Enayat–Visser class, let $M\models T$, and suppose
that there exists $S\subset M^{2}$ such that $(M,S)\in\mathscr{C}$. Then there
exists a model $M^{\prime}\succeq M$ and a full $\mathscr{L}$-satisfaction
class $S^{\prime}\supset S$ such that $(M^{\prime},S^{\prime})\in\mathscr{C}$.

###### Proof.

Fix a model $M\models T$, and a satisfaction class $S$ on $M$ such that
$(M,S)\in\mathscr{C}$. Using the second condition of the definition of
Enayat–Visser classes, we inductively build a chain of models $M=M_{0}\preceq
M_{1}\preceq M_{2}\preceq\ldots$ of length $\omega$ and satisfaction classes
$S_{i}\subset M_{i}$ such that for each $i<j$, $S_{i}\subseteq S_{j}$, the
domain of $S_{i+1}$ contains $\textnormal{Form}_{\mathscr{L}}(S_{i})$, and
$(M_{i},S_{i})\in\mathscr{C}$.

Let $M^{\prime}=\bigcup_{i<\omega}M_{i}$ and let
$S^{\prime}=\bigcup_{i<\omega}S_{i}$. By the third condition in the definition
of Enayat–Visser class, $(M^{\prime},S^{\prime})\in\mathscr{C}$, so it is
enough to verify that $S^{\prime}$ is a full satisfaction class. Since every
$\phi\in\textnormal{Form}_{\mathscr{L}}(M^{\prime})$ is in
$\textnormal{Form}_{\mathscr{L}}(M_{j})$ for some $j$, this implies that
$\phi$ is in the domain of $S_{j+1}$ and, consequently, in the domain of
$S^{\prime}$. ∎

The essence of Enayat–Visser technique is that the unboundedness condition in
the definition of EV is much easier to check than the existence of a full
satisfaction class $S^{\prime}$, since the former can be expressed as a scheme
which in turn allows us to use a compactness argument. We will use this method
in Section 6. Let us add that it would be nice to incorporate this "local"
nature of the argument to the statement of Theorem 18. Unfortunately, it seems
that general enough statements which cover actual applications of the
technique would be somewhat awkward to express.

##  4 Full satisfaction classes and definability

In this section, we will prove that in every countable, recursively saturated
model $M\models\textnormal{PA}$, there exists a full satisfaction class $S$
such that $(M,S)$ is minimal. We will actually demonstrate a more general
result.

######  Theorem 19.

Let $M\models\textnormal{PA}$ be a countable recursively saturated model and
let $A\subset M$ be an arbitrary set. There exists a full satisfaction class
$S\subset M^{2}$ such that $A$ is definable in $(M,S)$ without parametres.

###### Proof.

Let $M\models\textnormal{PA}$ be a countable recursively saturated model. Let
for $a\in M$,

$\eta_{a}=\forall x\underbrace{\Bigl{(}x=x\wedge x=x\wedge\ldots\wedge
x=x\Bigr{)}}_{a\textnormal{ times}}$

and let for $\bar{v}\in\textnormal{VarSeq}(M)$, $\eta_{a,\bar{v}}$ be the
following formula:

$\exists\bar{v}\ \eta_{a}.$

We will construct a satisfaction class such that:

  * •

If quantifier correctness fails for $\phi$, then $\phi=\eta_{a,\bar{v}}$ for
some $a\in A$ and some $\bar{v}\in\textnormal{VarSeq}(M)$ (where we also allow
the trivial block of quantifiers).

  * •

If $a\in A$, then the quantifier correctness fails for $\eta_{a}$.

Let us fix an enumeration $(a_{n})_{n\in\omega}$ of the elements of $M$ and a
cofinal increasing sequence of elements of $M$, $(b_{n})_{n\in\omega}$. We
inductively construct regular satisfaction classes $S_{0}\subseteq
S_{1}\subseteq\ldots\subseteq M$ such that:

  * •

The domain of $S_{n}$ contains exactly the formulae of syntactic depth at most
$b$ for some $b\geq b_{n}$.999Recall that the notion of syntactic depth was
introduced in Definition 1.

  * •

If $a_{n}\in A$, then the quantifier correctness fails for the formula
$\eta_{a_{n}}$.

  * •

If $\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$ is not of the
form $\eta_{a_{i},\bar{v}}$ for some $i\leq
n,\bar{v}\in\textnormal{VarSeq}(M)$, then the quantifier correctness holds for
$\phi$.

  * •

The model $(M,S_{n})$ is recursively saturated.

The inductive steps of the construction are handled via the following lemma:

######  Lemma 20 (Flexibility of quantifier correctness).

Let $M\models\textnormal{PA}$. Let $a,b\in S$ and let $S\subset M$ be a
regular satisfaction class whose domain consists exactly of formulae of
syntactic depth at most $b$. Then there exists an elementary extension
$(M,S)\preceq(M^{\prime},S^{\prime}_{0})$ and a full satisfaction class
$S^{\prime}\supset S^{\prime}_{0}$ such that the quantifier correctness fails
for the formula $\eta_{a}$ and if it fails for $\phi$ according to
$S^{\prime}$, then it fails according to $S_{0}^{\prime}$ or
$\phi=\eta_{a,\bar{v}}$ for some $\bar{v}\in\textnormal{VarSeq}(M^{\prime})$.

The above Lemma can be proved by the Enayat–Visser methods, but the proof
itself turns out to be somewhat complicated when we are trying to provide all
the relevant details which would be rather disruptive for the whole argument.
Therefore we postpone it until Section 6. Let us now finish the proof under
the assumption that the lemma holds. Suppose that we have constructed the set
$S_{n}$. Applying Lemma 20 to the model $(M,S_{n})$ and using its
resplendence, we find a full satisfaction class $S\supseteq S_{n}$ such that
$(M,S)$ is recursively saturated as a structure in the extended language, the
quantifier correctness fails for formulae of the form $\eta_{a_{i}}$ for
$i\leq n+1$ such that $a_{i}\in A$ and holds for all formulae not of the form
$\eta_{a_{i},\bar{v}}$. Finally, we let $S_{n+1}$ be $S$ restricted so that
$\textnormal{dom}(S_{n+1})$ contains exactly the formulae of syntactic depth
at most $b\geq b_{n+1}$, where $b$ is large enough that if the quantifier
correctness fails for $\eta_{a_{i}}$, $i\leq n+1$, then this failure is
already witnessed by the formulae of depth less than $b$. Since this
restriction is definable in $S$, the obtained model $(M,S_{n+1})$ is also
recursively saturated and clearly satisfies all the other requirements of the
inductive construction.

We set $S=\bigcup_{n\in\omega}S_{n}$. Since all $S_{n}$ are compatible
satisfaction classes, and the union of their domains is the whole model, $S$
is a full satisfaction class as well. Finally, we claim that $A$ is definable
in $(M,S)$. Indeed, it is enough to notice that $A$ is precisely the set of
$x$ such that the quantifier correctness fails for the formula $\eta_{x}$. ∎

The following corollary answers Question 9.5 from [3] in the positive.

######  Corollary 21.

Let $M$ be a countable recursively saturated model of PA. Then there exists a
full satisfaction class $S\subset M$ such that every element of $M$ is
definable in $(M,S)$ without parametres.

###### Proof.

Fix any bijection $f:\omega\to M$. This bijection can be coded by a subset of
$M^{2}$. Fix a satisfaction class $S\subset M$ such that $f$ is definable in
$M$. Then every element of $M$ is definable in $(M,S)$, as it is equal to
$f(n)$ for some $n\in\omega$. ∎

######  Corollary 22.

For any countable recursively saturated model $M\models\textnormal{PA}$, there
exists a full satisfaction class $S\subset M$ such that $(M,S)$ has no proper
elementary submodels and no nontrivial automorphisms.

###### Proof.

This follows immediately from the previous corollary. ∎

######  Corollary 23.

In every countable recursively saturated model $M\models\textnormal{PA}$,
there exist continuum many pairwise non-elementary-equivalent full
satisfaction classes.

###### Proof.

Let $M\models\textnormal{PA}$ be countable and recursively saturated. By
inspection of the proof of Theorem 19, we see that there exists a single
formula such that for every subset $A\subseteq M$, there exists a full
satisfaction class $S_{A}\subset M^{2}$ such that $A$ is definable in $(M,S)$
with that formula. Consequently, if $(M,A)$ and $(M,A^{\prime})$ are not
elementarily equivalent, then neither are $(M,S_{A}),(M,S_{A^{\prime}})$. ∎

It is natural to ask whether analogues of Theorem 19 hold also in higher
cardinalities. Unfortunately, we cannot immediately see whether our results
generalise to uncountable models $M\models\textnormal{PA}$, even if we assume
that the said models are, for instance, chronically resplendent. We can prove
a weaker result in the similar vein.

######  Corollary 24.

If $M$ is any model of PA (of an arbitrary cardinality), then for any
$A\subseteq M$, there exists an elementary extension
$(M^{\prime},A^{\prime})\succeq(M,A)$ and a satisfaction class
$S^{\prime}\subset{M^{\prime}}^{2}$ such that $A^{\prime}$ is definable in
$(M^{\prime},S^{\prime})$.

###### Proof.

Take a countable recursively saturated model $(M_{0},A_{0})\equiv(M,A)$. By
applying Theorem 19 to $(M_{0},A_{0})$, we see that the elementary diagram of
$(M,A)$ is consistent with the statement "$A$ is definable from a satisfaction
class $S$ via a formula $\phi$," where $\phi$ is implicitly given in the proof
of the theorem. The corollary follows. ∎

In [17], Theorem 3.3, another result similar to Theorem 19 was obtained.

######  Theorem 25 (Smith).

Let $M\models\textnormal{PA}$ be countable and recursively saturated. Let
$A\subset M$ be such that the expanded structure $(M,A)$ is recursively
saturated. Then there exists a full satisfaction class $S$ over $M$ and
$\phi(v)\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$ such that

$A=\\{x\in M\ \mid\ (\phi(v),\langle v,x\rangle)\in S\\}.$

Moreover, there exists a uniformly definable family of formulae
$(\varepsilon_{a}(v))_{a\in M}$ such that for each $a\notin\omega$, there
exists a satisfaction class $S$ for which

$A=\\{x\in M\ \mid\ (\varepsilon_{a}(v),\langle v,x\rangle)\in S\\}$

By writing $\phi(v)$, we mean that $v$ is a free variable of $\phi$. Notice
that $\langle v,x\rangle$ is an assignment which ascribes the value $x$ to the
only variable of $\phi$. The original proof relied on the $M$-provability
methods. A closely related result obtained via the Enayat–Visser construction
(and thus possibly easier to digest) can be found in [12].

Let us make one final remark. One could be dissatisfied with the fact that the
satisfaction class we have constructed is rather pathological and one could
wonder whether the result would still hold if we restricted our attention to
full satisfaction classes which satisfy the quantifier correctness property.

It seems that while we used some specific pathology, the way we did it is
rather generic. For instance if we require that the constructed class satisfy
the quantifier correctness, we could turn our attention to disjunctions of the
form $\eta_{a}\vee\eta_{a}\vee\ldots\vee\eta_{a}$ and ask for which $a$ all
such disjunctions are true.101010A similar flexibility property was used
independently by Mateusz Łełyk in his unpublished work on Tarski Boundary. If
we additionally require that all sentences true in the sense of some partial
arithmetical $\Sigma_{n}$ predicate are rendered true by our satisfaction
class, we can consider the set of sentences such that for every $c$, the
sentence $\forall v\xi_{a,c}$ is true, where the formulae $\xi_{a,c}$ are
defined inductively via the conditions:

$\displaystyle\xi_{a,0}$ $\displaystyle=$ $\displaystyle v=v\wedge\eta_{a}$
$\displaystyle\xi_{a,b+1}$ $\displaystyle=$ $\displaystyle\forall x_{b}\exists
y_{b}\ (x_{b}=v\wedge y_{b}=v\wedge\xi_{a,b}).$

With just a slightly more complicated proof than the one presented above, one
could show that the formulae $\xi_{a,c}$ are also flexible in the sense that
the set of those $a$ such that $\xi_{a,c}$ is true for all $c$ can be an
arbitrary set.

On the other hand, we always have to expect that full satisfaction classes
display some pathological behaviour, since already such benign principles as
"a finite disjunction is satisfied iff one of the disjuncts is," "truth is
closed under propositional proofs" or "every first-order tautology is true"
already allow us to draw nontrivial conclusions about the arithmetical theory
of the underlying model.111111See [2] for the result on disjunctions and [1]
for the other proofs and an extensive discussion of the Tarski Boundary
programme which investigates this phenomenon.

We conjecture that if a satisfaction class displays some pathological
behaviour, then those pathologies are flexible enough to define any subset of
the model (which will be slightly easier to phrase in terms of truth
predicates, as they are explicitly presented as axiomatic theories).

######  Question 26.

Suppose that $P\supseteq\textnormal{CT}^{-}$ is a finite
$\mathscr{L}_{\textnormal{CT}^{-}}$-theory conservative over PA. Let
$M\models\textnormal{PA}$ be a countable recursively saturated model. Is every
set $A\subset M$ definable in some structure of the form $(M,T)\models P$?

##  5 Satisfaction classes and automorphisms

In the previous section, we have shown that in every countable recursively
saturated model $M\models\textnormal{PA}$ there exists a rigid satisfaction
class, i.e. a satisfaction class $S\subset M$ such that $(M,S)$ admits no non-
trivial automorphisms. A natural question arises whether the opposite result
holds, i.e., whether given a countable recursively saturated model $M$, we can
find a satisfaction class $S$ on $M$ such that
$\textnormal{Aut}(M,S)=\textnormal{Aut}(M)$.

Clearly, if $f\in\textnormal{Aut}(M)$, then for any $a\in M$, the elements $a$
and $f(a)$ have the same arithmetical types. On the other hand, if $a,b\in M$
have the same arithmetical types and $M$ is countable and recursively
saturated, then by Theorem 7, there exists an automorphism
$f\in\textnormal{Aut}(M)$ such that $f(a)=b$. Therefore, it is enough to check
whether there exists a satisfaction class $S$ on $M$ such that for any two
pairs $(\phi,\alpha),(\psi,\beta)$ with the same arithmetical types,
$(\phi,\alpha)\in S$ iff $(\phi^{\prime},\alpha^{\prime})\in S$.121212We are
grateful for this observation to Roman Kossak who also suggested to study
automorphisms and definability properties of satisfaction classes.

One could guess that such a satisfaction class can be easily constructed by an
application of the Enayat–Visser techniques. It is rather surprising that this
intuition is wrong.

######  Theorem 27.

Let $M\models\textnormal{PA}$ and let $S\subset M^{2}$ be a full regular
satisfaction class. Then there exist two pairs
$(\phi,\alpha),(\phi^{\prime},\alpha^{\prime})\in M^{2}$ such that their
arithmetical types are equal, but exactly one of them is in $S$.

The proof will use the following fact:

######  Proposition 28.

Let $M\models\textnormal{PA}$ and let $S\subset M^{2}$ be a regular inductive
partial satisfaction class containing all formulae of standard syntactic
depth. Then there exist two sentences
$\phi,\psi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(M)$ such that
$\textnormal{tp}(\phi)=\textnormal{tp}(\psi)$, but $(\phi,\emptyset)\in
S,(\psi,\emptyset)\notin S$.

Moreover, for any element $a\in M$, there exists a pair of sentences
$\phi,\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}^{\leq 1}(M)$
such that $\textnormal{tp}(\phi,a)=\textnormal{tp}(\psi,a)$, but
$(\phi,\emptyset)\in S,(\psi,\emptyset)\notin S.$131313This Proposition
essentially appears in the second proof of Theorem 1 in [7], attributed to
Woodin, where it is stated and proved in the context of recursively saturated
satisfaction classes, rather than inductive ones. It is also formulated as a
remark in a MathOverflow question,
https://mathoverflow.net/questions/186823/is-there-a-nonstandard-model-of-
arithmetic-having-precisely-one-inductive-truth although the argument seems to
contain a gap. However, it is exactly that remark which inspired the results
in this section. Previously, we expected that a satisfaction class can in fact
have the same automorphism group as the original model.

In the proof below, by an $n$-type of an element $a$, we mean the set of
arithmetical formulae in a single variable of syntactic depth $n$ satisfied by
$a$. We denote the $n$-type of $a$ by $\textnormal{tp}_{n}(a)$. It is easy to
see that over relational languages the set of $n$-types is finite for each
$n$. In this paper, we actually assume that $\mathscr{L}_{\textnormal{PA}}$
contains function symbols. However, we can formulate a relational language,
where each $n$-ary arithmetical function symbol is replaced with an $n+1$-ary
relation symbol and translate every sentence in PA to an equivalent sentence
in that language, so we can indeed assume that for each $n$, the set of
arithmetical $n$-types over PA is finite.

###### Proof.

To prove the first part of the claim, notice that for every $n\in\omega$, it
is expressible in PA that two elements $a,b$ have the same arithmetical
$n$-type. Therefore, for every $n\in\omega$, there exist two sentences
$\phi,\psi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(M)$, such that
$\textnormal{tp}_{n}(\phi)=\textnormal{tp}_{n}(\psi)$, but only one of them is
in $S$, since otherwise $S$ would be arithmetically definable over $M$ (a
sentence would be true according to $S$ if its $n$-type is one of the finitely
many $n$-types which guarantee that the sentence is true).

By overspill, there exists a pair of sentences
$\phi,\psi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(M)$ and a
nonstandard element $c$ such that

$(M,S)\models\forall n\leq c\
S(\textnormal{tp}_{n}(\underline{\phi})=\textnormal{tp}_{n}(\underline{\psi}),\emptyset)\wedge
S(\phi,\emptyset)\wedge\neg S(\psi,\emptyset).$

These sentences $\phi,\psi$ satisfy our requirements.

To prove the "moreover" part, notice that we can consider sentences of the
form $\phi^{a}$ defined as $\underline{a}=\underline{a}\wedge\phi$. Again, for
any $n\in\omega$, there exists a pair of sentences
$\phi^{a},\psi^{a}\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(M)$
such that they have the same $n$-types and exactly one is in $S$, since
otherwise $S$ (and consequently, the elementary diagram of $M$) would be
definable in $M$ over the parameter $a$. Just like in the previous case, we
can find two sentences $\phi^{a},\psi^{a}$ which have the same arithmetical
types, but only one of them is true according to $S$. Finally, observe that
$a$ is definable from both $\phi^{a}$ and $\psi^{a}$, so if
$\textnormal{tp}(\phi^{a})=\textnormal{tp}(\psi^{a})$, it follows that
$\textnormal{tp}(\phi,a)=\textnormal{tp}(\psi,a)$. ∎

Now we are ready to prove Theorem 27. Our argument will make use of the
following fact. Its proof may be found in [12], Theorem 3.

######  Theorem 29.

Suppose that $M\models\textnormal{PA}$ and $S\subseteq M^{2}$ is a regular
full satisfaction class. Then there exists $S^{\prime}\subset M^{2}$ such that
$S^{\prime}$ is a regular inductive satisfaction class whose domain (properly)
contains all formulae of standard syntactic depth.

Moreover, there exists
$\gamma(v)\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$ such that
$S^{\prime}$ is definable in $(M,S)$ with the parameter $\gamma$ via:

$S^{\prime}=\\{(\phi,\alpha)\in M^{2}\ \mid\
\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M),\alpha\in\textnormal{Val}(\phi)\wedge(\gamma(\underline{\phi[\alpha]}),\emptyset)\in
S\\}.$

###### Proof of Theorem 27.

Let $M\models\textnormal{PA}$ and let $S$ be a full satisfaction class on $M$.
Let $S^{\prime}$ be the inductive satisfaction class on $M$ definable from
$(M,S)$ with the parameter $\gamma$, as in Theorem 29.

Let $\phi,\psi\in\textnormal{Sent}_{\mathscr{L}_{\textnormal{PA}}}(M)$ be two
elements such that $(\phi,\emptyset)\in S^{\prime},(\psi,\emptyset)\notin
S^{\prime}$ and $\textnormal{tp}(\phi,\gamma)=\textnormal{tp}(\psi,\gamma)$,
as given by Lemma 28. By definition of $S^{\prime}$, it follows that

$(\gamma(\underline{\phi}),\emptyset)\in
S,(\gamma(\underline{\psi}),\emptyset)\notin S.$

Since $\textnormal{tp}(\phi,\gamma)=\textnormal{tp}(\psi,\gamma)$, it follows
that
$\textnormal{tp}(\gamma(\underline{\phi}))=\textnormal{tp}(\gamma(\underline{\psi}))$,
because substitution is a definable operation. Thus
$(\gamma(\underline{\phi}),\emptyset),(\gamma(\underline{\psi}),\emptyset)$
are the desired pairs. ∎

######  Remark 30.

Actually, the regularity requirement is not needed in Theorem 29 and
consequently in Theorem 27. However, the cited result is formulated in [12] in
the context of $\textnormal{CT}^{-}$, where we automatically assume
regularity, so we decided to leave it as is.

##  6 Flexibility of quantifier correctness

In order to complete the proof of Theorem 19, we need to show that Lemma 20
holds. We restate it for convenience of the reader.

######  Lemma 31.

Let $M\models\textnormal{PA}$. Let $a,b\in S$ and let $S\subset M$ be a
regular satisfaction class whose domain consists exactly of formulae of
syntactic depth at most $b$. Then there exists an elementary extension
$(M,S)\preceq(M^{\prime},S^{\prime}_{0})$ and a full satisfaction class
$S^{\prime}\supset S^{\prime}_{0}$ such that the quantifier correctness fails
for the formula $\eta_{a}$ and if it fails for $\phi$ according to
$S^{\prime}$, then it fails according to $S_{0}^{\prime}$ or
$\phi=\eta_{a,\bar{v}}$ for some $\bar{v}\in\textnormal{VarSeq}(M^{\prime})$.

We will show that a suitable class of models is an Enayat–Visser class. Before
we proceed to the proof, let us introduce one more technical notion.

######  Definition 32.

Let $\phi$ be an arithmetical formula. By a template of $\phi$ we mean the
least formula $\widehat{\phi}$ (with respect to the Gödel code) such that:

  * •

$\phi$ can be obtained by substituting arithmetical terms in $\widehat{\phi}$.

  * •

Every free variable occurs in $\widehat{\phi}$ exactly once.

  * •

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

  * •

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

  * •

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

We say that formulae $\phi,\psi$ are syntactically similar if
$\widehat{\phi}=\widehat{\psi}$. We denote this relation with $\phi\sim\psi.$

Notice that if $\phi(\bar{s})=\eta(\bar{t})$ and $\psi(\bar{q})=\eta(\bar{r})$
for some sequences of terms $\bar{q},\bar{r},\bar{s},\bar{t}$, then
$\phi\sim\psi$. In particular, if $(\phi,\alpha)\simeq(\psi,\beta)$ are
extensionally equivalent, then $\phi$ and $\psi$ are syntactically similar,
but the reverse implication does not hold.

######  Example 33.

Let $\phi=\exists x\forall y\Big{(}x+(x\times 0)=(y\times
v)+(v\times(w+0))\Big{)}.$ Then

$\widehat{\phi}=\exists x\forall y\Big{(}x+(x\times v_{0})=(y\times
v_{1})+v_{2}\Big{)},$

where $v_{0},v_{1},v_{2}$ are chosen so as to minimise the Gödel code of
$\widehat{\phi}$. Let $\alpha$ be an assignment which sends $v$ to $17$ and
$w$ to $2$. Let $\beta$ be an assignment which sends $v_{0}$ to $0$, $v_{1}$
to $17$ and $v_{2}$ to $34$. Then $(\phi,\alpha)\simeq(\widehat{\phi},\beta)$.

Now, we can introduce the Enayat–Visser class relevant for Lemma 20.

######  Lemma 34.

Let $M\models\textnormal{PA}$, $a,b\in M$, and let $T\subset M$ be a regular
satisfaction class whose domain contains exactly the formulae of syntactic
depth $\leq b$. Then the class $\mathscr{C}$ is an Enayat–Visser class, where
$\mathscr{C}$ consists of the pairs $((N,P),S)$ such that:

  * •

$(N,P)\succeq(M,T)$.

  * •

$S\supset P$ is a regular satisfaction class (over
$\mathscr{L}_{\textnormal{PA}}$).

  * •

The quantifier correctness fails for $\eta_{a}$.

  * •

If the quantifier correctness fails for a formula $\phi$ according to $S$,
then it fails according to $P$ or there exists
$\bar{v}\in\textnormal{VarSeq}(N)$ such that $\phi=\eta_{a,\bar{v}}$.

  * •

For every $\phi\in\textnormal{dom}(S)$, if $\phi=Q\bar{v}\psi$ for some
$\bar{v}\in\textnormal{VarSeq}(N)$ and $\psi$ does not begin with $Q$, then
$\psi\in\textnormal{dom}(S).$

The last condition is technical. It clearly holds for satisfaction classes
which are defined exactly on formulae from an elementary submodel, which is
exactly what we will get in our construction. Notice that if the lemma holds,
then applying Theorem 18 to the class $\mathscr{C}$ defined above, we conclude
that $\mathscr{C}$ contains a model with a full satisfaction class. We can
then readily verify that such a model satisfies the claim of Lemma 31. So it
is enough to prove that $\mathscr{C}$ is indeed an Enayat–Visser class.

###### Proof.

Fix a model $M\models\textnormal{PA}$, elements $a,b\in M$, and a satisfaction
class $T$ on $M$ whose domain consists exactly of formulae of depth $\leq b$.
We will show that the class $\mathscr{C}$ defined with respect to this model
is an EV-class containing some pair $((M^{\prime},T^{\prime}),S)$. It is easy
to check that $\mathscr{C}$ is closed under unions of chains. It is enough to
observe that if a failure of quantifier correctness is witnessed by a pair of
formulae in a satisfaction class $S$, then it is also witnessed in any
$S^{\prime}$ containing $S$. On the other hand, if quantifier correctness
fails in a union of a chain of satisfaction classes, then this failure has to
be witnessed in one of the models.

We will check the unboundedness condition and explain how the argument can be
modified to show the existence of an elementary extension
$(M^{\prime},T^{\prime})\succeq(M,T)$ and a satisfaction class $S$ in that
extension such that the pair $((M^{\prime},T^{\prime}),S)$ belongs to
$\mathscr{C}$. In what follows, we will identify pairs $((X,Y),Z)$ with
triples $(X,Y,Z)$.

Fix a tuple $(N,P,S)\in\mathscr{C}$ or $(N,P,S)=(M,T,T)$ (to find any
$(M^{\prime},T^{\prime},S)\in\mathscr{C}$ witnessing its nonemptiness). We
will find $(N^{\prime},P^{\prime},S^{\prime})\in\mathscr{C}$ such that
$(N,P)\preceq(N^{\prime},P^{\prime})$, $S^{\prime}\supseteq S$ is a
satisfaction class, and the domain of $S^{\prime}$ contains
$\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(N)$. We will say that a
formula $\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(N)$ is
unproblematic if $\phi$ is not in the domain of $P$ and $\phi$ is not of the
form $\eta_{a,\bar{v}}$ for any $\bar{v}\in\textnormal{VarSeq}(N)$. The
structure $(N^{\prime},P^{\prime},S^{\prime})$ will be obtained as a model of
the theory $\Theta$ with the following axioms:

  * •

The elementary diagram of $(N,P)$, where the predicate $P$ is replaced with
$P^{\prime}$.

  * •

$\textnormal{Comp}(\phi),\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$
(The compositionality scheme for $S^{\prime}$.)

  * •

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

  * •

$S^{\prime}(\phi,\alpha)$ for all $(\phi,\alpha)\in S.$ (The compatibility
scheme.)

  * •

$\forall x,y\ P^{\prime}(x,y)\rightarrow S^{\prime}(x,y).$

  * •

$\forall\alpha\in\textnormal{Asn}(Q\bar{v}\phi)\
\Big{(}S^{\prime}(Q\bar{v}\phi,\alpha)\equiv Q\beta\sim_{\bar{v}}\alpha\
S^{\prime}(\phi,\beta)\Big{)}$, where
$Q\in\\{\forall,\exists\\},\bar{v}\in\textnormal{VarSeq}(M),\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$
and $\phi$ is unproblematic. (The quantifier correctness scheme.)

In the initial step, when $(N,P,S)=(M,T,T)$, we additionally pick two
sequences $\bar{w},\bar{w^{\prime}}\in\textnormal{VarSeq}(M)$ such that
$\bar{w}\lhd\bar{w^{\prime}}$ ($w$ is an initial segment of $w^{\prime}$) and
the differences $|\bar{w}|-b$, $|\bar{w^{\prime}}|-|\bar{w}|$ are nonstandard,
where $|\bar{w}|$, $|\bar{w^{\prime}}|$ are the lengths of the respective
sequences. We add the following axioms to $\Theta$:

  * •

$S^{\prime}(\eta_{a,\bar{w}},\emptyset).$

  * •

$\neg S^{\prime}(\eta_{a,\bar{w^{\prime}}},\emptyset)$.

This guarantees that the quantifier correctness fails for $\eta_{a}$. The
requirement on the length of $\bar{w}$ is to guarantee that the syntactic
depth of $\eta_{a,\bar{w}}$ is high enough that the formula is not in the
domain of $T$.

If we take any model $(N^{\prime},P^{\prime},S^{\prime})\models\Theta$ and
restrict the predicate $S^{\prime}$ to the formulae
$\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(N^{\prime})$ whose
syntactic templates $\widehat{\phi}$ are in
$\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(N)$ (i.e., they essentially
come from the original model), we obtain a model in $\mathscr{C}$
(compositionality and "non-failure" of quantifier correctness are easy to
verify; the closure conditions on the domain follow automatically by
elementarity and regularity). Therefore, it is enough to check that $\Theta$
is consistent which we will verify by a compactness argument. Let
$\Theta_{0}\subset\Theta$ be a finite subtheory. We will find a subset
$S^{\prime}\subset N$ such that $(N,S^{\prime})$ satisfies $\Theta_{0}$.

We introduce another technical notion which will be useful in this proof: if
$\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(N)$ begins with a
quantifier $Q$, then by its root, we mean the unique formula $\psi$ such that
$\phi=Q\bar{v}\psi$ for some $\bar{v}\in\textnormal{VarSeq}(M)$ and one of the
following holds:

  * •

$\psi$ has syntactic depth $b$.

  * •

There is no formula satisfying the first condition and $\psi$ does not begin
with a quantifier $Q$.

Let $\Gamma_{0}$ be the (finite) set of formulae that appear under the
satisfaction predicate $S^{\prime}$ in the theory $\Theta_{0}$. Let
$\phi_{1},\ldots,\phi_{n}$ be an enumeration of formulae from $\Gamma_{0}$ and
their roots (notice that we do not _close_ $\Gamma_{0}$ under taking roots; we
apply the operation only once). Without loss of generality, we can assume that
$\eta_{a,\bar{w}},\eta_{a,\bar{w^{\prime}}}$ are among $\phi_{i}$. (This will
play any role only in the "initial step.") Consider the equivalence classes
$[\phi_{i}]_{\sim}$ under the syntactic similarity relation $\sim$. We will
construct $S^{\prime}$ by induction on the following relation $\lhd$:
$[\phi]\lhd[\psi]$ iff there exist
$\phi^{\prime}\in[\phi],\psi^{\prime}\in\psi$ such that at least one of the
following conditions holds:

  * •

$\phi^{\prime}$ is a direct subformula of $\psi^{\prime}$.

  * •

$\phi^{\prime}$ is unproblematic, there exists a sequence
$\bar{v}\in\textnormal{VarSeq}(N)$ and $Q\in\\{\forall,\exists\\}$ such that
$\psi^{\prime}=Q\bar{v}\phi^{\prime}$, and there is no $\bar{w}\unlhd\bar{v}$
such that $\psi^{\prime}=Q\bar{w}\eta$, where $[\eta]=[\phi_{i}]$ for some
$i\leq n$.

The second condition is somewhat lengthy, but the idea is simple: we are
allowed to make jumps over nonstandard blocks of quantifiers, but the relation
$\lhd$ only holds for formulae linked by the shortest such jump. We could lift
that restriction, but this would make some later parts of the proof awkward to
express.

We construct $S^{\prime}$ as a union of a sequence of sets $S_{j}$ which we
define by induction on the rank in the relation $\lhd$. The rank of a class
$[\phi]$ is defined in a familiar way by the following equality:

$\textnormal{rk}([\phi])=\sup\\{\textnormal{rk}([\phi_{i}])\ \mid\ i\leq
n\wedge[\phi_{i}]\lhd[\phi]\\}.$

When showing the unboundedness of $\mathscr{C}$, we set:

$S_{0}=S.$

In this step, we are implicitly dealing with both the formulae from the domain
of $S$ and the formulae $\phi$ whose class $[\phi]$ is $\lhd$-minimal. We
implicitly make every such formula false under all assignments, since for such
$\phi$ there is no $\alpha\in\textnormal{Asn}(\phi)$ such that
$(\phi,\alpha)\in S_{0}$ (and it will remain so throughout the whole
construction). Without loss of generality, we assume that $S$ contains all
atomic formulae, i.e., equalities of terms, so they are also covered in this
step.

When dealing with $(N,P,S)=(M,T,T)$, we instead define $S_{0}$ as the set of
$(\phi,\alpha)$ such that one of the following conditions holds:

  * •

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

  * •

There exists a sequence $\bar{v}\in\textnormal{VarSeq}$ of a standard length
$k\in\omega$ (possibly $k=0$) such that $\eta_{a,\bar{w}}=\exists\bar{v}\phi$
(and $\alpha\in\textnormal{Asn}(\phi)$ is arbitrary).

The second condition guarantees that the sentence $\eta_{a,\bar{w}}$ which we
picked when we were defining the theory $\Theta$ will indeed be rendered true
(by construction, the sentence $\eta_{a,\bar{w^{\prime}}}$ and its direct
subformulae will be rendered false).

We extend $S_{j}$ to $S_{j+1}$ so that the compositional conditions and
quantifier correctness hold. More specifically, we define $S_{j+1}$ as a union
of $S_{j}$ and the $(\phi,\alpha)$ such that $\textnormal{rk}([\phi])=j+1$ and
one of the following conditions holds:

  * •

For some $\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(N)$,
$\phi=\neg\psi$ and $(\psi,\alpha)\notin S_{j}$.

  * •

For some $\psi,\eta\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(N)$,
$\phi=\psi\vee\eta$ and $(\psi,\alpha)\in S_{j}$ or $(\eta,\alpha)\in S_{j}$.

  * •

For some $\psi,\eta\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(N)$,
$\phi=\psi\wedge\eta$ and both $(\psi,\alpha)\in S_{j}$ and $(\eta,\alpha)\in
S_{j}$.

  * •

For some
$\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(N),v\in\textnormal{Var}$,
$\phi=\exists v\psi$ and there exists $\beta\sim_{v}\alpha$ such that
$(\psi,\beta)\in S_{j}$.

  * •

For some
$\psi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(N),v\in\textnormal{Var}$,
$\phi=\forall v\psi$ and for all $\beta\sim_{v}\alpha$, $(\psi,\beta)\in
S_{j}$.

  * •

There exists $\bar{v}\in\textnormal{VarSeq}(N)$ and an unproblematic $\psi$
such that $\phi=\exists\bar{v}\psi$, $[\psi]=[\phi_{i}]$ for some $i$,
$\textnormal{rk}([\psi])=j$, and there exists $\beta\sim_{\bar{v}}\alpha$ such
that $(\psi,\beta)\in S_{j}$.

  * •

There exists $\bar{v}\in\textnormal{VarSeq}(N)$ and an unproblematic $\psi$
such that $\phi=\forall\bar{v}\psi$, $[\psi]=[\phi_{i}]$ for some $i$,
$\textnormal{rk}([\psi])=j$, and for all $\beta\sim_{\bar{v}}\alpha$,
$(\psi,\beta)\in S_{j}$.

Since there are only finitely many classes $[\phi_{i}]$, there exists $j$ such
that $S_{j}=S_{j+1}$. We define $S^{\prime}$ as this last set in our
construction. We now have to check that the constructed predicate satisfies
the finite subtheory $\Theta_{0}\subset\Theta$.

Obviously, $(N,P,S^{\prime})$ sastisfies the elementary diagram of $(N,P)$,
$S^{\prime}$ satisfies all the instances of the compatibility scheme and it
extends $P$.

Let us now check that if we consider the case where $(N,P,S)=(M,T,T)$, then
indeed $\eta_{a,\bar{w}}$ is rendered true and $\eta_{a,\bar{w^{\prime}}}$ is
false. For either of the formulae, this is clear if its class is
$\lhd$-minimal. If $\textnormal{rk}[\eta_{a,\bar{w}}]=j>0$, then since
$\eta_{a,\bar{w}}$ is problematic, this means that the classes
$[\eta_{a,\bar{u_{1}}}],\ldots[\eta_{a,\bar{u_{j}}}]$ are among $[\phi_{i}]$,
where $\eta_{a,\bar{u_{k}}}$ is the formula obtained from $\eta_{a,\bar{w}}$
by removing the outermost $k$ quantifiers. Moreover, $[\eta_{a,\bar{u_{j}}}]$
is a minimal class. By construction, the formula $\eta_{a,\bar{u_{j}}}$ is
satisfied under all assignments. Then using compositional conditions, we can
check by induction that all the other formulae $\eta_{a,\bar{u_{j}}}$ are
satisfied under all assignments. The proof for $\eta_{a,\bar{w^{\prime}}}$ is
analogous, but now we consider the formulae $\eta_{a,\bar{u^{\prime}_{k}}}$
obtained by removing the outermost $k$ quantifiers from
$\eta_{a,\bar{w^{\prime}}}$. By construction, the minimal formula
$\eta{a,\bar{u^{\prime}_{j}}}$ is not satisfied under any assignment and we
check that the same holds for all $\eta_{a,\bar{u^{\prime}_{k}}}$ by induction
using the compositional conditions.

The set $S^{\prime}$ satisfies all the instances of the compositionality
scheme from $\Theta_{0}$ by construction and the compositionality of
$S^{\prime}$. Note that there is no conflict between defining $S_{0}$ to
simply contain $S$ and further extending it by compositional conditions, since
compositional clauses determine uniquely the behaviour of $S$ on a given
formula given the behaviour on its subformulae.

The quantifier correctness scheme is handled similarly. We have to check that
there is no conflict between the definition of $S_{0}$ and how it was extended
in the further steps. If $Q\bar{v}\phi$ is in the domain of $S$ and $\phi$ is
unproblematic, then the root of $Q\bar{v}\phi$ is a subformula of $\phi$
(possibly not proper) and by assumption it is in the domain of $S$. Therefore,
we can check by induction on rank that $S^{\prime}$ is defined both on $\phi$
and $Q\bar{v}\phi$ by applying the quantifier correctness clause to a formula
in the domain of $S$. (The assumption that $T$ is defined exactly on formulae
of depth $\leq b$ guarantees that the definition of the root makes sense).

Regularity holds for $S_{0}$ by the assumption on $S$ in the proof that
$\mathscr{C}$ is unbounded. In the case where $(N,P)=(M,T)$, we use the
assumption that $T$ is regular and the fact that the similarity classes of
formulae $\eta_{a,\bar{v}}$ are singletons (by definition of these specific
formulae). Then we show by induction that the regularity holds for all other
sets $S_{j}$. First, observe that for every class $[\phi]$ or rank $j+1$, the
predicate $S_{j+1}$ is defined using the same condition for every formula
$\phi^{\prime}\in[\phi]$, which follows by definition of syntactic similarity
(all similar formulae have the same syntactic tree) and the fact that either
all formulae in $[\phi]$ are problematic or none is (which, in turn, depends
on the definition of $\eta_{a}$ and the assumption that the domain of $P$
includes exactly the formulae of depth $b$). Then the claim follows, since
applying the same compositional or quantifier correctness clause to all
formulae in a class $[\phi]$ preserves regularity. This concludes the proof. ∎

The proof of Lemma 34 will still be valid if we ignore the mention of the
formulae $\eta_{\bar{u}}$ and require that the quantifier correctness holds
for every formula.

######  Corollary 35.

Let $M\models\textnormal{PA}$ be countable and recursively saturated. Then
there exists a regular full satisfaction class $S\subset M^{2}$ such that
every formula $\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}(M)$
satisfies the quantifier correctness.

We can formulate quantifier correctness as a pair of axioms for the
compositional truth in a natural way as follows:

$\forall\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}\forall\langle
v_{1},\ldots,v_{c}\rangle\in\textnormal{VarSeq}\ \Big{(}T\exists
v_{1}\ldots\exists
v_{c}\phi\equiv\exists\alpha\in\textnormal{Asn}(\phi)T\phi[\alpha]\Big{)}.$
$\forall\phi\in\textnormal{Form}_{\mathscr{L}_{\textnormal{PA}}}\forall\langle
v_{1},\ldots,v_{c}\rangle\in\textnormal{VarSeq}\ \Big{(}T\forall
v_{1}\ldots\forall
v_{c}\phi\equiv\forall\alpha\in\textnormal{Asn}(\phi)T\phi[\alpha]\Big{)}.$

Then by the previous observation, we conclude that the following holds:

######  Corollary 36.

The theory $\textnormal{CT}^{-}+$ "the quantifier correctness holds for all
formulae" is conservative over PA.

The above two corollaries were essentially proved by Enayat and Visser as
Theorem 6.1 in [3].141414Note that the formulation in [3] includes a claim
that we can elementarily extend an arbitrary model $M\models\textnormal{PA}$
to a one with a satisfaction class which is disjunctively correct. Now we know
that this part of the theorem is false. The crucial gap is that if $\phi\in M$
is a disjunction over a nonstandard set of formulae, it may have new disjuncts
when considered in an elementary extension of $M$. The quantifier correctness
part (called by the authors ”existential correctness”) is essentially proved
with the same argument as the one presented here. However, the reader should
be aware that certain, small and harmless, gaps can be found in the original
presentation which originate from ignoring the possibility that quantifier
blocks from a model $M$ may have new prefixes when considered in its
elementary extension.

## Acknowledgements

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

## References

  * [1] Cezary Cieśliński.  The Epistemic Lightness of Truth. Deflationism and its Logic.  Cambridge University Press, 2017.
  * [2] Ali Enayat and Fedor Pakhomov.  Truth, disjunction, and induction.  Archive for Mathematical Logic, 58:753–766, 2019.
  * [3] Ali Enayat and Albert Visser.  Full satisfaction classes in a general setting, 2012.
  * [4] 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.
  * [5] Petr Hájek and Pavel Pudlák.  Metamathematics of First-Order Arithmetic.  Springer-Verlag, 1993.
  * [6] Volker Halbach.  Axiomatic Theories of Truth.  Cambridge University Press, 2011.
  * [7] Joel David Hamkins and Ruizhi Yang.  Satisfaction is not absolute.  Review of Symbolic Logic, 7(1):1–34, 2014.
  * [8] Matt Kaufmann.  A rather classless model.  Proceedings of American Mathematical Society, 62(2):330–333, 1977\.
  * [9] Richard Kaye.  Models of Peano Arithmetic.  Oxford: Clarendon Press, 1991.
  * [10] Roman Kossak.  A note on satisfaction classes.  Notre Dame Journal for Formal Logic, 25(1):1–8, 1985.
  * [11] Roman Kossak and James Schmerl.  Minimal satisfaction classes with an application to rigid models of Peano arithmetic.  Notre Dame Journal of Formal Logic, 32:392–398, 1991.
  * [12] Roman Kossak and Bartosz Wcisło.  Disjunctions with stopping condition.  To appear in The Bulletin of Symbolic Logic.
  * [13] Henryk Kotlarski, Stanisław Krajewski, and Alistair Lachlan.  Construction of satisfaction classes for nonstandard models.  Canadian Mathematical Bulletin, 24:283–93, 1981.
  * [14] Alistair H. Lachlan.  Full satisfaction classes and recursive saturation.  Canadian Mathmematical Bulletin, 24:295–297, 1981.
  * [15] Abraham Robinson.  On languages based on non-standard arithmetic.  Nagoya Mathematical Journal, 22:83–107, 1963.
  * [16] James Schmerl.  Kernels, truth, and satisfaction.  Bulletin of the Polish Academy of Sciences, 67(1):31–35, 2019.
  * [17] Stuart T. Smith.  Nonstandard definability.  Annals of Pure and Applied Logic, 42(1):21–43, 1989.
  * [18] George Wilmers.  Some problems in set theory: non-standard models and their application to model theory., 1975.


# Interpretable 2D Vision Models for 3D Medical Images

###### Abstract

Training Artificial Intelligence (AI) models on 3D images presents unique
challenges compared to the 2D case: Firstly, the demand for computational
resources is significantly higher, and secondly, the availability of large
datasets for pre-training is often limited, impeding training success. This
study proposes a simple approach of adapting 2D networks with an intermediate
feature representation for processing 3D images. Our method employs attention
pooling to learn to assign each slice an importance weight and, by that,
obtain a weighted average of all 2D slices. These weights directly quantify
the contribution of each slice to the contribution and thus make the model
prediction inspectable. We show on all 3D MedMNIST datasets as benchmark and
two real-world datasets consisting of several hundred high-resolution CT or
MRI scans that our approach performs on par with existing methods.
Furthermore, we compare the in-built interpretability of our approach to
HiResCam, a state-of-the-art retrospective interpretability approach.

##  1 Introduction

Most computer vision applications focus on 2D image analysis, such as
photographs. Medical imaging, in contrast, stands out by capturing primarily
3D images through techniques like computed tomography (CT) or magnetic
resonance imaging (MRI). Adapting existing 2D models to 3D data is not
straightforward, as it poses challenges in obtaining high-quality pre-trained
weights from large datasets [1]. Additionally, training 3D models requires
significantly more computational and memory resources compared to their 2D
counterparts [2]. In response to these considerations, researchers have
explored 2.5D architectures as a compromise, aiming to combine the benefits of
strong pre-training with reasonable computational requirements while
leveraging the inherent nature of 3D volumes. These 2.5D architectures often
rely on recurrent neural networks (RNN) [3], e.g. long and short term memory
units (LSTM) [4].

Despite their strong performance, deep learning models are often criticised as
black-boxes, where only input and output are observed, but the internal
connections remain obscure. To address this concern, interpretability methods
have been developed, most prominently Grad-CAM and its successors, which allow
for the retrospective inspection of these connections [5, 6]. Another line of
work in this direction was the introduction of attention mechanisms. Initially
developed for natural language processing, attention mechanisms have also
demonstrated impressive performance in vision tasks [7]. These approaches are
based on the intuition of learning what is important and thus prioritising the
influence of more relevant input on the model’s prediction. Attention
mechanisms have also been extended to improve pooling operations [8], which
are commonly applied as a maximum or averaging operation over large inputs in
neural networks.

Fig. 1: Overview of our approach. (A) The 3D image gets disassembled into
slices along all axes. (B) Using the feature extractor from a 2D model each
slice obtains a feature representation. (C) Based on the features an attention
map is predicted, which assigns importance scores, which sum up to one to the
slices. The slice features are multiplied by their attention score. (D) The
weighted slice features are summed into a single feature vector. This is used
as input for the classifier. Example image stems from the MSD Liver dataset
[9]

In this study, we propose a conversion strategy for arbitrary 2D models with
intermediate feature representations for 2.5D architectures. Our method offers
several distinct advantages. Firstly, it is lightweight and only introduces a
minimal increase in parameters. Secondly, our approach allows for the
utilisation of strong pre-trained weights that are available for 2D
architectures. Thirdly, we implicitly generate an attention map during the
forward pass, which allows for the attribution of individual slices to the
final prediction. Opposed to retrospective methods, such as Grad-CAM [5], we
obtain this attribution for free during the forward pass. Furthermore, we
obtain quantifiable importance measures, not indirectly derived by inspecting
gradients, but directly used for the prediction. This leads to an inherent
interpretability of our method. Our experiments demonstrate the efficacy of
our method in both, model performance and prediction interpretability. Our
code is available at https://github.com/TUM-AIMED/2.5DAttention.

There exist several lines of work, which utilise 2.5D architecture designs. We
discuss here the two most relevant. Yang et al. [1] developed methods to make
pre-trained 2D architectures applicable to 3D images. They apply 2D
convolutional filters along all three axes and thus create an artificial 3D
kernel called ACS-convolution. Similar to our approach, this allows them to
re-use information learned in the 2D domain while keeping the number of
parameters almost constant. The work by Li et al. [10] combines 2D neural
networks as feature extractors with transformer blocks for lesion detection.
This allows them to learn the attention over all slices of the 3D input and
combine them into a single representation. There are numerous methods to
quantify inputs’ contribution to a model’s output. Most prominently, we note
Grad-CAM [5] and its successors, such as HiResCam [6]. However, most of them
are based on an indirect retrospective inspection of a trained model. Using
attention pooling yields such a contribution quantification directly during
the forward pass, making predictions inherently interpretable.

In this work, we introduce an intuitive and versatile approach for converting
2D to 2.5D models for 3D image analyses:

  * •

We propose a framework that adapts a 2D network for 3D tasks through slice-
wise feature extraction and attention-pooling aggregation.

  * •

We demonstrate the effectiveness of our approach on several benchmark datasets
as well as two real-world datasets and show that it performs on par with
previous methods.

  * •

We demonstrate the inherent interpretability of our method and compare it to
HiResCam as a retrospective state-of-the-art interpretability method.

By this, we hope to contribute towards high-performing and interpretable AI
for medical image analysis.

##  2 Methods

We leverage the prevalent structure commonly found in deep learning
architectures, which consists of a feature extraction module followed by a
classifier. Building on this pattern, we decompose the 3D image into 2D slices
along all axes. These individual slices are then fed into the feature
extraction component of the 2D network, resulting in the retrieval of $H+W+D$
feature representations, where $H$ represents the height, $W$ the width, and
$D$ the depth of the 3D image. To consolidate these feature representations
into a single comprehensive unit, we employ attention pooling.

Attention pooling utilises a Multihead Attention layer [11], which takes
query, key, and value inputs. Following the suggestion by Radford et al. [8],
we employ the mean of all slice features as the query, while the key and value
comprise the complete set of features. By doing so, our network is capable of
estimating the importance of each feature and generating a weighted
combination of the input features that best represents the input scan for a
given task. This approach generates attention maps during the forward pass,
providing insights into the contribution of each individual slice to the final
feature representation. The resultant aggregated feature representation is
then fed into the classification layer for prediction. For a visualization of
this process compare also Figure 1.

By adopting this framework, we aim to merge the inherent advantages of both 2D
and 3D architectures, leveraging the strong pre-training available for 2D
models while processing the complete 3D volumes. The attention pooling
mechanism not only facilitates feature reduction but also implicitly generates
attributable predictions through the attention maps. These attention maps
quantify the contribution of individual slices to the overall feature
representation, aiding in the comprehension of the decision-making process of
our model.

##  3 Results

###  3.1 Datasets

We use all 3D datasets from MedMNIST [12], which stem from real-world medical
datasets that have been pre-processed and standardised to a resolution of
$28\times 28\times 28$ to be used as benchmark problems. They represent
diverse medical AI problems and present distinct challenges. For more details,
we refer to [12].

| Method |  | MedMNIST 3D | PDAC | Glioma
---|---|---|---|---|---
|  | Organ | Nodule | Fracture | Adrenal | Vessel | Synapse
[1] | 3D-Conv | AUROC | 96.5% | 58.1% | 57.9% | 80.7% | 92.3% | 61.9% | 99.8% | 90.5%
ACC | 77.8% | 74.0% | 43.4% | 79.9% | 93.8% | 66.1% | 98.6% | 85.1%
ACS-Conv | AUROC | 99.2% | 79.0% | 58.1% | 79.1% | 84.3% | 61.5% | 100% | 93.2%
ACC | 89.7% | 81.9% | 43.8% | 80.1% | 91.0% | 71.1% | 99.8% | 87.9%
Ours | AttentionPool | AUROC | 99.5% | 82.3% | 58.8% | 80.9% | 91.4% | 74.3% | 99.1% | 93.3%
ACC | 92.0% | 83.9% | 42.7% | 78.9% | 91.8% | 75.5% | 98.6% | 86.8%
Table 1: Results of all approaches on various datasets. AUROC: area under the
receiver-operator curve, ACC: classification accuracy. All experiments were
performed five times and the mean result is reported.  Fig. 2: Boxplots of the
AUROC for the different MedMNIST3D datasets and the different approaches.

To showcase the clinical applicability of our approach, we incorporate an
internal dataset of 1625 full-resolution abdominal CT scans, classifying the
presence of pancreatic ductal adenocarcinoma (PDAC). Out of the total dataset,
867 patients are diagnosed with a tumour by a panel of medical experts, while
the remaining 758 CT scans are obtained from patients with diagnoses unrelated
to the pancreas, serving as the control group. All images encompass the
relevant body regions and are acquired following the same imaging protocol. We
split this dataset into 975 CTs as train images and 325 for validation and
testing each. We ensure that the distribution of classes in each subset is
approximately equal. Additionally, all CT scans are resized to a standardised
resolution of $224\times 224\times 128$ voxels and clipped to an abdominal
window of $(-150,250)$ Hounsfield units.
As a second clinically relevant real-world dataset, we classify glioma tumour
subtypes from preoperative brain MRI scans. We use three publicly available
datasets: UCSF [13], EGD [14] and TCGA [15], of which the first two are taken
for training, and the latter is held out as an external test set. Of the total
of 1173 patients, 849 are diagnosed with glioblastoma multiforme (GBM), and
the rest have other subtypes, boiling down the task into an unbalanced binary
prediction. We split the training cohort into 767 train and 192 validation
patients, maintaining the class distribution. The test cohort contains 214
patients with 139 GBMs. For each patient, we use three 3D MRI scans, i.e.,
T1-weighted, T1-contrast-enhanced and T2-weighted fluid-attenuated inversion
recovery (FLAIR) images. All images are co-registered, resampled to the 1-mm
isotropic resolution, and cropped into $96\times 96\times 96$ voxels around
the center of mass of the tumour computed using segmentation labels obtained
with BraTS Toolkit [16]. As the images are registered, we stack all modalities
into a tensor with multiple channels.

Approach | Params (Mio) | Memory (MiB) | Time (s)
---|---|---|---
3D | 33.2 | 15821 | 744.1$\pm$0.21
ACS | 11.2 | 14475 | 222.7$\pm$29.4
Ours | 12.2 | 19091 | 434.3$\pm$0.45
Table 2: Computational requirements on the PDAC dataset. Params: number of
trainable model parameters in million. Memory: memory consumption in Mebibyte
on a GPU. Time: mean and standard deviation of one epoch in seconds.

###  3.2 Setup

For our experiments, we adopted a ResNet-18 [17] as the base architecture.
Consistent with the approach by Yang et al. [12], we employed the framework by
the same authors [1] to convert the model into 3D and ACS form. We note that
in all conversions pre-trained weights from ImageNet are utilised and
converted. For the attention pooling, we employed eight heads. All our models
were trained for 50 epochs, using the NAdam optimiser [18], which almost
eliminates the need to tune the learning rate. We used a learning rate of
$2\cdot 10^{-4}$ and a batch size of 64. During the first two epochs, we
exclusively trained the feature reduction and classification modules, which
were randomly initialised. This was done to protect the pre-trained weights
from large gradients. After two epochs we also trained the feature extractor.
We report the test accuracy (ACC) and area under the receiver-operator curve
(AUROC) as evaluation metrics.

Fig. 3: Exemplary image of a correctly classified PDAC tumour from the test
set. The left panel shows the middle axial slice with overlaid attention
values of sagittal and coronal slices. The second panel shows the middle
coronal slice with overlaid axial attention values. The third panel shows the
slice with the highest attention weight. Attention is very sparse and a major
part of the slices with non-negligible attention values are on empty parts of
the scan. The by far highest attention value is on a slice through the liver,
where metastases (blue arrow) and an enlarged gall bladder (red arrow) are
visible. Both are strongly indicative of PDAC. The right panel shows the
highest peak when applying HiResCam using a trained 3D model to the same CT
scan. The highlighted area at the back of the patient contains no features
relevant to the task.

###  3.3 Experiments

First, we evaluated the same model and weights converted to a 3D, ACS, and our
attention-pooling approach on all 3D datasets in MedMNIST. We performed each
experiment with five random seeds. We report the results for ACC and AUROC in
Table 1 and illustrate the results in Figure 2. We find that the performance
of none of the approaches clearly stands out over all datasets. Our approach
has the best results on three of six datasets, the 3D convolution approach has
the best on the Vessel task, and the remaining two are ambiguous with AUROC
favouring our method and accuracy the ACS convolutions.

To assess the approaches under real-world conditions, we further evaluated
them on two high-resolution real-world medical imaging datasets. For the PDAC
dataset, we find that all approaches yield almost perfect predictions, yet,
the ACS approach stands out with a perfect AUROC score in all five
repetitions. On the glioma dataset, we observe that the ACS approach of [1]
yields the best accuracy while our approach performs best in AUROC. The
performance of the 3D ResNet is slightly below the other approaches. In
summary, all approaches perform well on real-world datasets, with ACS and our
approach slightly outperforming the 3D model. In Table 2, we see that while
our approach allows for a substantial speed-up compared to a 3D model, ACS is
the computationally most efficient method.
In addition to performance, attention pooling as a feature reduction module
introduces inherent interpretability by quantifying the weight of each
individual slice for 3D data classification. Figure 3 visualises these
capabilities of our architecture design. Upon evaluating several examples on
both PDAC and Glioma datasets, we observed that attention is often sparse,
with only a small subset of slices receiving the majority of attention
weights. Furthermore, we typically have a peak of attention in body regions
critical to the task, along with noticeable but not negligible attention on
background slices. One interesting finding is that on the PDAC dataset,
despite achieving almost perfect test accuracy, the attention weights were
rarely attributed to the tumour or the pancreas, but instead to secondary
features. When comparing our model interpretations to the explanations
produced by HiResCam [6] on the 3D model, we see that these highlight the
patient’s back, where we cannot detect any indication relevant to the task
(compare Figure 3).

##  4 Discussion

This work proposes a lightweight and versatile approach combining 2D vision
models with attention pooling to create 2.5D architectures. This design
facilitates the transfer of information from large pre-trainings on 2D vision
datasets to 3D data. We demonstrate its competitive results on several
benchmark datasets and two real-world clinical datasets. Crucially, our
approach provides inherent explanations for predictions, as the impact of each
slice on the final prediction is directly quantifiable with the use of
attention pooling.

We observed that although they have significantly fewer parameters, 2.5D
approaches are performance-wise on par or superior to 3D models. This supports
our reasoning that 2.5D approaches can show strong benefits over naively
expanding 2D CNN architectures to a third dimension, most importantly
leveraging pre-trained weights from the 2D domain and computational
efficiency. By introducing attention pooling, our approach inherently
attributes importance to slices. This exemplarily revealed that the PDAC model
predominantly focused on secondary features of tumour patients, such as
metastases, rather than the tumour or pancreas themselves. Unlike
retrospective inspection methods, we get this attribution alongside every
model prediction, making it directly available to the user without further
computations, substantially lowering the threshold for practical use.

We leave it to future work to explore how to obtain a more fine-grained pixel-
level attribution. This could trivially be obtained by multiplying or adding
slice attributions along sagittal, coronal, and axial directions. However,
such a procedure would not correspond to the intuition of attention and thus
it seems preferable to augment our approach with spatial attention mechanisms.
Furthermore, it would be interesting to combine retrospective inspection
methods with our approach to analyse the alignment of attribution.

We hope to contribute to the development of architectures which are real-world
applicable and, at the same time, not exhibit the opacity of black-box deep
learning architectures. We showcase the effectiveness of our approach across
various datasets and tasks, providing practitioners with tools to achieve
both: competitive performance and interpretable results.

##  5 Compliance with ethical standards

All subjects gave their informed consent for inclusion before they
participated in the study. The study was conducted in accordance with the
Declaration of Helsinki, and the protocol was approved by the Ethics Committee
of Klinikum Rechts der Isar (180/17S).

##  6 Acknowledgements

This work was supported by the European Research Council (Deep4MI - 884622),
German Research Foundation, Priority Programme SPP2177, Radiomics: Next
Generation of Biomedical Imaging, German Cancer Consortium Joint Funding
UPGRADE Programme: Subtyping of Pancreatic Cancer based on radiographic and
pathological Features, and the Munich Centre for Machine Learning. The funders
played no role in the design or execution of the study, nor on the decision to
prepare or submit the manuscript.

## References

  * [1] Jiancheng Yang, Xiaoyang Huang, Yi He, Jingwei Xu, Canqian Yang, Guozheng Xu, and Bingbing Ni,  “Reinventing 2d convolutions for 3d images,”  IEEE Journal of Biomedical and Health Informatics, vol. 25, no. 8, pp. 3009–3018, 2021.
  * [2] Chi Zhang, Qianqian Hua, Yingying Chu, and Pengwei Wang,  “Liver tumor segmentation using 2.5 d uv-net with multi-scale convolution,”  Computers in Biology and Medicine, vol. 133, pp. 104424, 2021.
  * [3] Bingjiang Qiu, Jiapan Guo, Joep Kraeima, Haye Hendrik Glas, Weichuan Zhang, Ronald JH Borra, Max Johannes Hendrikus Witjes, and Peter MA van Ooijen,  “Recurrent convolutional neural networks for 3d mandible segmentation in computed tomography,”  Journal of personalized medicine, vol. 11, no. 6, pp. 492, 2021\.
  * [4] Sepp Hochreiter and Jürgen Schmidhuber,  “Long short-term memory,”  Neural computation, vol. 9, no. 8, pp. 1735–1780, 1997.
  * [5] Ramprasaath R Selvaraju, Michael Cogswell, Abhishek Das, Ramakrishna Vedantam, Devi Parikh, and Dhruv Batra,  “Grad-cam: Visual explanations from deep networks via gradient-based localization,”  in Proceedings of the IEEE international conference on computer vision, 2017, pp. 618–626.
  * [6] Rachel Lea Draelos and Lawrence Carin,  “Use hirescam instead of grad-cam for faithful explanations of convolutional neural networks,”  arXiv preprint arXiv:2011.08891, 2020.
  * [7] Alexey Dosovitskiy, Lucas Beyer, Alexander Kolesnikov, Dirk Weissenborn, Xiaohua Zhai, Thomas Unterthiner, Mostafa Dehghani, Matthias Minderer, Georg Heigold, Sylvain Gelly, et al.,  “An image is worth 16x16 words: Transformers for image recognition at scale,”  arXiv preprint arXiv:2010.11929, 2020.
  * [8] Alec Radford, Jong Wook Kim, Chris Hallacy, Aditya Ramesh, Gabriel Goh, Sandhini Agarwal, Girish Sastry, Amanda Askell, Pamela Mishkin, Jack Clark, et al.,  “Learning transferable visual models from natural language supervision,”  in International conference on machine learning. PMLR, 2021, pp. 8748–8763.
  * [9] Michela Antonelli, Annika Reinke, Spyridon Bakas, Keyvan Farahani, Annette Kopp-Schneider, Bennett A Landman, Geert Litjens, Bjoern Menze, Olaf Ronneberger, Ronald M Summers, et al.,  “The medical segmentation decathlon,”  Nature communications, vol. 13, no. 1, pp. 4128, 2022.
  * [10] Han Li, Long Chen, Hu Han, and S Kevin Zhou,  “Satr: Slice attention with transformer for universal lesion detection,”  in Medical Image Computing and Computer Assisted Intervention–MICCAI 2022: 25th International Conference, Singapore, September 18–22, 2022, Proceedings, Part III. Springer, 2022, pp. 163–174.
  * [11] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin,  “Attention is all you need,”  Advances in neural information processing systems, vol. 30, 2017\.
  * [12] Jiancheng Yang, Rui Shi, Donglai Wei, Zequan Liu, Lin Zhao, Bilian Ke, Hanspeter Pfister, and Bingbing Ni,  “Medmnist v2-a large-scale lightweight benchmark for 2d and 3d biomedical image classification,”  Scientific Data, vol. 10, no. 1, pp. 41, 2023.
  * [13] Evan Calabrese, Javier E Villanueva-Meyer, Jeffrey D Rudie, Andreas M Rauschecker, Ujjwal Baid, Spyridon Bakas, Soonmee Cha, John T Mongan, and Christopher P Hess,  “The university of california san francisco preoperative diffuse glioma mri dataset,”  Radiology: Artificial Intelligence, vol. 4, no. 6, pp. e220058, 2022\.
  * [14] Sebastian R van der Voort, Fatih Incekara, Maarten MJ Wijnenga, Georgios Kapsas, Renske Gahrmann, Joost W Schouten, Hendrikus J Dubbink, Arnaud JPE Vincent, Martin J van den Bent, Pim J French, et al.,  “The erasmus glioma database (egd): Structural mri scans, who 2016 subtypes, and segmentations of 774 patients with glioma,”  Data in brief, vol. 37, pp. 107191, 2021.
  * [15] Spyridon Bakas, Hamed Akbari, Aristeidis Sotiras, Michel Bilello, Martin Rozycki, Justin S Kirby, John B Freymann, Keyvan Farahani, and Christos Davatzikos,  “Advancing the cancer genome atlas glioma mri collections with expert segmentation labels and radiomic features,”  Scientific data, vol. 4, no. 1, pp. 1–13, 2017.
  * [16] Florian Kofler, Christoph Berger, Diana Waldmannstetter, Jana Lipkova, Ivan Ezhov, Giles Tetteh, Jan Kirschke, Claus Zimmer, Benedikt Wiestler, and Bjoern H Menze,  “Brats toolkit: translating brats brain tumor segmentation algorithms into clinical and scientific practice,”  Frontiers in neuroscience, p. 125, 2020.
  * [17] Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun,  “Deep residual learning for image recognition,”  in Proceedings of the IEEE conference on computer vision and pattern recognition, 2016, pp. 770–778.
  * [18] Timothy Dozat,  “Incorporating nesterov momentum into adam,”  2016\.

Method |  | MedMNIST 3D
---|---|---
Organ | Nodule | Fracture | Adrenal | Vessel | Synapse |
AveragePool | AUC | 99.6% | 86.9% | 58.3% | 87.0% | 93.1% | 83.7%
ACC | 91.4% | 85.3% | 43.3% | 81.9% | 88.7% | 80.1%
MaxPool | AUC | 99.2% | 84.9% | 57.6% | 76.3% | 84.3% | 68.0%
ACC | 88.5% | 84.7% | 42.3% | 79.9% | 89.8% | 72.2%
LSTM | AUC | 99.4% | 84.6% | 56.1% | 78.9% | 88.3% | 70.7%
ACC | 92.2% | 82.3% | 40.2% | 76.3% | 89.9% | 72.0%
Transformer | AUC | 97.1% | 67.3% | 58.3% | 65.9% | 59.8% | 62.7%
ACC | 78.1% | 80.8% | 40.2% | 76.8% | 88.7% | 73.4%
AttentionPool | AUC | 99.5% | 82.3% | 58.8% | 80.9% | 91.4% | 74.3%
ACC | 92.0% | 83.9% | 42.7% | 78.9% | 91.8% | 75.5%

Table 3: Benchmarking of our method using various feature reduction modules on
the MedMNIST3D datasets. AUC denotes the area under the receiver-operator
curve, ACC the classification accuracy. Mean results over five runs of our
experiments.

##  Appendix A Appendix

Our method is furthermore compatible with other operations to reduce the
slice-wise features into a single representation vector. To illustrate this,
we have performed experiments with other obvious choices instead of attention
pooling. We note that the interpretability capacaties are only given with
attention pooling. The results are displayed in Table 3.