# Varieties of truth definitions

Piotr Gruza  Doctoral School of Exact and Natural Sciences, University of
Warsaw, mailto<EMAIL_ADDRESS>Mateusz Łełyk  Faculty of Philosophy,
University of Warsaw, mailto<EMAIL_ADDRESS>
###### Abstract

We study the structure of the partial order induced by the definability
relation on definitions of truth for the language of arithmetic. Formally, a
definition of truth is any sentence $\alpha$ which extends a weak arithmetical
theory (which we take to be $\operatorname{I\Delta_{0}+\exp}$) such that for
some formula $\Theta$ and any arithmetical sentence $\varphi$,
$\Theta(\ulcorner\varphi\urcorner)\equiv\varphi$ is provable in $\alpha$. We
say that a sentence $\beta$ is definable in a sentence $\alpha$, if there
exists an unrelativized translation from the language of $\beta$ to the
language of $\alpha$ which is identity on the arithmetical symbols and such
that the translation of $\beta$ is provable in $\alpha$. Our main result is
that the structure consisting of truth definitions which are conservative over
the basic arithmetical theory forms a countable universal distributive
lattice. Additionally, we generalize the result of Pakhomov and Visser showing
that the set of (Gödel codes of) definitions of truth is not
$\Sigma_{2}$-definable in the standard model of arithmetic. We conclude by
remarking that no $\Sigma_{2}$-sentence, satisfying certain further natural
conditions, can be a definition of truth for the language of arithmetic.

##### Acknowledgement

This research was supported by the NCN SONATA grant "Truth: Between
Disquotation and Compositionality." (2019/35/D/HS1/04502)

##  1 Introduction

The main goal of this paper is to understand in how many alternative ways can
a definition of truth be given. More precisely: assuming that a first-order
language $\mathcal{L}$ has been fixed, how many different truth definitions
for $\mathcal{L}$ are there? The far reaching objective is to understand
essential properties that any truth definition for $\mathcal{L}$ must have. In
particular, we would like to understand whether the definitions of truth need
to be compositional.111This question, along with its formal paraphrase, was
suggested by Albert Visser (see [24]) We say more about this problem in
Section 2.3.1.

In what follows, we define a definition of truth for $\mathcal{L}$ to be any
sentence $\alpha$, such that for some formula $\Theta$ of the language of
$\alpha$, all Tarski biconditionals for $\mathcal{L}$ are provable in
$\alpha$. More precisely, for $\alpha$ to be a truth definition, there must be
a formula $\Theta(x)$, such that for every $\mathcal{L}$-sentence $\psi$, the
sentence

$\Theta(\ulcorner\psi\urcorner)\leftrightarrow\psi$

is provable in $\alpha$. We specialize to the case when $\mathcal{L}$ is the
usual language of first-order arithmetic, denoted by
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$. We assume that all the truth
definitions extend a weak finitely axiomatised fragment of Peano Arithmetic,
which provides a metatheory for formalising the syntax for
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$. The set of all truth
definitions for $\operatorname{\mathcal{L}_{\operatorname{PA}}}$ is denoted by
$\operatorname{DEF}$. For most of the paper, we are interested in the subset
of $\operatorname{DEF}$ consisting of those truth definitions for
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$ which are (syntactically)
conservative extensions of the basic arithmetical theory. The set of such
truth definitions is denoted by $\operatorname{cDEF}$. To compare the
definitions of truth, we consider the definability pre-order
$\blacktriangleleft$ on $\operatorname{DEF}$ and determine its various
properties. Informally speaking, for two truth definitions $\alpha$, $\beta$,
we put $\alpha\blacktriangleleft\beta$ if there is a translation $\sigma$ from
the language of $\alpha$ to the language of $\beta$ which preserves the
symbols of $\mathcal{L}$ such that $\sigma[\alpha]$ is provable in $\beta$.

The main result of this paper is that the structure
$\langle\operatorname{cDEF},\blacktriangleleft\rangle$ is a countable
universal distributive lattice, i.e. it is a distributive lattice which embeds
every countable distributive lattice. The proof proceeds by constructing an
embedding of the lattice structure of the countable atomless Boolean algebra
into a sublattice of $\langle\operatorname{cDEF},\blacktriangleleft\rangle$,
which consists uniquely of truth definitions, which are provable in the
canonical truth theory $\operatorname{CT}^{-}$. Restricting to conservative
truth definitions is required to make sure that the result is non-trivial, in
particular that it does not immediately follow from the known facts about the
Lindenbaum algebras of r.e. extensions of basic arithmetical systems. Thus, we
take our main result to witness a great diversity among the possible
definitions of truth. We provide some further information about the structure
of $\langle\operatorname{DEF},\blacktriangleleft\rangle$ and include some
results of the possible complexities of truth definitions and the connection
between truth definitions and compositional Tarski clauses.

There are at least three important predecessors to the current paper: in [19]
it was proved that, in the order induced by the relation of definability,
there are no minimal finite axiomatization (in an extended language) of a
given non-finitely axiomatizable theory (such as $\operatorname{PA}$, ZF,
$\ldots$). In [24] the same reasoning was applied to show that, in the order
induced by definability, there are no minimal definitions of truth for
arithmetic. [6] shows, among other things, that the ordering induced by
provability on a very concrete set of natural finite axiomatizations (which
carry truth defintitions for the language of arithmetic) of
$\operatorname{PA}$ is a countable universal partial order.

The structure of the paper is as follows: in Section 2 we introduce all the
relevant preliminaries including the first-order arithmetic, axiomatic
theories of truth, interpretability and (basic) lattice theory. In Section 3
we prove our main result. In Section 4 we provide some further details on the
structure of the lattice
$\langle\operatorname{cDEF},\blacktriangleleft\rangle$, in particular showing
another way of realising the embedding of the countable atomless Boolean
algebra into $\operatorname{cDEF}$. The image of the latter embedding consists
uniquely of truth definitions which are _semantically_ conservative over the
base arithmetical theory, that is every model of the base theory can be
expanded to a model of any such truth definition. Last but not least, in this
section we prove that no truth definition, which satisfies some further
natural conditions, can be a $\Sigma_{2}$-sentence. We conclude in Section 5
with a number of open questions.

##  2 Preliminaries

###  2.1 Arithmetical Preliminaries

We take the language of arithmetic, denoted by
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$, to be the first-order with
equality language of the signature $\langle 0,1,+\times,<\rangle$, where $0$
and $1$ are constant symbols, $+$ and $\times$ are binary function symbols,
and $<$ is a binary relation symbol. In the definition below we recall the
standard definition of the arithmetical hierarchy, $\mathcal{L}$ being any
language extending $\operatorname{\mathcal{L}_{\operatorname{PA}}}$:

######  Definition 1.

A formula is _atomic_ iff it is of the form $R(t_{1},...,t_{n})$ or
$t_{1}=t_{2}$, where $R$ is an $n$-ary relation symbol and $t_{1}$, $t_{2}$,
…, $t_{n}$ are terms.

The class of _quantifier-free_ formulae of $\mathcal{L}$ is the smallest set
containing all atomic formualae of $\mathcal{L}$ and closed under
propositional connectives, i.e. if $\varphi$ and $\psi$ are quantifier-free,
then so are $\lnot\varphi$ and $\varphi\land\psi$.

The class of $\Delta_{0}$ formulae of $\mathcal{L}$ is the smallest set
containing all quantifier-free formulae of $\mathcal{L}$ and closed under the
adjoin of bounded quantifiers, i.e. if $\varphi$ is a $\Delta_{0}$ formula,
$x$ is a variable and $t$ is a term not containing $x$, then $\exists
x(x<t\land\varphi)$ (abbreviated $\exists x<t.\varphi$) and $\forall
x(x<t\rightarrow\varphi)$ (abbreviated $\forall x<t.\varphi$) are $\Delta_{0}$
as well.

The classes of $\Pi_{0}$ and $\Sigma_{0}$ formulae of $\mathcal{L}$ are
exactly the class of $\Delta_{0}$ formulae of $\mathcal{L}$.

For a natural number $n$ greater than $0$, the class of $\Pi_{n}$ formulae of
$\mathcal{L}$ is the smallest set containing all $\Sigma_{n-1}$ formulae of
$\mathcal{L}$ and closed under adding the universal quantifier.

For a natural number $n$ greater than $0$, the class of $\Sigma_{n}$ formulae
of $\mathcal{L}$ is the smallest set containing all $\Pi_{n-1}$ formulae of
$\mathcal{L}$ and closed under adding the existential quantifier.

For a natural number $n$ and a theory $Th$, the class of $\Delta_{n}(Th)$
formulae of $\mathcal{L}$ consists of formulae
$\varphi(\overline{x})\in\mathcal{L}$ for which there exist a $\Sigma_{n}$
formula $\sigma(\overline{x})\in\mathcal{L}$ and a $\Pi_{n}$ formula
$\pi(\overline{x})\in\mathcal{L}$ such that
$Th\vdash\forall\overline{x}(\varphi(\overline{x})\leftrightarrow\sigma(\overline{x}))$
and
$Th\vdash\forall\overline{x}(\varphi(\overline{x})\leftrightarrow\pi(\overline{x}))$.
In particular, $\Delta_{0}(Th)$ is exactly the set of formulae $Th$-provably
equivalent to some $\Delta_{0}$ formulae.

Apart from the $\Sigma_{n}\setminus\Pi_{n}$ measures of complexity we employ
also a simpler one. If $\varphi$ is any sentence, then
$\operatorname{dpt}(\varphi)$ denotes its logical depth, i.e. maximal nesting
of connectives and quantifiers. $\operatorname{dpt}(\varphi)$ is defined
recursively: if $\varphi$ is atomic, then $\operatorname{dpt}(\varphi)=0$,
$\operatorname{dpt}(\neg\varphi)=\operatorname{dpt}(\exists
z.\varphi)=\operatorname{dpt}(\varphi)+1$ and
$\operatorname{dpt}(\varphi\wedge\psi)=\max\\{\operatorname{dpt}(\varphi),\operatorname{dpt}(\psi)\\}+1$.

######  Definition 2.

The theory $\operatorname{PA}^{-}$ is the set of axioms of nonnegative parts
of discrete ordered rings (see Section 2.1 of Chapter 2 of [16].)

This theory is used as a basis for several arithmetical theories. In the
following, the subsequent theories are formed by adding the instances of the
parameter induction scheme for the subsequent classes of the arithmetical
hierarchy.

######  Definition 3.

Given a natural number $n$, the theory $\operatorname{I\Pi_{n}}$ is
$\operatorname{PA}^{-}$ augmented with the instances of the induction scheme
(with parameters) for $\Pi_{n}$ formulae of
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$. Likewise for
$\operatorname{I\Sigma_{n}}$ and $\operatorname{I\Delta_{0}}$. Peano
Arithmetic, $\operatorname{PA}$, is $\operatorname{PA}^{-}$ together with all
($\operatorname{\mathcal{L}_{\operatorname{PA}}}$) instances of parameter
induction scheme added. If $\mathcal{L}$ is any language (extending the
language of arithmetic), then $\operatorname{IND}(\mathcal{L})$ denotes the
collection of all induction axioms for formulae of $\mathcal{L}$.

The weakest system we are interested in lies in between
$\operatorname{I\Delta_{0}}$ and I$\Sigma_{1}$.

######  Definition 4.

We use symbol $\exp$ to denote arithmetical representation of an exponential
function, i.e. the formula $\exp(x,y)=z$ is to be interpreted as $x^{y}=z$.

An explicit definition of $\exp$ can be written as a $\Delta_{0}$ formula (for
more details see Section 3(c) of Chapter V of [14]).

######  Definition 5.

The theory $\operatorname{I\Delta_{0}+\exp}$ is $\operatorname{I\Delta_{0}}$
augmented with the axiom $\forall x\forall y\exists z.\exp(x,y)=z$.

In the case of our results, the choice of a language and a base theory in
principle plays a secondary role, altough the use of
$\operatorname{I\Delta_{0}+\exp}$ allows us to show that the theorems
presented do not require a strong base theory — the axiom $\forall x\forall
y\exists z.\exp(x,y)=z$ is $\operatorname{I\Sigma_{1}}$-provable (cf. the
remark following definition 4). An additional advantage of this theory, is
that it is finitely axiomatizable (Section 2(c) of Chapter I of [14]). In the
following, when we write $\operatorname{I\Delta_{0}+\exp}$, we mean its finite
axiomatisation.

######  Definition 6.

Let $\mathcal{L}_{E}$ denotes the language of the signature of
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$ augmented with a binary
function symbol $E$. The class of $\Delta_{0}(E)$ formulae is the class of
$\Delta_{0}$ formulae of $\mathcal{L}_{E}$.

######  Definition 7.

The theory $\operatorname{I\Delta_{0}}(\exp)$ is $\operatorname{PA}^{-}$
augmented with the axioms $\forall x.E(x,0)=1$, $\forall x\forall
y.E(x,y+1)=E(x,y)\times x$, and the instances of the parameter induction
scheme for $\Delta_{0}(E)$ formulae.

######  Fact 8.

The theory $\operatorname{I\Delta_{0}+\exp}+\forall x\forall
y.exp(x,y)=E(x,y)$ proves each axiom of $\operatorname{I\Delta_{0}}(\exp)$.

This theorem can be found in the corollary below Theorem 3.3 of [5]. [20]
introduces a set theory which is bi-interpretable with
$\operatorname{I\Delta_{0}+\exp}$ (Theorem 4 and Theorem 7).

##### The arithmetization of syntax and metalogic

We explain the basics of arithmetization of syntax in
$\operatorname{I\Delta_{0}+\exp}$ (for more details, consult [14]). Specific
issues are introduced when necessary. $\ulcorner\varphi\urcorner$ denotes the
Gödel code of a formula $\varphi$ and $\underline{n}$ denotes the numeral
naming $n$, i.e. the expression $0+1+1+\ldots+1$ ($n$ times 1). Usually, we
omit quotation marks to increase readability. $x\in\operatorname{Var}$,
$x\in\operatorname{Tm^{c}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}}$,
$x\in\operatorname{Sent}_{\mathcal{L}}$ denote the arithmetical formulae
representing the sets of (codes of) variables, closed terms of
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$ and (assuming that the coding
of $\mathcal{L}$ has been fixed) sentences of $\mathcal{L}$ (respectively).
$\operatorname{val}(x)=y$ denotes the arithmetical formula, which expresses
"$y$ is the value of the $\operatorname{\mathcal{L}_{\operatorname{PA}}}$-term
$x$" and $\operatorname{dpt}(x)=y$ expresses "the depth of a formula $x$ is
equal to $y$". The use of definable functions representing syntactical
operations is signalised with $[\cdot]$, e.g. "$x=[\alpha\land\beta]$" is a
shorthand for "the value of $x$ is equal to the code of a conjunction of
sentences $\alpha$ and $\beta$". The addition of a dot above a variable
indicates that a numeral is inserted instead of this variable, for example
"$y=[\varphi(\dot{x}/v)]$" is a shorthand for "the value of $y$ is equal to
the code of a formula formed by substituting the $x$-th numeral for all
occurrences of the variable $v$ into the formula $\varphi(v)$". We avoid
mentioning $v$ if it is clear from context. We assume that all operations
described above are provably total in $\operatorname{I\Delta_{0}+\exp}$ and
hence allow ourselves to treat them as new function symbols, writing e.g.
$\forall
x\bigl{(}x\in\operatorname{Sent}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}\rightarrow\varphi[\neg
x]\bigr{)}$ to express that the negation of every arithmetical sentence
satisfies formula $\varphi(x)$. If $Th$ is any r.e. theory, then
$\operatorname{Proof}_{Th}(y,x)$ denotes the canonical provability predicate
for $Th$ expressing "$y$ is a proof of $x$ from the axioms of $Th$". We put

