On Interpretability Between Some Weak Essentially Undecidable Theories

Abstract

We introduce two essentially undecidable first-order theories $\mathsf {WT}$ and $\mathsf {T}$. The intended model for the theories is a term model. We prove that $\mathsf {WT}$ is mutually interpretable with Robinson’s $\mathsf {R}$. Moreover, we prove that Robinson’s $\mathsf {Q}$ is interpretable in $\mathsf {T}$.

1 Introduction

A first-order theory T is undecidable if there is no algorithm for deciding if $T\vdash \phi$. If every consistent extension of an undecidable theory T also is undecidable, then T is essentially undecidable.

We introduce two first-order theories, $\mathsf {WT}$ and $\mathsf {T}$, over the language $\mathcal {L}_{ \mathsf {T} } = \lbrace \bot , \langle \cdot ,\,\cdot \rangle , \sqsubseteq \rbrace$ where $\bot$ is a constant symbol, $\langle \cdot ,\,\cdot \rangle$ is a binary function symbol and $\sqsubseteq$ is a binary relation symbol. The intended model for these theories is a term model: The universe is the set of all variable-free $\mathcal {L}_{ \mathsf {T} }$-terms. Each term is interpreted as itself, and $\sqsubseteq$ is interpreted as the subterm relation (s is a subterm of t iff $s = t$ or $t = \langle t_1,\,t_2 \rangle$ and s is a subterm of $t_1$ or $t_2$).

The non-logical axioms of $\mathsf {WT}$ are given by the two axiom schemes:

$(\mathsf {WT_1}) \qquad \qquad \qquad \qquad \qquad \qquad s\ne t$

where s and t are distinct variable-free terms.

$(\mathsf {WT_2}) \qquad \qquad \qquad \qquad \forall x [ \ x \sqsubseteq t \;\; \leftrightarrow \;\; \mathop {\bigvee }\limits _{ s\in \mathcal{S}(t) } x = s \ ]$

where t is a variable-free term and $\mathcal{S}(t)$ is the set of all subterms of t. There are no other non-logical axioms except those given by these two simple schemes, and at a first glance $\mathsf {WT}$ seems to be a very weak theory. Still it turns out that Robinson’s essentially undecidable theory $\mathsf {R}$ is interpretable in $\mathsf {WT}$, and thus it follows that also $\mathsf {WT}$ is essentially undecidable. The theory T is given by the four axioms:

It is not difficult to see that $\mathsf {T}$ is a consistent extension of $\mathsf {WT}$. Thus, since $\mathsf {WT}$ is essentially undecidable, we can conclude right away that also $\mathsf {T}$ is essentially undecidable. Furthermore, since every model of the finitely axiomatizable theory $\mathsf {T}$ is infinite, $\mathsf {T}$ cannot be interpretable in $\mathsf {WT}$, and the obvious conjecture would be that $\mathsf {T}$ is mutually interpretable with Robinson’s $\mathsf {Q}$.

Fig. 1.

The axioms of $\mathsf {R}$ are given by axiom schemes where $n,m\in \mathbb N$ and $\overline{n}$ denotes the $n^{\text{ th }}$ numeral, that is, $\overline{0}\equiv 0$ and $\overline{n+1} \equiv S\overline{n}$.

The seminal theories $\mathsf {R}$ and $\mathsf {Q}$ are theories of arithmetic. The theory $\mathsf {R}$ is given by axiom schemes, and $\mathsf {Q}$ is a finitely axiomatizable extension of $\mathsf {R}$, see Fig. 1 ($\mathsf {Q}$ is also known as Robinson arithmetic and is more or less Peano arithmetic without the induction scheme). It was proved in Tarski et al. [9] that $\mathsf {R}$ and $\mathsf {Q}$ are essentially undecidable. Another seminal essentially undecidable first-order theory is Grzegorcyk’s $\mathsf {TC}$. This is a theory of concatenation. The language is $\{*, \alpha , \beta \}$ where $\alpha$ and $\beta$ are constant symbols and $*$ is a binary function symbol. The standard $\mathsf {TC}$ model is the structure where the universe is $\{ a, b \}^+$ (all finite nonempty strings over the alphabet $\{ a, b \}$), $*$ is concatenation, $\alpha$ is the string a and $\beta$ is the string b. It was proved in Grzegorzyk and Zdanowski [3] that $\mathsf {TC}$ is essentially undecidable. It was later proved that $\mathsf {TC}$ is mutually interpretable with $\mathsf {Q}$, see Visser [10] for further references. The theory $\mathsf {WTC^{-\epsilon }}$ is a weaker variant of $\mathsf {TC}$ that has been shown to be mutually interpretable with $\mathsf {R}$, see Higuchi and Horihata [4] for more details and further references. The axioms of $\mathsf {TC}$ and $\mathsf {WTC^{-\epsilon }}$ can be found in Fig. 2.

Fig. 2.

$\mathsf {WTC^{-\epsilon }_1}$ and $\mathsf {WTC^{-\epsilon }_2}$ are axiom schemes where $t\in \{ a, b \}^+$ and $\underline{t}$ is a term inductively defined by: $\underline{a}\equiv \alpha$, $\underline{b}\equiv \beta$, $\underline{au}\equiv \alpha *\underline{u}$ and $\underline{bu}\equiv \beta *\underline{u}$.

The overall picture shows three finitely axiomatizable and essentially undecidable first-order theories of different character and nature: $\mathsf {Q}$ is a theory of arithmetic, $\mathsf {TC}$ is a theory of concatenation, and $\mathsf {T}$ is a theory of terms (it may also be viewed as a theory of binary trees). All three theories are mutually interpretable with each other, and each of them come with a weaker variant given by axiom schemes. These weaker variants are also essentially undecidable and mutually interpretable with each other.

The theory $\mathsf {T}$ has, in contrast to $\mathsf {Q}$ and $\mathsf {TC}$, a purely universal axiomatization, that is, there are no occurrences of existential quantifiers in the axioms. Moreover, its weaker variant $\mathsf {WT}$ has a neat and very compact axiomatization compared to $\mathsf {R}$ and $\mathsf {WTC^{-\epsilon }}$.

Another interesting theory which is known to be mutually interpretable with $\mathsf {Q}$, and thus also with $\mathsf {TC}$ and $\mathsf {T}$, is the adjunctive set theory $\mathsf {AST}$. More on $\mathsf {AST}$ and adjunctive set theory can found in Damnjanovic [2]. For recent results related to the work in the present paper, we refer the reader to Jerabek [5], Cheng [1] and Kristiansen and Murwanashyaka [7].

The rest of this paper is fairly technical, and we will assume that the reader is familiar with first-order theories and the interpretation techniques introduced in Tarski et al. [9]. In Sect. 2 we prove that $\mathsf {R}$ and $\mathsf {WT}$ are mutually interpretable. In Sect. 3 we prove that $\mathsf {Q}$ is interpretable in $\mathsf {T}$. We expect that $\mathsf {T}$ can be interpreted in $\mathsf {Q}$ by standard techniques available in the literature.

