Weak Sequential Theories of Finite Full Binary Trees

Abstract

We study a first-order theory of finite full binary trees with an axiom schema of open induction. We show that this theory is sequential by constructing a direct interpretation of Adjunctive Set Theory in a very weak finitely axiomatized subtheory. We show that weakening the latter theory by removal of an axiom which states that the subtree relation is transitive gives a theory that directly interprets Vaught’s weak set theory, a non-finitely axiomatizable fragment of Adjunctive Set Theory.

1 Introduction

In this paper, we show that a very weak finitely axiomatized first-order theory of finite full binary trees is sequential. Informally, sequential theories are theories with a coding machinery of a certain strength. It is possible to code any finite sequence in the domain of the theory. Furthermore, it is possible to extend any sequence by adjoining an arbitrary element. The concept of sequential theories was introduced by Pudlák [7] in the study of degrees of multidimensional local interpretations. Pudlák shows that sequential theories are prime in this degree structure. An element is prime if it is not the join of two smaller elements.

As a consequence of their expressive power, sequential theories are essentially undecidable. A computably enumerable first-order theory is called essentially undecidable if any consistent extension, in the same language, is undecidable (there is no algorithm for deciding whether an arbitrary sentence is a theorem). A computably enumerable first-order theory is called essentially incomplete if any recursively axiomatizable consistent extension is incomplete. It can be proved that a theory is essentially undecidable if and only if it is essentially incomplete (see Chapter 1 of Tarski et al. [9]). Two theories that are known to be essentially undecidable are Robinson arithmetic $\mathsf {Q}$ and the related theory $\mathsf {R}$ (see Chapter 2 of [9]).

Examples of sequential theories are Adjunctive Set Theory $\mathsf {AS}$ (see Fig. 1 for the axioms of $\mathsf {AS}$), the theory of discretely ordered commutative semirings with a least element $\mathsf {PA^-}$ (see Jeřábek [4]), Robinson Arithmetic with bounded induction $\mathsf {I \Delta _0}$ (see Hájek & Pudlák [3] Section V3b), Peano Arithmetic $\mathsf {PA}$, Zermelo-Fraenkel Set Theory $\mathsf {ZF}$. Examples of theories that are not sequential are Robinson Arithmetic $\mathsf {Q}$ (see Visser [11] Example 1 or Theorem 9 of [4]) and Gregorczyk’s theory of concatenation $\mathsf {TC}$ (see Visser [12] Sect. 5).

Fig. 1.

Non-logical axioms of the first-order theories $\mathsf {AS}$ and $\mathsf {VS}$.

Formally, sequential theories are theories that directly interpret $\mathsf {AS}$ (see Sect. 2). A weaker notion is the concept of theories that directly interpret the weak set theory $\mathsf {VS}$ of Vaught [10], which is a non-finitely axiomatizable fragment of $\mathsf {AS}$ (see Figure 1 for the axioms of $\mathsf {VS}$). Vaught introduces $\mathsf {VS}$ in the study of theories that are axiomatizable by a schema. A theory T is axiomatizable by a schema if there exists a formula $\varPhi$ in the language of T plus a fresh relation symbol R such that the set of universal closures of formulas obtained by substituting formulas for R in $\varPhi$ is an axiom set for T. Vaught shows that any computably enumerable first-order theory of finite signature that directly interprets $\mathsf {VS}$ is axiomatizable by a schema. For more on $\mathsf {VS}$, see Sect. 3.2 of Visser [11].