$\displaystyle\operatorname{Prov}_{Th}(x)$ $\displaystyle:=\exists
y.\operatorname{Proof}_{Th}(y,x)$ $\displaystyle\operatorname{Con}_{Th}(x)$
$\displaystyle:=\forall y<x.\neg\operatorname{Proof}_{Th}(y,\ulcorner
0=1\urcorner)$ $\displaystyle\operatorname{Con}_{Th}$ $\displaystyle:=\forall
x.\operatorname{Con}_{Th}(x).$

We recall the canonical construction of partial truth predicates,
$\operatorname{Tr}_{n}$, such that

  1. 1.

the function $n\mapsto\ulcorner\operatorname{Tr}_{n}(x)\urcorner$ is
elementary;

  2. 2.

for every $n$, $\operatorname{Tr}_{n}(x)$ satisfies compositional Tarski truth
clauses for formulae of logical depth at most $n$.

The construction of $\operatorname{Tr}_{n}$ is by elementary induction on $n$:
for $n=0$ we put $\operatorname{Tr}_{0}(x):=\exists
s,t\in\operatorname{Tm^{c}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}}(x=[s=t]\wedge\operatorname{val}(s)=\operatorname{val}(t)).$
For $n>0$ we put $\operatorname{Tr}_{n}(x)$ to be the disjunction of the
following formulae:

  * •

$\operatorname{dpt}(x)<\underline{n}\wedge\operatorname{Tr}_{n-1}(x)$

  * •

$\operatorname{dpt}(x)=\underline{n}\wedge\exists\varphi(y=[\neg\varphi]\wedge\neg\operatorname{Tr}_{n-1}(\varphi)\bigr{)}$

  * •

$\operatorname{dpt}(x)=\underline{n}\wedge\exists\varphi,\psi(x=[\varphi\wedge\psi]\wedge\operatorname{Tr}_{n-1}(\varphi)\wedge\operatorname{Tr}_{n-1}(\psi))$

  * •

$\operatorname{dpt}(x)=\underline{n}\wedge\exists\varphi\exists
v(\operatorname{Var}(v)\wedge x=[\exists v\varphi]\wedge\exists
z.\operatorname{Tr}_{n-1}[\varphi(\dot{z}/v)].$

Finally, we recall provable $\Sigma_{1}$-completeness of
$\operatorname{PA}^{-}$:

######  Fact 9.

For every $\Sigma_{1}$-sentence
$\sigma\in\operatorname{\mathcal{L}_{\operatorname{PA}}}$,
$\operatorname{PA}\vdash\sigma\rightarrow\operatorname{Prov}_{\operatorname{PA}^{-}}(\ulcorner\sigma\urcorner)$.
In particular, given a theory $Th\subseteq Th(\operatorname{\mathbb{N}})$ and
an arithmetical $\Delta_{1}(Th)$-sentence $\tau$,
$\operatorname{PA}+Th\vdash\operatorname{Prov}_{\operatorname{PA}^{-}}(\ulcorner\tau\urcorner)\lor\operatorname{Prov}_{\operatorname{PA}^{-}}(\ulcorner\lnot\tau\urcorner)$.

######  Definition 10 (Flexible formula).

Let $Th$ be any theory and let $\Gamma$ be a class of formulae. A formula
$\theta(x)$ is $\Gamma$-_flexible_ over $Th$ iff for every formula
$\varphi(x)\in\Gamma$, the theory $Th+\forall
x\bigl{(}\theta(x)\leftrightarrow\varphi(x)\bigr{)}$ is consistent.

######  Theorem 11 (Essentially due to Kripke, see [3], Theorem 4.2).

For every r.e. theory in the arithmetical language $Th$ extending
$\operatorname{I\Delta_{0}+\exp}$ and every $n$, there exists a
$\Sigma_{n}$-formula, which is $\Sigma_{n}$-flexible over $Th$.

The generalisation of this theorem to sequential theories, was proved in [10].

###  2.2 Definability

In this paper we consider only a very special, strong form of the
interpretability relation between theories. We focus on theories that extend
the language of arithmetic with finitely many relational symbols. In the
following, we present the most important relevant definitions (for a detailed
presentation see [25]):

######  Definition 12.

Given three signatures $A$, $B$ and $C\subseteq A\cap B$, a $C$-_conservative
translation_ from $A$ to $B$ is a mapping $\sigma$ constant on $C$ such that,
for every non-arithmetic $n$-ary predicate symbol $P$ of $A$, $\sigma(P)$ is a
formula of $B$ with exactly $n$ free variables. Each such translation can
naturally be extended to the set of all formulae over the signature $A$. The
result of applying the translation $\sigma$ to a sentence $\varphi$ is denoted
by $\sigma[\varphi]$.222As usual, we assume that the translation is preceded
with a process of variable renaming (if necessary).

######  Definition 13.

We say that a theory $U$ is _definable_ in a theory $V$ modulo signature $C$
if there exists a translation $\sigma$ from the language of $U$ to the
language of $V$ which is $C$-conservative and such that for every axiom
$\alpha$ of $U$, $V\vdash\sigma[\alpha]$.

######  Example 14.

Consider the theory $U$ extending $\operatorname{I\Delta_{0}+\exp}$ with an
axiom $\forall x.P(x)$, and a theory $V$ extending
$\operatorname{I\Delta_{0}+\exp}$ with an axiom $\forall x.\neg P(x)$, where
$P$ is a fresh predicate. Then the translation $\sigma(P)=\neg P(x)$ witnesses
that $U$ is definable in $V$ (and actually, $V$ is definable in $U$ via the
same translation).

In the rest of the paper we focus exclusively on the translations which are
conservative over the arithmetic signature. This is meaningful, since all
theories we consider are extensions of $\operatorname{I\Delta_{0}}+\exp$. We
note that in the context of the general interpretability theory, our
definition of definability corresponds to a direct and
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$-conservative interpretability
(see [25]).

######  Fact 15.

The definability relation between theories extending
$\operatorname{I\Delta_{0}+\exp}$ is a pre-order, i.e. it is transitive and
reflexive.

###  2.3 Axiomatic Theories of Truth

We begin by providing a fundamental definition.

######  Definition 16.

A consistent theory $Th$ containing $\operatorname{I\Delta_{0}+\exp}$ is a
_theory of truth_ for a language $\mathcal{L}$ iff there exists a formula
$\Theta$ with one free variable such that for each sentence
$\sigma\in\mathcal{L}$

$Th\vdash\Theta(\ulcorner\sigma\urcorner)\leftrightarrow\sigma\text{.}$

######  Theorem 17 (Tarski).

Suppose that $Th$ is a consistent theory extending
$\operatorname{I\Delta_{0}+\exp}$ in a language $\mathcal{L}$. Then $Th$ is
not a theory of truth for $\mathcal{L}$.

######  Definition 18 (Some prominent theories of truth for
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$).

The first three theories are formulated in the language
$\operatorname{\mathcal{L}_{T}}:=\operatorname{\mathcal{L}_{\operatorname{PA}}}\cup\\{T\\}$,
where $T$ is a fresh unary predicate. The last theory is formulated in the
language $\operatorname{\mathcal{L}_{\operatorname{PA}}}\cup\\{D\\}$, where
$D$ is a fresh binary predicate.

$\operatorname{TB}^{-}$ extends $\operatorname{I\Delta_{0}+\exp}$ with
infinitely many axioms of the form

$T(\ulcorner\sigma\urcorner)\leftrightarrow\sigma,$

where $\sigma$ is an
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$-sentence.

$\operatorname{UTB}^{-}$ extends $\operatorname{I\Delta_{0}+\exp}$ with
infinitely many axioms of the form

$\forall x\bigl{(}T[\sigma(\dot{x})]\leftrightarrow\sigma(x)\bigr{)},$

where $\sigma(x)$ is an
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$-formula with at most $x$
free.

$\operatorname{CT}^{-}$ extends $\operatorname{I\Delta_{0}+\exp}$ with the
following axioms

  * •

$\forall
s,t\big{(}s,t\in\operatorname{Tm^{c}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}}\rightarrow\big{(}T[s=t]\leftrightarrow\operatorname{val}(s)=\operatorname{val}(t)\big{)}\big{)}$,

  * •

$\forall\varphi\big{(}\varphi\in\operatorname{Sent}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}\rightarrow\big{(}T[\lnot\varphi]\leftrightarrow\lnot
T(\varphi)\big{)}\big{)}$,

  * •

$\forall\varphi,\psi\big{(}\varphi,\psi\in\operatorname{Sent}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}\rightarrow(T[\varphi\land\psi]\leftrightarrow
T(\varphi)\land T(\psi)\big{)}\big{)}$,

  * •

$\forall\varphi\forall y\big{(}y\in\operatorname{Var}\land[\exists
y.\varphi]\in\operatorname{Sent}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}\rightarrow\big{(}T[\exists
y.\varphi]\leftrightarrow\exists z.T[\varphi(\dot{z}/y)]\big{)}\big{)}$.

$\operatorname{DEF}^{-}$ extends $\operatorname{I\Delta_{0}+\exp}$ with all
axioms of the form

$\forall
z\bigl{(}D(\ulcorner\sigma\urcorner,a)\leftrightarrow\exists!x.\sigma\wedge\sigma(a)\bigr{)},$

where $\sigma(x)$ is an
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$-formula with at most $x$ free
and $\exists!x$ is understood as "There is exactly one $x$". The intuitive
reading of $D(\sigma,x)$ is "$x$ is definable by the formula $\sigma$."

######  Proposition 19.

$\operatorname{TB}^{-}$, $\operatorname{UTB}^{-}$, $\operatorname{CT}^{-}$ and
$\operatorname{DEF}^{-}$ are axiomatic theories of truth.

###### Proof.

This is immediate for $\operatorname{TB}^{-},\operatorname{UTB}^{-}$ and
$\operatorname{CT}^{-}$. For $\operatorname{DEF}^{-}$ it is enough to consider
the formula

$\Theta(\sigma):=D([\sigma\wedge x=0],0).$

The intuition is that for every
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$-sentence $\sigma$, provably
in $\operatorname{DEF}^{-}$, $\Theta(\ulcorner\sigma\urcorner)$ holds iff the
sentence $\sigma\wedge x=0$ is a definition of $0$, which is equivalent to
$\sigma$ being true. ∎

######  Definition 20.

$\operatorname{\operatorname{TB}}$, $\operatorname{UTB}$, $\operatorname{CT}$,
$\operatorname{DEF}$ denote the extensions of theories
$\operatorname{TB}^{-}$, $\operatorname{UTB}^{-}$, $\operatorname{CT}^{-}$ and
$\operatorname{DEF}^{-}$ with full induction scheme for their languages.

######  Definition 21.

$\operatorname{CT_{0}}$ extends $\operatorname{CT}^{-}$ with induction axioms
for $\Delta_{0}$-formulae of $\operatorname{\mathcal{L}_{T}}$.

The following fact is a crucial model-theoretical property of
$\operatorname{CT_{0}}$. For a proof see [12, Fact 31].

######  Fact 22.

Let $(\mathcal{M},T)\models\operatorname{CT}^{-}$. For $c\in M$, put
$T_{c}:=\\{\varphi\in M:\
(\mathcal{M},T)\models\operatorname{dpt}(\varphi)\leqslant c\wedge
T(\varphi)\\}$. Then the following are equivalent:

  * •

$(\mathcal{M},T)\models\operatorname{CT_{0}}$.

  * •

For every $c$,
$(\mathcal{M},T_{c})\models\operatorname{CT}^{-}+\operatorname{IND}(\operatorname{\mathcal{L}_{T}}).$

In particular, $\operatorname{CT_{0}}\vdash\operatorname{PA}$.

######  Definition 23.

Let $A\subseteq B$ be two theories (possibly in different languages). We say
that $B$ is _conservative_ over $A$ if every sentence $\varphi$ in the
language of $A$, which is provable in $B$, is provable in $A$. We say that $B$
is semantically (model-theoretically) conservative over $A$ if every model of
$A$ can be expanded to a model of $B$.333We say that a model
$\mathcal{M}^{\prime}$ is an expansion of a model $\mathcal{M}$, if
$\mathcal{M}$ can be obtained from $\mathcal{M}^{\prime}$ by simply erasing
the interpretations of some symbols.

######  Definition 24 (Definition of truth, the definability order).

A theory of truth $Th$ for $\mathcal{L}$ is called a _definition of truth_ iff
$Th$ is finitely axiomatizable. The set of definitions of truth is denoted by
$\operatorname{DEF}$. The set of definitions of truth which are conservative
extensions of $\operatorname{I\Delta_{0}+\exp}$ is denoted by
$\operatorname{cDEF}$. The _definability order_ is the structure
$\langle\operatorname{cDEF},\blacktriangleleft\rangle.$444We tacitly assume
that this is in fact a partial order, by passing to the quotient set of
$\operatorname{cDEF}$ modulo the equivalence relation of mutual definability.

######  Remark.

$\langle\operatorname{cDEF},\blacktriangleleft\rangle$ forms an initial
segment of $\langle\operatorname{DEF},\blacktriangleleft\rangle,$ that is if
$\beta\blacktriangleleft\alpha$ and $\alpha\in\operatorname{cDEF}$, then
$\beta\in\operatorname{cDEF}$ as well, and for every
$\alpha\in\operatorname{DEF}$, there is a $\beta\in\operatorname{cDEF}$ such
that $\beta\blacktriangleleft\alpha$.

######  Fact 25.