2 $\mathsf {R}$ and $\mathsf {WT}$ Are Mutually Interpretable

The theory $\mathsf {R^-}$ over the language of Robinson arithmetic is given by the axiom schemes

$$\begin{array}{l} \mathsf {R^{-}_1}\;\; \overline{n} + \overline{ m } = \overline{ n + m }\;\mathsf {;}\;\;\;\;\;\; \;\;\; \mathsf {R^{-}_2}\;\; \overline{n} \times \overline{ m } = \overline{ n m }\;\mathsf {;}\;\;\;\;\;\; \; \mathsf {R^{-}_3}\;\; \overline{n } \ne \overline{ m} \;\;\; \text{ for } n\ne m\;\mathsf {;}\\ \mathsf {R^{-}_4}\;\; \forall x[ \ x \le \overline{n} \, \leftrightarrow \, x= 0 \, \vee \, \ldots \, \vee \, x=\overline{n} \ ] \end{array}$$

where $n,m\in \mathbb N$. Recall that $\overline{n}$ denotes the $n^{\text{ th }}$ numeral, that is, $\overline{0}\equiv 0$ and $\overline{n+1} \equiv S\overline{n}$.

We now proceed to interpret $\mathsf {R^-}$ in $\mathsf {WT}$. We choose the domain $I(x) \equiv \ x=x$ (thus we can just ignore the domain). Furthermore, we translate the successor function S(x) as the function given by $\lambda x . \langle x,\,\bot \rangle$, and we translate the constant 0 as $\langle \bot ,\,\bot \rangle$. Let $\overline{n}^\star$ denote the translation of the numeral $\overline{n}$. Then we have $\overline{n+1}^\star \equiv \langle \overline{n}^\star ,\, \bot \rangle$. It follows from $\mathsf {WT_1}$ that the translation of each instance of $\mathsf {R^{-}_3}$ is a theorem of $\mathsf {WT}$ since $\overline{m}^\star$ and $\overline{n}^\star$ are different terms whenever $m \ne n$.

We translate $x \le y$ as $x \sqsubseteq y \wedge x\ne \bot$. It is easy to see that

$$\begin{aligned} \mathsf {WT} \vdash \forall x [ \ x \sqsubseteq \overline{n}^\star \wedge x\ne \bot \;\; \leftrightarrow \;\; \bigvee _{ s\in \mathcal{T}(n) } x = s \ ] \end{aligned}$$

(1)

where $\mathcal{T}(n) = \mathcal{S}(\overline{n}^\star ) \setminus \{ \bot \}$ and $\mathcal{S}(\overline{n}^\star )$ denotes the set of all subterms of $\overline{n}^\star$. We observe that $\mathcal{T}(n) = \{ \overline{k}^\star \mid k\le n\}$ and that (1) indeed is the translation of the axiom scheme $\mathsf {R^{-}_4}$. Hence we conclude that the translation of each instance of $\mathsf {R^{-}_4}$ is a theorem of $\mathsf {WT}$.

Next we discuss the translation of $+$. The idea is to obtain $n+i$ through a formation sequence of length i. Such a sequence will be represented by a term of the form

$$\begin{aligned} \langle \ldots \langle \langle \langle \overline{n}^\star ,\,\overline{0}^\star \rangle ,\,\langle \overline{n+1}^\star ,\,\overline{1}^\star \rangle \rangle ,\,\langle \overline{n+2}^\star ,\,\overline{2}^\star \rangle \rangle \ldots ,\, \langle \overline{n+i}^\star ,\,\overline{i}^\star \rangle \rangle . \end{aligned}$$

(2)

Accordingly we translate $x+y=z$ by the predicate add(x, y, z) given by the formula

$$\begin{aligned} ( \ y = \overline{0}^\star \wedge z = x \ ) \; \vee \; \Big \{ \ y \ne \overline{0}^\star \; \wedge \; \exists W \big [ \ \langle x,\, \overline{0}^\star \rangle \sqsubseteq W \; \wedge \; \qquad \qquad \qquad \qquad \qquad \\ \forall X \ \forall Y \sqsubseteq y \big [ \ \langle X,\,Y \rangle \sqsubseteq W \; \wedge \; Y \ne y \; \wedge \; Y\ne \bot \;\;\;\; \rightarrow \;\;\;\; \qquad \qquad \qquad \\ \big ( \ \langle \langle X,\,\bot \rangle ,\,\langle Y,\,\bot \rangle \rangle \sqsubseteq W \; \wedge \; ( \ \langle Y,\,\bot \rangle = y \rightarrow \langle X,\,\bot \rangle = z \ ) \ \big ) \ \big ] \ \big ] \ \Big \} \;.\quad \,\,\, \end{aligned}$$

Lemma 1

For any $m,n\in \mathbb N$, we have

$$\begin{aligned}\mathsf {WT} \vdash \forall z \big [ \ {\text {\textit{add}}}( \overline{n}^\star , \overline{m}^\star , z ) \leftrightarrow z = \overline{n+m}^\star \ \big ] \;. \end{aligned}$$

Proof

First we prove that $\mathsf {WT} \vdash$ add$( \overline{n}^\star , \overline{m}^\star , \overline{n+m}^\star )$. This is obvious if $m=0$. Assume $m> 0$. Let

$$ S^n_0 \equiv \langle \overline{n}^\star ,\,\overline{0}^\star \rangle \;\;\;\;\; \text{ and } \;\;\;\;\; S^n_{i+1} \equiv \langle S^n_i,\,\langle \overline{n + i + 1 }^\star ,\,\overline{i+1}^\star \rangle \rangle $$

and observe that $S^n_i$ is of the form (2). We will argue that we can choose the W in the definition of add(x, y, z) to be the term $S^n_m$.

So let $W= S^n_m$. By the axioms of $\mathsf {WT}$, we have $\langle \overline{n}^\star ,\, \overline{0}^\star \rangle \sqsubseteq W$. Assume

$$ \langle X,\,Y \rangle \sqsubseteq W \text{ and } Y \ne y=\overline{m}^\star \text{ and } Y \sqsubseteq y = \overline{m}^\star \text{ and } Y\ne \bot . $$