In [11] and [12], Visser shows that $\mathsf {Q}$ and $\mathsf {TC}$ are not sequential by showing that they do not have pairing. A theory S has pairing if there exists a formula $\mathsf {Pair} (x, y , z )$ in the language of S such that S proves $\forall x y \; \exists z \; [\! \ \mathsf {Pair} (x, y , z )\ \!]$ and $\forall x y z u v \; [\! \ (\! \ \mathsf {Pair} (x, y , z ) \; \wedge \; \mathsf {Pair} (u, v , z ) \ \! ) \rightarrow (\! \ x = u \; \wedge \; y = v \ \!) \ \!]$. In Kristiansen & Murwanashyaka [5], we introduce an essentially undecidable theory $\mathsf {T}$ with pairing (see Fig. 2 for the axioms of $\mathsf {T}$). The language of $\mathsf {T}$ is $\mathcal {L}_{\mathsf {T}} = \lbrace \perp , \langle \cdot , \cdot \rangle , \sqsubseteq \rbrace$ where $\perp$ is a constant symbol, $\langle \cdot , \cdot \rangle$ is a binary function symbol and $\sqsubseteq$ is a binary relation symbol. The intended model of $\mathsf {T}$ is a term algebra extended with the subterm relation: The universe is the set of all variable-free $\mathcal {L}_{\mathsf {T}}$-terms (equivalently, finite full binary trees). The constant symbol $\perp$ is interpreted as itself. The function symbol $\langle \cdot , \cdot \rangle$ is interpreted as the function that maps the pair (s, t) to the term $\langle s, t \rangle$. The relation symbol $\sqsubseteq$ is interpreted as the subterm relation (equivalently, the subtree 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$. In [5], we show that $\mathsf {T}$ is essentially undecidable by showing that it interprets $\mathsf {Q}$ but leave open the problem of whether the converse holds. In [2], Damnjanovic shows that $\mathsf {Q}$ interprets $\mathsf {T}$.

Fig. 2.

Non-logical axioms of the first-order theory $\mathsf {T}$.

It is not clear to us whether $\mathsf {T}$ is sequential or even expressive enough to directly interpret $\mathsf {VS}$. It appears as if the subtree relation does not provide a good notion of occurrence since $\mathsf {T}$ has models where there exist distinct elements u, v such that $u \sqsubseteq v$ and $v \sqsubseteq u$. In this paper, we consider the theory $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$ we obtain by extending $\mathsf {T}$ with an axiom schema of open induction:

$$ \phi ( \perp , \vec {p} \, ) \; \wedge \; \forall x y \; [\! \ \phi ( x , \vec {p} \, ) \; \wedge \; \phi (y , \vec {p} \, ) \rightarrow \phi ( \langle x, y \rangle , \vec {p} \, ) \ \!] \rightarrow \forall x \; \phi (x , \vec {p} \, ) $$

where $\phi$ is a quantifier-free $\mathcal {L}_{\mathsf {T}}$-formula. We study two extensions of $\mathsf {T}$ that are subtheories of $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$. Let $\mathsf {T}^{(1)}$ denote the theory we obtain by extending $\mathsf {T}$ with the axiom $\forall x y \; [\! \ \langle x , y \rangle \not \sqsubseteq x \ \!]$. In Sect. 4, we show that $\mathsf {T}^{(1)}$ directly interprets $\mathsf {VS}$ (the proof shows that we can in fact do with $\forall x y \; [\!\ x \sqsubseteq x \rightarrow \langle x , y \rangle \not \sqsubseteq x \ \!]$). The proof we give can be easily modified to show that $\mathsf {VS}$ is directly interpretable in $\mathsf {T} + \forall x y \; [\! \ \langle x , y \rangle \not \sqsubseteq y \ \!]$. Let $\mathsf {T}^{(2)}$ denote the theory we obtain by extending $\mathsf {T}$ with the axioms: $\forall x y z \; [\! \ x \sqsubseteq y \; \wedge \; y \sqsubseteq z \rightarrow x \sqsubseteq z \ \!]$, $\forall x y z \; [\! \ x \sqsubseteq y \rightarrow \langle y , z \rangle \not \sqsubseteq x \ \!]$ (we could also have used $\forall x y z \; [\! \ x \sqsubseteq z \rightarrow \langle y , z \rangle \not \sqsubseteq x \ \!]$). In Sect. 5.2, we show that $\mathsf {T}^{(2)}$ is a sequential theory by constructing a direct interpretation of $\mathsf {AS}$. In Sect. 5.1, we formulate the coding technique that is the basis of this interpretation. Since $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$ is an extension of the sequential theory $\mathsf {T}^{(2)}$, it is also a sequential theory. One of the referees found a shorter and neat direct interpretation of $\mathsf {AS}$ in $\mathsf {T}^{(2)}$. We present their proof in Sect. 5.3.

2 Sequential Theories

Hájek & Pudlák [3, p. 151] characterize sequential theories as those theories that interpret Robinson Arithmetic $\mathsf {Q}$ and for which there are formulas $\mathsf {Seq} (z, u)$ (z codes a sequence of length u) and $\beta (x, v, z )$ (x is the v-th element of z) with the following two properties: (1) If z codes a sequence s of length u, then for each number v that is strictly less than u, there is a unique x that is the v-th element of z. (2) If z codes a sequence s of length u, then given y, there exists $z^{\prime }$ that codes a sequence $s^{\prime }$ of length $u+1$ obtained by extending s with y. This definition differs slightly from the original definition of Pudlák [7]. Instead of an interpretation of $\mathsf {Q}$, Pudlák requires that there exist formulas $x \le y$, $\mathsf {N} (x)$ such that $\le$ is a total ordering of $\mathsf {N}$ and each element of $\mathsf {N}$ has a successor in $\mathsf {N}$. In this paper, we use the equivalent definition of sequentiality in terms of Adjunctive Set Theory $\mathsf {AS}$ (see Pudlák [7, p. 274] and Visser [11] Sect. 3.3). See Fig. 1 for the axioms of $\mathsf {AS}$.

Definition 1

Let T be a first-order theory in the language of set theory $\lbrace \in \rbrace$. A first-order theory S directly interprets T if there exists a formula $\phi (x , y )$ in the language of S with only x and y free such that the extension by definitions $S + \forall x y \; [\! \ x \in y \leftrightarrow \phi (x, y ) \ \!]$ proves each axiom of T. A first-order theory is sequential if it directly interprets $\mathsf {AS}$.

For a more comprehensive discussion of the notion of sequentiality, we refer the reader to Visser [11]. In Mycielski et al. [6, Appendix III], it is shown that a theory of sequences can be developed in any theory that directly interprets $\mathsf {AS}$. This can be used to show that $\mathsf {AS}$ interprets $\mathsf {Q}$ (see Pudlák [7] Sect. 2). See also Damnjanovic [1] for mutual interpretability of $\mathsf {AS}$ and $\mathsf {Q}$.

3 Open Induction

In this section, we verify that $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$ is an extension of $\mathsf {T}^{(1)}$ and $\mathsf {T}^{(2)}$. Thus, when we show that $\mathsf {T}^{(2)}$ is a sequential theory, it will also follow that $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$ is a sequential theory.

Theorem 1

$\varSigma _{\mathsf {open}}^{ \mathsf {T} }$ is an extension of $\mathsf {T}^{(1)}$ and $\mathsf {T}^{(2)}$.

Proof

It suffices to show that $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$ proves the following: (A) $\forall x \; [\! \ x \sqsubseteq x \ \!]$, (B) $\forall x y z \; [\! \ x \sqsubseteq y \; \wedge \; y \sqsubseteq z \rightarrow x \sqsubseteq z \ \!]$, (C) $\forall x y z \; [\! \ x \sqsubseteq y \rightarrow \langle y , z \rangle \not \sqsubseteq x \ \!]$.

We prove (A) by induction on x. The base case $\perp \sqsubseteq \perp$ holds by the axiom $\mathsf {T}_3 \equiv \ \forall x \; [\! \; x \sqsubseteq \perp \; \leftrightarrow \; x= \perp \; \!]$. The inductive case $( x \sqsubseteq x \; \wedge \; y \sqsubseteq y \ ) \rightarrow \langle x, y \rangle \sqsubseteq \langle x, y \rangle$ holds by the axiom $\mathsf {T}_4 \equiv \ \forall x y z \; [\! \ x \sqsubseteq \langle y , z \rangle \leftrightarrow ( \ x = \langle y , z \rangle \vee x \sqsubseteq y \vee x \sqsubseteq z \ ) \ \!]$. Thus, by induction, $\forall x \; [\! \ x \sqsubseteq x \ \!]$ is a theorem of $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$.

We prove (B) by induction on z using x and y as parameters. The base case $x \sqsubseteq y \; \wedge \; y \sqsubseteq \perp \rightarrow x \sqsubseteq \perp$ holds by $\mathsf {T}_3$. We consider the inductive case $z = \langle z_0 , z_1 \rangle$. Assume the following formulas hold: (I) $x \sqsubseteq y \; \wedge \; y \sqsubseteq z_0 \rightarrow x \sqsubseteq z_0$, (II) $x \sqsubseteq y \; \wedge \; y \sqsubseteq z_1 \rightarrow x \sqsubseteq z_1$. We need to show that $x \sqsubseteq y \; \wedge \; y \sqsubseteq z \rightarrow x \sqsubseteq z$. So, assume $x \sqsubseteq y$ and $y \sqsubseteq z$. By $\mathsf {T}_4$, we have the following cases: (1) $y = z$, (2) $y \sqsubseteq z_0$, (3) $y \sqsubseteq z_1$. Case (1) implies $x \sqsubseteq z$. We consider (2). Since $x \sqsubseteq y$ and $y \sqsubseteq z_0$, we have $x \sqsubseteq z_0$ by (I). Hence, $x \sqsubseteq \langle z_0 , z_1 \rangle = z$ by $\mathsf {T}_4$ . By similar reasoning, Case (3) also implies $x \sqsubseteq z$. Thus, $x \sqsubseteq y \; \wedge \; y \sqsubseteq z \rightarrow x \sqsubseteq z$. By induction, $\forall x y z \; [\! \ x \sqsubseteq y \; \wedge \; y \sqsubseteq z \rightarrow x \sqsubseteq z \ \!]$ is a theorem of $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$.

We prove (C) by induction on x with y and z as parameters. We consider the base case $x = \perp$. By $\mathsf {T}_3$ and $\mathsf {T}_1 \equiv \ \forall x y \; [\! \ \langle x , y \rangle \ne \perp \ \!]$, we have $\langle y , z \rangle \not \sqsubseteq \perp$. We consider the inductive case $x = \langle x_0 , x_1 \rangle$. Assume the following formulas hold: (IV) $x_0 \sqsubseteq y \rightarrow \langle y, z \rangle \not \sqsubseteq x_0$, (V) $x_1 \sqsubseteq y \rightarrow \langle y, z \rangle \not \sqsubseteq x_1$. We need to show that $x \sqsubseteq y \rightarrow \langle y, z \rangle \not \sqsubseteq x$. Assume for the sake of a contradiction $x \sqsubseteq y$ and $\langle y , z \rangle \sqsubseteq x$. By $\mathsf {T}_4$, we have the following cases: (i) $\langle y , z \rangle = x$, (ii) $\langle y , z \rangle \sqsubseteq x_0$, (iii) $\langle y , z \rangle \sqsubseteq x_1$. We consider (i). By $\mathsf {T}_2 \equiv \ \forall x y z w \; [\! \ \langle x, y \rangle = \langle z, w \rangle \rightarrow ( \ x=z \; \wedge \; y=w \ ) \ \!]$, we have $y = x_0$. Hence, by (A), we have $x_0 \sqsubseteq y$. Since $\langle x_0 , x_1 \rangle \sqsubseteq y$ and $\langle x_0 , x_1 \rangle = \langle y, z \rangle$ and $x_0 = y$, we find $\langle y, z \rangle \sqsubseteq x_0$. But $x_0 \sqsubseteq y$ and $\langle y, z \rangle \sqsubseteq x_0$ contradicts (IV).

We consider (ii). By (A), we have $x_0 \sqsubseteq x_0$. By $\mathsf {T}_4$, we have $x_0 \sqsubseteq \langle x_0 , x_1 \rangle$. Since $x_0 \sqsubseteq \langle x_0 , x_1 \rangle$ and $x \sqsubseteq y$, we have $x_0 \sqsubseteq y$ by (B). Thus, we have $x_0 \sqsubseteq y$ and $\langle y , z \rangle \sqsubseteq x_0$, which contradicts (IV). By similar reasoning, (iii) leads to a contradiction.

Thus, by induction, $\forall x y z \; [\! \ x \sqsubseteq y \rightarrow \langle y , z \rangle \not \sqsubseteq x \ \!]$ is a theorem of $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$.    $\square$

4 Direct Interpretation of $\mathsf {VS}$

Recall that $\mathsf {T}^{(1)}$ is $\mathsf {T}$ extended with the axiom $\mathsf {T}^{(1)}_5 \equiv \ \forall x y \; [\! \ \langle x , y \rangle \not \sqsubseteq x \ \!]$. In this section, we show that $\mathsf {VS}$ is directly interpretable in $\mathsf {T}^{(1)}$. Since in the proof $\mathsf {T}^{(1)}_5$ is applied to cases where x is of the form $x = \langle x_0 , x_1 \rangle$, we can by $\mathsf {T}_4$ do with the weaker axiom $\forall x y \; [\! \ x \sqsubseteq x \rightarrow \langle x , y \rangle \not \sqsubseteq x \ \!]$.

To improve readability, we introduce the following notation: By recursion, let $( ) := \, \perp$ and $( x_1, \ldots , x_n ) := \langle ( x_1, \ldots , x_{n-1} ) \, , \, x_n \rangle$ for $n \ge 1$. So, $(x) := \langle \perp \, , \, x \rangle$, $(x, y ) := \langle \, \langle \perp \, , \, x \rangle \, , \, y \, \rangle$, and so on.

Theorem 2

$\mathsf {VS}$ is directly interpretable in $\mathsf {T}^{(1)}$.

Proof

We translate the membership relation as follows

$$ x \in y \equiv \ \exists u v w \; \big [\! \ y = \langle u, \langle w, v \rangle \rangle \ \wedge \ \langle w, x \rangle \sqsubseteq y \ \big ] \ . $$

By $\mathsf {T}_1 \equiv \ \forall x y \; [\! \ \langle x , y \rangle \ne \perp \ \!]$, there does not exist u, v, w such that $\perp = \langle u, \langle w , v \rangle \rangle$. Hence, $\mathsf {T}^{(1)} \vdash \forall u \; [\! \ u \not \in \perp \ \!]$. Thus, the translation of $\mathsf {VS}_0$ is a theorem of $\mathsf {T}^{(1)}$. We verify that the translation of $\mathsf {VS}_m$ is a theorem of $\mathsf {T}^{( 1)}$ for each $0< m < \omega$.

We code a finite sequence $x_0, x_1, \ldots , x_n$ as $y = \big ( \langle w, x_0 \rangle \, , \, \langle w, x_1 \rangle , \ldots , \langle w, x_n \rangle \big )$ where $w = \big ( x_0 \, , \, x_1 \, , \, \ldots \, , \, x_n \big )$. By $\mathsf {T}_1$ and $\mathsf {T}_4$, we have $w \ne \perp$ and $w \sqsubseteq w$ by how w is defined. By $\mathsf {T}_2 \equiv \ \forall x y z w \; [\! \ \langle x, y \rangle = \langle z, w \rangle \rightarrow ( \ x=z \, \wedge \, y=w \ ) \ \!]$, w is the unique element $w^{\prime }$ such that $y = \langle u, \langle w^{\prime } , v \rangle \rangle$ for some u and v. By the axiom $\mathsf {T}_4 \equiv \ \forall x y z \; [\! \ x \sqsubseteq \langle y , z \rangle \leftrightarrow ( \ x = \langle y , z \rangle \; \vee \; x \sqsubseteq y \; \vee \; x \sqsubseteq z \ ) \ \!]$, we have $\ \langle w, x_i \rangle \sqsubseteq y$ for all $i \le n$. Hence, $x_i \in y$ for all $i \le n$. We need to show that $y = \lbrace x_0, x_1 , \ldots , x_n \rbrace$. So, assume $z \in y$. By definition of $\in$ and uniqueness of w, this is equivalent to $\langle w, z \rangle \sqsubseteq y$. We need to show that there exists $i \le n$ such that $z = x_i$. For $k \le n$, let $y_0 = ( )$ and $y_{k +1} = \big ( \, \langle w, x_0 \rangle \, , \, \langle w, x_1 \rangle , \ldots , \langle w, x_{k} \rangle \, \big )$. Observe that $y_{k+1} = \langle \, y_k \, , \, \langle w, x_{k} \rangle \, \rangle$. By $\mathsf {T_3} \equiv \ \forall x \; [\! \; x \sqsubseteq \perp \; \leftrightarrow \; x= \perp \; \!]$ and $\mathsf {T_1}$, we have $\langle w, z \rangle \not \sqsubseteq \perp = y_0$. Thus, it suffices to show that the following holds: If $\langle w, z \rangle \sqsubseteq y_{k+1}$, then $z = x_k$ or $\langle w, z \rangle \sqsubseteq y_k$.

So, assume $\langle w, z \rangle \sqsubseteq y_{k+1}$. By $\mathsf {T_4}$, we have one of the following cases: (i) $\langle w, z \rangle = y_{k+1}$, (ii) $\langle w, z \rangle \sqsubseteq \langle w, x_k \rangle$, (iii) $\langle w, z \rangle \sqsubseteq y_{k}$. Thus, it suffices to show that (i) leads to a contradiction while (ii) implies $z = x_k$. We show that (i) leads to a contradiction. By $\mathsf {T_2}$, the equality $\langle w, z \rangle = y_{k+1}$ implies $w = y_{k}$. If $k = 0$, then $w = y_{k } = \perp$ which contradicts $\mathsf {T}_1$ by definition of w. If $k > 0$, then by $\mathsf {T}_4$ and the definition of $y_k$, we have $\langle w, x_0 \rangle \sqsubseteq y_{k } = w$ which contradicts $\mathsf {T}^{(1)}_5$.

We show (ii) implies $z = x_k$. By $\mathsf {T}_4$, we have one of the following cases: (iia) $\langle w, z \rangle = \langle w, x_k \rangle$, (iib) $\langle w, z \rangle \sqsubseteq w$, (iic) $\langle w, z \rangle \sqsubseteq x_k$. Case (iia) implies $z = x_k$ by $\mathsf {T_2}$. Case (iib) contradicts $\mathsf {T}^{(1)}_5$. We consider (iic). We have $\langle w, z \rangle \sqsubseteq x_k$. Recall that $w = \big ( \, x_0 \, , \, x_1 \, , \, \ldots \, , \, x_n \, \big )$. Hence, by $\mathsf {T_4}$, $\langle w, z \rangle \sqsubseteq x_k$ implies $\langle w, z \rangle \sqsubseteq w$ which contradicts $\mathsf {T}^{(1)}_5$. Thus, $z = x_k$.    $\square$

It is not clear to us whether it is possible to directly interpret $\mathsf {VS}$ in $\mathsf {T}$ since it appears as if we do not have a good notion of occurrence without the axiom $\forall x y \; [\! \ \langle x , y \rangle \not \sqsubseteq x \ \!]$.

Open Problem 2

Is $\mathsf {VS}$ directly interpretable in $\mathsf {T}$?

5 A Sequential Subtheory of $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$

In this section, we show that the theory $\mathsf {T}^{(2)}$ is sequential by constructing a direct interpretation of $\mathsf {AS}$. The construction is given in Sect. 5.2. In Sect. 5.1, we present the intuition behind the construction. In Sect. 5.3, we give an alternative proof that was suggested by one of the referees.

5.1 Coding Sequences

In this section, we explain how we intend to construct a formula $x \in y$ that provably in $\mathsf {T}^{(2)}$ satisfies the axioms of $\mathsf {AS}$.

We reason in the standard model of $\mathsf {T}$. We start by observing that there is a one-to-one correspondence between finite binary trees and finite sequences of finite binary trees. We introduce the following notation: By recursion, let $( )_{\alpha } := \, \alpha$ and $( x_1, \ldots , x_n )_{\alpha } := \langle ( x_1, \ldots , x_{n-1} )_{\alpha } \, , \, x_n \rangle$ for $n \ge 1$. So, $(x)_{\alpha } := \langle \alpha \, , \, x \rangle$, $(x, y )_{\alpha } := \langle \, \langle \alpha \, , \, x \rangle \, , \, y \, \rangle$, and so on. We associate the empty sequence with $\perp$. We associate a finite sequence of finite binary trees $T_1, T_2, \ldots , T_N$ with the finite binary tree

$$\begin{aligned} T = \big ( \, T_1, T_2, \ldots , T_N \, \big )_{\perp } \ . \end{aligned}$$

(*)

Each non-empty finite binary tree T can be written uniquely on the form (*). Now, the idea is to let the empty tree represent the empty set and to let a finite binary tree of the form (*) represent the set $\lbrace T_1, \ldots , T_N \rbrace$. We observe that the finite binary tree $\big ( \, T_1, T_2, \ldots , T_N , T_N \, \big )_{\perp }$ also represents the set $\lbrace T_1, \ldots , T_N \rbrace$. This is not a problem since $\mathsf {AS}$ does not require sets to be uniquely determined by their elements. Axiom $\mathsf {AS}_2$ requires that we have an adjunction operator $\mathsf {adj} ( \cdot , \cdot )$ that takes two finite binary trees T and u and gives a finite binary tree S that represents the set $T \cup \lbrace u \rbrace$. Clearly, $\mathsf {adj} ( T , u ) = \langle T , u \rangle$ does the job.

The next step is to construct an $\mathcal {L}_{\mathsf {T}}$-formula $x \in T$ that expresses that x is an element of T. With T as in (*), the idea is to express that there exists a finite binary tree W that encodes a sequence $V_1, V_2, \ldots , V_k$ where $V_1 = T$, for all $i \in \lbrace 1, \ldots , k-1 \rbrace$ there exists $u_i$ such that $V_i = \langle V_{i+1} , u_i \rangle$ and there exist $j \in \lbrace 1, \ldots , k \rbrace$ and S such that $V_j = \langle S, x \rangle$ (this is respectively what clauses (C), (D), (E) in Sect. 5.2 try to capture). We let W be of the form

$$ W = \big ( \; V_k \, , \, V_{k-1} \, , \ldots , \, V_{2} \, , \, V_{1} \; \big )_{\alpha } $$

where $\alpha$ is a finite binary tree whose purpose is to allow us to recognize the subtrees of W of the form $\big ( \, V_k \, , \, V_{k-1} \, , \ldots , \, V_{i} \, \big )_{\alpha }$. This property is essential since the formula $x \in T$ needs to say that W is of a certain form by quantifying over subtrees of W. We require that $\alpha$ is not a subtree of T (this is what Clause (A) in Sect. 5.2 tries to capture). Then, the subtrees of W of the form $\big ( \, V_k \, , \, V_{k-1} \, , \ldots , \, V_{i} \, \big )_{\alpha }$ are exactly those subtrees of W that have $\alpha$ as a subtree.

The problem with this approach is that we need to update $\alpha$ to find a finite binary tree $W^{\prime }$ that witnesses that x is also an element of $T^{\prime } = \langle T, u \rangle$ when u is such that $\alpha$ is a subtree of $T^{\prime }$. Since $x \in T^{\prime }$, we need to ensure the existence of a finite binary tree of the form $W^{\prime } = \big ( \; V_k \, , \, V_{k-1} \, , \, V_{2} \, , \ldots , \, V_{1} \, , \, T^{\prime } \; \big )_{\alpha ^{\prime } }$ where $\alpha ^{\prime }$ is not a subtree of $T^{\prime }$. Although this is not problematic when reasoning in the standard model, it appears as if we do not have in $\mathsf {T}^{(2)}$ the resources necessary to show that we can construct $W^{\prime }$ from W. Our solution is to let $x \in T$ be witnessed by infinitely many finite binary trees so that any finite binary tree that witnesses $x \in T^{\prime }$ also witnesses $x \in T$. More precisely, we let $x \in T$ mean that there exists a marker $\alpha$ (a finite binary tree that is not a subtree of T) such that for any finite binary $\beta$ that has $\alpha$ as a subtree, there exists a finite binary tree $W_{\beta }$ of the form $\big ( \, V_k \, , \, V_{k-1} \, , \ldots , \, V_{2} \, , \, V_{1} \; \big )_{ \beta }$.

The problem of markers that grow in size is similar to the problem of growing commas that is encountered when coding finite sequences of strings. In [8], W.V. Quine shows that first-order arithmetic is directly interpretable in the free semigroup with two generators by devising a way of coding arbitrary finite sequences of strings. Let a, b denote the generators of the semigroup. Let $\lbrace a \rbrace ^*$ denote the set of all finite sequences of a’s. Quine codes a finite set of strings $\lbrace w_0, \ldots , w_{n} \rbrace$ as a string of the form $w_0 b u b w_1 \ldots b u b w_{n}$ where $u \in \lbrace a \rbrace ^*$ is such that if $v \in \lbrace a \rbrace ^*$ is a substring of some $w_i$, then v is a proper substring of u. If u is a substring of a string $w_{n+1}$, we need to encode the set $\lbrace w_0, \ldots , w_{n} , w_{n+1} \rbrace$ as $w_0 b u^{\prime } b w_1 \ldots b u^{\prime } b w_{n} b u^{\prime } b w_{n+1}$ where $u^{\prime } \in \lbrace a \rbrace ^*$ is longer than u. In [12], Albert Visser observes that this approach has some disadvantages in the setting of weak theories since we need to be able to update u when we wish to extend the coded sequence. The solution he provides is to represent a finite set $\lbrace w_0, \ldots , w_{n} \rbrace$ as a string of the form $b u_0 b w_0 b u_1 b w_1 \ldots b u_{n} b w_{n}$ where each $u_i$ is in $\lbrace a \rbrace ^*$, $u_i$ is a substring of $u_j$ when $i \le j$ and if $v \in \lbrace a \rbrace ^*$ is a substring of some $w_i$, then v is a proper substring of $u_i$. So, the commas (the $u_i$’s) grow in length.

5.2 Direct Interpretation of $\mathsf {AS}$

In this section, we construct a formula $x \in y$ that provably in $\mathsf {T}^{(2)}$ satisfies the axioms of $\mathsf {AS}$. Recall that $\mathsf {T}^{(2)}$ is $\mathsf {T}$ extended with the following axioms $\mathsf {T}_5^{(2)} \equiv \ \forall x y z \; [\! \ ( \ x \sqsubseteq y \; \wedge \; y \sqsubseteq z \ ) \rightarrow x \sqsubseteq z \ \!]$, $\mathsf {T}^{(2)}_6 \equiv \ \forall x y z \; [\! \ x \sqsubseteq y \rightarrow \langle y , z \rangle \not \sqsubseteq x \ \!]$.

We start by constructing a formula $W , \beta \Vdash u \in z$ which states that W is a finite binary tree using the marker $\beta$ to witness that u is an element of z. Let $W , \beta \Vdash u \in z$ be shorthand for

• (A) $\beta \not \sqsubseteq z$

• (B) there exist $z_0, z_1$ such that $z = \langle z_0 , z_1 \rangle$

• (C) there exists $W_0$ such that $\beta \sqsubseteq W_0 \; \wedge \; W = \langle W_0 , z \rangle$

• (D) if $\langle W_1 , v \rangle \sqsubseteq W \ \wedge \ \beta \sqsubseteq W_1 \ \wedge \ W_1 \ne \beta$, then there exist $v_0, v_1$ such that

  $$ v = \langle v_0 , v_1 \rangle \ \wedge \ \exists W_2 \; [\! \ \beta \sqsubseteq W_2 \ \wedge \ W_1 = \langle W_2 , v_0 \rangle \ \!] $$

• (E) there exist $W_3$ and v such that $\langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W \ \wedge \ \beta \sqsubseteq W_3$.

We let $W , \beta \not \Vdash u \in z$ be shorthand for $\lnot \big ( \ W , \beta \Vdash u \in z \ \big )$. We let $\mathsf {adj} (x, y ) = \langle x, y \rangle$.

Lemma 1

$\mathsf {T} \vdash \forall W , \beta , u \; [\! \ W , \beta \not \Vdash u \in \perp \ \!]$.

Proof

By $\mathsf {T}_1$, Clause (B) of $W , \beta \Vdash u \in \perp$ does not hold.    $\square$

Lemma 2

Let $W = \langle \beta , \mathsf {adj} (x, y ) \rangle$. Then

$$ \mathsf {T}^{(2) } \vdash ( \ \beta \sqsubseteq \beta \; \wedge \; \beta \not \sqsubseteq \mathsf {adj} (x, y ) \ ) \rightarrow W , \beta \Vdash y \in \mathsf {adj} (x, y ) \ . $$

Proof

Assume $\beta \sqsubseteq \beta \; \wedge \; \beta \not \sqsubseteq \mathsf {adj} (x, y )$ holds. We need to show that each one of the following clauses holds

• (A) $\beta \not \sqsubseteq \mathsf {adj} (x, y )$

• (B) there exist $z_0, z_1$ such that $\mathsf {adj} (x, y ) = \langle z_0 , z_1 \rangle$

• (C) there exists $W_0$ such that $\beta \sqsubseteq W_0 \; \wedge \; W = \langle W_0 , \mathsf {adj} (x, y ) \rangle$

• (D) if $\langle W_1 , v \rangle \sqsubseteq W \ \wedge \ \beta \sqsubseteq W_1 \ \wedge \ W_1 \ne \beta$, then there exist $v_0, v_1$ such that

  $$ v = \langle v_0 , v_1 \rangle \ \wedge \ \exists W_2 \; [\! \ \beta \sqsubseteq W_2 \ \wedge \ W_1 = \langle W_2 , v_0 \rangle \ \!] $$

• (E) there exist $W_3$ and v such that $\langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W \ \wedge \ \beta \sqsubseteq W_3$.

Since $\beta \not \sqsubseteq \mathsf {adj} (x, y )$, (A) holds. By definition, $\mathsf {adj} (x, y ) = \langle x, y \rangle$. Hence, (B) holds. It follows from $\beta \sqsubseteq \beta$ and the definition of W that (C) holds. We verify that (D) holds. Assume $\langle W_1 , v \rangle \sqsubseteq W \; \wedge \; \beta \sqsubseteq W_1$. By $\mathsf {T}_4$, we have

$$ \langle W_1 , v \rangle = \big \langle \, \beta \, , \, \mathsf {adj} (x, y ) \, \big \rangle \ \vee \ \langle W_1 , v \rangle \sqsubseteq \beta \ \vee \ \beta \sqsubseteq \langle W_1 , v \rangle \sqsubseteq \mathsf {adj} (x, y ) \ . $$

By $\mathsf {T}^{(2)}_5$, we have $\langle W_1 , v \rangle = \big \langle \, \beta \, , \, \mathsf {adj} (x, y ) \, \big \rangle \ \vee \ \langle W_1 , v \rangle \sqsubseteq \beta \ \vee \ \beta \sqsubseteq \mathsf {adj} (x, y )$. Since $\beta \sqsubseteq W_1$, we have $\langle W_1 , v \rangle \not \sqsubseteq \beta$ by $\mathsf {T}^{(2)}_6$. By assumption, $\beta \not \sqsubseteq \mathsf {adj} (x, y )$. Hence, $\langle W_1 , v \rangle = \big \langle \, \beta \, , \, \mathsf {adj} (x, y ) \, \big \rangle$. By $\mathsf {T}_2$, we have $W_1 = \beta$. Thus, (D) holds.

Finally, we verify that (E) holds. By assumption, $\beta \sqsubseteq \beta \; \wedge \; W = \langle \beta , \mathsf {adj} (x, y ) \rangle$. By $\mathsf {T}_4$, $W \sqsubseteq W$. Since $\mathsf {adj} (x, y ) = \langle x, y \rangle$, (E) holds.    $\square$

Lemma 3

$\mathsf {T}^{(2)}$ proves the universal closure of

$$ \big ( \ u \ne y \ \wedge \ \langle W , \mathsf {adj} (x, y ) \rangle , \beta \Vdash u \in \mathsf {adj} (x, y ) \ \big ) \rightarrow W , \beta \Vdash u \in x \ . $$

Proof

Assume $u \ne y$ and that each one of the following clauses holds

• (A) $\beta \not \sqsubseteq \mathsf {adj} (x, y )$

• (B) there exist $z_0, z_1$ such that $\mathsf {adj} (x, y ) = \langle z_0 , z_1 \rangle$

• (C) there exists $W_0$ such that $\beta \sqsubseteq W_0 \; \wedge \; \langle W , \mathsf {adj} (x, y ) \rangle = \langle W_0 , \mathsf {adj} (x, y ) \rangle$

• (D) if $\langle W_1 , v \rangle \sqsubseteq \langle W , \mathsf {adj} (x, y ) \rangle \ \wedge \ \beta \sqsubseteq W_1 \ \wedge \ W_1 \ne \beta$, then there exist $v_0, v_1$ such that

  $$ v = \langle v_0 , v_1 \rangle \ \wedge \ \exists W_2 \; [\! \ \beta \sqsubseteq W_2 \ \wedge \ W_1 = \langle W_2 , v_0 \rangle \ \!] $$

• (E) there exist $W_3$ and v such that $\langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq \langle W , \mathsf {adj} (x, y ) \rangle \ \wedge \ \beta \sqsubseteq W_3$.

Let $( \text{ A}^{\prime } )$, $( \text{ B}^{\prime } )$, $( \text{ C}^{\prime } )$, $( \text{ D}^{\prime } )$, $( \text{ E}^{\prime } )$ denote the corresponding clauses where we use W instead of $\langle W , \mathsf {adj} (x, y ) \rangle$, and we use x instead of $\mathsf {adj} (x, y )$. We need to show that $( \text{ A}^{\prime } ) \! - \! ( \text{ E}^{\prime } )$ hold.

We show that $( \text{ A}^{\prime } )$ holds. By (A) , we have $\beta \not \sqsubseteq \mathsf {adj} (x, y )$. By $\mathsf {T}_4$ and the definition of $\mathsf {adj} (x, y )$, $\beta \sqsubseteq x$ implies $\beta \sqsubseteq \mathsf {adj} (x, y )$. Hence, $\beta \not \sqsubseteq x$. Thus, $( \text{ A}^{\prime } )$ holds.

We show that $( \text{ E}^{\prime } )$, $( \text{ C}^{\prime } )$ and $( \text{ B}^{\prime } )$ hold. By $\mathsf {T}_4$, $\mathsf {T}_2$ and (C) , we have $\beta \sqsubseteq W$ and $\langle W , \mathsf {adj} (x, y ) \rangle \sqsubseteq \langle W , \mathsf {adj} (x, y ) \rangle$. We show that $W \ne \beta$. By (E), there exist $W_3$ and v such that $\langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq \langle W , \mathsf {adj} (x, y ) \rangle \ \wedge \ \beta \sqsubseteq W_3$. By $\mathsf {T}_4$, we have

$$ \langle W_3 \, , \, \langle v, u \rangle \rangle = \langle W , \mathsf {adj} (x, y ) \rangle \ \vee \ \langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W \ \vee \ \beta \sqsubseteq \langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq \mathsf {adj} (x, y ) \ . $$

By $\mathsf {T}_2$ and $\mathsf {T}_5^{(2)}$, we have $u = y \ \vee \ \langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W \ \vee \ \beta \sqsubseteq \mathsf {adj} (x, y )$. Since $u \ne y$ and $\beta \not \sqsubseteq \mathsf {adj} (x, y )$, we have $\langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W$. This shows that $( \text{ E}^{\prime } )$ holds. Since $\beta \sqsubseteq W_3$, we have $\langle W_3 \, , \, \langle v, u \rangle \rangle \not \sqsubseteq \beta$ by $\mathsf {T}^{(2)}_6$. Hence, $W \ne \beta$. So

$$ \langle W , \mathsf {adj} (x, y ) \rangle \sqsubseteq \langle W , \mathsf {adj} (x, y ) \rangle \; \wedge \; \beta \sqsubseteq W \; \wedge \; W \ne \beta . $$

Then, by $\mathsf {T}_2$ and (D), there exists $W_0$ such that $\beta \sqsubseteq W_0 \; \wedge \; W = \langle W_0 , x \rangle$. Thus, $( \text{ C}^{\prime } )$ holds. Since $\langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W = \langle W_0 , x \rangle$ and $\beta \sqsubseteq W_3$, we have by $\mathsf {T}_4$ and $\mathsf {T}_2$

$$ \langle v, u \rangle = x \ \vee \ \langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W_0 \ \vee \ \langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq x \ . $$

If $\langle v, u \rangle = x$, then $( \text{ B}^{\prime } )$ holds. We have $\langle W_3 \, , \, \langle v, u \rangle \rangle \not \sqsubseteq x$ since $\beta \sqsubseteq W_3$ would otherwise imply $\beta \sqsubseteq \mathsf {adj} (x, y )$ by $\mathsf {T}_4$ and $\mathsf {T}_5^{(2)}$. Assume $\langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W_0$. Since $\beta \sqsubseteq W_3$, we have $W_0 \ne \beta$ by $\mathsf {T}_6^{(2)}$. Hence, by $\mathsf {T}_4$, we have

$$ \langle W_0 , x \rangle \sqsubseteq \langle W , \mathsf {adj} (x, y ) \rangle \ \wedge \ \beta \sqsubseteq W_0 \ \wedge \ W_0 \ne \beta \ . $$

Then, by (D), there exists $x_0, x_1$ such that $x = \langle x_0 , x_1 \rangle$. Thus, $( \text{ B}^{\prime } )$ holds.

We verify that $( \text{ D}^{\prime } )$ holds. Assume $\langle W_1 , v \rangle \sqsubseteq W \; \wedge \; \beta \sqsubseteq W_1 \; \wedge \; W_1 \ne \beta$. By $\mathsf {T}_4$, we have $\langle W_1 , v \rangle \sqsubseteq \langle W , \mathsf {adj} (x, y ) \rangle \; \wedge \; \beta \sqsubseteq W_1 \; \wedge \; W_1 \ne \beta$. It then follows from (D) that $( \text{ D}^{\prime } )$ holds.    $\square$

Lemma 4

Let $W^{\prime } = \langle W , \mathsf {adj} (x, y ) \rangle$. Then, $\mathsf {T}^{(2) }$ proves the universal closure of

$$ ( \ \beta \not \sqsubseteq \mathsf {adj} (x, y ) \; \wedge \; W , \beta \Vdash u \in x \ ) \rightarrow W^{\prime } , \beta \Vdash u \in \mathsf {adj} (x, y ) \ . $$

Proof

Assume $\beta \not \sqsubseteq \mathsf {adj} (x, y )$ and that each one of the following clauses holds

• (A) $\beta \not \sqsubseteq x$

• (B) there exist $z_0, z_1$ such that $x = \langle z_0 , z_1 \rangle$

• (C) there exists $W_0$ such that $\beta \sqsubseteq W_0 \; \wedge \; W = \langle W_0 , x \rangle$

• (D) if $\langle W_1 , v \rangle \sqsubseteq W \ \wedge \ \beta \sqsubseteq W_1 \ \wedge \ W_1 \ne \beta$, then there exist $v_0, v_1$ such that

  $$ v = \langle v_0 , v_1 \rangle \ \wedge \ \exists W_2 \; [\! \ \beta \sqsubseteq W_2 \ \wedge \ W_1 = \langle W_2 , v_0 \rangle \ \!] $$

• (E) there exist $W_3$ and v such that $\langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W \ \wedge \ \beta \sqsubseteq W_3$.

Let $( \text{ A}^{\prime } )$, $( \text{ B}^{\prime } )$, $( \text{ C}^{\prime } )$, $( \text{ D}^{\prime } )$, $( \text{ E}^{\prime } )$ denote the corresponding clauses where we use $W^{\prime }$ instead of W, and we use $\mathsf {adj} (x, y )$ instead of x. We need to show that $( \text{ A}^{\prime } ) \! - \! ( \text{ E}^{\prime } )$ hold.

By assumption, $\beta \not \sqsubseteq \mathsf {adj} (x, y )$. Thus, $( \text{ A}^{\prime } )$ holds. Since $\mathsf {adj} (x, y ) = \langle x, y \rangle$, $( \text{ B}^{\prime } )$ holds. By (C), there exists $W_0$ such that $\beta \sqsubseteq W_0 \; \wedge \; W = \langle W_0 , x \rangle$. By $\mathsf {T}_4$ and the definition of $W^{\prime }$, we have $\beta \sqsubseteq W \; \wedge \; W^{\prime } = \langle W , \mathsf {adj} (x, y ) \rangle$. Thus, $( \text{ C}^{\prime } )$ holds.

We verify that $( \text{ E}^{\prime } )$ holds. By (E), there exist $W_3$ and v such that $\beta \sqsubseteq W_3$ and $\langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W$. By $\mathsf {T}_4$ and the definition of $W^{\prime }$, we have $\beta \sqsubseteq W_3$ and $\langle W_3 \, , \, \langle v, u \rangle \rangle \sqsubseteq W^{\prime }$. Thus, $( \text{ E}^{\prime } )$ holds.

It remains to verify that $( \text{ D}^{\prime } )$ holds. Assume $\langle W_1 , v \rangle \sqsubseteq W^{ \prime }$, $\beta \sqsubseteq W_1$ and $W_1 \ne \beta$. By $\mathsf {T}_4$ and the definition of $W^{ \prime }$, we have

$$ \langle W_1 , v \rangle = \langle W , \mathsf {adj} (x, y ) \rangle \ \vee \ \langle W_1 , v \rangle \sqsubseteq W \ \vee \ \langle W_1 , v \rangle \sqsubseteq \mathsf {adj} (x, y ) \ . $$

We cannot have $\langle W_1 , v \rangle \sqsubseteq \mathsf {adj} (x, y )$ since $\beta \sqsubseteq W_1$ would otherwise by $\mathsf {T}_4$ and $\mathsf {T}_5^{(2)}$ imply $\beta \sqsubseteq \mathsf {adj} (x, y )$. Hence, $\langle W_1 , v \rangle = \langle W , \mathsf {adj} (x, y ) \rangle \ \vee \ \langle W_1 , v \rangle \sqsubseteq W$. Assume $\langle W_1 , v \rangle = \langle W , \mathsf {adj} (x, y ) \rangle$. By $\mathsf {T}_2$ and (C), there exists $W_0$ such that $v = \langle x, y \rangle$, $W_1 = W = \langle W_0 , x \rangle$ and $\beta \sqsubseteq W_0$. Assume now $\langle W_1 , v \rangle \sqsubseteq W$. Then, by (D), there exist $v_0, v_1$ such that $v = \langle v_0 , v_1 \rangle \ \wedge \ \exists W_2 \; [\! \ \beta \sqsubseteq W_2 \ \wedge \ W_1 = \langle W_2 , v_0 \rangle \ \!]$. Thus, $( \text{ D}^{\prime } )$ holds.    $\square$

We now have everything we need to show that $\mathsf {T}^{(2)}$ is sequential.

Theorem 3

$\mathsf {AS}$ is directly interpretable in $\mathsf {T}^{(2)}$.

Proof

We translate the membership relation as follows

$$ u \in z \equiv \ \exists \alpha \; \Big [\! \ \alpha \sqsubseteq \alpha \ \wedge \ \forall \beta \; \big [\! \ ( \ \alpha \sqsubseteq \beta \ \wedge \ \beta \sqsubseteq \beta \ ) \rightarrow \exists W \; [\! \ W , \beta \Vdash u \in z \ \!] \ \big ] \ \Big ] \ . $$

By Lemma 1, the translation of $\mathsf {AS}_1$ is a theorem of $\mathsf {T}^{(2)}$. It remains to show that the translation of $\mathsf {AS}_2$ is a theorem of $\mathsf {T}^{(2)}$. It suffices to show that the sentence $\forall x y u \; [\! \ u \in \mathsf {adj} (x, y ) \leftrightarrow ( \ u = y \; \vee \; u \in x \ ) \ \!]$ is a theorem of $\mathsf {T}^{(2)}$.

We show that $\mathsf {T}^{(2)} \vdash \forall x y \; [\! \ y \in \mathsf {adj} (x, y ) \ \!]$. Let $\alpha = \langle \mathsf {adj} (x, y ) , \mathsf {adj} (x, y ) \rangle$. By $\mathsf {T}_4$, we have $\alpha \sqsubseteq \alpha$. Let $\beta$ be such that $\alpha \sqsubseteq \beta$ and $\beta \sqsubseteq \beta$. We need to find W such that $W , \beta \Vdash y \in \mathsf {adj} (x, y )$. By $\mathsf {T}_5^{(2)}$, $\beta \sqsubseteq \mathsf {adj} (x, y )$ implies $\alpha \sqsubseteq \mathsf {adj} (x, y )$, which contradicts $\mathsf {T}^{(2)}_6$ since $\mathsf {adj} (x, y ) \sqsubseteq \mathsf {adj} (x, y )$ by $\mathsf {T}_4$. Hence, $\beta \sqsubseteq \beta$ and $\beta \not \sqsubseteq \mathsf {adj} (x, y )$. Then, by Lemma 2, we have $\big \langle \beta , \mathsf {adj} (x, y ) \big \rangle , \beta \Vdash y \in \mathsf {adj} (x, y )$. Thus, $\mathsf {T}^{(2)} \vdash \forall x y \; [\! \ y \in \mathsf {adj} (x, y ) \ \!]$.

We show that $\mathsf {T}^{(2)} \vdash \forall x y u \; [\! \ u \in \mathsf {adj} (x, y ) \rightarrow ( \ u = y \; \vee \; u \in x \ ) \ \!]$. Assume $u \in \mathsf {adj} (x, y ) \; \wedge \; u \ne y$. We need to show that $u \in x$. Since $u \in \mathsf {adj} (x, y )$, there exists $\alpha$ such that

$$ \alpha \sqsubseteq \alpha \ \wedge \ \forall \beta \; \big [\! \ ( \ \alpha \sqsubseteq \beta \ \wedge \ \beta \sqsubseteq \beta \ ) \rightarrow \exists W \; [\! \ W, \beta \Vdash u \in \mathsf {adj} (x, y ) \ \!] \ \big ] \ . $$

By Clause (C) of $W , \beta \Vdash u \in \mathsf {adj} (x, y )$, we have

$$ \alpha \sqsubseteq \alpha \ \wedge \ \forall \beta \; \big [\! \ ( \ \alpha \sqsubseteq \beta \ \wedge \ \beta \sqsubseteq \beta \ ) \rightarrow \exists V \; [\! \ \langle V , \mathsf {adj} (x, y ) \rangle , \beta \Vdash u \in \mathsf {adj} (x, y ) \ \!] \ \big ] \ . $$

Then, by Lemma 3, we have

$$ \alpha \sqsubseteq \alpha \ \wedge \ \forall \beta \; \big [\! \ ( \ \alpha \sqsubseteq \beta \ \wedge \ \beta \sqsubseteq \beta \ ) \rightarrow \exists V \; [\! \ V , \beta \Vdash u \in x \ \!] \ \big ] \ . $$

Thus, $\mathsf {T}^{(2)} \vdash \forall x y u \; [\! \ u \in \mathsf {adj} (x, y ) \rightarrow ( \ u = y \; \vee \; u \in x \ ) \ \!]$.

We show that $\mathsf {T}^{(2)} \vdash \forall x y u \; [\! \ u \in x \rightarrow u \in \mathsf {adj} (x, y ) \ \!]$. Assume $u \in x$ holds. Then, there exists $\alpha ^{\prime }$ such that

$$\begin{aligned} \alpha ^{\prime } \sqsubseteq \alpha ^{\prime } \ \wedge \ \forall \beta \; \big [\! \ ( \ \alpha ^{\prime } \sqsubseteq \beta \ \wedge \ \beta \sqsubseteq \beta \ ) \rightarrow \exists V \; [\! \ V , \beta \Vdash u \in x \ \!] \ \big ] \ . \end{aligned}$$

(*)

Let $\alpha = \langle \mathsf {adj} (x, y ) , \alpha ^{\prime } \rangle$. By $\mathsf {T}_4$ and $\alpha ^{\prime } \sqsubseteq \alpha ^{\prime }$, we have $\alpha \sqsubseteq \alpha \; \wedge \; \alpha ^{\prime } \sqsubseteq \alpha$. Hence, by $\mathsf {T}^{(2)}_5$, we have $\alpha \sqsubseteq \alpha \; \wedge \; \forall \beta \; [\! \ \alpha \sqsubseteq \beta \rightarrow \alpha ^{\prime } \sqsubseteq \beta \ \!]$. We have $\mathsf {adj} (x, y ) \sqsubseteq \mathsf {adj} (x, y )$ by $\mathsf {T}_4$. Hence, $\alpha \not \sqsubseteq \mathsf {adj} (x, y )$ by $\mathsf {T}^{(2)}_6$. Then, by $\mathsf {T}^{(2)}_5$, we have $\alpha \sqsubseteq \beta \rightarrow \beta \not \sqsubseteq \mathsf {adj} (x, y )$. It then follows from (*) and Lemma 4 that

$$ \alpha \sqsubseteq \alpha \ \wedge \ \forall \beta \; \big [\! \ ( \ \alpha \sqsubseteq \beta \ \wedge \ \beta \sqsubseteq \beta \ ) \rightarrow \exists V \; [\! \ \langle V , \mathsf {adj} (x, y ) \rangle , \beta \Vdash u \in \mathsf {adj} (x, y ) \ \!] \ \big ] \ . $$

Thus, $\mathsf {T}^{(2)} \vdash \forall x y u \; [\! \ u \in x \rightarrow u \in \mathsf {adj} (x, y ) \ \!]$.    $\square$

Corollary 1

$\mathsf {AS}$ is directly interpretable in $\varSigma _{\mathsf {open}}^{ \mathsf {T} }$.

Our interpretation of $\mathsf {AS}$ relies heavily on the transitivity of the subtree relation and it is not clear to us whether it is possible to directly interpret $\mathsf {AS}$ without using this property.

Open Problem 3

Is $\mathsf {AS}$ directly interpretable in $\mathsf {T}$? Is $\mathsf {AS}$ directly interpretable in $\mathsf {T}^{(1)}$?

5.3 An Alternative Proof

In this final section, we present an alternative direct interpretation of $\mathsf {AS}$ in $\mathsf {T}^{(2)}$ that was suggested by one of the referees. Let $\mathsf {Pair} (x ) \equiv \ \exists y z \; [\! \ x = \langle y, z \rangle \ \!]$ and $x \in ^{\prime } y \equiv \ \exists u v \; [\! \ y = \langle u, v \rangle \; \wedge \; \langle v, x \rangle \sqsubseteq y \ \!]$. Let $\mathsf {BSh} (x )$ be shorthand for: there exist u, v such that the following holds: (i) $x = \langle u, v \rangle$, (ii) $\mathsf {Pair} (v)$, (iii) $\forall v^{\prime } \; \big [\! \ v \sqsubseteq v^{\prime } \; \wedge \; \mathsf {Pair} (v^{\prime } ) \rightarrow \exists u^{\prime } \; \forall y \; [\! \ y \in ^{\prime } x \leftrightarrow y \in ^{\prime } \langle u^{\prime } , v^{\prime } \rangle \ \!] \ \big ]$. We translate the membership relation as follows: $x \in y \equiv \ x \in ^{\prime } y \; \wedge \; \mathsf {BSh} (y )$.

It is easy to verify, using $\mathsf {T}_1$ and $\mathsf {T}_3$, that the translation of $\mathsf {AS}_1$ is a theorem of $\mathsf {T}^{(2)}$. We verify that the translation of $\mathsf {AS}_2$ is a theorem of $\mathsf {T}^{(2)}$. We are given x and y and need to find z such that (1) $\forall w \; {[}\!\ w \in z \leftrightarrow {(}\! \ w \in x \; \vee \; w = y \ \!{)} \ \!{]}$. We assume first x is not an empty set according to $\in$. Then, there exist u, v such that $x = \langle u, v \rangle$, $\mathsf {Pair} ( v )$ and for any $v^{\prime } \sqsupseteq v$ such that $\mathsf {Pair} ( v^{\prime } )$, there exist $u^{\prime }$ such that x and $\langle u^{\prime } , v^{\prime } \rangle$ have the same $\in ^{\prime }$-elements. To construct z we pick $v^{\prime } = \langle v , y \rangle$. Since $\mathsf {Pair} ( v )$, we have $v \sqsubseteq v^{\prime }$ by $\mathsf {T}_4$. We then pick a corresponding $u^{\prime }$ and put $z = \big \langle \, \langle u^{\prime } \, , \, \langle v^{\prime } , y \rangle \, \rangle \, , \, v^{\prime } \, \big \rangle$. It is easy to see that in order to verify (1) it is enough to fix arbitrary $v^{\prime \prime } \sqsupseteq v^{\prime }$ and any $u^{\prime \prime }$ such that $\mathsf {Pair} ( v^{\prime \prime } )$ and $\forall w \; [\! \ w \in ^{\prime } \langle u^{\prime } , v^{\prime } \rangle \leftrightarrow w \in \langle u^{\prime \prime } , v^{\prime \prime } \rangle \ {]}$ and show that the $\in ^{\prime }$ elements of $\big \langle \, \langle u^{\prime \prime } \, , \, \langle v^{\prime \prime } , y \rangle \, \rangle \, , \, v^{\prime \prime } \, \big \rangle$ precisely are y and all w such that $w \in ^{\prime } x$.

We have $w \in ^{\prime } \big \langle \, \langle u^{\prime \prime } \, , \, \langle v^{\prime \prime } , y \rangle \, \rangle \, , \, v^{\prime \prime } \, \big \rangle$ if and only if $\langle u^{\prime \prime } , w \rangle \sqsubseteq \langle u^{\prime \prime } \, , \, \langle v^{\prime \prime } , y \rangle \, \rangle$. By $\mathsf {T}_4$, the latter happens in exactly the following cases: (a) $\langle v^{\prime \prime } , w \rangle \sqsubseteq u^{\prime \prime }$, (b) $\langle v^{\prime \prime } , w \rangle \sqsubseteq y$, (c) $\langle v^{\prime \prime } , w \rangle \sqsubseteq v^{\prime \prime }$, (d) $\langle v^{\prime \prime } , w \rangle = \langle v^{\prime \prime } , y \rangle$, (e) $\langle v^{\prime \prime } , w \rangle = \langle u^{\prime \prime } \, , \, \langle v^{\prime \prime } , y \rangle \, \rangle$. By the choice of $v^{\prime \prime }$ and $u^{\prime \prime }$, (a) holds if and only if $w \in ^{\prime } \langle u^{\prime } , v^{\prime } \rangle$, which in turn by the choice of $v^{\prime }$ and $u^{\prime }$ happens if and only if $w \in ^{\prime } x$. By $\mathsf {T}_2$, Case (d) happens if and only if $w = y$. By definition, $v^{ \prime } = \langle v , y \rangle$. Since $\mathsf {Pair} (v)$, we have $v \sqsubseteq v^{ \prime } \sqsubseteq v^{ \prime \prime }$ by $\mathsf {T}_4$. By $\mathsf {T}_4$, (b) implies $\langle u^{\prime \prime } , w \rangle \sqsubseteq \langle v, y \rangle = v^{ \prime } \sqsubseteq v^{ \prime \prime }$. By $\mathsf {T}^{(2)}_5$, (b) implies $\langle u^{\prime \prime } , w \rangle \sqsubseteq v^{ \prime \prime }$, which contradicts $\mathsf {T}^{(2)}_6$ since $v^{ \prime \prime } \sqsubseteq v^{ \prime \prime }$ by $\mathsf {T}_4$ as $\mathsf {Pair} ( v^{ \prime \prime } )$. Similarly, Case (c) contradicts $\mathsf {T}^{(2)}_6$. By $\mathsf {T}_2$, Case (e) holds if and only if $v^{\prime \prime } = u^{\prime \prime }$ and $w = \langle v^{\prime \prime } , y \rangle$. Since x is not an empty set according to $\in$, there exists $w^{\prime }$ such that $\langle v^{\prime \prime } , w^{\prime } \rangle \sqsubseteq u^{\prime \prime } = v^{\prime \prime }$ (since x and $\langle u^{\prime \prime } , v^{\prime \prime } \rangle$ have the same $\in ^{\prime }$ elements) which contradicts $\mathsf {T}^{(2)}_6$. This concludes the verification of (1) when x is not an empty set according to $\in$.

If x is an empty set according to $\in$, we replace x with $\langle \perp , \langle \perp , \perp \rangle \rangle$ and proceed as above always choosing $u^{\prime } = \perp$ and $u^{\prime \prime } = \perp$. This concludes the verification of $\mathsf {AS}_2$. This completes the proof.