Among the aforementioned theories of truth, only $\operatorname{CT}^{-}$ and
$\operatorname{CT_{0}}$ are definitions of truth. For $\operatorname{CT}^{-}$
this is clear from the presentation. As shown e.g. in [9] over
$\operatorname{CT}^{-}$, $\operatorname{CT_{0}}$ is equivalent to a single
sentence
$\forall\varphi\bigl{(}\operatorname{Prov}_{\operatorname{PA}}(\varphi)\rightarrow
T(\varphi)\bigr{)}.$ $\operatorname{CT}^{-}$ is a conservative extension of
$\operatorname{I\Delta_{0}+\exp}$, but $\operatorname{CT_{0}}$ is not, as its
arithmetical consequences properly exceeds those of $\operatorname{PA}$.

####  2.3.1 Between Disquotation and Compositionality

######  Definition 26.

$\operatorname{CT}^{-}(x)$ is the conjunction of the following formulae of
$\operatorname{\mathcal{L}_{T}}$:

  * •

$\operatorname{I\Delta_{0}+\exp}$

  * •

$\forall
s,t\big{(}s,t\in\operatorname{Tm^{c}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}}\rightarrow\big{(}T[s=t]\leftrightarrow\operatorname{val}(s)=\operatorname{val}(t)\big{)}\big{)}$,

  * •

$\forall\varphi\big{(}\sigma\in\operatorname{Sent}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}\land\operatorname{dpt}[\lnot\varphi]\leqslant
x\rightarrow\big{(}T[\lnot\varphi]\leftrightarrow\lnot
T(\varphi)\big{)}\big{)}$,

  * •

$\forall\varphi,\psi\big{(}\varphi,\psi\in\operatorname{Sent}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}\land\operatorname{dpt}[\varphi\land\psi]\leqslant
x\rightarrow(T[\varphi\land\psi]\leftrightarrow T(\varphi)\land
T(\psi)\big{)}\big{)}$,

  * •

$\forall\varphi\forall v\big{(}v\in\operatorname{Var}\land[\exists
v.\varphi]\in\operatorname{Sent}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}\land\operatorname{dpt}[\exists
v.\varphi]\leqslant x\rightarrow\big{(}T[\exists
v.\varphi]\leftrightarrow\exists z.T[\varphi(\dot{z}/v)]\big{)}\big{)}$.

######  Proposition 27.

For every $n$,
$\operatorname{I\Delta_{0}+\exp}\blacktriangleright\operatorname{CT}^{-}(\underline{n})$.

###### Sketch of proof.

This follows since for every $n$ there is an arithmetical formula
$\operatorname{Tr}_{n}(x)$, which, provably in
$\operatorname{I\Delta_{0}+\exp}$ satisfies Tarski’s inductive truth clauses
for formulae of complexity at most $x$. ∎

The proposition below was well known for some time already (a variant of it is
given e.g. in [2] and [24]). We include a simple proof for the Reader’s
convenience.

######  Proposition 28.

$\\{\operatorname{CT}^{-}(\underline{n}):\
n\in\omega\\}\blacktriangleright\\!\\!\blacktriangleleft\operatorname{UTB}^{-}$

###### Sketch of proof.

By a standard argument using induction on the depth of formulae, it is easy to
show that actually $\\{\operatorname{CT}^{-}(\underline{n}):\
n\in\omega\\}\vdash\operatorname{UTB}^{-}$. In the reverse direction, we
define the following truth predicate $T^{\prime}(x)$:

$\operatorname{Sent}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}(x)\wedge\exists
z(\operatorname{dpt}(x)=z\wedge T[\operatorname{Tr}_{z}(\dot{x})]).$

In the above $\operatorname{Tr}_{z}$ denotes the representation of the
elementary mapping $n\mapsto\ulcorner\operatorname{Tr}_{n}(x)\urcorner$
described in Section 2.1. One easily checks that the mapping $\sigma$ given by
$\sigma(T)=T^{\prime}(x)$ makes each
$\sigma(\operatorname{CT}^{-}(\underline{n}))$ provable in
$\operatorname{UTB}^{-}$.

∎

The above proposition witnesses that $\operatorname{UTB}^{-}$ can be treated
as the infimum of compositional theories: it can accomodate a truth predicate
which satisfies compositional Tarski truth conditions for all formulae of
standard complexity. Therefore it is natural to treat a definition of truth as
compositional if it can define the theory $\operatorname{UTB}^{-}$. This is
the philosophical intuition underlying the following formal question by Albert
Visser (see [24]):

######  Question 29 (Visser).

Is there a definition of truth (for
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$) which does not define
$\operatorname{UTB}^{-}$?

This is the question which initiated our research. Unfortunately it still
remains unanswered.

###  2.4 Algebraical Preliminaries

We take all the basic definitions from [13] and [17].

######  Definition 30 (Lattice).

A _lattice_ is a set $L$ with two operations $\cap$ and $\cup$ each of which
is associative and symmetric and additionally satisfying $a\cap(b\cup a)=a$
and $a\cup(b\cap a)=a$, for all $a,b\in L$. A lattice $L$ is _distributive_ if
for all $a,b,c$ it holds that $a\cup(b\cap c)=(a\cup b)\cap(a\cup c)$ and
$a\cap(b\cup c)=(a\cap b)\cup(a\cap c)$.

One can show that each lattice $L$ originates from a partial order
$(L,\leqslant_{L})$ by putting $a\cup b=\sup\\{a,b\\}$ and $a\cap
b=\inf\\{a,b\\}$. In fact, this partial order $\leqslant_{L}$ is canonically
determined by $L$ by letting $a\leqslant_{L}b:=a\cap b=a$. Conversely, for
every partial order, so defined structure is a lattice.

######  Definition 31 (Countable universal distributive lattice).

Lattice $L$ is _countable universal_ iff $L$ contains an isomorphic copy of
every countable lattice.

######  Definition 32 (Boolean algebra).

A _Boolean algebra_ is a structure $\langle
B,\cap,\cup,\mathbb{0},\mathbb{1},\neg\rangle$ such that $\neg$ is a unary
function, $\mathbb{0},\mathbb{1}\in L$ and $\langle B,\cap,\cup\rangle$ is a
distributive lattice, which additionally satisfies $\forall a\in
L(a\cup\mathbb{1}=\mathbb{1}\wedge\mathbb{0}\cap a=\mathbb{0})$ and $\forall
a\in L(a\cap\neg a=\mathbb{0}\wedge a\cup\neg a=\mathbb{1}).$

An atom in a Boolean algebra is any nonzero element $a$, such that for every
$b$, if $b\leqslant_{B}a$, then $b=a\vee b=\mathbb{0}$. A Boolean algebra $B$
is called _atomless_ iff there are no atoms in $B$.

It is an easy exercise in back-and-forth arguments that any two countable
atomless Boolean algebras are isomorphic. Additionally, we have the following
observation which we use in the rest of the paper.

######  Fact 33.

If $\langle B,\cap,\cup,\mathbb{0},\mathbb{1},\neg\rangle$ is the countable
atomless Boolean algebra, then $\langle B,\cap,\cup\rangle$ is a countable
universal distributive lattice.

For a proof see Theorem 10 of [23].

######  Example 34 (An elementarily presented countable atomless Boolean
algebra).

There are many different ways of realizing the countable atomless Boolean
algebra. In what follows we need one, whose basic properties are provable in
$\operatorname{I\Delta_{0}+\exp}$. One of the simplest such algebras is the
Boolean algebra of (equivalence classes) of propositional formulae over
countable many propositional variables. To be more precise, let Prop be the
set of all formulae of propositional logic over $\\{p_{i}\\}_{i\in\omega}.$
Let $B$ be the set of equivalence classes of Prop modulo propositional
equivalence, $\sim$. We define the operations of $\cap$, $\cup$, $\neg$ and
$\mathbb{0}$ and $\mathbb{1}$ in the canonical way, for example

$[\varphi]_{\sim}\cap[\psi]_{\sim}=[\varphi\wedge\psi]_{\sim}.$

Let us observe that there is the canonical way to represent $B$ inside
$\operatorname{I\Delta_{0}+\exp}$: since $\sim$ is an elementary relation, we
can take the elements of $B$ to be the least (according to a fixed coding of
Prop) elements of equivalence classes. In this way, we obtain elementary
formulae $\delta_{B}(x)$, $\cap(x,y,z)$, $\cup(x,y,z)$, $\mathbb{0}(x)$,
$\mathbb{1}(x)$, $\neg(x,y)$ such that

$\operatorname{I\Delta_{0}+\exp}\vdash"\langle\delta_{B}(x),\cap(x,y,z),\cup(x,y,z),\mathbb{0}(x),\mathbb{1}(x),\neg(x,y)\rangle\textnormal{
is an atomless Boolean algebra }".$

######  Definition 35.

A subset $\mathcal{F}$ of a Boolean algebra $\mathbb{B}$ is a _filter_ if and
only if it satisfies the following:

  * •

$\mathbb{1}\in\mathcal{F}$,

  * •

$\forall x,y\in\mathbb{B}(x\in\mathcal{F}\land
x\leqslant_{\mathbb{B}}y\rightarrow y\in\mathcal{F})$,

  * •

$\forall x,y\in\mathbb{B}(x\in\mathcal{F}\land y\in\mathcal{F}\rightarrow
x\cap y\in\mathcal{F})$.

It is an _ultrafilter_ if additionally $\mathbb{0}\notin\mathcal{F}$ and every
filter $\mathcal{E}$ properly containing $\mathcal{F}$ is the entire algebra.

Ultrafilters are sometimes described as measures of the size of elements of a
Boolean algebra (elements of an ultrafilter are considered large). We also use
a different point of view.

######  Fact 36.

Let $\mathcal{F}$ be a subset of a Boolean algebra $\mathbb{B}$. The following
are equivalent:

  * •

$\mathcal{F}$ is an ultrafilter;

  * •

$\mathcal{F}$ is a filter, $\forall x(x\in\mathcal{F}\lor\lnot
x\in\mathcal{F}$), and $\mathbb{0}\notin\mathcal{F}$;

  * •

$\mathcal{F}$ satisfies

    * –

$\mathbb{1}\in\mathcal{F}$ and $\mathbb{0}\notin\mathcal{F}$,

    * –

$\forall x,y(x\in\mathcal{F}\land y\in\mathcal{F}\leftrightarrow x\cap
y\in\mathcal{F})$,

    * –

$\forall x,y(x\in\mathcal{F}\lor y\in\mathcal{F}\leftrightarrow x\cup
y\in\mathcal{F})$,

    * –

$\forall x(x\in\mathcal{F}\lor\lnot x\in\mathcal{F})$.

For more informations see Section 2.2. of [17].

##  3 Structure of Definability Order

###  3.1 Dense Subsets of $\operatorname{DEF}$

We begin by presenting a tiny generalisation of the argument due to Pakhomov
and Visser (see [24] and [19]). The proof uses a class of natural weakly
compositional definitions of truth. The definition of this class utilises the
formula $\operatorname{CT}^{-}(x)$ as introduced in Definition 26.

######  Definition 37 (Weakly compositional definitions of truth).

For a formula $\varphi(x)$, we define
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi(x)}$ as
$\operatorname{I\Delta_{0}+\exp}\ +\ \forall
x(\varphi(x)\rightarrow\operatorname{CT}^{-}(x))$.

######  Theorem 38 (Essentially Pakhomov-Visser).

$\operatorname{DEF}$ is not $\Sigma_{2}$-definable.

###### Proof.

Aiming at a contradiction, suppose the contrary. Let $\sigma(x)$ be a
$\Sigma_{2}$-definition of $\operatorname{DEF}$. By the fixed point lemma, let
$\delta(x)$ be a $\Pi_{1}$-formula such that $\operatorname{I\Delta_{0}+\exp}$
proves

$\exists
x.\delta(x)\leftrightarrow\sigma(\ulcorner\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\forall
y<x.\lnot\delta(y)}\urcorner){.}$

More precisely, the fixed point lemma is applied to the following formula with
a free variable $z$:

$z\in\operatorname{Sent}_{\operatorname{\mathcal{L}_{\operatorname{PA}}}}\land\exists\delta\in\Pi_{1}\bigl{(}z=[\exists
x.\delta]\land\sigma[\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\forall
y<x.\neg\delta(y)}]\bigr{)}\text{.}$ (1)

In the above, $z=\exists x.\delta$ denotes a formula with two variables $z$
and $\delta$, formalising a relation "$z$ is the Gödel code of a sentence
formed by prefixing a formula $\delta$ with an existential quantifier binding
the variable $x$". Similarly,
$\sigma[\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\forall
y<x.\neg\delta(y)}]$ is a formula with a free variable $\delta$. When
constructing a fixed point formula, we make sure that it is in the proper
$\Sigma_{2}$-form, beginning with exactly one existential quantifier. This is
possible by the standard textbook proof of the diagonal lemma (see e.g. [14],
Chapter III, Theorem 2.1).555We stress that we are not taking an arbitrary
fixed point of (1). It is easy to observe that, for trivial reasons, any
disprovable formula which is not in a proper $\Sigma_{2}$-form will be a fixed
point of (1).

The sentence $\exists x.\delta(x)$ must then be false in the standard model.
To prove this, suppose the opposite. Then
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\forall
y<x.\lnot\delta(y)}\in\operatorname{DEF}$. At the same time there exists the
smallest natural number $n$ such that
$\operatorname{\mathbb{N}}\models\delta(\underline{n})$. It follows that

$\operatorname{\mathbb{N}}\models\forall y<x.\lnot\delta(y)\leftrightarrow
x<\underline{n}\text{.}$

Hence $\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\forall
y<x.\lnot\delta(y)}+\operatorname{Th}(\operatorname{\mathbb{N}})$ is
equivalent to
$\operatorname{CT}^{-}(\underline{n})+\operatorname{Th}(\operatorname{\mathbb{N}})$,
where $\operatorname{Th}(\operatorname{\mathbb{N}})$ denotes the set of
arithmetical sentences which are true in the standard model of arithmetic. It
follows that
$\operatorname{CT}^{-}(\underline{n})+\operatorname{Th}(\operatorname{\mathbb{N}})$
is a theory of truth for $\operatorname{\mathcal{L}_{\operatorname{PA}}}$. But
$\operatorname{Th}(\operatorname{\mathbb{N}})\blacktriangleright\operatorname{CT}^{-}(\underline{n})+\operatorname{Th}(\operatorname{\mathbb{N}})$,
using partial truth predicates $\operatorname{Tr}_{n}$. Hence
$\operatorname{Th}(\operatorname{\mathbb{N}})$ is a theory of truth for
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$. This contradicts Tarski’s
theorem on the undefinability of truth.

Since the sentence $\exists x.\delta(x)$ is false in the standard model,
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\forall
y<x.\lnot\delta(y)}\notin\operatorname{DEF}$. At the same time
$\operatorname{I\Delta_{0}+\exp}\vdash\lnot\delta(\underline{n})$ for every
natural number $n$, by $\Sigma_{1}$-completeness. Hence
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\forall
y<x.\lnot\delta(y)}$ is a definition of truth. A contradiction.