By the axioms of $\mathsf {WT}$, we have that $Y \sqsubseteq \overline{m}^\star$, $Y \ne \overline{m}^\star$ and $Y\ne \bot$ imply $Y = \overline{k}^\star$ for some $k < m$. Since $\langle X,\,Y \rangle \sqsubseteq W$, we know by $\mathsf {WT_2}$ that $\langle X,\,Y \rangle$ is one of the subterms of W. By $\mathsf {WT_1}$ and the form of $S^n_m$, we conclude that $X = \overline{ n+k}^\star$. Furthermore, the form of $S^n_m$ and $\mathsf {WT_2}$ then ensures that $\langle \langle X,\,\bot \rangle ,\, \langle Y,\,\bot \rangle \rangle \sqsubseteq W = S^n_m$. Moreover, if $\langle Y,\,\bot \rangle = \overline{m}^\star$, then by $\mathsf {WT_1}$, we must have $k = m-1$, and thus, $\langle X,\,\bot \rangle = \langle \overline{ n+ (m-1)}^\star ,\, \bot \rangle = \overline{ n+ m }^\star$. This proves that we can deduce add$( \overline{n}^\star , \overline{m}^\star , \overline{n+m}^\star )$ from the axioms of $\mathsf {WT}$, and thus we also have

$$\begin{aligned}\mathsf {WT} \vdash \forall z \big [ \ z = \overline{n+m}^\star \rightarrow \ {\text {\textit{add}}}( \overline{n}^\star , \overline{m}^\star , z ) \big ] . \end{aligned}$$

Next we prove that the converse implication add$( \overline{n}^\star , \overline{m}^\star , z ) \rightarrow z = \overline{n+m}^\star$ follows from the axioms of $\mathsf {WT}$ (and thus the lemma follows). This is obvious when $m=0$. Assume $m\ne 0$ and add$( \overline{n}^\star , \overline{m}^\star , z )$. Then we have W such that $\langle \overline{n}^\star ,\, \overline{0}^\star \rangle \sqsubseteq W$ and

$$\begin{aligned} \forall X \ \forall Y \sqsubseteq \overline{m}^\star \big [ \ \langle X,\,Y \rangle \sqsubseteq W \; \wedge \; Y \ne \overline{m}^\star \; \wedge \; Y\ne \bot \;\;\;\; \rightarrow \;\;\;\; \nonumber \qquad \qquad \qquad \,\, \\ \big ( \ \langle \langle X,\,\bot \rangle ,\,\langle Y,\,\bot \rangle \rangle \sqsubseteq W \; \wedge \; ( \ \langle Y,\,\bot \rangle = \overline{m}^\star \rightarrow \langle X,\,\bot \rangle = z \ ) \ \big ) \ \big ]. \end{aligned}$$

(3)

Since $\langle n,\, \overline{0}^\star \rangle \sqsubseteq W$ and (3) hold, we have $\langle \overline{n+k+1}^\star ,\, \overline{k+1}^\star \rangle \sqsubseteq W$ for any $k<m$. It also follows from (3) that $z=\overline{n+k+1}^\star$ when $m=k+1$.    $\square$

It follows from the preceding lemma that there for any $n,m\in \mathbb N$ exists a unique $k\in \mathbb N$ such that $\mathsf {WT} \vdash$ add$(\overline{n}^\star ,\overline{m}^\star ,\overline{k}^\star )$. We translate $x+y=z$ by the predicate $\phi _{+}$ where $\phi _{ + } (x, y, z )$ is the formula

$$\begin{aligned} \big ( \ \exists ! u [ {\text {\textit{add}}} (x, y, u) ] \ \wedge \ {\text {\textit{add}}} (x, y, z) \ \big ) \; \vee \; \big ( \ \lnot \exists ! u [ {\text {\textit{add}}} (x, y, u) ] \ \wedge \ z=\bot \ \big ).\end{aligned}$$

(4)

The second disjunct of (4) ensures the functionality of our translation, that is, it ensures that $\mathsf {WT} \vdash \forall xy\exists !x\phi _{+}(x,y,z)$ (the same technique is used in [6]). By Lemma 1, we have $\mathsf {WT} \vdash \phi _{+}(\overline{n}^\star ,\overline{m}^\star ,\overline{n+m}^\star )$. This shows that the translation of any instance of the axiom scheme $\mathsf {R^{-}_1}$ can be deduced from the axioms of $\mathsf {WT}$.

We can also achieve a translation of $x \times y = z$ such that the translation of each instance of $\mathsf {R^{-}_2}$ can be deduced from the axioms of $\mathsf {WT}$. Such a translation claims the existence of a term $S^n_m$ where

$$\begin{aligned} S^n_1 \equiv \langle \overline{n}^\star ,\,\overline{1}^\star \rangle \;\;\;\;\; \text{ and } \;\;\;\;\; S^n_{i+1} \equiv \langle S^n_i,\,\langle \overline{ (i + 1)n }^\star ,\,\overline{i+1}^\star \rangle \rangle \end{aligned}$$

and will more or less be based on the same ideas as our translation of $x + y = z$. We omit the details.

Theorem 2

$\mathsf {R}$ and $\mathsf {WT}$ are mutually interpretable.

Proof

We have seen how to interpret $\mathsf {R^{-} }$ in $\mathsf {WT}$. It follows straightforwardly from results proved in Jones and Shepherdson [6] that $\mathsf {R^{-} }$ and $\mathsf {R}$ are mutually interpretable. Thus $\mathsf {R }$ is interpretable in $\mathsf {WT}$. A result of Visser [11] states that a theory is interpretable in $\mathsf {R}$ if and only if it is locally finitely satisfiable, that is, each finite subset of the non-logical axioms has a finite model. Since $\mathsf {WT}$ clearly is locally finitely satisfiable, $\mathsf {WT}$ is interpretable in $\mathsf {R}$.    $\square$

3 $\mathsf {Q}$ is Interpretable in $\mathsf {T}$

The language of the arithmetical theory $\mathsf {Q^-}$ is $\{0, S, M, A \}$ where 0 is a constant symbol, S is a unary function symbol, and A and M are ternary predicate symbols. The non-logical axioms of the first-order theory $\mathsf {Q^{-} }$ are the the following:

$$\begin{array}{l} \mathsf {A}\; \forall x y z_1 z_2 [ \ A(x,y, z_1 ) \wedge A(x,y, z_2 ) \rightarrow z_1=z_2 \ ] \;\mathsf {;}\\ \mathsf {M}\; \forall x y z_1 z_2 [ \ M(x,y, z_1 ) \wedge M(x,y, z_2 ) \rightarrow z_1=z_2 \ ] \;\mathsf {;}\\ \mathsf {Q_1}\; \forall x y [ \ x \ne y \rightarrow Sx \ne Sy \ ] \;\mathsf {;}\;\;\;\; \mathsf {Q_2}\; \forall x [ \ Sx \ne 0 \ ] \;\mathsf {;}\;\;\;\; \mathsf {Q_3}\; \forall x [ \ x = 0 \vee \exists y [ \ x= Sy \ ] \ ] \;\mathsf {;}\\ \mathsf {G_4}\; \forall x [ \ A (x, 0, x ) \ ] \;\mathsf {;}\;\;\;\; \mathsf {G_5}\; \forall x y u [ \ \exists z [ \ A (x, y, z ) \wedge u = Sz \ ] \rightarrow A (x, Sy, u ) \ ] \;\mathsf {;}\\ \mathsf {G_6}\; \forall x [ \ M (x, 0, 0 ) \ ] \;\mathsf {;}\;\;\;\; \mathsf {G_7}\; \forall x y u [ \ \exists z [ \ M (x, y, z ) \wedge A (z, x, u ) \ ] \rightarrow M (x, Sy, u ) \ ] \; . \end{array} $$

Svejdar [8] proved that $\mathsf {Q^{-} }$ and $\mathsf {Q}$ are mutually interpretable. We will prove that $\mathsf {Q^{-} }$ is interpretable in $\mathsf {T }$.

The first-order theory $\mathsf {T^+}$ is $\mathsf {T}$ extended by the two non-logical axioms

$$\begin{array}{l} \mathsf {T_5} \;\, \forall x [ \ x \sqsubseteq x \ ] \;\;\; \text{ and } \;\;\; \mathsf {T_6} \;\, \forall x y z [ \ x \sqsubseteq y \, \wedge \, y \sqsubseteq z \; \rightarrow \; x \sqsubseteq z \ ]. \end{array} $$

Lemma 3

$\mathsf {T^+}$ is interpretable in $\mathsf {T}$.

Proof

We simply relativize quantification to the domain

$$ I \;\; = \;\; \lbrace \ x \mid \ x \sqsubseteq x \; \wedge \; \forall u v [ \ u \sqsubseteq v \wedge v \sqsubseteq x \, \rightarrow \, u \sqsubseteq x \ ] \ \rbrace \ . $$

Suppose $x_1 , x_2 \in I$. We show that $\langle x_1,\, x_2 \rangle \in I$. Since $\langle x_1,\, x_2 \rangle =\langle x_1,\, x_2 \rangle$, we have $\langle x_1,\, x_2 \rangle \sqsubseteq \langle x_1,\, x_2 \rangle$ by $\mathsf {T_4}$. Suppose now that $u \sqsubseteq v \wedge v \sqsubseteq \langle x_1,\, x_2 \rangle$. We need to show that $u \sqsubseteq \langle x_1,\, x_2 \rangle$. By $\mathsf {T_4}$ and $v \sqsubseteq \langle x_1,\, x_2 \rangle$, at least one of the following three cases holds: (a) $v = \langle x_1,\, x_2 \rangle$, (b) $v \sqsubseteq x_1$, (c) $v \sqsubseteq x_2$. Case (a): Since $u \sqsubseteq v$ and $v = \langle x_1,\, x_2 \rangle$, we have $u \sqsubseteq \langle x_1,\, x_2 \rangle$ by our logical axioms. Case (b): $u \sqsubseteq v \wedge v \sqsubseteq x_1$ implies $u \sqsubseteq x_1$ since $x_1 \in I$. By $\mathsf {T_4}$, we have $u \sqsubseteq \langle x_1,\, x_2 \rangle$. Case (c): We have $u \sqsubseteq \langle x_1,\, x_2 \rangle$ by an argument symmetric to the one used in Case (b). Hence, $\forall u v [ \ u \sqsubseteq v \wedge v \sqsubseteq \langle x_1,\, x_2 \rangle \rightarrow u \sqsubseteq \langle x_1,\, x_2 \rangle \ ]$.

This proves that I is closed under $\langle \cdot ,\,\cdot \rangle$. It follows from $\mathsf {T_3}$ that $\bot \in I$, and thus I satisfies the domain condition. Clearly, the translation of each non-logical axiom of $\mathsf {T^+}$ is a theorem of $\mathsf {T}$.    $\square$

We now proceed to interpret $\mathsf {Q^{-} }$ in $\mathsf {T^+}$. We choose the domain N given by

$$ N(x) \; \equiv \; x\ne \bot \; \wedge \; \forall y \sqsubseteq x [ \ y = \bot \, \vee \, \exists z [ \ y = \langle z,\,\bot \rangle \ ] \ ] \ . $$

Lemma 4

We have (i) $\mathsf {T^+}\vdash N(\langle \bot ,\,\bot \rangle )$, (ii) $\mathsf {T^+}\vdash \forall x[ N(x)\rightarrow N(\langle x,\,\bot \rangle )]$ and (iii) $\mathsf {T^+}\vdash \forall y z [ \ N(y) \, \wedge \, z \sqsubseteq y \; \rightarrow \; ( \ z=\bot \, \vee \, N(z) \ ) \ ]$.

Proof

It follows from $\mathsf {T_1}$, $\mathsf {T_3}$ and $\mathsf {T_4}$ that (i) holds. In order to see that (ii) holds, assume N(x) (we will argue that $N(\langle x,\,\bot \rangle )$ holds). Suppose $y \sqsubseteq \langle x,\,\bot \rangle$. Now, $N(\langle x,\,\bot \rangle )$ follows from

$$\begin{aligned} y = \bot \; \vee \; \exists z [ \ y = \langle z,\,\bot \rangle \ ] . \end{aligned}$$

(5)

Thus it is sufficient to argue that (5) holds. By $\mathsf {T_4}$, we know that $y \sqsubseteq \langle x,\,\bot \rangle$ implies $y = \langle x,\,\bot \rangle \vee y \sqsubseteq x \vee y\sqsubseteq \bot$. The case $y = \langle x,\,\bot \rangle$: We obviously have $\exists z [ \ y = \langle z,\,\bot \rangle \ ]$ and thus (5) holds. The case $y \sqsubseteq x$: (5) holds since N(x) holds. The case $y \sqsubseteq \bot$: We have $y = \bot$ by $\mathsf {T_3}$, and thus (5) holds. This proves (ii).

We turn to the proof of (iii). Suppose $N(y) \wedge z \sqsubseteq y$ (we show $z = \bot \vee N(z)$). Assume $w\sqsubseteq z$. By $\mathsf {T_6}$, we have $w \sqsubseteq y$, moreover, since N(y) holds, we have $w = \bot \vee \exists u [ w = \langle u,\,\bot \rangle ]$. Thus, we conclude that

$$\begin{aligned} \forall w\sqsubseteq z [ \ w = \bot \, \vee \, \exists u [ \ w = \langle u,\,\bot \rangle \ ] \ ]. \end{aligned}$$

(6)

Now

$$ z=\bot \; \vee \; \underbrace{( \ z\ne \bot \; \wedge \; \forall w\sqsubseteq z [ \ w = \bot \, \vee \, \exists u [ \ w = \langle u,\,\bot \rangle \ ] \ ] \ )}_{N(z)} $$

follows tautologically from (6).    $\square$