∎

We say that a subset $B$ of a pre-order $(A,\leqslant)$ is _dense_ if for
every $a\in A$ there is $b\in B$ such that $b\leqslant a$.

######  Corollary 39.

Suppose that $B$ is a $\Sigma_{2}$-definable subset of $\operatorname{DEF}$.
Then $B$ is not dense in
$\langle\operatorname{DEF},\blacktriangleleft\rangle.$

###### Proof.

Assume that $B$ is dense in
$\langle\operatorname{DEF},\blacktriangleleft\rangle$, then
$\sigma(x):=\exists\beta\in B.\beta\blacktriangleleft x$ is a definition of
$\operatorname{DEF}$. If $B$ had a $\Sigma_{2}$ definition, then $\sigma(x)$
would be $\Sigma_{2}$, contradicting Theorem 38. ∎

######  Corollary 40.

There are no minimal elements in
$\langle\operatorname{DEF},\blacktriangleleft\rangle$.

###### Proof.

Fix any $\alpha\in\operatorname{DEF}$. Since finite subsets are
$\Sigma_{2}$-definable, then $\\{\alpha\\}$ is not dense, so there is $\beta$
such that $\beta\not\blacktriangleright\alpha$. Then $\alpha\vee\beta$ is a
definition of truth which is strictly smaller than $\alpha$ in
$\langle\operatorname{DEF},\blacktriangleleft\rangle.$ Indeed, let
$\Theta_{\alpha}(x)$ and $\Theta_{\beta}(x)$ be two formulae interpreting the
truth predicate in $\alpha$ and $\beta$ respectively. Then

$(\alpha\rightarrow\Theta_{\alpha}(x))\land(\lnot\alpha\rightarrow\Theta_{\beta}(x))$

acts as a truth-predicate in $\alpha\lor\beta$. Finally,
$\alpha\blacktriangleright\alpha\lor\beta$, because
$\alpha\vdash\alpha\lor\beta$, and
$\alpha\lor\beta\not\blacktriangleright\alpha$, because otherwise
$\beta\blacktriangleright\alpha$, as
$\beta\blacktriangleright\alpha\lor\beta$.

∎

By the remark immediately following Fact 25 we obtain the following

######  Corollary 41.

There are no minimal elements in
$\langle\operatorname{cDEF},\blacktriangleleft\rangle.$

###  3.2 Countable Universal Distributive Lattice

####  3.2.1 Suprema and Infima

theoremthmsupinf The definability order forms a distributive lattice. The
infimum and supremum operations are derived from the propositional operations
as follows.

  * •

The infimum of $\alpha$ and $\beta$ is $\alpha\lor\beta$.

  * •

The supremum of $\alpha$ and $\beta$ is
$\alpha\land\operatorname{rs}_{\alpha}(\beta)$, where
$\operatorname{rs}_{\alpha}(\cdot)$ is a fixed translation that replaces non-
arithmetic relational symbols in $\cdot$ with symbols of the same arity that
are not present in $\alpha$.

The proof is sketched below. See Appendix B for the complete proof.

###### Sketch of proof.

The proof has three parts. First, we show that $\alpha\lor\beta$ and
$\alpha\land\operatorname{rs}_{\alpha}(\beta)$ are syntactically conservative
over $\operatorname{I\Delta_{0}+\exp}$ definitions of truth (whenever $\alpha$
and $\beta$ are such). Then we show that $\alpha\lor\beta$ is an infimum and
$\alpha\land\operatorname{rs}_{\alpha}(\beta)$ is a supremum of $\alpha$ and
$\beta$ (the proof also shows that the operations are well defined as
operations on the equivalence classes of truth definitions modulo the relation
of mutual definability, i.e. if
$\alpha\blacktriangleright\\!\\!\blacktriangleleft\alpha^{\prime}$ and
$\beta\blacktriangleright\\!\\!\blacktriangleleft\beta^{\prime}$, then
$\alpha\lor\beta\blacktriangleright\\!\\!\blacktriangleleft\alpha^{\prime}\lor\beta^{\prime}$
and
$\alpha\land\operatorname{rs}_{\alpha}(\beta)\blacktriangleright\\!\\!\blacktriangleleft\alpha^{\prime}\lor\operatorname{rs}_{\alpha^{\prime}}(\beta^{\prime})$).
We complete the proof by showing that the structure satisfies distributivity
axioms. Only the first part of the proof is presented in full here.

Both $\alpha\lor\beta$ and $\alpha\land\operatorname{rs}_{\alpha}(\beta)$
extend $\operatorname{I\Delta_{0}+\exp}$. Given a sentence
$\sigma\in\operatorname{\mathcal{L}_{\operatorname{PA}}}$, suppose that
$\alpha\lor\beta\vdash\sigma$, then in particular $\alpha\vdash\sigma$, so
$\operatorname{I\Delta_{0}+\exp}\vdash\sigma$ by the conservativity of
$\alpha$. Now suppose that
$\alpha\land\operatorname{rs}_{\alpha}(\beta)\vdash\sigma$, then

$\emptyset\vdash\alpha\rightarrow(\operatorname{rs}_{\alpha}(\beta)\rightarrow\sigma)\text{.}$

Since the sets of the symbols present in $\alpha$ and
$\operatorname{rs}_{\alpha}(\beta)$ respectively, intersect exactly at the
arithmetic symbols, by Craig’s interpolation theorem (see 2.5.5 of [4]), there
exists an arithmetical sentence $\tau$ such that

$\emptyset\vdash\alpha\rightarrow\tau\text{ \ \ and \ \
}\emptyset\vdash\tau\rightarrow(\operatorname{rs}_{\alpha}(\beta)\rightarrow\sigma)\text{,}$

and hence
$\emptyset\vdash\operatorname{rs}_{\alpha}(\beta)\rightarrow(\tau\rightarrow\sigma)$.
The arithmetical consequences of $\alpha$ and
$\operatorname{rs}_{\alpha}(\beta)$ are exactly the same, so
$\emptyset\vdash\operatorname{rs}_{\alpha}(\beta)\rightarrow\tau$, and
therefore $\operatorname{rs}_{\alpha}(\beta)\vdash\sigma$. Hence
$\operatorname{I\Delta_{0}+\exp}\vdash\sigma$, since
$\operatorname{rs}_{\alpha}(\beta)$ is syntactically conservative over
$\operatorname{I\Delta_{0}+\exp}$.

The second part of the proof is analogous to the one given in [18]. The
"$x\cap(y\cup z)=(x\cap y)\cup(x\cap z)$" part of the third part of the proof
is immediate: given definitions of truth $\alpha$, $\beta$ and $\gamma$,

$\alpha\land\operatorname{rs}_{\alpha}(\beta\lor\gamma)=(\alpha\land\operatorname{rs}_{\alpha}(\beta))\lor(\alpha\land\operatorname{rs}_{\alpha}(\gamma))\text{.}$

The "$x\cup(y\cap z)=(x\cup y)\cap(x\cup z)$" part is a little less
straightforward, as the supremum operation involves a language change. To deal
with this, we show how to build suitable "check-case-by-case" translations. ∎

####  3.2.2 Main Result

In this section, we prove that the distributive lattice determined by the
definability order between definitions of truth is a countable universal
distributive lattice.

The range of our embedding consists of weakly compositional defintions of
truth – the definition below uses truth definitions of the form
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}$ as
introduced in Definition 37.

######  Definition 42 (Codomain).

For a formula $\varphi(x)$, we define

$\Delta:=\\{\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi(x)}:\
\forall n\in\omega\
\operatorname{I\Delta_{0}+\exp}\vdash\varphi(\underline{n})\ \land\
\operatorname{I\Delta_{0}+\exp}\vdash\forall x(\varphi(x)\rightarrow\forall
y<x.\varphi(y))\\}.$

######  Remark.

Each member of $\Delta$ is a syntactically conservative over
$\operatorname{I\Delta_{0}+\exp}$ definition of truth. Moreover, if
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi(x)}\in\Delta$,
then, provably in $\operatorname{I\Delta_{0}+\exp}$, $\varphi(x)$ defines an
initial segment containing all natural numbers.

The two lemmata below are crucial in arguing for comparability and
incomparability of elements of $\Delta$ with respect to $\blacktriangleleft$.

######  Lemma 43 (Comparability lemma).

For $\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}$ and
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}$ being
members of $\Delta$,

$\text{if }\operatorname{I\Delta_{0}+\exp}\vdash\forall
x(\alpha(x)\rightarrow\beta(x))\text{, then
}\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}\blacktriangleleft\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\text{.}$

######  Remark.

The antecedant can be weakened to $\exists n\in\omega\
\operatorname{I\Delta_{0}+\exp}\vdash\forall
x(\alpha(x+\underline{n})\rightarrow\beta(x))$.

###### Proof.

If $\operatorname{I\Delta_{0}+\exp}\vdash\forall
x(\alpha(x)\rightarrow\beta(x))$, then

$\operatorname{I\Delta_{0}+\exp}\vdash\forall
x(\beta(x)\rightarrow\operatorname{CT}^{-}(x))\rightarrow\forall
x(\alpha(x)\rightarrow\operatorname{CT}^{-}(x))\text{.}$

Hence
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\vdash\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}$.
Thus
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\blacktriangleright\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}$
via the identity translation. ∎

######  Remark.

To prove the remark, we can use a partial truth predicate built on the top of
the truth predicate of
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}$ (we omit
the details).

######  Lemma 44 (Incomparability lemma).

For $\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}$ and
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}$ being
members of $\Delta$,

$\text{if
}\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}\blacktriangleleft\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\text{,
then }\operatorname{CT_{0}}\vdash\forall x.\alpha(x)\rightarrow\forall
x.\beta(x)\text{.}$

###### Proof.

For a contradiction, suppose that
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\blacktriangleright\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}$
and that $\operatorname{CT_{0}}+\forall x.\alpha(x)\land\exists
x.\lnot\beta(x)$ is consistent. In particular, by the second Gödel’s
incompleteness theorem, there is a model

$\langle\mathcal{M},T\rangle\models\operatorname{CT_{0}}+\forall
x.\alpha(x)\land\exists
x.\lnot\beta(x)+\lnot\operatorname{Con}_{\operatorname{CT_{0}}+\forall
x.\alpha(x)\land\exists x.\lnot\beta(x)}\text{.}$

Let $c\in\mathcal{M}$ be the smallest element such that
$\mathcal{M}\models\lnot\beta(c)$ – such an element exists since
$\operatorname{CT_{0}}\vdash\operatorname{PA}$ and $\beta$ is an arithmetical
formula. Let $T_{c}$ be the set $\\{\varphi\in\mathcal{M}:\
\langle\mathcal{M},T\rangle\models
T(\varphi)\land\operatorname{dpt}(\varphi)\leqslant c\\}$. Then
$\langle\mathcal{M},T_{c}\rangle\models\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}$
and simultaneously $\langle\mathcal{M},T_{c}\rangle$ satisfies the induction
scheme for formulae of $\operatorname{\mathcal{L}_{T}}$ by Fact 22.

We assumed that
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\blacktriangleright\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}$.
This means that there exists $\langle\mathcal{M},T_{c}\rangle$-definable set
$T^{\prime}$ such that
$\langle\mathcal{M},T^{\prime}\rangle\models\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}$.
Since $T^{\prime}$ is definable in $\langle\mathcal{M},T_{c}\rangle$ and
$\langle\mathcal{M},T_{c}\rangle$ satisfies the induction axioms for all
formulae of $\operatorname{\mathcal{L}_{T}}$, then also
$\langle\mathcal{M},T^{\prime}\rangle$ satisfies all induction axioms for
formulae of $\operatorname{\mathcal{L}_{T}}$. Hence
$\langle\mathcal{M},T^{\prime}\rangle\models\operatorname{CT}$, because
$\mathcal{M}\models\forall x.\alpha(x)$.

For a natural number $n$, let
$\operatorname{Tr}^{\operatorname{\mathcal{L}_{T}}}_{n}$ denote the partial
truth predicate for $\operatorname{\mathcal{L}_{T}}$-sentences of logical
depth at most $n$, for which $\operatorname{CT}$ proves the Tarski
compositional clauses. Let us observe that the cut elemination theorem is
provable in Peano Arithmetic (see [14], ch. V, sec. 5(c), thm 5.17), so, by
induction on the lengths of proofs, for each natural number $n$ and
$\operatorname{\mathcal{L}_{T}}$-sentences $\sigma$ and $\tau$ of syntactical
depth not greater than $n$, $\operatorname{CT}$ proves
$\operatorname{Tr}^{\operatorname{\mathcal{L}_{T}}}_{n}(\ulcorner\sigma\urcorner)\land\operatorname{Prov}_{\sigma}(\ulcorner\tau\urcorner)\rightarrow\operatorname{Tr}^{\operatorname{\mathcal{L}_{T}}}_{n}(\ulcorner\tau\urcorner)$.
In particular, $\operatorname{CT}$ proves

$\operatorname{Tr}^{\operatorname{\mathcal{L}_{T}}}_{n}(\ulcorner\operatorname{CT_{0}}+\forall
x.\alpha(x)\land\exists
x.\lnot\beta(x)\urcorner)\land\text{Pr}_{\operatorname{CT_{0}}+\forall
x.\alpha(x)\land\exists x.\lnot\beta(x)}(\ulcorner
0=1\urcorner)\rightarrow\operatorname{Tr}^{\operatorname{\mathcal{L}_{T}}}_{n}(\ulcorner
0=1\urcorner)\text{.}$

Because $\langle\mathcal{M},T^{\prime}\rangle$ is a model of
$\operatorname{CT_{0}}+\forall x.\alpha(x)\land\exists x.\lnot\beta(x)$ and
simultaneously it satisfies $\operatorname{CT}$, it follows from the above
considerations that
$\langle\mathcal{M},T^{\prime}\rangle\models\operatorname{Con}_{\operatorname{CT_{0}}+\forall
x.\alpha(x)\land\exists x.\lnot\beta(x)}$. But this means that
$\mathcal{M}\models\operatorname{Con}_{\operatorname{CT_{0}}+\forall
x.\alpha(x)\land\exists x.\lnot\beta(x)}$ and therefore
$\langle\mathcal{M},T\rangle\models\operatorname{Con}_{\operatorname{CT_{0}}+\forall
x.\alpha(x)\land\exists x.\lnot\beta(x)}$. This contradicts our initial
assumption. ∎

######  Remark.

Ideally, we would like to collapse the comparability and incomparability
lemmata into a single lemma characterising the definability relation between
theories of the form
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}$ in terms
of provability in a fixed theory. At this point we see no natural way of doing
this. Various obstacles and possible ways to overcome them are discussed in
Appendix A.666We thank the anonymous referee for suggestions that led to this
discussion.