We interpret 0 as $\langle \bot ,\,\bot \rangle$. We interpret the successor function Sx as $\lambda x . \langle x,\,\bot \rangle$. To improve the readability we will occasionally write $\dot{\mathrm {0}}$ in place of $\langle \bot ,\,\bot \rangle$, $\dot{\mathrm {S}} t$ in place of $\langle t,\,\bot \rangle$ and $t\in N$ in place of N(t). We will also write $\exists x\in N [ \ \eta \ ]$ and $\forall x \in N [ \ \eta \ ]$ in place of, respectively, $\exists x [ \ N(x) \wedge \eta \ ]$ and $\forall x [ \ N(x) \rightarrow \eta \ ]$. Furthermore, $\mathbf {Q}x_1, \ldots , x_n\in N$ is shorthand for $\mathbf {Q}x_1\in N\ldots \mathbf {Q}x_n\in N$ where $\mathbf {Q}$ is either $\forall$ or $\exists$.

Lemma 5

The translations of $\mathsf {Q_1}$, $\mathsf {Q_2}$ and $\mathsf {Q_3}$ are theorems of $\mathsf {T^+}$.

Proof

The translation of $\mathsf {Q_1}$ is $\forall x, y\in N [ \ x \ne y \rightarrow \dot{\mathrm {S}} x \ne \dot{\mathrm {S}} y \ ]$. By $\mathsf {T_2}$, we have $x \ne y \rightarrow \dot{\mathrm {S}} x \ne \dot{\mathrm {S}} y$ for any x, y, and thus, the translation of $\mathsf {Q_1}$ is a theorem of $\mathsf {T^+}$.

The translation of $\mathsf {Q_2}$ is $\forall x\in N [ \ \dot{\mathrm {S}} x \ne \dot{\mathrm {0}}\ ]$. Assume $x\in N$. Then we have $x\ne \bot$, and by $\mathsf {T_2}$, we have $\dot{\mathrm {S}} n \equiv \langle x,\,\bot \rangle \ne \langle \bot ,\,\bot \rangle \equiv \dot{\mathrm {0}}$.

The translation of $\mathsf {Q_3}$ is $\forall x\in N [ \ x= \dot{\mathrm {0}}\vee \exists y\in N[ \ x= \dot{\mathrm {S}} y \ ] \ ]$. Assume $x\in N$, that is, assume

$$\begin{aligned} x\ne \bot \; \wedge \; \forall y \sqsubseteq x [ \ y = \bot \, \vee \, \exists z [ \ y = \langle z,\,\bot \rangle \ ] \ ] \ . \end{aligned}$$

(7)

By $\mathsf {T_5}$, we have $x\sqsubseteq x$. By (7) and $x\sqsubseteq x$, we have

$$\begin{aligned} x\ne \bot \; \wedge \; ( \ x = \bot \, \vee \, \exists z [ \ x = \langle z,\,\bot \rangle \ ] \ ) \end{aligned}$$

and then, by a tautological inference, we also have $\exists z [ x = \langle z,\,\bot \rangle ]$. Thus, we have z such that $\langle z,\,\bot \rangle \equiv \dot{\mathrm {S}} z = x \in N$. By Lemma 4 (iii), we have $z=\bot \vee z\in N$. If $z=\bot$, we have $x = \langle \bot ,\,\bot \rangle \equiv \dot{\mathrm {0}}$. If $z\in N$, we have $z \in N$ such that $x = \dot{\mathrm {S}} z$. Thus, $\mathsf {T^+} \vdash \forall x\in N [ x= \dot{\mathrm {0}}\vee \exists y\in N[ x= \dot{\mathrm {S}} y ] ]$.    $\square$

Before we give the translation of A, we will provide some intuition. The predicate A(a, b, c) holds in the standard model for $\mathsf {Q^{-}}$ iff $a+b=c$. Let $\widetilde{0}\equiv \dot{\mathrm {0}}$ and $\widetilde{n+1}\equiv \dot{\mathrm {S}} \widetilde{n}$, and observe that $a+b=c$ iff there exists an $\mathcal {L}_{\mathsf {T}}$-term of the form

$$\begin{aligned} \langle \ldots \langle \langle \langle \bot ,\,\langle \widetilde{a},\,\widetilde{0} \rangle \rangle ,\, \langle \widetilde{a+1},\,\widetilde{1} \rangle \rangle ,\,\langle \widetilde{a+2},\,\widetilde{2} \rangle \rangle \ldots ,\,\langle \widetilde{a+b},\,\widetilde{b} \rangle \rangle \end{aligned}$$

(8)

where $c=a+b$. We will give a predicate $\phi _A$ such that $\phi _A(\widetilde{a},\widetilde{b},w)$ holds in $\mathsf {T^{+}}$ iff w is of the form (8). Thereafter we will use $\phi _A$ to give the translation $\varPsi _A$ of A.

Let $\phi _{A} (x, y, w ) \equiv$

$$\begin{aligned} ( \ y = \dot{\mathrm {0}}\rightarrow w= \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle \ ) \; \wedge \; \exists w^{ \prime } \exists z\in N [ \ w = \langle w^{ \prime },\,\langle z,\,y \rangle \rangle \ ] \; \wedge \; \qquad \qquad \quad \\ \forall u \forall Y, Z\in N [ \ \theta _{A} (u, w, Y, Z ) \ ] \end{aligned}$$

where $\theta _{A} (u, w, Y, Z ) \equiv$

The translation $\varPsi _A$ of A is $\varPsi _{A} (x, y, z ) \equiv$

$$ \exists w \big [ \ \phi _{A} (x , y , w ) \; \wedge \; \exists w^{ \prime } [ \ w = \langle w^{ \prime },\, \langle z,\,y \rangle \rangle \ ]\; \wedge \; \forall u [ \ \phi _{A} (x , y , u ) \rightarrow u=w \ ] \ \big ] \ . $$

Lemma 6

$$\mathsf {T^{+}} \vdash \forall x\in N \forall w [ \ \phi _{A}(x, \dot{\mathrm {0}}, w) \; \leftrightarrow \; w = \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle \ ] \; . $$

Proof

We assume $x\in N$ and prove the equivalence

$$\begin{aligned} \phi _{A}(x, \dot{\mathrm {0}}, w) \; \leftrightarrow \; w = \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle \end{aligned}$$

(9)

The left-right direction of (9) follows straightforwardly from the definition of $\phi _A$. To prove the right-left implication of (9), we need to prove $\phi _{A}(x, \dot{\mathrm {0}}, \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle )$. It is easy to see that $\phi _{A}(x, \dot{\mathrm {0}}, \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle )$ holds if

$$\begin{aligned} \forall u \forall Y, Z\in N [ \ \theta _{A} (u, \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle , Y, Z ) \ ] \end{aligned}$$

(10)

holds, and to show (10), it suffices to show that

$$\begin{aligned} x,Y,Z\in N \; \text{ and } \; \langle u,\, \langle Z,\,Y \rangle \rangle \sqsubseteq \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle \; \text{ and } \; Y \ne \dot{\mathrm {0}}\end{aligned}$$

(11)