######  Lemma 45 (Infima & Suprema).

For $\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}$ and
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}$ being
members of $\Delta$,
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha\land\beta}$
and
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha\lor\beta}$
are members of $\Delta$. In the order generated by
$\langle\Delta,\blacktriangleleft\rangle$,

$\inf\\{\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha},\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\\}=\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha\land\beta}\
\ \text{and}\ \
\sup\\{\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha},\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\\}=\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha\lor\beta}\text{.}$

Moreover, these operations are the same in the definability order
$\langle\operatorname{cDEF},\blacktriangleleft\rangle$.

###### Proof.

Both $\alpha$ and $\beta$ are members of $\Delta$, so they determine cuts in
any model of $\operatorname{I\Delta_{0}+\exp}$. Hence
$\operatorname{I\Delta_{0}+\exp}\vdash\big{(}\forall
x(\alpha(x)\rightarrow\operatorname{CT}^{-}(x))\lor\forall
x(\beta(x)\rightarrow\operatorname{CT}^{-}(x))\big{)}\leftrightarrow\forall
x(\alpha(x)\land\beta(x)\rightarrow\operatorname{CT}^{-}(x))$. and
$\operatorname{I\Delta_{0}+\exp}\vdash\big{(}\forall
x(\alpha(x)\rightarrow\operatorname{CT}^{-}(x))\land\forall
x(\beta(x)\rightarrow\operatorname{CT}^{-}(x))\big{)}\leftrightarrow\forall
x(\alpha(x)\lor\beta(x)\rightarrow\operatorname{CT}^{-}(x))$. In consequence,
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}\land\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\leftrightarrow\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha\lor\beta}$
and
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}\lor\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\leftrightarrow\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha\land\beta}$.
To prove the moreover part, it is enough to observe that
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}\wedge\operatorname{rs}_{\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}\alpha}(\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta})\blacktriangleright\\!\\!\blacktriangleleft\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}\land\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}$.
The definability
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}\land\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\blacktriangleright\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}\wedge\operatorname{rs}_{\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}\alpha}(\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta})$
is straightforward, and the converse direction is witnessed by a disjunctive
translation which first measures which one of $\alpha,\beta$ defines longer
initial segment and then chooses the right truth predicate for the
interpretation. Formally, the interpretation of the predicate is the following
formula:

$\bigl{(}\alpha\subseteq\beta\rightarrow\operatorname{rs}_{\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}\alpha}(T)(x)\bigr{)}\land\bigl{(}\beta\subsetneq\alpha\rightarrow
T(x)\bigr{)}.$

In the above, $\alpha\subseteq\beta$ abbreviates $\forall
x(\alpha(x)\rightarrow\beta(x))$ and the abbreviation $\beta\subsetneq\alpha$
is unravelled accordingly. ∎

######  Definition 46 (Domain of the embedding).

We denote by $\mathbb{B}=\langle
B,\mathbb{0},\mathbb{1},\cap,\cup,\lnot\rangle$ a fixed countable atomless
Boolean algebra such that its domain and all symbols can be represented in
$\operatorname{\mathbb{N}}$ by elementary formulae such that
$\operatorname{I\Delta_{0}+\exp}$ proves that $\mathbb{B}$ is the countable
atomless Boolean algebra. We denote by the above symbols also the formulae
representing the algebra. We let $\leqslant_{\mathbb{B}}$ be the partial order
determined by $\cap$. An example of such a Boolean algebra is given in Section
2.4.

######  Definition 47 (Embedding).

We define a function $F:B\longrightarrow\Delta$. Let $\eta(y)$ be a
$\Sigma_{1}$-formula $\Sigma_{1}$-flexible over arithmetical consequences of
$\operatorname{CT_{0}}+\neg\operatorname{Con}_{\operatorname{CT_{0}}}$ (see
Theorem 11). For $a\in B$, we define $\varphi_{a}(x)$ as
$\operatorname{Con}_{\operatorname{CT_{0}}}(x)\ \lor\ $"$\\{y:\ \eta(y)\\}$ is
an ultrafilter on $\mathbb{B}$ containing $\underline{a}$" and put
$F(a)=\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}}$.
By "$\\{y:\ \eta(y)\\}$ is an ultrafilter on $\mathbb{B}$ containing
$\underline{a}$" we mean the conjunction of the following sentences (cf. 36):

  * •

$\forall y(\eta(y)\rightarrow y\in B)$,

  * •

$\eta(\mathbb{1})\land\lnot\eta(\mathbb{0})\land\eta(\underline{a})$,

  * •

$\forall y,z\in B(\eta(y)\land\eta(z)\rightarrow\eta(y\cap z))$,

  * •

$\forall y,z\in B(\eta(y)\land y\leqslant_{\mathbb{B}}z\rightarrow\eta(z))$,

  * •

$\forall y\in B(\eta(y)\lor\eta(\lnot y))$.

######  Remark.

Since for each $n\in\omega$,
$\operatorname{Con}_{\operatorname{CT}_{0}}(\underline{n})$ is a true
$\Delta_{0}$-sentence, then for each $a\in B$ and $n\in\omega$,
$\operatorname{I\Delta_{0}+\exp}\vdash\varphi_{a}(\underline{n})$. Downward
closure of each $\varphi_{a}(x)$ is immediate. In consequence for each $a\in
B$, $\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}}$
is a member of $\Delta$.

######  Theorem 48 (Main Theorem).

The above defined function $F$ is a lattice embedding. Therefore the
definability order $\langle\operatorname{cDEF},\blacktriangleleft\rangle$ is a
countable universal distributive lattice.

###### Proof.

The second part of the theorem follows by the first part and Lemma 45. To
prove that $F$ is a lattice embedding, we show that $F$ is injective and that
it preservers operations of taking infimum and supremum.

For the former, assume the contrary and let $a$ and $b$ be elements of $B$
s.t. $a\nleqslant_{\mathbb{B}}b$ but
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}}\blacktriangleleft\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{b}}$.
By Lemma 44, $\operatorname{CT_{0}}\vdash\forall
x.\varphi_{a}(x)\rightarrow\forall x.\varphi_{b}(x)$. Hence, by definitions of
$\varphi_{a}$ and $\varphi_{b}$,
$\operatorname{CT_{0}}+\neg\operatorname{Con}_{\operatorname{CT_{0}}}$ proves

$\text{"}\\{y:\ \eta(y)\\}\text{ is an ultrafilter containing
}\underline{a}\text{"}\rightarrow\text{"}\\{y:\ \eta(y)\\}\text{ is an
ultrafilter containing }\underline{b}\text{".}$

By the fliexibility of $\eta(y)$ and properties of Boolean algebras (provable
in $\operatorname{I\Delta_{0}+\exp}$), to obtain a contradiction, it is enough
to show that there is an arithmetical $\Sigma_{1}$-formula $\mu(y)$ s.t.

$\operatorname{PA}\vdash\text{"}\\{y:\ \mu(y)\\}\text{ is an ultrafilter
containing }\underline{a\cap\lnot b}\text{"}$

(notice that $a\cap\lnot b\neq\mathbb{0}$ as $a\nleqslant_{\mathbb{B}}b$). To
this end, we use a formula which describes an explicit process of computing an
ultrafilter on $\mathbb{B}$ which contains $a\cap\lnot b$. Let $\nu(s,y)$ be
the conjunction of the following formulae ($s_{z}$ denotes the $z$-th element
of the sequence $s$):

  * •

$y\in B$,

  * •

$s_{0}=\underline{a\cap\lnot b}$,

  * •

$s_{y+1}\cap y\neq\mathbb{0}$,

  * •

$\forall z\leqslant y(z\in B\land s_{z}\cap z\neq\mathbb{0}\rightarrow
s_{z+1}=s_{z}\cap z)$,

  * •

$\forall z\leqslant y(z\in B\land s_{z}\cap z=\mathbb{0}\rightarrow
s_{z+1}=s_{z}\cap\lnot z)$,

  * •

$\forall z\leqslant y(z\notin B\rightarrow s_{z+1}=s_{z})$.

We put: $\mu(y):=\exists s.\nu(s,y)$. In $\operatorname{PA}$, the above is
equivalent to a $\Sigma_{1}$-formula by the assumption that $\mathbb{B}$ has
an elementary definition. Because
$\operatorname{CT_{0}}\vdash\operatorname{PA}$ (see 22), we can use induction
to check that $\operatorname{CT_{0}}$ proves each of the following (the
details are omitted):

  * •

$\mu(\mathbb{1})\land\lnot\mu(\mathbb{0})$,

  * •

$\forall y,z\in B(\mu(y)\land\mu(z)\rightarrow\mu(y\cap z))$,

  * •

$\forall y,z\in B(\mu(y)\land y\leqslant_{\mathbb{B}}z\rightarrow\mu(z))$,

  * •

$\forall y\in B(\mu(y)\lor\mu(\lnot y))$,

  * •

$\mu(\underline{a})\land\lnot\mu(\underline{b})$.

It remains to prove that $F$ preserves operations of taking infimum and
supremum. Let $a$ and $b$ be elements of $B$. Then
$\inf\\{F(a),F(b)\\}=\inf\\{\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}},\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{b}}\\}=\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}\land\varphi_{b}}$,
by definition of $F$ and Lemma 45. Analogously,
$\sup\\{F(a),F(b)\\}=\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}\lor\varphi_{b}}$.
Hence it is enough to show that $\operatorname{I\Delta_{0}+\exp}\vdash\forall
x(\varphi_{a}(x)\land\varphi_{b}(x)\leftrightarrow\varphi_{a\cap b}(x))$ and
$\operatorname{I\Delta_{0}+\exp}\vdash\forall
x(\varphi_{a}(x)\lor\varphi_{b}(x)\leftrightarrow\varphi_{a\cup b}(x))$. By
definitions of $\varphi_{a}$ and $\varphi_{b}$, it suffices to check that
$\operatorname{I\Delta_{0}+\exp}$ proves

$\text{"}\\{y:\ \eta(y)\\}\text{ is an
ultrafilter"}\rightarrow\big{(}(\eta(\underline{a})\land\eta(\underline{b})\leftrightarrow\eta(\underline{a\cap
b}))\land(\eta(\underline{a})\lor\eta(\underline{b})\leftrightarrow\eta(\underline{a\cup
b}))\big{)}\text{.}$

This is true because $\mathbb{B}$ is elementarily presented, so the
equivalence between the second and third points in Fact 36 for
$\mathcal{F}=\eta$ can be proved in $\operatorname{I\Delta_{0}+\exp}$.

∎

##  4 Other Structural Properties

Let us begin by introducing a definition of truth that is essentially
different from any of the theories
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}$ used in
the construction of our embedding.

######  Definition 49.

Let $\operatorname{TCut}$ be the conjunction of
$\operatorname{I\Delta_{0}+\exp}$ and the following
$\operatorname{\mathcal{L}_{T}}$-sentence:

$\forall x\bigl{(}\forall
y<x.\operatorname{CT}^{-}(y)\rightarrow\operatorname{CT}^{-}(x)\bigr{)}.$

######  Remark.

$\operatorname{TCut}$ is a definition of truth and
$\operatorname{CT}^{-}\vdash\operatorname{TCut}$. In particular
$\operatorname{TCut}$ is conservative over $\operatorname{I\Delta_{0}+\exp}$.
In [11] it is shown that $\operatorname{TCut}$ is mutually definable with a
theory WPT-, which is a compositional theory of truth which compositional
axioms are modelled after the Weak Kleene Logic.

The following proposition witnesses that $\operatorname{TCut}$ is semantically
conservative over $\operatorname{I\Delta_{0}+\exp}$.

######  Proposition 50.

For every model $\mathcal{M}\models\operatorname{I\Delta_{0}+\exp}$ there
exists $T\subseteq M$ such that
$\langle\mathcal{M},T\rangle\models\operatorname{TCut}$.

###### Sketch of proof.

Fix $\mathcal{M}$. We put $T=\\{\varphi\in M:\exists n\in\omega\ \
\mathcal{M}\models\operatorname{Tr}_{n}(\varphi)\\}.$ ∎

For the notion of recursive saturation, consult [16].

######  Proposition 51.

If $\mathcal{M}\models\operatorname{PA}$ is such that for some
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}\in\Delta$
and some $T\subseteq M$,
$\langle\mathcal{M},T\rangle\models\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}$,
then $\mathcal{M}$ is recursively saturated.

###### Proof.

Assume $\mathcal{M}\models\operatorname{PA}$ and fix $\varphi$ such that
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}\in\Delta$.
By the overspill principle (see [16]) it follows that there is a nonstandard
$a\in M$ such that $\mathcal{M}\models\forall x<a.\varphi(x).$ Assume that for
some $T\subseteq M$,
$\langle\mathcal{M},T\rangle\models\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}$.
In particular $\langle\mathcal{M},T\rangle\models\operatorname{CT}^{-}(a)$,
hence $T$ is a partial nonstandard satisfaction class on $\mathcal{M}$.777More
precisely $T$ encodes in a canonical way a partial nonstandard satisfaction
class. Hence $\mathcal{M}$ must be recursively saturated by Lachlan’s theorem
(see [16]). ∎

The first part of the next proposition follows directly from the observation
that if $A$ is semantically conservative over $B$ and $A$ defines a theory
$C$, then $C$ must also be semantically conservative over $B$ as well (we
include a proof below for the sake of completeness; for an overview of various
reducibility notions between theories of truth, see [8]).

######  Proposition 52.

In $\langle\operatorname{DEF},\blacktriangleleft\rangle$:

  1. 1.

no element of $\Delta$ is below $\operatorname{TCut}$,

  2. 2.

for every
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}\in\Delta$
such that $\operatorname{CT_{0}}\nvdash\forall x.\varphi(x)$,
$\operatorname{TCut}$ is not below
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}$.

In particular for every $a\in\mathbb{B}$,
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}}$ is
incomparable with $\operatorname{TCut}$.

###### Proof.

For the first, suppose that there is
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}\in\Delta$
such that
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}\blacktriangleleft\operatorname{TCut}$.
Let $\Theta(x)$ be a definition of $T$, such that
$\operatorname{TCut}\vdash\sigma[\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}]$,
where $\sigma$ is the (unique) translation such that $\sigma(T)=\Theta$. Take
any $\mathcal{M}\models\operatorname{PA}$ which is not recursively saturated.
By Proposition 50, let $T$ be such that
$\langle\mathcal{M},T\rangle\models\operatorname{TCut}$. Let $T^{\prime}$ be
the set defined in $\langle\mathcal{M},T\rangle$ by $\Theta$. Then
$\langle\mathcal{M},T^{\prime}\rangle\models\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}$,
what contradicts Proposition 51.

For the second, we use an analogous argument to that presented in 44. This is
possible since
$\operatorname{TCut}+\operatorname{IND}(\operatorname{\mathcal{L}_{T}})\vdash\operatorname{CT}$.
Aiming at a contradiction, assume that for some $\varphi$, such that
$\operatorname{CT_{0}}\nvdash\forall x.\varphi(x)$,
$\operatorname{TCut}\blacktriangleleft\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}$.
Take $\langle\mathcal{M},T\rangle\models\operatorname{CT_{0}}+\exists
x.\neg\varphi(x)+\neg\operatorname{Con}_{\operatorname{CT_{0}}+\exists
x.\neg\varphi(x)}.$ For the least $a$ such that
$\mathcal{M}\models\neg\varphi(a)$, we see that
$\langle\mathcal{M},T_{a}\rangle\models\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}+\operatorname{IND}(\operatorname{\mathcal{L}_{T}})$.
Hence, by our assumption, there is $T^{\prime}$ such that
$\langle\mathcal{M},T^{\prime}\rangle\models\operatorname{TCut}+\operatorname{IND}(\operatorname{\mathcal{L}_{T}})$.
However, then
$\mathcal{M}\models\operatorname{Con}_{\operatorname{CT_{0}}+\exists
x.\neg\varphi(x)},$ a contradiction. ∎

Let us put
$\Delta\vee\operatorname{TCut}:=\\{\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}\vee\operatorname{TCut}:\
\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi}\in\Delta\\}$.
Then we can reprove Main Theorem for $\Delta\vee\operatorname{TCut}$ instead
of $\Delta$. The next theorem provides us with another way of realizing the
embedding of $\mathbb{B}$ into c$\operatorname{DEF}$. This time the image of
the embedding consists uniquely of theories $\blacktriangleleft$-below
$\operatorname{TCut}$.

######  Theorem 53.

$\Delta\vee\operatorname{TCut}$ is a countable universal distributive lattice.

###### Sketch of proof.

It is easy to see that $\Delta\vee\operatorname{TCut}$ is indeed a sublattice
of c$\operatorname{DEF}$. It is also easy to see that the function

$a\longmapsto\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}}\lor\
\operatorname{TCut}\text{,}$

where $\varphi_{a}$ is defined as in Section 3.2.2, preserves suprema and
infima as the function $F$ from Section 3.2.2 preserves them. Hence it is
enough to show that this function is injective. Equivalently, for
$a\neq\mathbb{0}$, it is not true that

$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}}\lor\
\operatorname{TCut}\blacktriangleright\\!\\!\blacktriangleleft\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{\mathbb{0}}}\lor\
\operatorname{TCut}\text{.}$

We prove that
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}}\lor\
\operatorname{TCut}\not\blacktriangleleft\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{\mathbb{0}}}$.
We begin by constructing a model of

$\operatorname{CT_{0}}+\forall x.\varphi_{a}+\lnot\forall
x.\varphi_{\mathbb{0}}=\operatorname{CT_{0}}+\forall
x.\varphi_{a}+\lnot\operatorname{Con}_{\operatorname{CT_{0}}}\text{.}$

Then proceed similarly as in the proof of Lemma 44 obtaining a model
$\langle\mathcal{M},T_{c}\rangle\models\forall
x.\varphi_{a}+\text{IND}(\operatorname{\mathcal{L}_{T}})+\lnot\operatorname{Con}_{\operatorname{CT_{0}}}$.
It cannot define
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\varphi_{a}}\lor\
\operatorname{TCut}$ as $\mathcal{M}$ cannot be expanded to a model of
$\operatorname{CT}$.

∎

Unfortunately, we still do not know if there is a truth definition for
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$ that does not define
$\operatorname{UTB}^{-}$. We get the following small insight, which crucially
relies on the observation due to Volker Halbach (see [15], Proposition 9.2).

######  Proposition 54.

If $\alpha$ is a definition of truth for
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$, then there is a true
$\Pi_{2}$-sentence $\pi$, such that
$\operatorname{UTB}\blacktriangleleft\alpha+\pi+\operatorname{IND}(\mathcal{L}_{\alpha}).$

###### Proof.

Fix $\alpha\in\operatorname{DEF}$ and let $\pi$ be the $\Pi_{2}$
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$-sentence saying “$\alpha$
defines $\operatorname{TB}^{-}$ by the use of $\Theta(x)$”, where $\Theta(x)$
witnesses the definability of $\operatorname{TB}^{-}$ in $\alpha$. By the
Kreisel-Levy theorem (see [1]) we conclude that the uniform reflection
principle over $\alpha$ is provable in
$\alpha+\operatorname{IND}(\mathcal{L}_{\alpha})$. That is, for every
$\mathcal{L}_{\alpha}$-formula $\varphi(x)$ the following sentence is provable
in $\alpha+\operatorname{IND}(\mathcal{L}_{\alpha})$

$\forall
x\bigl{(}\operatorname{Prov}_{\alpha}[\varphi(\dot{x})]\rightarrow\varphi(x)\bigr{)}.$

Fix any $\operatorname{\mathcal{L}_{\operatorname{PA}}}$ formula $\psi(x)$ and
observe that

$\pi+\operatorname{I\Delta_{0}+\exp}\vdash\forall
x.\operatorname{Prov}_{\alpha}[\Theta[\psi(\dot{\dot{x}})]\leftrightarrow\psi(\dot{x})].$

Hence, by uniform reflection, we obtain

$\pi+\operatorname{IND}(\mathcal{L}_{\alpha})+\alpha\vdash\forall
x\bigl{(}\Theta[\psi(\dot{x})]\leftrightarrow\psi(x)\bigr{)}.$

∎

The corollary below witnesses that the canonical compositional definition of
truth is optimal up to the quantifier complexity. The core of the argument (in
the proof of Theorem 57) follows from the well-known property of strict
$\Sigma^{1}_{1}$ formulae. Since we would like to make the paper self-
contained we present also a proof which does not use a detour through
subsystems of Second Order Arithmetic. Both reasonings are essentially the
same: the key role in the first one is played by the Weak König’s Lemma, while
the second uses the arithmetized completeness theorem. We recall the
definition and theorem from [21], Section VIII.2

######  Definition 55.

A formula $\phi$ is strict $\Sigma_{1}^{1}$ ($\phi\in S\Sigma^{1}_{1}$) if
$\phi$ is of the form $\exists X\psi$, for some $\psi\in\Pi^{0}_{1}$.

######  Theorem 56.

Let $\mathcal{M}^{\prime}$ be a model of WKL0 and $\mathcal{M}$ be an
arbitrary $\omega$-submodel of $\mathcal{M}^{\prime}$ (that is the universe of
first-order objects of $\mathcal{M}$ and $\mathcal{M}^{\prime}$ are the same).
Then the following conditions are quivalent

  1. 1.

$\mathcal{M}$ is a model of WKL0.

  2. 2.

$\mathcal{M}$ and $\mathcal{M}^{\prime}$ satisfy the same strict
$\Sigma^{1}_{1}$ formulae (with parameters from $\mathcal{M}$).

We say that a sentence $\alpha$ has a standard model if the standard model of
arithmetic, $\operatorname{\mathbb{N}}$, can be expanded to a model of
$\alpha$. That is, in $\operatorname{\mathbb{N}}$ one can find interpretations
for additional symbols used in $\alpha$ in such a way that the expanded
structure makes $\alpha$ true. Without loss of generality, we assume that
apart from the symbols for the arithmetical operations, sentences that we
consider use a single unary predicate $P$ (this can be assumed thanks to the
definable pairing function in $\operatorname{I\Delta_{0}+\exp}$).

######  Theorem 57.

If $\alpha$ is a $\Sigma_{2}$-sentence such that

  * •

$\alpha$ has a standard model and

  * •

the only non-logical, non-arithmetic symbol that occurs in $\alpha$ is a unary
relation symbol $P$,

then there is an arithmetically definable set $A$ such that
$(\mathbb{N},A)\models\alpha$.

###### First proof.

Fix $\alpha:=\exists x.\beta(x)$, where $\beta$ is $\Pi_{1}$, and assume that
$B$ is such that $(\mathbb{N},B)\models\alpha$. Fix $n$ such that
$(\mathbb{N},B)\models\beta(n)$. Since $n$ can be named with a standard
numeral we will stop mentioning it. Let $\mathcal{X}$ be the least set
containing $B$, closed under the Turing Jumps and Turing Reducibility. Then
$(\mathbb{N},\mathcal{X})\models\textnormal{ACA}_{0}$. Since
$B\in\mathcal{X}$, $(\mathbb{N},\mathcal{X})\models\exists X.\beta[t\in
X/P(t)]$ (that is: each occurrence of $P(t)$ for a term $t$ is replaced in
$\beta$ with $t\in X$). Since $\beta[t\in X/P(t)]$ is $\Pi^{0}_{1}$, $\exists
X.\beta[t\in X/P(t)]$ is a strict $\Sigma^{1}_{1}$ formula. Therefore, since
$\textnormal{Def}(\mathbb{N})\subseteq\mathcal{X}$, by Theorem 56,
$(\mathbb{N},\textnormal{Def}(\mathbb{N}))\models\exists X.\beta[t\in
X/P(t)],$ where $\textnormal{Def}(\mathbb{N})$ is the collection of
arithmetically definable subsets of $\mathbb{N}$. Hence, there is an
arithmetically definable subset $A$ such that $(\mathbb{N},A)\models\alpha$. ∎

The second proof of the theorem uses, instead of the Weak König’s Lemma, some
standard techniques related to the arithmetized completeness theorem. We
briefly recall this material, redirecting to [9], Section 2.3 for the details.
We say that a model $\mathcal{N}$ is _strongly interpretable_ in a model
$\mathcal{M}$ if:

  1. 1.

the domain of $\mathcal{N}$ and the functions and relations of $\mathcal{N}$
are definable subsets of $\mathcal{M}$;

  2. 2.

there is an $\mathcal{M}$-definable relation $S_{\mathcal{N}}$ such that in
$\mathcal{M}$ it is true that $S_{\mathcal{N}}$ is a satisfaction relation for
$\mathcal{N}$.

If $\mathcal{N}\models\operatorname{PA}^{-}$ is strongly interpretable in
$\mathcal{M}\models\operatorname{PA}$, then there is an
$\mathcal{M}$-definable initial embedding $\iota:M\rightarrow N$, which makes
$\mathcal{M}$ an initial segment of $\mathcal{N}$ (if $b\in M$ and
$\mathcal{N}\models a<b$, then $a\in M$). Finally, if
$\mathcal{M}\models\operatorname{PA}+\operatorname{Con}(Th)$, then there is a
model $\mathcal{N}\models Th$, which is strongly interpretable in
$\mathcal{M}$.

###### Second proof of Theorem 57.

Fix any $\alpha:=\exists x.\beta(x)$, where $\beta$ is $\Pi_{1}$, and suppose
it satisfies the assumptions. Since $\alpha$ has a standard model, there is an
$n\in\omega$ such that $\beta(\underline{n})$ has a standard model as well. By
our assumptions
$\mathbb{N}\models\operatorname{Con}(\ulcorner\beta(\underline{n})\urcorner)$.
By the arithmetized completeness theorem, there is
$\mathcal{M}\models\beta(\underline{n})$ which is strongly interpretable in
$\mathbb{N}$. Let $\iota$ be the embedding of $\mathbb{N}$ onto an initial
segment of $\mathcal{M}$, $P^{\mathcal{M}}$ be the $\mathbb{N}$-definable
interpretation for $P$ in $\mathcal{M}$ and $\iota[\mathbb{N}]$ be the image
of $\iota$ (which is $\mathbb{N}$-definable as well). Define
$A:=\iota[\mathbb{N}]\cap P^{\mathcal{M}}$. Then $A$ is definable in
$\mathbb{N}$ and $(\mathbb{N},A)$ is a submodel of $\mathcal{M}$. Also, since
$\mathbb{N}$ is an initial segment of $\mathcal{M}$ closed under
multiplication and $\beta(\underline{n})$ is a $\Pi_{1}$-formula, then
$(\mathbb{N},A)\models\beta(\underline{n})$. ∎

######  Corollary 58.

If $\alpha$ satisfies the assumptions of Theorem 57, then
$\operatorname{Th}(\mathbb{N})+\alpha$ is not a theory of truth for
$\operatorname{\mathcal{L}_{\operatorname{PA}}}$.

##  5 Open Questions

Despite our efforts, the main question motivating our investigations remains
open. We state it once again for future reference:

##### Question 1

Is there $\alpha\in\operatorname{DEF}$ that does not define
$\operatorname{UTB}^{-}$?

In Theorem 38 we proved that $\operatorname{DEF}$ is not
$\Sigma_{2}$-definable. The natural definition of this set is $\Sigma_{3}$, so
it is natural to ask:

##### Question 2

Is $\operatorname{DEF}$ a $\Pi_{3}$-definable set?

Additionally we would like to know more about the structure of
$(\operatorname{DEF},\blacktriangleleft)$. For two definitions of truth
$\alpha,\ \beta$, let us put $[\alpha,\beta]:=\\{\gamma:\
\alpha\blacktriangleleft\gamma\blacktriangleleft\beta\\}$.

##### Question 3

Is it true that for all $\alpha\blacktriangleleft\beta$, if the interval
$[\alpha,\beta]$ is finite, then $\beta\blacktriangleleft\alpha$?

##### Question 4

Are there $\alpha,\beta\in\operatorname{cDEF}$ such that the sublattice
$\langle[\alpha,\beta],\blacktriangleleft\rangle\subseteq\langle\operatorname{DEF},\blacktriangleleft\rangle$
has the structure of the atomless Boolean algebra? In particular, is it true
for $\alpha=\operatorname{TCut}$ and $\beta=\operatorname{CT}^{-}$? Does the
answer change if we drop the requirement that the algebra is atomless?

The last question is motivated by the typical uses of the truth predicate in
obtaining finite axiomatizations of infinite theories. See [7] for relevant
context and definitions.

##### Question 5

Is there a definition of truth $\alpha$ (with a formula $\Theta(x)$ as an
interpretation of the truth predicate) such that $\alpha+\forall
x\bigl{(}\textnormal{Ax}_{\operatorname{PA}}(x)\rightarrow\Theta(x)\bigr{)}$
has at most polynomial speed-up over $\operatorname{PA}$?
$\textnormal{Ax}_{\operatorname{PA}}(x)$ is the canonical formula which
strongly represents the set of axioms of $\operatorname{PA}$ in
$\operatorname{I\Delta_{0}+\exp}$.