is a contradiction. (If (11) is a contradiction, then (10) will hold as the antecedent of $\theta _{A}$ will be false for all $x,Y,Z\in N$ and all u.)

By $\mathsf {T_4}$ and $\langle u,\, \langle Z,\,Y \rangle \rangle \sqsubseteq \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle$ we have to deal with the following three cases: (a) $\langle u,\, \langle Z,\,Y \rangle \rangle = \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle$, (b) $\langle u,\, \langle Z,\,Y \rangle \rangle \sqsubseteq \bot$ and (c) $\langle u,\, \langle Z,\,Y \rangle \rangle \sqsubseteq \langle x,\,\dot{\mathrm {0}} \rangle$. Case: (a): We have $Y=\dot{\mathrm {0}}$ by $\mathsf {T_2}$, but we have $Y \ne \dot{\mathrm {0}}$ in (11). Case (b): We have $\langle u,\, \langle Z,\,Y \rangle \rangle = \bot$ by $\mathsf {T_3}$, and this contradicts $\mathsf {T_1}$. Case (c): By $\mathsf {T_4}$, this case splits into the three subcases: (a’) $\langle u,\, \langle Z,\,Y \rangle \rangle = \langle x,\,\dot{\mathrm {0}} \rangle$, (b’) $\langle u,\, \langle Z,\,Y \rangle \rangle \sqsubseteq x$ and (c’) $\langle u,\, \langle Z,\,Y \rangle \rangle \sqsubseteq \dot{\mathrm {0}}$. Case (a’): We have $\langle u,\, \langle Z,\,Y \rangle \rangle = \langle x,\,\langle \bot ,\,\bot \rangle \rangle$ since $\dot{\mathrm {0}}$ is shorthand for $\langle \bot ,\,\bot \rangle$. Thus, by $\mathsf {T_2}$, we have $Z=\bot$ and $Y=\bot$. This contradicts $Y,Z\in N$. Case (b’): We have $\langle u,\, \langle Z,\,Y \rangle \rangle \sqsubseteq x$ and $x\in N$. By Lemma 4 (iii), we have $\langle u,\, \langle Z,\,Y \rangle \rangle =\bot$ or $\langle u,\, \langle Z,\,Y \rangle \rangle \in N$. Now, $\langle u,\, \langle Z,\,Y \rangle \rangle =\bot$ contradicts $\mathsf {T_1}$. Furthermore, by our definitions, $\langle u,\, \langle Z,\,Y \rangle \rangle \in N$ implies that

$$ \forall y_0 \sqsubseteq \langle u,\, \langle Z,\,Y \rangle \rangle [ \ y_0 = \bot \, \vee \, \exists z_0 [ \ y_0 = \langle z_0,\,\bot \rangle \ ] \ ] . $$

By $\mathsf {T_5}$, we have $\langle u,\, \langle Z,\,Y \rangle \rangle = \bot \, \vee \, \exists z_0 [ \ \langle u,\, \langle Z,\,Y \rangle \rangle = \langle z_0,\,\bot \rangle \ ]$, and this yields a contradiction together with $\mathsf {T_1}$ and $\mathsf {T_2}$. Case (c’) is similar to Case (a’), but a bit simpler. This completes the proof of the lemma.    $\square$

Lemma 7

$$\begin{aligned} \mathsf {T^{+}} \vdash \forall x, y\in N \forall z w w^{ \prime } [ \ w = \langle w^{ \prime },\,\langle z,\,y \rangle \rangle \; \wedge \; \phi _{A}(x, y, w) \;\; \rightarrow \;\; \qquad \qquad \qquad \quad \\ \phi _{A}(x, \dot{\mathrm {S}} y , \langle w,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle ) \ ] . \end{aligned}$$

Proof

We assume

$$\begin{aligned} x, y\in N \text{ and } w = \langle w^{ \prime },\,\langle z,\,y \rangle \rangle \text{ and } \phi _{A}(x, y, w)\; . \end{aligned}$$

(12)

We need to prove $\phi _{A}(x, \dot{\mathrm {S}} y , \langle w,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle ) \equiv$

$$\begin{aligned} ( \ \dot{\mathrm {S}} y = \dot{\mathrm {0}}\rightarrow w= \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle \ ) \; \wedge \; \nonumber \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \\ \exists w_0 \exists z_0\in N [ \ \langle w,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle = \langle w_0,\,\langle z_0,\,\dot{\mathrm {S}} y \rangle \rangle \ ] \; \wedge \; \nonumber \qquad \qquad \qquad \qquad \quad \\ \forall u \forall Y, Z\in N [ \ \theta _{A} (u, \langle w,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle , Y, Z ) \ ] \qquad \qquad \quad \end{aligned}$$

(13)

First we prove

$$\begin{aligned} z\in N \;\; \text{ and } \;\; \dot{\mathrm {S}} z \in N \; \end{aligned}$$

(14)

Since $\phi _{A}(x, y, w)$ holds by our assumptions (12), we have $z_1 \in N$ and $w_1$ such that $w = \langle w_1,\,\langle z_1,\,y \rangle \rangle$. We have also assumed $w = \langle w^{ \prime },\,\langle z,\,y \rangle \rangle$. By $\mathsf {T_2}$, we have $z=z_1$, and thus $z\in N$. By Lemma 4 (ii), we have $\dot{\mathrm {S}} z \in N$. This proves (14).

The second conjunct of (13) follows straightforwardly from (14). (simply let $z_0$ be $\dot{\mathrm {S}} z$ and let $w_0$ be w). The first conjunct follows easily from $\mathsf {T_2}$ and the assumption $y\in N$. Thus, we are left to prove the third conjunct of (13), namely

$$\begin{aligned} \forall u \forall Y, Z\in N \big [ \ \langle u,\,\langle Z,\,Y \rangle \rangle \sqsubseteq \langle w,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle \; \wedge \; Y \ne \dot{\mathrm {0}}\rightarrow \nonumber \qquad \qquad \qquad \qquad \qquad \\ \exists v \ \exists Y^{ \prime } Z^{ \prime }\in N \big [ \ Z = \dot{\mathrm {S}} Z^{ \prime } \; \wedge \; Y = \dot{\mathrm {S}} Y^{ \prime } \; \wedge \; u = \langle v,\,\langle Z^{ \prime },\,Y^{\prime } \rangle \rangle \; \wedge \; \nonumber \qquad \qquad \\ ( \ Y^{ \prime } = \dot{\mathrm {0}}\rightarrow ( \ Z^{ \prime } = x \, \wedge \, v=\bot \ ) \ ) \ \big ] \ \big ] \quad \quad \quad \end{aligned}$$

(15)

In order to do so, we assume

$$\begin{aligned} Y, Z\in N \text{ and } \langle u,\,\langle Z,\,Y \rangle \rangle \sqsubseteq \langle w,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle \text{ and } Y \ne \dot{\mathrm {0}}\end{aligned}$$

(16)

and prove

$$\begin{aligned} \exists v \ \exists Y^{ \prime } Z^{ \prime }\in N \big [ \ Z = \dot{\mathrm {S}} Z^{ \prime } \; \wedge \; Y = \dot{\mathrm {S}} Y^{ \prime } \; \wedge \; u = \langle v,\,\langle Z^{ \prime },\,Y^{\prime } \rangle \rangle \; \wedge \; \nonumber \qquad \qquad \\ ( \ Y^{ \prime } = \dot{\mathrm {0}}\rightarrow ( \ Z^{ \prime } = x \, \wedge \, v=\bot \ ) \ ) \ \big ]. \end{aligned}$$

(17)

By our assumptions (16), we have $\langle u,\,\langle Z,\,Y \rangle \rangle \sqsubseteq \langle w,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle$, and then $\mathsf {T_4}$ yields three cases: (a) $\langle u,\,\langle Z,\,Y \rangle \rangle = \langle w,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle$, (b) $\langle u,\,\langle Z,\,Y \rangle \rangle \sqsubseteq w$ and (c) $\langle u,\,\langle Z,\,Y \rangle \rangle \sqsubseteq \langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle$. We prove that that (17) holds in each of these three cases.

Case (a): By $\mathsf {T_2}$, we have $u=w$, $Z= \dot{\mathrm {S}} z$ and $Y= \dot{\mathrm {S}} y$. By (14), we have $z\in N$. By (12), we have $y\in N$. Moreover, by (12), we also have $u=w = \langle w^{ \prime },\,\langle z,\,y \rangle \rangle$. Thus there exist v and $Y^{ \prime }, Z^{ \prime }\in N$ such that

$$ Z = \dot{\mathrm {S}} Z^{ \prime } \; \wedge \; Y = \dot{\mathrm {S}} Y^{ \prime } \; \wedge \; u = \langle v,\,\langle Z^{ \prime },\,Y^{\prime } \rangle \rangle \; .$$

If $y = \dot{\mathrm {0}}$, we must have $\langle v,\,\langle z,\,y \rangle \rangle = w = \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle$ since $\phi _{A}(x, y, w)$ holds by our assumptions (12). By $\mathsf {T_2}$, this implies $z = x$ and $v= \bot$. This proves that (17) holds in Case (a).

Case (b): By our assumptions (12), we have $\phi _{A}(x, y, w)$, and thus we also have $\theta _{A}(u, w, Y, Z)\equiv$

$$\begin{aligned} \langle u,\,\langle Z,\,Y \rangle \rangle \sqsubseteq w \; \wedge \; Y \ne \dot{\mathrm {0}}\rightarrow \nonumber \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \\ \exists v \ \exists Y^{ \prime } Z^{ \prime }\in N \big [ \ Z = \dot{\mathrm {S}} Z^{ \prime } \; \wedge \; Y = \dot{\mathrm {S}} Y^{ \prime } \; \wedge \; u = \langle v,\,\langle Z^{ \prime },\,Y^{\prime } \rangle \rangle ) \; \wedge \; \nonumber \qquad \\ ( \ Y^{ \prime } = \dot{\mathrm {0}}\rightarrow ( \ Z^{ \prime } = x \, \wedge \, v=\bot \ ) \ ) \ \big ] \ \!. \quad \quad \end{aligned}$$

(18)

We are dealing with a case where the antecedent of (18) holds, and thus (17) holds.

Case (c): This case is not possible. By $\mathsf {T_4}$, this case splits into the subcases: (a’) $\langle u,\,\langle Z,\,Y \rangle \rangle = \langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle$, (b’) $\langle u,\,\langle Z,\,Y \rangle \rangle \sqsubseteq \dot{\mathrm {S}} z$ and (c’) $\langle u,\,\langle Z,\,Y \rangle \rangle \sqsubseteq \dot{\mathrm {S}} y$. We prove that each of these subcases contradicts our axioms. Case (a’): Recall that $\dot{\mathrm {S}} y$ is shorthand for $\langle y,\,\bot \rangle$. Thus, by $\mathsf {T_2}$, we have $Y=\bot$. This contradicts the assumption (12) that $Y\in N$. Case (b’): By Lemma 4 (iii), we have $\langle u,\,\langle Z,\,Y \rangle \rangle =\bot \, \vee \, N(\langle u,\,\langle Z,\,Y \rangle \rangle )$. Now, $\langle u,\,\langle Z,\,Y \rangle \rangle =\bot$ contradicts $\mathsf {T_1}$. Furthermore, $N(\langle u,\,\langle Z,\,Y \rangle \rangle )$ implies that there is $z_0$ such that $\langle u,\,\langle Z,\,Y \rangle \rangle = \langle z_0,\,\bot \rangle$. By $\mathsf {T_2}$, we have $\langle Z,\,Y \rangle =\bot$. This contradicts $\mathsf {T_1}$. Case (c’) is similar to Case (b’). This proves that (17) holds, and thus we conclude that the lemma holds.    $\square$

Lemma 8

Proof

Let $x,y\in N$ and assume $\phi _{A} (x, \dot{\mathrm {S}} y , w )$. Thus, we have $w'$ and $z\in N$ such that

$$\begin{aligned} w = \langle w^{ \prime },\,\langle z,\,\dot{\mathrm {S}} y \rangle \rangle \;\; \text{ and } \;\; \forall u \forall Y, Z\in N [ \ \theta _{A} (u, w, Y, Z ) \ ] \end{aligned}$$

(19)

Use the assumptions (19) to prove that $\phi _{A}(x, y, w^{ \prime } )\equiv$