## References

  * [1] Lev Beklemishev.  Reflection principles and provability algebras in formal arithmetic.  Russian Mathematical Surveys, 60(2):197–268, 2005.
  * [2] Lev Beklemishev and Fedor Pakhomov.  Reflection algebras and conservation results for theories of iterated truth.  Annals of Pure and Applied Logic, 173(5):103093, 2022.
  * [3] Rasmus Blanck.  Contributions to the Metamathematics of Arithmetic: Fixed Points, Independence, and Flexibility, volume 30 of Acta Philosophica Gothoburgensia.  University of Gothenburg, 2017.
  * [4] Samuel Buss, editor.  Handbook of proof theory.  Elsevier, 1998.
  * [5] Costas Dimitracopoulos and Haim Gaifman.  Fragments of Peano’s arithmetic and the MRDP theorem.  In Logic and Algorithmic, volume 30 of Monographie de L’Enseignement Mathématique. Université de Genève, 1982.
  * [6] Ali Enayat and Mateusz Łełyk.  Axiomatizations of Peano arithmetic: A truth-theoretic view.  The Journal of Symbolic Logic, page 1–30, 2022.
  * [7] Ali Enayat, Mateusz Łełyk, and Bartosz Wcisło.  Truth and feasible reducibility.  The Journal of Symbolic Logic, 85(1):367–421, 2020.
  * [8] Mateusz Łełyk.  Comparing axiomatic theories of truth.  Studia Semiotyczne, 33(2):255–286, 2019.
  * [9] Mateusz Łełyk.  Model theory and proof theory of the global reflection principle.  The Journal of Symbolic Logic, 88(2):738–779, 2023.
  * [10] Mateusz Łełyk and Bartosz Wcisło.  Universal properties of truth.  https://arxiv.org/abs/2304.00370.
  * [11] Mateusz Łełyk and Bartosz Wcisło.  Models of positive truth.  The Review of Symbolic Logic, 12(1):144–172, 2019.
  * [12] Mateusz Łełyk and Bartosz Wcisło.  Local collection and end-extensions of models of compositional truth.  Annals of Pure and Applied Logic, 172(6):102941, 2021.
  * [13] George Grätzer.  Lattice Theory: Foundation.  Birkhauser, 2011.
  * [14] Petr Hájek and Pavel Pudlák.  Metamathematics of first-order arithmetic.  Springer, 1998.
  * [15] Volker Halbach.  Disquotational truth and analyticity.  The Journal of Symbolic Logic, 66(4):1959–1973, 2001.
  * [16] Richard Kaye.  Models of Peano Arithmetic.  Oxford: Clarendon Press, 1991.
  * [17] James Monk and Robert Bonnet, editors.  Handbook of Boolean algebras.  Elsevier, 1989.
  * [18] Jan Mycielski.  A lattice of interpretability types of theories.  The Journal of Symbolic Logic, 42(2):297–305, June 1977.
  * [19] Fedor Pakhomov and Albert Visser.  On a question of Krajewski’s.  The Journal of Symbolic Logic, 84:343 – 358, 2019.
  * [20] Richard Pettigrew.  On interpretations of bounded arithmetic and bounded set theory.  Notre Dame Journal of Formal Logic, 50:141–151, 2008.
  * [21] Stephen G. Simpson.  Subsystems of Second Order Arithmetic.  Perspectives in Logic. Cambridge University Press, 2 edition, 2009.
  * [22] Stuart T. Smith.  Nonstandard definability.  Annals of Pure and Applied Logic, 42(1):21–43, 1989.
  * [23] Stijn Vermeeren.  Embedding into the countable atomless Boolean algebra, 2010.  https://stijnvermeeren.be/files/mathematics/embeddings.pdf.
  * [24] Albert Visser.  Enayat theories, 2019.  https://arxiv.org/abs/1909.08877.
  * [25] Albert Visser.  The small-is-very-small principle.  Mathematical Logic Quarterly, 65(4):453–478, 2019.
  * [26] Albert Visser and Ali Enayat.  New constructions of satisfaction classes.  In Kentaro Fujimoto, José Martínez Fernández, Henri Galinon, and Theodora Achourioti, editors, Unifying the Philosophy of Truth. Springer Verlag, 2015.

##  Appendix A Characterizations of definability in terms of provability

Now we return to the problem of unifying our methods of showing comparability
(Lemma 43) and incomparability (Lemma 44) of theories of the form
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}$, with
respect to the relation of definability. We note that there is indeed a
significant logical gap between the two lemmata: the sufficient condition for
the definability is given in the comparability lemma in terms of provability
in $\operatorname{I\Delta_{0}+\exp}$, while the necessary condition in the
incomparability lemma uses a much stronger theory, $\operatorname{CT}_{0}$.
The arithmetical consequences of the latter theory of truth are exhausted only
by the union of all finite iterations of uniform reflection principles over
$\operatorname{PA}$, the theory usually denoted by
$\textnormal{RFN}^{<\omega}(\operatorname{PA})$. A natural conjecture would be
that the condition mentioned in the remark immediately following the
comparability lemma is not only sufficient, but also necessary, i.e. we have
the following equivalence for any $\alpha,\beta$ such that
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha},\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\in\Delta$:

$\bigl{(}\exists n\in\omega\ \operatorname{I\Delta_{0}+\exp}\vdash\forall
x(\alpha(x+\underline{n})\rightarrow\beta(x))\bigr{)}\iff\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}\blacktriangleleft\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}.$
($*$)

As we already remarked, the left-to-right implication indeed holds. For the
converse one, one could try the following strategy: assume that
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}\blacktriangleleft\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}$
but for every $n\in\omega$ $\operatorname{I\Delta_{0}+\exp}+\exists
x(\alpha(x+n)\wedge\neg\beta(x))$ is consistent. Then by a straightforward
compactness argument, one can show that there is a model
$\mathcal{M}\models\operatorname{I\Delta_{0}+\exp}$, in which for some number
$c>\omega$, the length of the initial segment determined by $\alpha$ is at
least by $c$ greater than the length of the initial segment determined by
$\beta$. The same relation between $\alpha$ and $\beta$ holds in any
elementary extension of $\mathcal{M}$. However, there is $\mathcal{N}$, an
elementary extension of $\mathcal{M}$, in which there is a subset $T\subseteq
N$ such that $(\mathcal{N},T)\models\operatorname{CT}^{-}$ (see e.g. [26]).
Consider $T_{\beta}:=\\{\sigma\in N:\sigma\in
T\wedge\mathcal{N}\models\beta(\operatorname{dpt}(\sigma))\\}$. Then
$(\mathcal{N},T_{\beta})\models\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}$.
So there is a formula $\Theta(x)\in\operatorname{\mathcal{L}_{T}}$ such that
$(\mathcal{N},T_{\beta})\models\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}[\Theta(x)/T(x)]$.
In the previous sentence, and below, for
$\Phi(x)\in\operatorname{\mathcal{L}_{T}}$ and any formu $\Psi(x)$,

$\Phi[\Psi(t)/T(t)]$

denotes the result if a substitution of a formula $\Psi(t)$ for any occurrence
of a formula $T(t)$, possibly preceded by renaming the bounded variables. The
last conclusion may seem contradictory, since e.g. in the standard model one
can define partial truth predicates, but the truth predicate for all formulae
is not definable. However, this intuition breaks down in the case of
nonstadard models and truth predicates that do not have to satisfy induction
axioms888We are grateful to Bartosz Wcisło for pointing out this application
of Smith’s theorem..

######  Proposition 59 (Wcisło).

Assume that $\mathcal{M}$ is a countable and recursively saturated model of
$\operatorname{PA}$ and $c\in M$ is a nonstadard element which is definable
without parameters in $\mathcal{M}$. Then, there is $T\subseteq M$ such that
$(\mathcal{M},T)\models\operatorname{CT}^{-}(c)\wedge\forall
x\bigl{(}T(x)\rightarrow\operatorname{dpt}(x)\leqslant c\bigr{)}$ and for some
formula $\Theta(x)$,
$(\mathcal{M},T)\models\operatorname{CT}^{-}[\Theta(x)/T(x)]$.

In other words, for an arbitrary countable recursively satrurated model and
for an arbitrary nonstandard definable $c$, one can find a truth predicate for
sentences of depth at most $c$, which can define a full truth predicate for
all sentences in the sense of $\mathcal{M}$.

###### Sketch of proof.

Fix $\mathcal{M}$ and $c$ as in the assumptions. Let $\varepsilon_{k}(x)$ be a
formula defined inductively

$\displaystyle\varepsilon_{0}(x)$ $\displaystyle:=x=x$
$\displaystyle\varepsilon_{k+1}(x)$
$\displaystyle:=\varepsilon_{k}(x)\vee\varepsilon_{k}(x)$

Thus the syntactic tree of $\varepsilon_{k}(x)$ is a full binary tree of depth
$k$ with internal vertices and root labelled by disjunctions and with the
formula $x=x$ in the leaves. Let $T^{\prime}\subseteq M$ be such that
$(\mathcal{M},T^{\prime})\models\operatorname{CT}^{-}$ and
$(\mathcal{M},T^{\prime})$ is recursively saturated (such a $T^{\prime}$
exists by the conservativity of $\operatorname{CT}^{-}$ over
$\operatorname{PA}$ and the chronic resplendency of countable recursively
saturated models). Then, by Theorem 3.3 of [22], there is a
$T^{\prime\prime}\subseteq M$ such that
$(\mathcal{M},T^{\prime\prime})\models\operatorname{CT}^{-}$ and999Smith’s
theorem is stated for a satisfaction class, but it also works for models of
$\operatorname{CT}^{-}$.

$T^{\prime}:=\\{a\in M:(\mathcal{M},T^{\prime\prime})\models
T^{\prime\prime}[\varepsilon_{c}(\dot{a})]\\}.$

Observe now that $\varepsilon_{c}(x)$ is a formula of depth $c$ and it is
definable without parameters (since it is definable from $c$). Hence, for
$T:=\\{\sigma\in M:\sigma\in
T^{\prime\prime}\wedge\mathcal{M}\models\operatorname{dpt}(\sigma)\leqslant
c\\}$, set $T^{\prime}$ is definable without parameters in
$(\mathcal{M},T)\models\operatorname{CT}^{-}(c)\wedge\forall
x\bigl{(}T(x)\rightarrow\operatorname{dpt}(x)\leqslant c\bigr{)}.$ ∎

Obviously, the above example is not sufficient to disprove conjecture ($*$ ‣
A). However, we see no way to fix the proof strategy described above.

Having said that, we note that if we assume that our definitions of truth
extend $\operatorname{PA}$ instead of $\operatorname{I\Delta_{0}+\exp}$ (i.e.
are "finitely axiomatisable modulo $\operatorname{PA}$"), then we have the
following version of the incomparability lemma. To motivate the formulation of
the thesis, let us observe that there is a constant $k$ such that for all
$n>0$, $\operatorname{Tr}_{n}(x)$ (see "The arithmetization of syntax and
metalogic" in the preliminaries) has depth at most $k\cdot n$. Let $k_{0}$ be
the least such $k$.

######  Proposition 60.

For all $\alpha$, $\beta$ such that
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha},\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}\in\Delta$,

$(\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}+\operatorname{PA})\blacktriangleleft(\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}+\operatorname{PA})\Longrightarrow\bigl{(}\exists
n\in\omega\ \operatorname{PA}\vdash\forall x(\alpha(k_{0}\cdot
x+n)\rightarrow\beta(x))\bigr{)}\text{.}$

###### Sketch of proof.

In the proof we deal with two satisfaction relations for models that are
strongly interpretable in a fixed model $\mathcal{M}\models\operatorname{PA}$.
For a model $\mathcal{K}$ strongly interpretable in $\mathcal{M}$,
$\mathcal{K}\models\phi$ denotes the satisfiability of $\phi$ by $\mathcal{K}$
according to the standard satisfaction relation (as defined outside of
$\mathcal{M}$), and $\mathcal{K}\models^{\mathcal{M}}\phi$ denotes the
satisfiability according to the $\mathcal{M}$-definable satisfaction relation.
We observe that whenever $\phi$ is a standard sentence and $\mathcal{K}$ is
any model which is strongly interpretable in $\mathcal{M}$, then
$\mathcal{K}\models\phi$ iff $\mathcal{K}\models^{\mathcal{M}}\phi$
("satisfaction is absolute"). We now pass to the argument.

As previously, suppose that
$(\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}+\operatorname{PA})\blacktriangleleft(\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}+\operatorname{PA})$
and that there exists a nonstandard model
$\mathcal{M}\models\operatorname{PA}$ with nonstandard numbers $a,c\in M$ such
that $\mathcal{M}\models\alpha(k_{0}\cdot a+c)\wedge\neg\beta(a)$. Let $\Phi$
be such that
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}+\operatorname{PA}\vdash\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}[\Phi(x)/T(x)]$.
Since both $\alpha$ and $\beta$ define initial segments, this means that in
$\mathcal{M}$ the length of the initial segment defined by $\alpha$ is much
greater than the length of the initial segment defined by $\beta$. Let $n$ be
such that both $\alpha$ and $\beta$ are of depth at most $n$ and let $k$ be
the depth of $\Phi$. By the reflexivity of $\operatorname{PA}$ and an easy
overspill argument there is a nonstandard number $d$ such that in
$\mathcal{M}$ there is no proof of $0=1$ from the axioms of
$\operatorname{I\Sigma_{d}}$ and true arithmetical sentences of depth at most
$n$, i.e.

$\mathcal{M}\models\operatorname{Con}(\operatorname{I\Sigma_{d}}+\operatorname{Tr}_{n}).$

By the arithmetized completeness theorem, there is a strongly interpretable in
$\mathcal{M}$ model $\mathcal{N}$ such that
$\mathcal{N}\models^{\mathcal{M}}\operatorname{I\Sigma_{d}}+\operatorname{Tr}_{n}$.
In particular, $\mathcal{M}$ is ($\mathcal{M}$-definably isomorphic to) an
$n$-elementary initial segment of $\mathcal{N}$, hence we have
$\mathcal{N}\models\alpha(k_{0}\cdot a+c)\wedge\neg\beta(a)$. Moreover, from
an external perspective, $\mathcal{N}\models\operatorname{PA}$ (but
$\mathcal{M}$ may not know this).

We now work in $\mathcal{M}$. Let $e$ be the greatest element such that
$\mathcal{N}\models^{\mathcal{M}}\beta(e)$. Then $e\leqslant a$. For any $y\in
M$, a formula $\operatorname{Tr}_{y}(x)$ is a partial truth predicate for
sentences of complexity $y$ in the sense of $\mathcal{N}$. Even though for
nonstandard $y$, $\operatorname{Tr}_{y}$ is a nonstandard formula, we can make
sense of it using $\models^{\mathcal{M}}$. Observe that
$\mathcal{N}\models^{\mathcal{M}}\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}[\operatorname{Tr}_{e}(x)/T(x)]$.
Put $T_{e}:=\\{x\in
N:\mathcal{N}\models^{\mathcal{M}}\operatorname{Tr}_{e}(x)\\}$. Since $T_{e}$
is a definable subset of $\mathcal{N}$, there is an $\mathcal{M}$-definable
satisfaction relation for the model $(\mathcal{N},T_{e})$. Seen from the
external (to $\mathcal{M}$) perspective,
$(\mathcal{N},T_{e})\models\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\beta}+\operatorname{PA}$,
hence also it is true that
$(\mathcal{N},T_{e})\models\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}[\Phi(x)/T(x)]$.
Since
$\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}[\Phi(x)/T(x)]$
is a standard sentence,
$(\mathcal{N},T_{e})\models^{\mathcal{M}}\operatorname{CT}^{-}\\!\\!\operatorname{\upharpoonright}_{\alpha}[\Phi(x)/T(x)]$.
Let $\Psi:=\Phi[\operatorname{Tr}_{e}(x)/T(x)]$. Then $\Psi$ is an
arithmetical formula (in the sense of $\mathcal{M}$) of depth at most
$k_{0}\cdot e+k$. It follows that
$\mathcal{N}\models^{\mathcal{M}}\operatorname{CT}^{-}(k_{0}\cdot
a+c)[\Psi(x)/T(x)]$, so in $\mathcal{N}$, $\Psi$ is a truth predicate for
sentences of complexity $k_{0}\cdot a+c$. Let $\lambda$ be the $\Psi$-liar
sentence, i.e. a sentence constructed as in the standard proof of Tarski’s
theorem on the undefinability, such that
$\mathcal{N}\models^{\mathcal{M}}\lambda\leftrightarrow\neg\Psi(\ulcorner\lambda\urcorner)$.
By the inspection of the usual proof of the fixed point lemma, $\lambda$ is of
depth $k_{0}\cdot e+l$ for some standard number $l$. In particular
$\mathcal{N}\models^{\mathcal{M}}\lambda\leftrightarrow\Psi(\ulcorner\lambda\urcorner)$.
A contradiction. ∎

What makes the above proof possible is the reflexivity of $\operatorname{PA}$.
We use it to show that every model of $\operatorname{PA}$ strongly interprets
a suitable model of $\operatorname{PA}$.

##  Appendix B The lattice structure of the definability order

*

###### Proof.

The proof has three parts. First, we show that $\alpha\lor\beta$ and
$\alpha\land\operatorname{rs}_{\alpha}(\beta)$ are syntactically conservative
over $\operatorname{I\Delta_{0}+\exp}$ definitions of truth (whenever $\alpha$
and $\beta$ are such). Then we show that $\alpha\lor\beta$ is an infimum and
$\alpha\land\operatorname{rs}_{\alpha}(\beta)$ is a supremum of $\alpha$ and
$\beta$ (the proof also shows that the operations are well defined as
operations on the equivalence classes of truth definitions modulo the relation
of mutual definability, i.e. if
$\alpha\blacktriangleright\\!\\!\blacktriangleleft\alpha^{\prime}$ and
$\beta\blacktriangleright\\!\\!\blacktriangleleft\beta^{\prime}$, then
$\alpha\lor\beta\blacktriangleright\\!\\!\blacktriangleleft\alpha^{\prime}\lor\beta^{\prime}$
and
$\alpha\land\operatorname{rs}_{\alpha}(\beta)\blacktriangleright\\!\\!\blacktriangleleft\alpha^{\prime}\lor\operatorname{rs}_{\alpha^{\prime}}(\beta^{\prime})$).
We complete the proof by showing that the structure satisfies distributivity
axioms.

Both $\alpha\lor\beta$ and $\alpha\land\operatorname{rs}_{\alpha}(\beta)$
extend $\operatorname{I\Delta_{0}+\exp}$. Given a sentence
$\sigma\in\operatorname{\mathcal{L}_{\operatorname{PA}}}$, suppose that
$\alpha\lor\beta\vdash\sigma$, then in particular $\alpha\vdash\sigma$, so
$\operatorname{I\Delta_{0}+\exp}\vdash\sigma$ by the conservativity of
$\alpha$. Now suppose that
$\alpha\land\operatorname{rs}_{\alpha}(\beta)\vdash\sigma$, then

$\emptyset\vdash\alpha\rightarrow(\operatorname{rs}_{\alpha}(\beta)\rightarrow\sigma)\text{.}$

Since the sets of the symbols present in $\alpha$ and
$\operatorname{rs}_{\alpha}(\beta)$ respectively, intersect exactly at the
arithmetic symbols, by Craig’s interpolation theorem (see 2.5.5 in [4]), there
exists an arithmetical sentence $\tau$ such that

$\emptyset\vdash\alpha\rightarrow\tau\text{ \ \ and \ \
}\emptyset\vdash\tau\rightarrow(\operatorname{rs}_{\alpha}(\beta)\rightarrow\sigma)\text{,}$

and hence
$\emptyset\vdash\operatorname{rs}_{\alpha}(\beta)\rightarrow(\tau\rightarrow\sigma)$.
The arithmetical consequences of $\alpha$ and
$\operatorname{rs}_{\alpha}(\beta)$ are exactly the same, so
$\emptyset\vdash\operatorname{rs}_{\alpha}(\beta)\rightarrow\tau$, and
therefore $\operatorname{rs}_{\alpha}(\beta)\vdash\sigma$. Hence
$\operatorname{I\Delta_{0}+\exp}\vdash\sigma$, since
$\operatorname{rs}_{\alpha}(\beta)$ is syntactically conservative over
$\operatorname{I\Delta_{0}+\exp}$.

Now suppose that $\Theta_{\alpha}(x)$ and $\Theta_{\beta}(x)$ act as truth-
predicates in $\alpha$ and $\beta$ respectively. Then $\Theta_{\alpha}(x)$
also acts as a truth-predicate in
$\alpha\land\operatorname{rs}_{\alpha}(\beta)$. As a truth-predicate in
$\alpha\lor\beta$ we can use

$(\alpha\rightarrow\Theta_{\alpha}(x))\land(\lnot\alpha\rightarrow\Theta_{\beta}(x))\text{.}$

We now come to the second part of the proof. We see that both $\alpha$ and
$\beta$ define $\alpha\lor\beta$, as each of them proves it. Similarly,
$\alpha\land\operatorname{rs}_{\alpha}(\beta)\blacktriangleright\alpha\text{,
}\beta$. Now assume that $\alpha\blacktriangleright\gamma$ and
$\beta\blacktriangleright\gamma$. Suppose that the former definability is
given by the translation of the form
$\mathcal{L}_{\gamma}\ni\mathfrak{R}(\overline{x})\longmapsto\varphi_{\mathfrak{R}}(\overline{x})\in\mathcal{L}_{\alpha}$
and that the second is given by the translation of the form
$\mathcal{L}_{\gamma}\ni\mathfrak{R}(\overline{x})\longmapsto\psi_{\mathfrak{R}}(\overline{x})\in\mathcal{L}_{\beta}$.
Then "$\alpha\lor\beta\blacktriangleright\gamma$" is given by the translation
of the form

$\mathfrak{R}(\overline{x})\longmapsto(\alpha\rightarrow\varphi_{\mathfrak{R}}(\overline{x}))\land(\lnot\alpha\rightarrow\psi_{\mathfrak{R}}(\overline{x}))\text{.}$

Now assume that $\delta\blacktriangleright\alpha$ and
$\delta\blacktriangleright\beta$. Suppose that the first is given by the
translation of the form
$\mathcal{L}_{\alpha}\ni\mathfrak{R}(\overline{x})\longmapsto\varphi_{\mathfrak{R}}(\overline{x})\in\mathcal{L}_{\delta}$
and that the second is given by the translation of the form
$\mathcal{L}_{\beta}\ni\mathfrak{R}(\overline{x})\longmapsto\psi_{\mathfrak{R}}(\overline{x})\in\mathcal{L}_{\delta}$.
Then "$\delta\blacktriangleright\alpha\land\operatorname{rs}_{\alpha}(\beta)$"
is given by the translation of the form:

  * •

$\mathfrak{R}(\overline{x})\longmapsto\varphi_{\mathfrak{R}}(\overline{x})$,
for $\mathfrak{R}\in\mathcal{L}_{\alpha}$,

  * •

$\mathfrak{R}(\overline{x})\longmapsto\psi_{\operatorname{rs}_{\alpha}^{-1}(\mathfrak{R})}(\overline{x})$,
for $\mathfrak{R}\in\mathcal{L}_{\operatorname{rs}_{\alpha}(\beta)}$.

Now we come to the third part of the proof. First, we see that "$x\cap(y\cup
z)=(x\cap y)\cup(x\cap z)$" holds: given definitions of truth $\alpha$,
$\beta$ and $\gamma$,

$\alpha\land\operatorname{rs}_{\alpha}(\beta\lor\gamma)=(\alpha\land\operatorname{rs}_{\alpha}(\beta))\lor(\alpha\land\operatorname{rs}_{\alpha}(\gamma))\text{.}$

Now we show that "$x\cup(y\cap z)=(x\cup y)\cap(x\cup z)$" holds, i.e. given
definitions of truth $\alpha$, $\beta$ and $\gamma$,

$\alpha\lor(\beta\land\operatorname{rs}_{\beta}(\gamma))\blacktriangleright\\!\\!\blacktriangleleft(\alpha\lor\beta)\land\operatorname{rs}_{\alpha\lor\beta}(\alpha\lor\gamma)\text{.}$

The definability
$\alpha\lor(\beta\land\operatorname{rs}_{\beta}(\gamma))\blacktriangleright(\alpha\lor\beta)\land\operatorname{rs}_{\alpha\lor\beta}(\alpha\lor\gamma)$
is given by the translation of the form:

  * •

$\mathfrak{R}(\overline{x})\longmapsto\mathfrak{R}(\overline{x})$, for
$\mathfrak{R}\in\mathcal{L}_{\alpha}\cup\mathcal{L}_{\beta}$,

  * •

$\mathfrak{R}(\overline{x})\longmapsto\operatorname{rs}_{\alpha\lor\beta}^{-1}(\mathfrak{R})(\overline{x})$,
for
$\mathfrak{R}\in\mathcal{L}_{\operatorname{rs}_{\alpha\lor\beta}(\alpha)}\setminus\mathcal{L}_{\operatorname{rs}_{\alpha\lor\beta}(\gamma)}$,

  * •

$\mathfrak{R}(\overline{x})\longmapsto\operatorname{rs}_{\beta}(\operatorname{rs}_{\alpha\lor\beta}^{-1}(\mathfrak{R}))(\overline{x})$,
for
$\mathfrak{R}\in\mathcal{L}_{\operatorname{rs}_{\alpha\lor\beta}(\gamma)}\setminus\mathcal{L}_{\operatorname{rs}_{\alpha\lor\beta}(\alpha)}$,

  * •

$\mathfrak{R}(\overline{x})\longmapsto(\alpha\rightarrow\operatorname{rs}_{\alpha\lor\beta}^{-1}(\mathfrak{R})(\overline{x}))\land(\lnot\alpha\rightarrow\operatorname{rs}_{\beta}(\operatorname{rs}_{\alpha\lor\beta}^{-1}(\mathfrak{R}))(\overline{x}))$,
for
$\mathfrak{R}\in\mathcal{L}_{\operatorname{rs}_{\alpha\lor\beta}(\alpha)}\cap\mathcal{L}_{\operatorname{rs}_{\alpha\lor\beta}(\gamma)}$.

We complete the proof claiming that the definability
$(\alpha\lor\beta)\land\operatorname{rs}_{\alpha\lor\beta}(\alpha\lor\gamma))\blacktriangleright\alpha\lor(\beta\land\operatorname{rs}_{\beta}(\gamma))$
is given by the translation which maps $\mathfrak{R}(\overline{x})$ to:

  * •

$\mathfrak{R}(\overline{x})$, for
$\mathfrak{R}\in\mathcal{L}_{\beta}\setminus\mathcal{L}_{\alpha}$,

  * •

$\bigl{[}\operatorname{rs}_{\alpha\lor\beta}(\alpha)\rightarrow\operatorname{rs}_{\alpha\lor\beta}(\mathfrak{R})(\overline{x})\bigr{]}\land\bigl{[}\lnot\operatorname{rs}_{\alpha\lor\beta}(\alpha)\rightarrow\bigl{(}(\alpha\rightarrow\mathfrak{R}(\overline{x}))\land(\lnot\alpha\rightarrow\operatorname{rs}_{\alpha\lor\beta}(\operatorname{rs}_{\beta}^{-1}(\mathfrak{R}))(\overline{x}))\bigr{)}\bigr{]}$,
for
$\mathfrak{R}\in\mathcal{L}_{\alpha}\cap\mathcal{L}_{\operatorname{rs}_{\beta}(\gamma)}$,

  * •

$(\operatorname{rs}_{\alpha\lor\beta}(\alpha)\rightarrow\operatorname{rs}_{\alpha\lor\beta}(\mathfrak{R})(\overline{x}))\land(\lnot\operatorname{rs}_{\alpha\lor\beta}(\alpha)\rightarrow\mathfrak{R}(\overline{x}))$,
for
$\mathfrak{R}\in\mathcal{L}_{\alpha}\setminus\mathcal{L}_{\operatorname{rs}_{\beta}(\gamma)}$,

  * •

$\operatorname{rs}_{\alpha\lor\beta}(\operatorname{rs}_{\beta}^{-1}(\mathfrak{R}))(\overline{x})$,
for
$\mathfrak{R}\in\mathcal{L}_{\operatorname{rs}_{\beta}(\gamma)}\setminus\mathcal{L}_{\alpha}$.

Notice that
$\mathcal{L}_{\alpha}\cup\mathcal{L}_{\beta}\cup\mathcal{L}_{\operatorname{rs}_{\beta}(\gamma)}=(\mathcal{L}_{\beta}\setminus\mathcal{L}_{\alpha})\oplus(\mathcal{L}_{\alpha}\cap\mathcal{L}_{\operatorname{rs}_{\beta}(\gamma)})\oplus(\mathcal{L}_{\alpha}\setminus\mathcal{L}_{\operatorname{rs}_{\beta}(\gamma)})\oplus(\mathcal{L}_{\operatorname{rs}_{\beta}(\gamma)}\setminus\mathcal{L}_{\alpha})$
as
$\mathcal{L}_{\alpha}\setminus\mathcal{L}_{\operatorname{rs}_{\beta}(\gamma)}\supseteq\mathcal{L}_{\alpha}\cap\mathcal{L}_{\beta}$.

∎