$$\begin{aligned} ( \ y = \dot{\mathrm {0}}\rightarrow w' = \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle \ ) \; \wedge \; \exists w^{ \prime \prime } \exists z\in N [ \ w' = \langle w^{ \prime \prime },\,\langle z,\,y \rangle \rangle \ ] \; \wedge \; \nonumber \qquad \qquad \\ \forall u \forall Y, Z\in N [ \ \theta _{A} (u, w', Y, Z ) \ ] \qquad \end{aligned}$$

(20)

holds. We omit the details.    $\square$

Lemma 9

The translations of $\mathsf {A}$, $\mathsf {G_4}$ and $\mathsf {G_5}$ are theorems of $\mathsf {T^+}$.

Proof

The translation of the axiom $\mathsf {A}$ is

$$ \forall x,y,z_1,z_2\in N [ \ \varPsi _A(x,y,z_1) \wedge \varPsi _A(x,y,z_2) \; \rightarrow \; z_1 = z_2 \ ]\; . $$

Assume $\varPsi _A(x,y,z_1)$ and $\varPsi _A(x,y,z_2)$. Then it follows straightforwardly from the definition of $\varPsi _A$ and $\mathsf {T_2}$ that $z_1 = z_2$. Hence the translation is a theorem of $\mathsf {T^+}$.

The translation of $\mathsf {G_4}$ is $\forall x \in N [ \varPsi _A(x,\dot{\mathrm {0}}, x) ]$, that is

$$\begin{aligned} \forall x \in N \exists w \big [ \ \phi _{A} (x , \dot{\mathrm {0}}, w ) \; \wedge \; \exists w^{ \prime } [ \ w = \langle w^{ \prime },\, \langle x,\,\dot{\mathrm {0}} \rangle \rangle \ ] \; \wedge \; \nonumber \qquad \qquad \qquad \qquad \qquad \\ \forall u [ \ \phi _{A} (x , \dot{\mathrm {0}}, u ) \rightarrow u=w \ ] \ \big ] \ . \end{aligned}$$

We have

$$\mathsf {T^{+}} \vdash \phi _{A}(x, \dot{\mathrm {0}}, \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle ) \text{ and } \mathsf {T^{+}} \vdash \forall u [\phi _{A}(x, \dot{\mathrm {0}}, u) \rightarrow u= \langle \bot ,\,\langle x,\,\dot{\mathrm {0}} \rangle \rangle $$

by Lemma 6, and it easy to see that the translation of $\mathsf {G_4}$ is a theorem of $\mathsf {T^+}$.

The translation of $\mathsf {G_5}$ is

$$\begin{aligned} \forall x, y, u \in N [ \ \exists z\in N [ \ \varPsi _A (x, y, z ) \wedge u = \dot{\mathrm {S}} z \ ] \rightarrow \varPsi _A (x, \dot{\mathrm {S}} y , u ) \ ] \; . \end{aligned}$$

(21)

In order to prove that (21) can be deduced from the axioms of $\mathsf {T^+}$, we assume $\varPsi _A (x, y, z ) \wedge u = \dot{\mathrm {S}} z$. Then we need to prove $\varPsi _A (x, \dot{\mathrm {S}} y , \dot{\mathrm {S}} z ) \equiv$

$$\begin{aligned} \exists w \big [ \ \phi _{A} (x , \dot{\mathrm {S}} y , w ) \; \wedge \; \exists w^{ \prime } [ \ w = \langle w^{ \prime },\, \langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle \ ] \; \wedge \; \nonumber \qquad \qquad \qquad \qquad \qquad \qquad \\ \forall u [ \ \phi _{A} (x , \dot{\mathrm {S}} y , u ) \rightarrow u=w \ ] \ \big ].\qquad \ . \end{aligned}$$

(22)

By our assumption $\varPsi _A (x, y, z )$ there is a unique $w_1$ such that $\phi _A(x,y,w_1)$ and $w_1=\langle w_0,\,\langle z,\,y \rangle \rangle$ for some $w_0$. By Lemma 7, we have $\phi _A(x,\dot{\mathrm {S}} y ,\langle w_1,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle )$. Thus, we have $w_2$ such that $\phi _A(x,\dot{\mathrm {S}} y ,w_2)$ and $w_2 =\langle w_1,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle$. It is easy to see that (22) holds if $w_2$ is unique. Thus we are left to prove the uniqueness of $w_2$, more precisely, we need to prove that

$$\begin{aligned} \forall W_2 [ \ \phi _A (x, \dot{\mathrm {S}} y , W_2 ) \; \rightarrow \; W_2 = w_2 \ ] \; . \end{aligned}$$

(23)

In order to prove (23), we assume $\phi _A (x, \dot{\mathrm {S}} y , W_2 )$ (we will prove $W_2 = w_2 = \langle w_1,\,\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle \rangle$). By our assumption $\phi _A (x, \dot{\mathrm {S}} y , W_2 )$ and Lemma 8, we have $u_0\in N$ and $W_1$ such that $W_2 = \langle W_1,\,\langle u_0,\,\dot{\mathrm {S}} y \rangle \rangle$ and $\phi _A(x,y,W_1)$. We have argued that there is a unique $w_1= \langle w_0,\,\langle z,\,y \rangle \rangle$ such that $\phi _A(x,y,w_1)$ holds. By this uniqueness, we have $W_1= w_1= \langle w_0,\,\langle z,\,y \rangle \rangle$. So far we have proved

$$ w_2 \; = \; \langle \, \overbrace{\langle w_0,\,\langle z,\,y \rangle \rangle }^{w_1} \, ,\, \, {\langle \dot{\mathrm {S}} z ,\,\dot{\mathrm {S}} y \rangle } \, \rangle \text{ and } W_2 \; = \; \langle \, \overbrace{\langle w_0,\,\langle z,\,y \rangle \rangle }^{W_1} \, ,\, \, {\langle u_0,\,\dot{\mathrm {S}} y \rangle } \, \rangle $$

and then we are left to prove that $u_0= \dot{\mathrm {S}} z$. By our assumption $\phi _A (x, \dot{\mathrm {S}} y , W_2 )$, we have v and $Z',Y'\in N$ such that $u_0 = \dot{\mathrm {S}} Z'$, $\dot{\mathrm {S}} y = \dot{\mathrm {S}} Y'$ and $W_1 = \langle v,\,\langle Z',\,Y' \rangle \rangle$. Thus, $\langle v,\,\langle Z',\,Y' \rangle \rangle =\langle w_0,\,\langle z,\,y \rangle \rangle$. By $\mathsf {T_2}$, we have $z= Z'$, and thus, $u_0= \dot{\mathrm {S}} Z' = \dot{\mathrm {S}} z$. This proves that (23) holds.    $\square$

We will now give the translation $\varPsi _M$ of M. Let $\phi _{M} (x, y, w ) \equiv$

where $\theta _{M} (u, w, Y, Z ) \equiv$

We let $\varPsi _{M} (x, y, z ) \equiv$

$$ \exists w \big [ \ \phi _{M} (x , y , w ) \; \wedge \; \exists w^{ \prime } [ \ w = \langle w^{ \prime },\,\langle z,\,y \rangle \rangle \; \wedge \; \forall u [ \ \phi _{M} (x , y , u ) \rightarrow u=w \ ] \ \big ] \ . $$

The translations of $\mathsf {M}$, $\mathsf {G_6}$ and $\mathsf {G_7}$ are

The proof of the next lemma follows the lines of the proof of Lemma 9. We omit the details.

Lemma 10

The translations of $\mathsf {M}$, $\mathsf {G_6}$ and $\mathsf {G_7}$ are theorems of $\mathsf {T^+}$.

Theorem 11

$\mathsf {Q}$ is interpretable in $\mathsf {T}$.

Proof

It is proved in Svejdar [8] that $\mathsf {Q }$ is interpretable in $\mathsf {Q^{-} }$. It follows from the lemmas above that $\mathsf {Q^{-} }$ is interpretable in $\mathsf {T^+}$ which again is interpretable in $\mathsf {T}$. Hence the theorem holds.    $\square$