TREE THEORY: INTERPRETABILITY BETWEEN WEAK FIRST-ORDER THEORIES OF TREES

Abstract

Elementary first-order theories of trees allowing at most, exactly $\mathrm{m}$, and any finite number of immediate descendants are introduced and proved mutually interpretable among themselves and with Robinson arithmetic, Adjunctive Set Theory with Extensionality and other well-known weak theories of numbers, sets, and strings.

1 Introduction

In logic, trees are almost everywhere. Algorithmic tests for basic syntactic and semantic properties such as well-formedness, satisfiability, or validity typically involve construction of tree-like arrays. Elementary model theory of first-order logic is often presented as revolving around properties of a certain kind of tree—witness König’s Lemma—and basic objects of proof theory, such as proofs, derivations, and sequents, are most directly represented in tree-like form. One does get the feeling that trees might be as fundamental to logical theory as are numbers and sets. Yet they seem not have to been systematically and explicitly investigated as subject of a specific theory in axiomatic form.

An important step in this direction was taken recently in the work of Kristiansen and Murwanashyaka [4] who introduced an elementary theory $\mathrm{T}$ of full binary trees, finite trees in which every non-terminal node has exactly two immediate descendants. (We shall call such trees dyadic.) They showed that the basic arithmetical operations of addition and multiplication are definable in $\mathrm{T}$ , and more specifically, that Robinson arithmetic, $\mathrm{Q}$ , is formally interpretable in $\mathrm{T}$ . In [3], we showed that $\mathrm{T}$ , on the other hand, is also interpretable in $\mathrm{Q}$ , and hence mutually interpretable with several other well-known theories of numbers, sets, and strings. The argument given in [3] hinges on a formalized representation of dyadic trees by binary strings in elementary concatenation theory ${\mathrm{QT}}^{+}$ .

Here we extend and generalize this approach to finite trees in general. We take a planar tree to be a connected and acyclical planar graph with one node singled out as the “root” of the tree. We consider the vocabulary ${{\mathcal{L}}}_{\mathrm{T}^\ast}=\{0,{\tau}_1,{\tau}_2,\dots, \sqsubseteq \}$ with a single individual constant $0$ and infinitely many function symbols ${\tau}_1,{\tau}_2,\dots$ where ${\tau}_{\mathrm{n}}$ has arity n for each $\mathrm{n}\ge 1$ , and a $2$ -place relation symbol $\sqsubseteq$ , along with the (universal closures) of the following formulae as axioms:

$$\begin{align*}&(\mathrm{T}{1}_{\mathrm{n}})\quad \neg {\tau}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}})=0\quad \mathrm{for}\ \mathrm{each}\;\mathrm{n}\ge 1.\\ &(\mathrm{T}{2}_{\mathrm{m},\mathrm{n}})\hspace{10pt} \neg {\tau}_{\mathrm{m}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{m}})={\tau}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}})\hspace{10pt} \mathrm{for}\ \mathrm{each}\;\mathrm{m},\mathrm{n}\;\mathrm{where}\;\mathrm{m}\ne \mathrm{n}.\\&(\mathrm{T}{3}_{\mathrm{n}})\quad {\tau}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}})={\tau}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}})\to \wedge_{1\le \mathrm{i}\le \mathrm{n}}{\mathrm{x}}_{\mathrm{i}}={\mathrm{y}}_{\mathrm{i}}\quad \mathrm{for}\ \mathrm{each}\;\mathrm{n}\ge 1.\\&(\mathrm{T}{4}_{\mathrm{n}})\hspace{2pt} \mathrm{x}\sqsubseteq {\tau}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}})\leftrightarrow \mathrm{x}={\tau}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}})\,\mathrm{v}\,{\vee}_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{i}}\hspace{2pt} \mathrm{for}\ \mathrm{each}\;\mathrm{n}\ge 1.\\&(\mathrm{T}5)\quad \mathrm{x}\sqsubseteq \mathrm{x}.\\&(\mathrm{T}6)\quad 0\sqsubseteq \mathrm{x}.\\&(\mathrm{T}7)\quad\mathrm{x}\sqsubseteq \mathrm{y}\ \& \ \mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{x}=\mathrm{y}.\\&(\mathrm{T}8)\quad \mathrm{x}\sqsubseteq \mathrm{y}\ \& \ \mathrm{y}\sqsubseteq \mathrm{z}\to \mathrm{x}\sqsubseteq \mathrm{z}.\end{align*}$$

We call the resulting first-order theory with identity $\mathrm{T}^\ast$ . The domain of the intended interpretation consists of finite planar trees whose nodes may have any number, including single, immediate descendants. (Alternatively, we may think of the domain as consisting of all variable-free ${{\mathcal{L}}}_{\mathrm{T}^\ast }$ -terms.) Here we are thinking of finite trees as constructed from $0$ by finitely many applications of any combination of tree building operations associated with ${\tau}_1,{\tau}_2,\dots$ . The individual constant $0$ refers to a trivial, single node tree, and, for each $\mathrm{n}\ge 1$ , the $\mathrm{n}$ -ary operation associated with ${\tau}_{\mathrm{n}}$ applied to trees ${T}_1,\dots, {T}_{\mathrm{n}}$ yields the tree ${\tau}_{\mathrm{n}}({T}_1,\dots, {T}_{\mathrm{n}})$ whose root node has as its immediate descendants the root nodes of ${T}_1,\dots, {T}_{\mathrm{n}}$ , respectively. We think of these trees as linearly ordered in that the immediate subtrees ${T}_1,\dots, {T}_{\mathrm{n}}$ of ${\tau}_{\mathrm{n}}({T}_1,\dots, {T}_{\mathrm{n}})$ are ordered, say, from left to right. However, when considering nodes with a single immediate descendant (singleton), we do not distinguish between “branching to the right” and “branching to the left.” (This we will do in Section 9 with appropriate modifications to the corresponding theories.) The relational symbol $\sqsubseteq$ is meant to express the subtree relation between trees, where subtrees are defined so that for a given tree $T$ , any of its nodes $\mathrm{x}$ determines a subtree ${T}_{\mathrm{x}}$ consisting of all and only the descendants of $\mathrm{x}$ in $T$ including itself.

By including only the appropriate instances of each of the schemas $(\mathrm{T}{1}_{\mathrm{n}})$ , $(\mathrm{T}{2}_{\mathrm{m},\mathrm{n}})$ , $(\mathrm{T}{3}_{\mathrm{n}})$ , and $(\mathrm{T}{4}_{\mathrm{n}})$ along with $(\mathrm{T}5){-}(\mathrm{T}8)$ we obtain theories ${\mathrm{T}}_{\mathrm{m}}$ of trees of fixed arity or theories ${\mathrm{T}}_{\le \mathrm{m}}$ of $\le \mathrm{m}$ -trees with at most $\mathrm{m}$ branchings, for fixed $\mathrm{m}$ . The theory $\mathrm{T}$ of dyadic trees formulated by Kristiansen and Murwanashyaka and further investigated in [3] is a subtheory of ${\mathrm{T}}_2$ , with $\mathrm{x}\sqsubseteq 0\leftrightarrow \mathrm{x}=0$ in place of $(\mathrm{T}5){-}(\mathrm{T}8)$ . The latter formula is easily seen to be implied by $(\mathrm{T}5){-}(\mathrm{T}7)$ .

In Section 2 we identify characteristic traces of tree structure in binary strings. On that basis in Section 3 we set up a formal coding apparatus for finite trees, which we call Catalan coding. In Section 4 we establish that, for $\mathrm{m}\ge 2$ , theories ${\mathrm{T}}_{\le \mathrm{m}}$ (and ${\mathrm{T}}_{\mathrm{m}}$ ) are each formally interpretable in ${\mathrm{T}}_{\le 2}$ , and in Section 5 that, in turn, ${\mathrm{T}}_{\le 2}$ is interpretable in the concatenation theory ${\mathrm{QT}}^{+}$ . We use this in Section 6 to establish mutual interpretability of all of the finitely axiomatized theories ${\mathrm{T}}_{\le \mathrm{m}}$ and ${\mathrm{T}}_{\mathrm{m}}$ . In Section 7 we interpret the theory of all finite trees $\mathrm{T}^\ast$ in ${\mathrm{QT}}^{+}$ . In Section 8 we consider some theories of dyadic trees that extend $\mathrm{T}$ and establish their mutual interpretability, showing, among other things, that ${\mathrm{T}}_2$ is also interpretable in $\mathrm{T}$ . In Section 9 we introduce theories ${\mathrm{T}}_{\mathrm{e}}$ , ${\mathrm{T}}_{\le \mathrm{n},\mathrm{e}}$ , and ${{\mathrm{T}}^{\ast}}_{\mathrm{e}}$ that distinguish between left and right single branchings and prove their mutual interpretability with $\mathrm{T}$ , ${\mathrm{T}}_{\le \mathrm{n}}$ , and ${\mathrm{T}}^{\ast }$ , respectively. Finally, in Section 10 we prove that all these theories are mutually interpretable among themselves and with $\mathrm{Q}$ , Adjunctive Set Theory with or without Extensionality, various concatenation theories, etc.

2 Almost even strings

We first turn to concatenation theory. The language ${{\mathcal{L}}}_{\mathrm{C}}=\{\mathrm{a},\mathrm{b},{}^{\ast} \}$ of concatenation theory has two individual constants $a$ and $b$ , and a single binary operation symbol ${}^\ast$ . Its intended interpretation ${\varSigma}^{\ast }$ has as its domain the set of all non-empty finite strings of $a$ ’s and $b$ ’s, the constants “ $\mathrm{a}$ ” and “ $\mathrm{b}$ ,” respectively, stand for the digits $a$ and $b$ (or $0$ and $1$ , resp.), and, for given strings $\mathrm{x}$ and $\mathrm{y}$ from the domain of ${\varSigma}^{\ast }$ , we let $\mathrm{x}^\ast \mathrm{y}$ be the string obtained by concatenation (i.e., juxtaposition) of the successive digits of $\mathrm{y}$ to the right of the end digit of $\mathrm{x}$ . For the moment we reason informally in the first-order theory $\mathrm{Th}{(}{\varSigma}^{\ast})$ consisting of all true sentences of ${{\mathcal{L}}}_{\mathrm{C}}$ in ${\varSigma}^{\ast }$ . (Later, in Section 5, we introduce a finitely axiomatized subtheory ${\mathrm{QT}}^{+}$ of $\mathrm{Th}{(}{\varSigma}^{\ast})$ that will play a key role in our formal argument.)

We shall pay particular attention to the number of occurrences of $a$ ’s and $b$ ’s in a given string. The functions $\alpha{(}\mathrm{x})$ and $\beta{(}\mathrm{x})$ that count the number of $a$ ’s and $b$ ’s, respectively, in a string $\mathrm{x}$ are defined by a straightforward recursion on strings:

$$\begin{align*}&\alpha (\mathrm{a})=1\quad\quad\quad\quad\quad\quad\quad \beta (\mathrm{a})=0.\\&\alpha (\mathrm{b})=0\quad\quad\quad\quad\quad\quad\quad \beta (\mathrm{b})=1.\\&\alpha (\mathrm{x}^\ast \mathrm{a})=\alpha (\mathrm{x})+1\qquad\quad \beta (\mathrm{x}^\ast \mathrm{a})=\beta (\mathrm{x}).\\&\alpha (\mathrm{x}^\ast \mathrm{b})=\alpha (\mathrm{x})\qquad\qquad\hspace{6pt} \beta (\mathrm{x}^\ast \mathrm{b})=\beta (\mathrm{x})+1.\end{align*}$$

An equally straightforward induction on strings shows that the functions $\alpha$ and $\beta$ are additive with respect to concatenation operation ${}^\ast$ on strings:

$$\begin{align*}\alpha (\mathrm{x}^\ast \mathrm{y})=\alpha (\mathrm{x})+\alpha (\mathrm{y})\quad\mathrm{and}\quad\beta (\mathrm{x}^\ast \mathrm{y})=\beta (\mathrm{x})+\beta (\mathrm{y}),\end{align*}$$

and that for each string $\mathrm{x}$ , $\alpha (\mathrm{x})+\beta (\mathrm{x})>0$ .

On account of associativity of the binary concatenation operation we sometimes omit writing the symbol ${}^\ast$ and parentheses, simply juxtaposing concatenated strings one next to another. We let

$$\begin{align*}&\mathrm{x}\mathrm{By}\equiv \exists \mathrm{z}\;\mathrm{x}^\ast \mathrm{z}=\mathrm{y}\kern0.24em \;\mathrm{and}\kern0.24em \mathrm{x}\mathrm{Ey}\equiv \exists \mathrm{z}\;\mathrm{z}^\ast \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{and}\kern0.17em \mathrm{also}\\&\mathrm{x}{\subseteq}_{\mathrm{p}}\mathrm{y}\equiv \mathrm{x}=\mathrm{y}\;\mathrm{v}\;\mathrm{xBy}\;\mathrm{v}\;\mathrm{xEy}\;\mathrm{v}\; \exists {\mathrm{y}}_1\exists {\mathrm{y}}_2\mathrm{y}={\mathrm{y}}_1^\ast (\mathrm{x}^\ast {\mathrm{y}}_2).\end{align*}$$

We define ${\mathrm{Tally}}_{\mathrm{b}}{(}\mathrm{x})\equiv \forall \mathrm{y}{\subseteq}_{\mathrm{p}}\mathrm{x}{(}\mathrm{Digit}{(}\mathrm{y})\to \mathrm{y}=\mathrm{b})$ where $\mathrm{Digit}(\mathrm{x})\equiv \mathrm{x}=\mathrm{a}\;\mathrm{v}\;\mathrm{x}=\mathrm{b}$ . In ${{\mathcal{L}}}_{\mathrm{C}}$ , the $\mathrm{b}$ -tallies $\mathrm{b}$ , $\mathrm{bb}$ , $\mathrm{bbb}$ , … may be identified with the formal numerals $\underline{0}$ , $\underline{1}$ , $\underline{2}$ , …, so we sometimes write $\underline {\mathrm{n}}$ for the string ${\mathrm{b}}^{\mathrm{n}+1}$ of $\mathrm{n}+1$ consecutive $b$ ’s.

One of the principal results of [3] is that (the graphs of) the functions $\alpha{(}\mathrm{x})$ and $\beta (\mathrm{x})$ are expressible by ${{\mathcal{L}}}_{\mathrm{C}}$ formulae ${\mathrm{A}}^{\#}{(}\mathrm{x},\mathrm{y})$ and ${\mathrm{B}}^{\#}{(}\mathrm{x},\mathrm{y})$ , respectively, along with (the graph of) the binary operation AddTally on strings that simulates addition of non-negative integers by concatenation of $\mathrm{b}$ -tallies. With that in mind, we shall write, e.g., “ $\alpha{(}\mathrm{x})=\beta {(}\mathrm{y}{)}+\underline{1}$ ” and “ $\alpha {(}\mathrm{x})+\beta {(}\mathrm{x})=\underline {\mathrm{n}}$ ” with the understanding that these expressions abbreviate appropriately chosen ${{\mathcal{L}}}_{\mathrm{C}}$ formulas such as “ $\exists {\mathrm{x}}_1,{\mathrm{y}}_1({\mathrm{A}}^{\#}(\mathrm{x},{\mathrm{x}}_1)\ \&\ {\mathrm{B}}^{\#}(\mathrm{y},{\mathrm{y}}_1)\ \&\ {\mathrm{x}}_1={\mathrm{by}}_1)$ ” and “ $\exists {\mathrm{x}}_1{\mathrm{y}}_1\big({\mathrm{A}}^{\#}(\mathrm{x},{\mathrm{x}}_1)\ \&\ {\mathrm{B}}^{\#}(\mathrm{x},{\mathrm{y}}_1)\ \&\ \mathrm{AddTally}({\mathrm{x}}_1,{\mathrm{y}}_1,{\mathrm{b}}^{\mathrm{n}+1})$ ,” respectively. We then have :

2.1

For each $\mathrm{n}\ge 1$ ,

$$\begin{align*}{\varSigma}^{\ast}\models \forall \mathrm{x}\;[\alpha (\mathrm{x})+\beta (\mathrm{x})=\underline {\mathrm{n}}\leftrightarrow \exists {\mathrm{x}}_1\dots {\mathrm{x}}_{\mathrm{n}}(\wedge_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{Digit}({\mathrm{x}}_{\mathrm{i}})\ \&\ \mathrm{x}={\mathrm{x}}_1\dots {\mathrm{x}}_{\mathrm{n}})].\end{align*}$$

We omit the proof.

We call a string $\mathrm{x}$ almost even, writing , if (ci) $\alpha (\mathrm{x})=\beta (\mathrm{x})+1$ , (“the $+1$ property”) and (cii) for each proper initial segment $\mathrm{u}$ of $\mathrm{x}$ , $\alpha (\mathrm{u})\le \beta (\mathrm{u})$ .

In other words, the almost even strings are the shortest initial segments of themselves in which the number of $a$ ’s strictly exceeds the number of $b$ ’s. We let abbreviate the ${{\mathcal{L}}}_{\mathrm{C}}$ formula

$$\begin{align*}\begin{array}{l}\exists \mathrm{y},\mathrm{z}\;({\mathrm{A}}^{\#}(\mathrm{x},\mathrm{y})\ \&\ {\mathrm{B}}^{\#}(\mathrm{x},\mathrm{z})\ \& \ \mathrm{y}=\mathrm{z}^\ast \mathrm{b})\ \&\\ {}\kern0.6em \&\ \forall \mathrm{u},\mathrm{v},\mathrm{w}\;(\mathrm{u}\mathrm{Bx}\ \&\ {\mathrm{A}}^{\#}(\mathrm{u},\mathrm{v})\ \&\ {\mathrm{B}}^{\#}(\mathrm{u},\mathrm{w})\to \mathrm{v}\le \mathrm{w}).\end{array}\end{align*}$$

(See [3] for details.)

We note the following:

2.2

For the proof see [3, 2.1(a)].

2.3

(a)

(b)

(c)

(d)

Proof (a) is immediate from (ci) and (cii). For (b), see the proof in [3, 2.1(b)]; (c) and (d) follow from (b).

2.4

For any $\mathrm{n}\ge 1$ ,

Proof Assume that ${\varSigma}^{\ast}\models \mathrm{x}={\mathrm{sax}}_1\dots {\mathrm{x}}_{\mathrm{n}}\ \&\ \mathrm{y}={\mathrm{tay}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ , where ${\varSigma}^{\ast}\models {\mathrm{Tally}}_{\mathrm{b}}(\mathrm{s})\ \&\ {\mathrm{Tally}}_{\mathrm{b}}(\mathrm{t})$ and . Suppose ${\varSigma}^{\ast}\models \mathrm{x}=\mathrm{y}$ . Then ${\varSigma}^{\ast}\models {\mathrm{sax}}_1\dots {\mathrm{x}}_{\mathrm{n}}={\mathrm{tay}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ , whence ${\varSigma}^{\ast}\models \mathrm{sBx}\ \& \ \mathrm{tBx}$ . In that case, we have that ${\varSigma}^{\ast}\models \mathrm{sBt}\;\mathrm{v}\;\mathrm{s}=\mathrm{t}\;\mathrm{v}\;\mathrm{t}\mathrm{Bs}$ . Suppose, for a reductio, that ${\varSigma}^{\ast}\models \mathrm{sBt}$ . Then ${\varSigma}^{\ast}\models \exists \mathrm{u}\;({\mathrm{Tally}}_{\mathrm{b}}(\mathrm{u})\ \& \ \mathrm{t}=\mathrm{su})$ , whence ${\varSigma}^{\ast}\models {\mathrm{sax}}_1\dots {\mathrm{x}}_{\mathrm{n}}={\mathrm{suay}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ . But then ${\varSigma}^{\ast}\models {\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}={\mathrm{uay}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ , which is a contradiction because ${\varSigma}^{\ast}\models {\mathrm{Tally}}_{\mathrm{b}}(\mathrm{u})$ . Hence ${\varSigma}^{\ast}\models \neg \mathrm{sBt}$ . Exactly analogously, ${\varSigma}^{\ast}\models \neg \mathrm{tBs}$ . It follows that ${\varSigma}^{\ast}\models \mathrm{s}=\mathrm{t}$ .

Thus we obtain that ${\varSigma}^{\ast}\models {\mathrm{sax}}_1\dots {\mathrm{x}}_{\mathrm{n}}={\mathrm{say}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ , whence ${\varSigma}^{\ast}\models {\mathrm{x}}_1\dots {\mathrm{x}}_{\mathrm{n}}=\mathrm{z}={\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ . So ${\varSigma}^{\ast}\models {\mathrm{x}}_1\mathrm{Bz}\ \&\ {\mathrm{y}}_1\mathrm{Bz}$ . Then ${\varSigma}^{\ast}\models {\mathrm{x}}_1{\mathrm{By}}_1\mathrm{v}\;{\mathrm{x}}_1={\mathrm{y}}_1\;\mathrm{v}\;{\mathrm{y}}_1{\mathrm{Bx}}_1$ . But from , by 2.3(a), we have ${\varSigma}^{\ast}\models \neg {\mathrm{x}}_1{\mathrm{By}}_1\ \&\ \neg {\mathrm{y}}_1{\mathrm{Bx}}_1$ . Therefore, ${\varSigma}^{\ast}\models {\mathrm{x}}_1={\mathrm{y}}_1$ . Assume now that ${\varSigma}^{\ast }{\models}\wedge_{1\le \mathrm{i}\le \mathrm{k}}{\mathrm{x}}_{\mathrm{i}}={\mathrm{y}}_{\mathrm{i}}$ for $\mathrm{k}<\mathrm{n}$ . Then from ${\varSigma}^{\ast}\models \mathrm{s}=\mathrm{t}$ and hypothesis ${\varSigma}^{\ast}\models {\mathrm{sax}}_1\dots {\mathrm{x}}_{\mathrm{n}}={\mathrm{tay}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ we obtain

$$\begin{align*}{\varSigma}^{\ast}\models {\mathrm{sax}}_1\dots {\mathrm{x}}_{\mathrm{k}}({\mathrm{x}}_{\mathrm{k}+1}\dots {\mathrm{x}}_{\mathrm{n}})={\mathrm{sax}}_1\dots {\mathrm{x}}_{\mathrm{k}}({\mathrm{y}}_{\mathrm{k}+1}\dots {\mathrm{y}}_{\mathrm{n}}),\end{align*}$$

whence ${\varSigma}^{\ast}\models {\mathrm{x}}_{\mathrm{k}+1}\dots {\mathrm{x}}_{\mathrm{n}}={\mathrm{y}}_{\mathrm{k}+1}\dots {\mathrm{y}}_{\mathrm{n}}$ . Then the same argument as above shows that ${\varSigma}^{\ast}\models {\mathrm{x}}_{\mathrm{k}+1}={\mathrm{y}}_{\mathrm{k}+1}$ . Hence for all $\mathrm{j}$ , $1\le \mathrm{j}\le \mathrm{n}$ , ${\varSigma}^{\ast}\models {\mathrm{x}}_{\mathrm{j}}={\mathrm{y}}_{\mathrm{j}}$ .

2.5

(a)

(b)

Proof For (a), assume . By 2.2, ${\varSigma}^{\ast}\models \mathrm{bBx}\ \&\ \mathrm{aaEx}$ . Hence ${\varSigma}^{\ast}\models \exists {\mathrm{x}}_1\mathrm{x}={\mathrm{x}}_1\mathrm{aa}$ . So $\mathrm{x}$ has at least one proper initial segment $(={\mathrm{x}}_1\mathrm{a})$ that ends with $\mathrm{a}$ . Let ${\mathrm{s}}_0$ be the shortest such initial segment. Then ${\varSigma}^{\ast}\models {\mathrm{aEs}}_0$ , so ${\varSigma}^{\ast}\models \exists \mathrm{t}\;{\mathrm{s}}_0=\mathrm{ta}$ . But then ${\varSigma}^{\ast}\models {\mathrm{s}}_0\mathrm{Bx}\ \&\ {\mathrm{bBs}}_0$ , so we must have ${\varSigma}^{\ast}\models {\mathrm{Tally}}_{\mathrm{b}}(\mathrm{t})$ by the choice of ${\mathrm{s}}_0$ .

For (b), assume ${\varSigma}^{\ast}\models \mathrm{x}=\mathrm{bay}$ where . Then

$$\begin{align*}{\varSigma}^{\ast}\models \alpha (\mathrm{y})=\alpha (\mathrm{bay}){-}\underline{1}=(\beta (\mathrm{bay})+\underline{1}){-}\underline{1}=\beta (\mathrm{bay})=\beta (\mathrm{y})+\underline{1}.\end{align*}$$

Suppose ${\varSigma}^{\ast}\models \mathrm{zBy}$ . Then ${\varSigma}^{\ast}\models (\mathrm{baz})\mathrm{B}(\mathrm{bay})$ . Hence from hypothesis we have ${\varSigma}^{\ast}\models \alpha (\mathrm{z})=\alpha (\mathrm{baz})\hbox{--} \underline{1}\le \beta (\mathrm{baz})\hbox{--} \underline{1}=(\beta (\mathrm{z})+\underline{1})\hbox{--} \underline{1} =\beta (\mathrm{z})$ . Hence also ${\varSigma}^{\ast}\models \forall \mathrm{z}\;(\mathrm{z}\mathrm{By}\to \alpha (\mathrm{z})\le \beta (\mathrm{z}))$ . Therefore, .

2.6

Let $\mathrm{u}$ be any closed ${{\mathcal{L}}}_{\mathrm{C}}$ term. If , then for some $\mathrm{n}\ge 1$ , ${\varSigma}^{\ast}\models \exists {\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{n}}\mathrm{u}={\mathrm{b}}^{\mathrm{n}}{\mathrm{au}}_1\dots {\mathrm{u}}_{\mathrm{n}}$ .

Proof Assume . Then, by 2.5(a), ${\varSigma}^{\ast}\models \exists \mathrm{y}\;\mathrm{u}=\mathrm{tay}$ where ${\varSigma}^{\ast}\models {\mathrm{Tally}}_{\mathrm{b}}(\mathrm{t})$ . Let $\mathrm{t}={\mathrm{b}}^{\mathrm{n}}$ . If $\mathrm{n}=1$ , we are done, for we can let ${\varSigma}^{\ast}\models {\mathrm{u}}_1=\mathrm{y}$ .

Suppose $\mathrm{n}>1$ . We claim that if ${\varSigma}^{\ast}\models \mathrm{u}={\mathrm{b}}^{\mathrm{n}}\mathrm{ay}$ , then ${\varSigma}^{\ast}\models \alpha (\mathrm{y})+\beta (\mathrm{y})\ge \underline {\mathrm{n}}$ .

We have that

$$\begin{align*}{\varSigma}^{\ast}\models \alpha (\mathrm{u})=\alpha ({\mathrm{b}}^{\mathrm{n}}\mathrm{ay})=\underline{1}+\alpha (\mathrm{y})\kern0.24em \mathrm{and}\;{\varSigma}^{\ast}\models \beta (\mathrm{u})=\beta ({\mathrm{b}}^{\mathrm{n}}\mathrm{ay})=\underline {\mathrm{n}}+\beta (\mathrm{y}).\end{align*}$$

From , we have ${\varSigma}^{\ast}\models \alpha (\mathrm{u})=\beta (\mathrm{u})+\underline{1}$ .

Then ${\varSigma}^{\ast}\models \underline{1}+\alpha (\mathrm{y})=\mathrm{n}+\beta (\mathrm{y})+1$ . So ${\varSigma}^{\ast}\models \alpha (\mathrm{y})=\beta (\mathrm{y})+\underline {\mathrm{n}}\ge \underline {\mathrm{n}}$ . But then ${\varSigma}^{\ast}\models \alpha (\mathrm{y})+\beta (\mathrm{y})\ge \underline {\mathrm{n}}+\beta (\mathrm{y})\ge \underline {\mathrm{n}}$ , which proves the claim.

Now let ${\varSigma}^{\ast}\models \alpha (\mathrm{y})+\beta (\mathrm{y})=\underline {\mathrm{k}}\ge \underline {\mathrm{n}}$ . By 2.1 we have that

$$\begin{align*}{\varSigma}^{\ast}\models \exists {\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{k}}(\wedge_{1\le \mathrm{i}\le \mathrm{k}}\mathrm{Digit}({\mathrm{y}}_{\mathrm{i}})\ \&\ \mathrm{y}={\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{k}}).\end{align*}$$

If $\mathrm{k}=\mathrm{n}$ , we are done. If $\mathrm{k}>\mathrm{n}$ , then ${\varSigma}^{\ast}\models \exists \mathrm{z}\;\mathrm{y}={\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}\mathrm{z}={\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}-1}({\mathrm{y}}_{\mathrm{n}}\mathrm{z})$ .

But then ${\varSigma}^{\ast}\models \mathrm{u}={\mathrm{b}}^{\mathrm{n}}\mathrm{ay}={\mathrm{b}}^{\mathrm{n}}{\mathrm{au}}_1\dots {\mathrm{u}}_{\mathrm{n}}$ where ${\varSigma}^{\ast }{\models}\wedge_{1\le \mathrm{i}<\mathrm{n}}\;{\mathrm{u}}_{\mathrm{i}}={\mathrm{y}}_{\mathrm{i}}\ \&\ {\mathrm{u}}_{\mathrm{n}}={\mathrm{y}}_{\mathrm{n}}\mathrm{z}$ .

2.7

For any $\mathrm{n}\ge 1$ , .

Proof Assume , and let ${\varSigma}^{\ast}\models \mathrm{y}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}$ . Then

$$\begin{align*} \begin{array}{l}{\varSigma}^{\ast}\models \alpha (\mathrm{y})=\alpha ({\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}})=\underline{1}+{\sum}_{1\le \mathrm{i}\le \mathrm{n}}\alpha ({\mathrm{x}}_{\mathrm{i}})=\underline{1}+{\sum}_{1\le \mathrm{i}\le \mathrm{n}}(\beta ({\mathrm{x}}_{\mathrm{i}})+\underline{1})=\\ {}\kern0.84em =\underline{1}+\underline {\mathrm{n}}+{\sum}_{1\le \mathrm{i}\le \mathrm{n}}\beta ({\mathrm{x}}_{\mathrm{i}})=\beta ({\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}})+\underline{1}=\beta (\mathrm{y})+\underline{1}.\end{array}\end{align*}$$

Hence (ci) holds. Suppose now that ${\varSigma}^{\ast}\models \mathrm{wBy}$ . We have that

$$\begin{align*} \begin{array}{l}{\varSigma}^{\ast}\models \mathrm{y}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}\ \&\ \mathrm{w}\mathrm{By}\to {\mathrm{wBb}}^{\mathrm{n}}\;\mathrm{v}\;\mathrm{w}={\mathrm{b}}^{\mathrm{n}}\;\mathrm{v}\;\mathrm{w}={\mathrm{b}}^{\mathrm{n}}\mathrm{a}\;\mathrm{v}\\[2pt] \hspace{9pt}\qquad\qquad{}\mathrm{v}\;(\exists {\mathrm{z}}_1({\mathrm{z}}_1{\mathrm{Bx}}_1\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{n}}{\mathrm{az}}_1)\;\mathrm{v}\kern0.24em \mathrm{w}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1)\;\mathrm{v}\\[2pt] \hspace{-9pt}\mathrm{v}\;{\vee}_{1<\mathrm{i}<\mathrm{n}}(\exists {\mathrm{z}}_{\mathrm{i}}({\mathrm{z}}_{\mathrm{i}}{\mathrm{Bx}}_{\mathrm{i}}\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}-1}{\mathrm{z}}_{\mathrm{i}})\;\mathrm{v}\;\mathrm{w}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}})\;\mathrm{v}\\[2pt] \qquad\qquad\qquad\qquad\quad\qquad{}\mathrm{v}\;\exists {\mathrm{z}}_{\mathrm{n}}({\mathrm{z}}_{\mathrm{n}}{\mathrm{Bx}}_{\mathrm{n}}\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-1}{\mathrm{z}}_{\mathrm{n}}).\end{array}\end{align*}$$

We consider one of the cases as an illustration of the proof. Suppose

$$\begin{align*}{\varSigma}^{\ast}\models \exists {\mathrm{z}}_{\mathrm{i}}({\mathrm{z}}_{\mathrm{i}}{\mathrm{Bx}}_{\mathrm{i}}\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}-1}{\mathrm{z}}_{\mathrm{i}})\kern0.36em \mathrm{where}\kern0.36em 1<\mathrm{i}<\mathrm{n}.\end{align*}$$

From we have ${\varSigma}^{\ast }{\models}\wedge_{1\le \mathrm{j}<\mathrm{i}}\alpha ({\mathrm{x}}_{\mathrm{j}})=\beta ({\mathrm{x}}_{\mathrm{j}})+\underline{1}$ . On the other hand, from , we have ${\varSigma}^{\ast}\models \alpha ({\mathrm{z}}_{\mathrm{i}})\le \beta ({\mathrm{z}}_{\mathrm{i}})$ . Then

$$\begin{align*} \begin{array}{l}\hspace{-8pt}{\varSigma}^{\ast}\models \alpha (\mathrm{w})=\alpha ({\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}-1}{\mathrm{z}}_{\mathrm{i}})=\underline{1}+{\sum}_{1\le \mathrm{j}<\mathrm{i}}\alpha ({\mathrm{x}}_{\mathrm{j}})+\alpha ({\mathrm{z}}_{\mathrm{i}})=\\ {}\hspace{45pt} =\underline{1}+{\sum}_{1\le \mathrm{j}<\mathrm{i}}(\beta ({\mathrm{x}}_{\mathrm{j}})+\underline{1})+\alpha ({\mathrm{z}}_{\mathrm{i}})\le {\sum}_{1\le \mathrm{j}<\mathrm{i}}\beta ({\mathrm{x}}_{\mathrm{j}})+\underline {\mathrm{i}}+\beta ({\mathrm{z}}_{\mathrm{i}})\le \\ {}\hspace{45pt} \le \underline {\mathrm{n}}+{\sum}_{1\le \mathrm{j}<\mathrm{i}}\beta ({\mathrm{x}}_{\mathrm{j}})+\beta ({\mathrm{z}}_{\mathrm{i}})=\beta ({\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}-1}{\mathrm{z}}_{\mathrm{i}})=\beta (\mathrm{w}),\end{array}\end{align*}$$

as required. Detailed consideration of the cases shows that ${\varSigma}^{\ast}\models \forall \mathrm{w}\;(\mathrm{w}\mathrm{By}\to \alpha (\mathrm{w})\le \beta (\mathrm{w}))$ . This establishes (cii), and so .

It will be useful to have a sharpened form of this result. For $\mathrm{m}\ge 1$ , let

that is, the almost even string $\mathrm{x}$ contains no $\mathrm{b}$ -tallies of length $>\mathrm{m}$ . Clearly, we have:

2.8

(a) For any $\mathrm{m}\ge 1$ , .

(b) For each $\mathrm{m}\ge 1$ , .

(c) If $\mathrm{m}\le \mathrm{n}$ , then .

We can then restate 2.7 as follows:

2.9

For any $\mathrm{m}(1),\dots, \mathrm{m}(\mathrm{n})\ge 1$ , , where $\mathrm{k}=\max (\mathrm{n},\mathrm{m}(1),\dots, \mathrm{m}(\mathrm{n}))$ .

We omit the proof, which is straightforward.

2.10

For each $\mathrm{n}\ge 1$ , ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}={\mathrm{x}}_1\mathrm{aa}\to {\mathrm{x}}_1={\mathrm{b}}^{\mathrm{n}}\;\mathrm{v}\;{\mathrm{b}}^{\mathrm{n}}{\mathrm{Bx}}_1$ .

Proof We have from ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}=\mathrm{z}={\mathrm{x}}_1\mathrm{aa}$ that ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}\mathrm{Bz}\ \& {\mathrm{x}}_1\mathrm{Bz}$ . Then ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{Bx}}_1\mathrm{v}\;{\mathrm{b}}^{\mathrm{n}}={\mathrm{x}}_1\;\mathrm{v}\;{\mathrm{x}}_1{\mathrm{Bb}}^{\mathrm{n}}$ . Suppose, for a reductio, that ${\varSigma}^{\ast}\models {\mathrm{x}}_1{\mathrm{Bb}}^{\mathrm{n}}$ . Then ${\varSigma}^{\ast}\models \exists {\mathrm{z}}_1{\mathrm{b}}^{\mathrm{n}}={\mathrm{x}}_1{\mathrm{z}}_1$ where ${\varSigma}^{\ast}\models {\mathrm{Tally}}_{\mathrm{b}}({\mathrm{z}}_1)$ . But then ${\varSigma}^{\ast}\models ({\mathrm{x}}_1{\mathrm{z}}_1){\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}={\mathrm{x}}_1\mathrm{aa}$ , that is, ${\varSigma}^{\ast}\models {\mathrm{x}}_1({\mathrm{z}}_1{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}})={\mathrm{x}}_1\mathrm{aa}$ , whence ${\varSigma}^{\ast}\models {\mathrm{z}}_1{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}=\mathrm{aa}$ , which is a contradiction because ${\varSigma}^{\ast}\models {\mathrm{Tally}}_{\mathrm{b}}({\mathrm{z}}_1)$ . Therefore, ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{Bx}}_1\mathrm{v}\kern0.24em {\mathrm{b}}^{\mathrm{n}}={\mathrm{x}}_1$ .

Now, 2.7 tells us that strings are closed under the operation of prefixing a juxtaposition of $\mathrm{n}$ such strings with a $\mathrm{b}$ -tally of length $\mathrm{n}$ followed by a single occurrence of digit $\mathrm{a}$ . On the other hand, 2.4 tells us that the juxtaposed strings are uniquely recoverable from the resulting string. Along with 2.6, all this suggests that the strings may be inductively characterized as the smallest set of strings that contains the single digit a and is closed under the $\mathrm{n}$ -ary juxtaposition operations of the type just described, and that each string has a unique decomposition. That is exactly what we’ll do now.

Theorem 2.11 (Unique decomposition of strings). Let $\mathrm{u}$ be any closed ${{\mathcal{L}}}_{\mathrm{C}}$ -term. If , then for some $\mathrm{n}\ge 1$ ,

Proof Assume . By 2.6 we have that ${\varSigma}^{\ast}\models \exists {\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}\mathrm{u}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ . We need to show that there are unique strings ${\mathrm{u}}_1,\dots, {\mathrm{u}}_{\mathrm{n}}$ such that ${\varSigma}^{\ast}\models {\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{n}}={\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ .

If $\mathrm{n}=1$ , then ${\varSigma}^{\ast}\models \mathrm{u}=\mathrm{bay}$ . From hypothesis we have by 2.5(b) that . So we may let ${\mathrm{u}}_1=\mathrm{y}$ . Uniqueness is immediate.

So we may assume that $\mathrm{n}\ge 2$ . By 2.2, from we have that ${\varSigma}^{\ast}\models \mathrm{aaEu}$ . Hence ${\varSigma}^{\ast}\models \exists {\mathrm{x}}_1\mathrm{u}={\mathrm{x}}_1\mathrm{aa}$ . By 2.10, we have that ${\varSigma}^{\ast}\models {\mathrm{x}}_1={\mathrm{b}}^{\mathrm{n}}\;\mathrm{v}\;{\mathrm{b}}^{\mathrm{n}}{\mathrm{Bx}}_1$ . Now, we cannot have ${\varSigma}^{\ast}\models {\mathrm{x}}_1={\mathrm{b}}^{\mathrm{n}}$ , for then ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}={\mathrm{b}}^{\mathrm{n}}\mathrm{aa}$ , whence ${\varSigma}^{\ast}\models {\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}=\mathrm{a}$ , which is impossible given that $\mathrm{n}\ge 2$ . Therefore, ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{Bx}}_1$ . Then ${\varSigma}^{\ast}\models \exists {\mathrm{x}}_2{\mathrm{x}}_1={\mathrm{b}}^{\mathrm{n}}{\mathrm{x}}_2$ , whence

$$\begin{align*}{\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}=\mathrm{u}={\mathrm{x}}_1\mathrm{aa}=({\mathrm{b}}^{\mathrm{n}}{\mathrm{x}}_2)\mathrm{aa}={\mathrm{b}}^{\mathrm{n}}({\mathrm{x}}_2\mathrm{aa}).\end{align*}$$

Then ${\varSigma}^{\ast}\models {\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}={\mathrm{x}}_2\mathrm{aa}$ , and further, ${\varSigma}^{\ast}\models {\mathrm{x}}_2=\mathrm{a}\;\mathrm{v}\;{\mathrm{aBx}}_2$ .

If ${\varSigma}^{\ast}\models {\mathrm{x}}_2=\mathrm{a}$ , then ${\varSigma}^{\ast}\models {\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}=\mathrm{aaa}$ , so ${\varSigma}^{\ast}\models {\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}=\mathrm{aa}$ . But then $\mathrm{n}=2$ and ${\varSigma}^{\ast}\models {\mathrm{y}}_1={\mathrm{y}}_2=\mathrm{a}$ . If we let ${\mathrm{u}}_1={\mathrm{u}}_2=\mathrm{a}$ we have that and uniqueness is immediate. In this case we are done. So we may assume that ${\varSigma}^{\ast}\models {\mathrm{aBx}}_2$ . Then ${\varSigma}^{\ast}\models \exists {\mathrm{x}}_3{\mathrm{x}}_2={\mathrm{ax}}_3$ , that is, ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}=\mathrm{u}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_3\mathrm{aa}$ . Thus ${\varSigma}^{\ast}\models {\mathrm{x}}_3\mathrm{aaEu}$ , and from , by 2.3(b), we have that ${\varSigma}^{\ast}\models \alpha ({\mathrm{x}}_3\mathrm{aa})\ge \beta ({\mathrm{x}}_3\mathrm{aa})+\underline{1}$ . Then ${\mathrm{x}}_3\mathrm{aa}$ has at least one initial segment $\mathrm{v}$ , namely itself, such that ${\varSigma}^{\ast}\models \alpha (\mathrm{v})\ge \beta (\mathrm{v})+\underline{1}$ . Let ${\mathrm{u}}_1$ be the shortest such initial segment of ${\mathrm{x}}_3\mathrm{aa}$ .

Claim 1. .

By choice of ${\mathrm{u}}_1$ we have that ${\varSigma}^{\ast}\models \alpha ({\mathrm{u}}_1)\ge \beta ({\mathrm{u}}_1)+1$ . We may assume that ${\varSigma}^{\ast}\models {\mathrm{u}}_1\ne \mathrm{a}$ ; otherwise, we are done. Suppose, for a reductio, that ${\varSigma}^{\ast}\models \alpha ({\mathrm{u}}_1)>\beta ({\mathrm{u}}_1)+\underline{1}$ . Then ${\varSigma}^{\ast}\models {\mathrm{u}}_1\ne \mathrm{b}$ .

Suppose that ${\varSigma}^{\ast}\models {\mathrm{aEu}}_1$ . Then ${\varSigma}^{\ast}\models \exists \mathrm{z}\;{\mathrm{u}}_1=\mathrm{za}$ . Then from hypothesis ${\varSigma}^{\ast}\models \alpha ({\mathrm{u}}_1)>\beta ({\mathrm{u}}_1)+\underline{1}$ , we obtain ${\varSigma}^{\ast}\models \alpha (\mathrm{z})=\alpha ({\mathrm{u}}_1)\hbox{--} \underline{1}>\beta ({\mathrm{u}}_1)=\beta (\mathrm{z})$ , so ${\varSigma}^{\ast}\models \alpha (\mathrm{z})\ge \beta (\mathrm{z})+\underline{1}$ . Since ${\varSigma}^{\ast}\models {\mathrm{zBu}}_1\ \&\ ({\mathrm{u}}_1{\mathrm{Bx}}_3\mathrm{aa}\;\mathrm{v}\;{\mathrm{u}}_1={\mathrm{x}}_3\mathrm{aa})$ , we have that ${\varSigma}^{\ast}\models {\mathrm{zBx}}_3\mathrm{aa}$ . But this contradicts the choice of ${\mathrm{u}}_1$ . Hence ${\varSigma}^{\ast}\models \neg {\mathrm{aEu}}_1$ .

Suppose that ${\varSigma}^{\ast}\models {\mathrm{bEu}}_1$ . Then ${\varSigma}^{\ast}\models \exists \mathrm{z}\;{\mathrm{u}}_1=\mathrm{zb}$ ; hence

$$\begin{align*}{\varSigma}^{\ast}\models \alpha (\mathrm{z})=\alpha (\mathrm{z}\mathrm{b})=\alpha ({\mathrm{u}}_1)\ge \beta ({\mathrm{u}}_1)+\underline{1}=\beta (\mathrm{z}\mathrm{b})+\underline{1}>\beta (\mathrm{z})+\underline{1},\end{align*}$$

where ${\varSigma}^{\ast}\models {\mathrm{zBu}}_1\ \&\ ({\mathrm{u}}_1{\mathrm{Bx}}_3\mathrm{aa}\;\mathrm{v}\;{\mathrm{u}}_1={\mathrm{x}}_3\mathrm{aa})$ . So ${\varSigma}^{\ast}\models {\mathrm{zBx}}_3\mathrm{aa}$ , again contradicting the choice of ${\mathrm{u}}_1$ . Hence also ${\varSigma}^{\ast}\models \neg {\mathrm{bEu}}_1$ .

But then we have that ${\varSigma}^{\ast}\models {\mathrm{u}}_1\ne \mathrm{a}\ \&\ {\mathrm{u}}_1\ne \mathrm{b}\ \&\ \neg {\mathrm{aEu}}_1\ \&\ \neg {\mathrm{bEu}}_1$ , which is impossible. Therefore ${\varSigma}^{\ast}\models \alpha ({\mathrm{u}}_1)=\beta ({\mathrm{u}}_1)+\underline{1}$ . By choice of ${\mathrm{u}}_1$ it follows also that ${\varSigma}^{\ast}\models \forall \mathrm{w}\;({\mathrm{wBu}}_1\to \alpha (\mathrm{w})\le \beta (\mathrm{w}))$ . This completes the proof of Claim 1.

We have that ${\varSigma}^{\ast}\models {\mathrm{u}}_1{\mathrm{Bx}}_3\mathrm{aa}\;\mathrm{v}\;{\mathrm{u}}_1={\mathrm{x}}_3\mathrm{aa}$ .

If ${\varSigma}^{\ast}\models {\mathrm{u}}_1={\mathrm{x}}_3\mathrm{aa}$ , then ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{au}}_1={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_3\mathrm{aa}=\mathrm{u}$ . Since , we then have ${\varSigma}^{\ast}\models \alpha (\mathrm{u})=\alpha ({\mathrm{b}}^{\mathrm{n}}{\mathrm{au}}_1)=\underline{1}+\alpha ({\mathrm{u}}_1)=\underline{1}+(\beta ({\mathrm{u}}_1)+\underline{1})=\beta ({\mathrm{u}}_1)+\underline{2}$ , whereas ${\varSigma}^{\ast}\models \beta (\mathrm{u})=\beta ({\mathrm{b}}^{\mathrm{n}}{\mathrm{au}}_1)=\underline {\mathrm{n}}+\beta ({\mathrm{u}}_1)$ . But from hypothesis we have ${\varSigma}^{\ast}\models \alpha (\mathrm{u})=\beta (\mathrm{u})+1$ . Hence ${\varSigma}^{\ast}\models \beta ({\mathrm{u}}_1)+\underline{2}=\beta ({\mathrm{u}}_1)+\underline {\mathrm{n}}+\underline{1}$ , contradicting hypothesis $\mathrm{n}\ge 2$ . Therefore ${\varSigma}^{\ast}\models {\mathrm{u}}_1\ne {\mathrm{x}}_3\mathrm{aa}$ . But then it follows that ${\varSigma}^{\ast}\models {\mathrm{u}}_1{\mathrm{Bx}}_3\mathrm{aa}$ . So ${\varSigma}^{\ast}\models \exists {\mathrm{v}}_1{\mathrm{x}}_3\mathrm{aa}={\mathrm{u}}_1{\mathrm{v}}_1$ , whence ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{au}}_1{\mathrm{v}}_1={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_3\mathrm{aa}=\mathrm{u}$ , which means that ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{au}}_1\mathrm{Bu}$ .

Claim 2. For each $\mathrm{i}$ , $1\le \mathrm{i}<\mathrm{n}$ ,

Assume that ${\mathrm{v}}_1,\dots, {\mathrm{v}}_{\mathrm{i}}$ have been picked such that

Then ${\varSigma}^{\ast}\models \exists {\mathrm{w}}_{\mathrm{i}}\;\mathrm{u}={\mathrm{b}}^{\mathrm{n}}{\mathrm{av}}_1\dots {\mathrm{v}}_{\mathrm{i}}{\mathrm{w}}_{\mathrm{i}}$ ; hence ${\varSigma}^{\ast}\models {\mathrm{w}}_{\mathrm{i}}\mathrm{Eu}$ . From hypothesis by 2.3(b) we then have that ${\varSigma}^{\ast}\models \alpha ({\mathrm{w}}_{\mathrm{i}})\ge \beta ({\mathrm{w}}_{\mathrm{i}})+\underline{1}$ . Then we have

$$\begin{align*} \begin{array}{l}\hspace{-5pt}{\varSigma}^{\ast}\models \alpha (\mathrm{u})=\alpha ({\mathrm{b}}^{\mathrm{n}}{\mathrm{av}}_1\dots {\mathrm{v}}_{\mathrm{i}}{\mathrm{w}}_{\mathrm{i}})=\underline{1}+\alpha ({\mathrm{v}}_1\dots {\mathrm{v}}_{\mathrm{i}})+\alpha ({\mathrm{w}}_{\mathrm{i}})=\\ {}\hspace{40pt}=\underline{1}+{\sum}_{1\le \mathrm{j}\le \mathrm{i}}\alpha ({\mathrm{v}}_{\mathrm{j}})+\alpha ({\mathrm{w}}_{\mathrm{i}})=\underline{1}+{\sum}_{1\le \mathrm{j}\le \mathrm{i}}(\beta ({\mathrm{v}}_{\mathrm{j}})+\underline{1})+\alpha ({\mathrm{w}}_{\mathrm{i}})=\\ \hspace{40pt} =\underline{1}+\underline {\mathrm{i}}+{\sum}_{1\le \mathrm{j}\le \mathrm{i}}\beta ({\mathrm{v}}_{\mathrm{j}})+\alpha ({\mathrm{w}}_{\mathrm{i}}),\end{array}\end{align*}$$

whereas ${\begin{array}{l}{\varSigma}^{\ast}\models \beta (\mathrm{u})=\beta ({\mathrm{b}}^{\mathrm{n}}{\mathrm{av}}_1\dots {\mathrm{v}}_{\mathrm{i}}{\mathrm{w}}_{\mathrm{i}})=\underline {\mathrm{n}}+\beta ({\mathrm{v}}_1\dots {\mathrm{v}}_{\mathrm{i}})+\beta ({\mathrm{w}}_{\mathrm{i}})=\\ \quad\qquad\qquad\qquad\qquad\qquad\hspace{20pt} =\underline {\mathrm{n}}+{\sum}_{1\le \mathrm{j}\le \mathrm{i}}\beta ({\mathrm{v}}_{\mathrm{j}})+\beta ({\mathrm{w}}_{\mathrm{i}}).\end{array}}$

But from hypothesis we have ${\varSigma}^{\ast}\models \alpha (\mathrm{u})=\beta (\mathrm{u})+\underline{1}$ . Then ${\varSigma}^{\ast}\models \underline{1}+\underline {\mathrm{i}}+{\sum}_{1\le \mathrm{j}\le \mathrm{i}}\beta ({\mathrm{v}}_{\mathrm{j}})+\alpha ({\mathrm{w}}_{\mathrm{i}})=\underline {\mathrm{n}}+{\sum}_{1\le \mathrm{j}\le \mathrm{i}}\beta ({\mathrm{v}}_{\mathrm{j}})+\beta ({\mathrm{w}}_{\mathrm{i}})+\underline{1}$ , whence

(#) $$\begin{align}\qquad\qquad\quad{\varSigma}^{\ast}\models \underline {\mathrm{i}}+\alpha ({\mathrm{w}}_{\mathrm{i}})=\underline {\mathrm{n}}+\beta ({\mathrm{w}}_{\mathrm{i}}).\end{align}$$

We pick ${\mathrm{v}}_{\mathrm{i}+1}$ as follows: if ${\varSigma}^{\ast}\models {\mathrm{w}}_{\mathrm{i}}=\mathrm{a}$ , we let ${\mathrm{v}}_{\mathrm{i}+1}=\mathrm{a}$ ; if ${\varSigma}^{\ast}\models {\mathrm{w}}_{\mathrm{i}}\ne \mathrm{a}$ , let ${\mathrm{v}}_{\mathrm{i}+1}$ be the shortest initial segment $\mathrm{v}$ of ${\mathrm{w}}_{\mathrm{i}}$ such that ${\varSigma}^{\ast}\models \alpha (\mathrm{v})\ge \beta (\mathrm{v})+\underline{1}$ .

If ${\varSigma}^{\ast}\models {\mathrm{w}}_{\mathrm{i}}=\mathrm{a}$ , then ${\varSigma}^{\ast}\models \mathrm{u}={\mathrm{b}}^{\mathrm{n}}{\mathrm{av}}_1\dots {\mathrm{v}}_{\mathrm{i}}{\mathrm{w}}_{\mathrm{i}}={\mathrm{b}}^{\mathrm{n}}{\mathrm{av}}_1\dots {\mathrm{v}}_{\mathrm{i}}\mathrm{a}$ , and we of course have that . Since ${\varSigma}^{\ast}\models {\mathrm{w}}_{\mathrm{i}}=\mathrm{a}$ , we have ${\varSigma}^{\ast}\models \alpha ({\mathrm{w}}_{\mathrm{i}})=\underline{1}\ \&\ \beta ({\mathrm{w}}_{\mathrm{i}})=\underline{0}$ , so from $(\#)$ we obtain ${\varSigma}^{\ast}\models \underline {\mathrm{i}}+\underline{1}=\underline {\mathrm{n}}$ .

If ${\varSigma}^{\ast}\models {\mathrm{w}}_{\mathrm{i}}\ne \mathrm{a}$ , then the same argument as in Claim 1 with ${\mathrm{v}}_{\mathrm{i}+1}$ in place of ${\mathrm{u}}_1$ and ${\mathrm{w}}_{\mathrm{i}}$ in place of ${\mathrm{x}}_3\mathrm{aa}$ shows that ${\varSigma}^{\ast}\models \alpha ({\mathrm{v}}_{\mathrm{i}+1})=\beta ({\mathrm{v}}_{\mathrm{i}+1})+\underline{1}$ , and that . By choice of ${\mathrm{v}}_{\mathrm{i}+1}$ we have that ${\varSigma}^{\ast}\models {\mathrm{v}}_{\mathrm{i}+1}={\mathrm{w}}_{\mathrm{i}}\;\mathrm{v}\;{\mathrm{v}}_{\mathrm{i}+1}{\mathrm{Bw}}_{\mathrm{i}}$ .

If ${\varSigma}^{\ast}\models {\mathrm{v}}_{\mathrm{i}+1}={\mathrm{w}}_{\mathrm{i}}$ , then ${\varSigma}^{\ast}\models \mathrm{u}={\mathrm{b}}^{\mathrm{n}}{\mathrm{av}}_1\dots {\mathrm{v}}_{\mathrm{i}}{\mathrm{w}}_{\mathrm{i}}={\mathrm{b}}^{\mathrm{n}}{\mathrm{av}}_1\dots {\mathrm{v}}_{\mathrm{i}}{\mathrm{v}}_{\mathrm{i}+1}$ . Then ${\varSigma}^{\ast}\models \alpha ({\mathrm{w}}_{\mathrm{i}})=\beta ({\mathrm{w}}_{\mathrm{i}})+\underline{1}$ , so from $(\#)$ we obtain

${\varSigma}^{\ast}\models \underline {\mathrm{i}}+\beta ({\mathrm{w}}_{\mathrm{i}})+\underline{1}=\underline {\mathrm{n}}+\beta ({\mathrm{w}}_{\mathrm{i}})$ , whence ${\varSigma}^{\ast}\models \underline {\mathrm{i}}+\underline{1}=\underline {\mathrm{n}}$ .

If ${\varSigma}^{\ast}\models {\mathrm{v}}_{\mathrm{i}+1}{\mathrm{Bw}}_{\mathrm{i}}$ , then ${\varSigma}^{\ast}\models \exists {\mathrm{w}}_{\mathrm{i}+1}{\mathrm{w}}_{\mathrm{i}}={\mathrm{v}}_{\mathrm{i}+1}{\mathrm{w}}_{\mathrm{i}+1}$ . So

$$\begin{align*}{\varSigma}^{\ast}\models \mathrm{u}={\mathrm{b}}^{\mathrm{n}}{\mathrm{av}}_1\dots {\mathrm{v}}_{\mathrm{i}}{\mathrm{w}}_{\mathrm{i}}={\mathrm{b}}^{\mathrm{n}}{\mathrm{av}}_1\dots {\mathrm{v}}_{\mathrm{i}}({\mathrm{v}}_{\mathrm{i}+1}{\mathrm{w}}_{\mathrm{i}+1}).\end{align*}$$

Then we have that

$$\begin{align*}{\varSigma}^{\ast}\models \alpha ({\mathrm{w}}_{\mathrm{i}})=\alpha ({\mathrm{v}}_{\mathrm{i}+1}{\mathrm{w}}_{\mathrm{i}+1})=\alpha ({\mathrm{v}}_{\mathrm{i}+1})+\alpha ({\mathrm{w}}_{\mathrm{i}+1})=\beta ({\mathrm{v}}_{\mathrm{i}+1})+\underline{1}+\alpha ({\mathrm{w}}_{\mathrm{i}+1})\end{align*}$$

and $\beta ({\mathrm{w}}_{\mathrm{i}})=\beta ({\mathrm{v}}_{\mathrm{i}+1}{\mathrm{w}}_{\mathrm{i}+1})=\beta ({\mathrm{v}}_{\mathrm{i}+1})+\beta ({\mathrm{w}}_{\mathrm{i}+1})$ . Hence from $(\#)$ we obtain ${\varSigma}^{\ast}\models \underline {\mathrm{i}}+\beta ({\mathrm{v}}_{\mathrm{i}+1})+\underline{1}+\alpha ({\mathrm{w}}_{\mathrm{i}+1})=\underline {\mathrm{n}}+\beta ({\mathrm{v}}_{\mathrm{i}+1})+\beta ({\mathrm{w}}_{\mathrm{i}+1})$ . But ${\varSigma}^{\ast}\models {\mathrm{w}}_{\mathrm{i}+1}\mathrm{Eu}$ , so from by 2.3(b), we have ${\varSigma}^{\ast}\models \alpha ({\mathrm{w}}_{\mathrm{i}+1})\ge \beta ({\mathrm{w}}_{\mathrm{i}+1})+\underline{1}>\beta ({\mathrm{w}}_{\mathrm{i}+1})$ . But then ${\varSigma}^{\ast}\models \underline {\mathrm{i}}+\underline{1}<\mathrm{n}\ \&\ ({\mathrm{b}}^{\mathrm{n}}{\mathrm{av}}_1\dots {\mathrm{v}}_{\mathrm{i}}{\mathrm{v}}_{\mathrm{i}+1})\mathrm{Bu}$ .

This completes the proof of Claim 2.

From Claim 1 and $\mathrm{n}\hbox{--} 1$ applications of Claim 2 we obtain strings ${\mathrm{u}}_1,\dots, {\mathrm{u}}_{\mathrm{n}}$ such that . Hence ${\varSigma}^{\ast}\models {\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}={\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{n}}$ . Then uniqueness follows from 2.4.

Theorem 2.12. Let $\mathrm{u}$ be any closed ${{\mathcal{L}}}_{\mathrm{C}}$ -term.

For each $\mathrm{m}\ge 1$ , if , then for some $\mathrm{n}$ , $1\le \mathrm{n}\le \mathrm{m}$ ,

Proof Assume . Then . We proceed exactly as in the proof of Theorem 2.11. If ${\varSigma}^{\ast}\models \mathrm{u}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ we have that $\mathrm{n}\le \mathrm{m}$ . If $\mathrm{n}=1$ and ${\varSigma}^{\ast}\models {\mathrm{u}}_1=\mathrm{a}$ , then , and if $\mathrm{n}=2$ and ${\varSigma}^{\ast}\models {\mathrm{u}}_1={\mathrm{u}}_2=\mathrm{a}$ , then and so . In the general case, once we reach the end of the proof of Theorem 2.11, since ${\varSigma}^{\ast}\models {\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}={\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{n}}$ we have that ${\varSigma}^{\ast }{\models }\wedge_{1\le \mathrm{i}\le \mathrm{n}}{\mathrm{u}}_{\mathrm{i}}{\subseteq}_{\mathrm{p}}\mathrm{u}$ . But then from the principal hypothesis it follows that as claimed.

Remark. If we let

we have:

2.13

(a)

(b) For each $\mathrm{m}\ge 1$ , .

(c) If $\mathrm{m}\ne \mathrm{n}$ , then .

We omit the proof.

2.14

Let $\mathrm{u}$ be any closed ${{\mathcal{L}}}_{\mathrm{C}}$ -term. For each $\mathrm{m}\ge 1$ , if , then ${\varSigma}^{\ast}\models \exists {\mathrm{x}}_1\dots {\mathrm{x}}_{\mathrm{m}}\mathrm{u}={\mathrm{b}}^{\mathrm{m}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{m}}$ .

Proof Assume . Then , and by 2.6 we have that, for some $\mathrm{n}\ge 1$ , ${\varSigma}^{\ast}\models \exists {\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{n}}\mathrm{u}={\mathrm{b}}^{\mathrm{n}}{\mathrm{au}}_1\dots {\mathrm{u}}_{\mathrm{n}}$ . Then ${\varSigma}^{\ast}\models {\mathrm{Tally}}_{\mathrm{b}}({\mathrm{b}}^{\mathrm{n}})\ \&\ {\mathrm{b}}^{\mathrm{n}}\mathrm{aBu}$ , so from we have ${\varSigma}^{\ast}\models {\mathrm{b}}^{\mathrm{n}}={\mathrm{b}}^{\mathrm{m}}$ , whence $\mathrm{n}=\mathrm{m}$ . But then we may take ${\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{m}}$ to be ${\mathrm{u}}_1,\dots, {\mathrm{u}}_{\mathrm{n}}$ .

2.15

(a) For each $\mathrm{m}\ge 1$ ,

(b) Let $\mathrm{u}$ be any closed ${{\mathcal{L}}}_{\mathrm{C}}$ -term. For each $\mathrm{m}\ge 1$ , if , then .

These are proved analogously to 2.9 and Theorem 2.12 with appropriate modifications.

The inductive characterization of strings given in 2.9 and Theorem 2.12 opens up the possibility of defining operations by recursion with respect to the corresponding generating relations for strings. In Section 4 we will need to employ operations $\mathrm{f}$ of that type, satisfying, e.g., the schema

$$\begin{align*}\mathrm{f}(\mathrm{a})=\mathrm{p}\quad \mathrm{f}({\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}})={\mathrm{g}}_{\mathrm{k}}(\mathrm{f}({\mathrm{x}}_1),\dots, \mathrm{f}({\mathrm{x}}_{\mathrm{k}}))\;\mathrm{for}\;\mathrm{any}\;\mathrm{k},1\le \mathrm{k}\le \mathrm{n},\end{align*}$$

where $\mathrm{p}$ is a fixed string and ${\mathrm{g}}_{\mathrm{k}}$ some given $\mathrm{k}$ -ary operations on strings taking values from for some fixed $\mathrm{m}$ .

Theorem 2.16 (Recursion on strings). Let $\mathrm{n}\ge 1$ , let $\mathrm{p}$ be a closed ${{\mathcal{L}}}_{\mathrm{C}}$ -term, and let ${\mathrm{G}}_{\mathrm{k}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{k}},\mathrm{y})$ be ${{\mathcal{L}}}_{\mathrm{C}}$ -formulae for $1\le \mathrm{k}\le \mathrm{n}$ . Let $\mathrm{m}\ge 1$ . Suppose that (a) , and

(b)

Then there is an ${{\mathcal{L}}}_{\mathrm{C}}$ -formula $\mathrm{F}(\mathrm{x},\mathrm{y})$ such that:

1. (i)

2. (ii) ${\varSigma}^{\ast}\models \forall \mathrm{y}\;(\mathrm{F}(\mathrm{a},\mathrm{y})\leftrightarrow \mathrm{y}=\mathrm{p})$ .

3. (iii) For each $\mathrm{k}$ , $1\le \mathrm{k}\le \mathrm{n}$ ,

$$\begin{align*} \begin{array}{l}{\varSigma}^{\ast}\models \forall {\mathrm{x}}_1\dots {\mathrm{x}}_{\mathrm{k}}\forall {\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{k}}\big({\wedge}_{1\le \mathrm{i}\le \mathrm{k}}\mathrm{F}({\mathrm{x}}_{\mathrm{i}},{\mathrm{y}}_{\mathrm{i}})\to \\ {}\to \forall \mathrm{x},\mathrm{z}\;(\mathrm{x}={\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}}\to (\mathrm{F}(\mathrm{x},\mathrm{z})\leftrightarrow {\mathrm{G}}_{\mathrm{k}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{k}},\mathrm{z})))\big).\end{array}\end{align*}$$

Proof We rely on the coding scheme for sequences of strings explained in [3, Section 4], and follow the notation used there. In particular, we have that ${\varSigma}^{\ast}\models \mathrm{Pair}[\mathrm{x},\mathrm{y},\mathrm{z}]$ iff string $\mathrm{z}$ codes the pair of strings $\mathrm{x}$ and $\mathrm{y}$ , ${\varSigma}^{\ast}\models \mathrm{Set}(\mathrm{x})$ iff $\mathrm{x}$ is a set code, and ${\varSigma}^{\ast}\models \mathrm{x}\;\varepsilon\;\mathrm{y}$ just in case string $\mathrm{x}$ is a member of the set coded by string $\mathrm{y}$ . Let ${\mathrm{R}}_{\mathrm{k}}{(}\mathrm{u},\mathrm{x})$ abbreviate the ${{\mathcal{L}}}_{\mathrm{C}}$ -formula

Let ${\mathrm{Comp}}_{\le \mathrm{n}}{(}\mathrm{u},\mathrm{x})$ abbreviate

Let ${\mathrm{MinComp}}_{\le \mathrm{n}}{(}\mathrm{u},\mathrm{x})$ abbreviate

We then let $\mathrm{F}(\mathrm{x},\mathrm{y})\equiv \exists \mathrm{u},\mathrm{w}({\mathrm{MinComp}}_{\le \mathrm{n}}(\mathrm{u},\mathrm{x})\ \&\ \mathrm{Pair}[\mathrm{x},\mathrm{y},\mathrm{w}]\ \&\ \mathrm{w}\;\varepsilon\;\mathrm{u}).$

Now, suppose (a) and (b) hold. For (i), assume that . We argue by induction on the generating relation of strings. If ${\varSigma}^{\ast}\models \mathrm{x}=\mathrm{a}$ , let ${\mathrm{w}}_0$ be the string such that ${\varSigma}^{\ast}\models \mathrm{Pair}[\mathrm{a},\mathrm{p},{\mathrm{w}}_0]$ , and let ${\mathrm{u}}_0$ be the string that codes the singleton sequence of ${\mathrm{w}}_0$ . Then the desired claim follows immediately from (a) and the definition of $\mathrm{F}(\mathrm{x},\mathrm{y})$ . Assume ${\varSigma}^{\ast}\models \mathrm{x}={\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}}$ where the claim holds for ${\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{k}}$ with $\mathrm{k}\le \mathrm{n}$ . Then

Let ${\mathrm{w}}_1,\dots, {\mathrm{w}}_{\mathrm{k}}$ be the strings such that ${\varSigma}^{\ast }{\models }\wedge_{1\le \mathrm{i}\le \mathrm{k}}\mathrm{Pair}[{\mathrm{x}}_{\mathrm{i}},{\mathrm{y}}_{\mathrm{i}},{\mathrm{w}}_{\mathrm{i}}]$ , and let $\mathrm{u}$ be the string that codes the sequence ${\mathrm{w}}_1,\dots, {\mathrm{w}}_{\mathrm{k}}$ . From (b) we have that . Pick the string $\mathrm{w}$ such that ${\varSigma}^{\ast}\models \mathrm{Pair}[{\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}},\mathrm{y},\mathrm{w}]$ , and let $\mathrm{u}'$ be the string that codes the sequence ${\mathrm{w}}_1,\dots, {\mathrm{w}}_{\mathrm{k}},\mathrm{w}$ . Then the claim follows immediately from the definition of $\mathrm{F}(\mathrm{x},\mathrm{y})$ . (ii) and (iii) follow straightforwardly from the definition of $\mathrm{F}(\mathrm{x},\mathrm{y})$ and (i).

We say that the function whose graph is expressed by the formula $\mathrm{F}(\mathrm{x},\mathrm{y})$ is defined by recursion. If in the proof of Theorem 2.16 the formulae and ${\mathrm{G}}_{\mathrm{k}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{k}},\mathrm{y})$ for $1\le \mathrm{k}\le \mathrm{n}$ and , respectively, are replaced by and $\mathrm{G}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{k}},\mathrm{y})$ for $1\le \mathrm{k}\le \mathrm{n}$ and , respectively, we obtain:

Theorem 2.17 (Recursion on strings). Let $\mathrm{n}\ge 1$ , let $\mathrm{p}$ be a closed ${{\mathcal{L}}}_{\mathrm{C}}$ -term, and let $\mathrm{G}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{k}},\mathrm{y})$ be an ${{\mathcal{L}}}_{\mathrm{C}}$ -formula. Let $\mathrm{m}\ge 1$ . Suppose that

(a) , and

(b) .

Then there is an ${{\mathcal{L}}}_{\mathrm{C}}$ -formula $\mathrm{F}(\mathrm{x},\mathrm{y})$ such that:

1. (i)

2. (ii) ${\varSigma}^{\ast}\models \forall \mathrm{y}\;(\mathrm{F}(\mathrm{a},\mathrm{y})\leftrightarrow \mathrm{y}=\mathrm{p})$ .

3. (iii) ${\displaystyle \begin{array}{l}\hspace{-4pt} {\varSigma}^{\ast}\models \forall {\mathrm{x}}_1\dots {\mathrm{x}}_{\mathrm{n}}\forall {\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}\big({\wedge}_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{F}({\mathrm{x}}_{\mathrm{i}},{\mathrm{y}}_{\mathrm{i}})\to \\ \qquad\to \forall \mathrm{x},\mathrm{z}\;(\mathrm{x}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}\to (\mathrm{F}(\mathrm{x},\mathrm{z})\leftrightarrow \mathrm{G}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{k}},\mathrm{z})))\big).\end{array}}$

3 Catalan coding of trees

Theorem 2.11 yields an algorithm—“peel off the prefix ${\mathrm{b}}^{\mathrm{n}}\mathrm{a}$ and search for the shortest initial segment of the remainder having the $+1$ property”—which, when applied to a given string $\mathrm{x}$ and then repeatedly to the resulting component strings, eventually terminates in a unique tree-like arrangement ${T}_{\mathrm{x}}$ of substrings of $\mathrm{x}$ in which every node is an string and all of the endnodes $=\mathrm{a}$ . And, conversely, given any finite tree $T$ , by labelling each endnode with $\mathrm{a}$ , we can obtain, by repeatedly applying 2.7, a unique string ${\mathrm{c}}_T$ that we may think of as a code for $T$ , providing an explicit formal representation in linear form of the characteristic structure of the tree $T$ .

There are other ways to directly display the structure of planar trees in linear form, e.g., via symmetric bracketing. Because in concatenation theory parentheses are used associatively, and the symmetric bracketing notation is not associative— $\mathrm{x}(\mathrm{xx})$ does not represent the same tree as $(\mathrm{xx})\mathrm{x}$ —for our purposes we need to be able to rely exclusively on juxtaposition along with some indicators of arity as the sole means of expressing the tree structure by concatenation of binary strings. A simplified variant of this approach was used in [3] (see [3, 2.2]) to obtain a result analogous to Theorem 2.12, which served there as a basis for a coding of full binary, or dyadic, finite trees, where every non-terminal node has exactly two immediate descendants. Even though here we are allowing, in principle, any finite number of immediate descendants, remarkably, the very same strings, the strings, function as codes for trees in both cases.

We call the coding of finite trees given here the Catalan coding. Eugene Charles Catalan (1814–1894) identified the numbers, now named after him, that count different ways to fully (symmetrically) parenthesize a string of given lengths. As we defined them, strings are finite words in the alphabet $\{\mathrm{a},\mathrm{b}\}$ of the form $wa$ where $w$ is either empty or has exactly as many $a$ ’s as $b$ ’s and has no initial segment in which $a$ ’s strictly outnumber $b$ ’s. Words with this property have been extensively studied in combinatorics where they are called Catalan words (see, e.g., [5]).

The dyadic coding given in [3] and the Catalan coding parse strings differently. For example, bbbbaaaaa $(={\mathrm{b}}^4{\mathrm{a}}^5)$ produces, via the dyadic coding, the full binary tree on the left,

and via the Catalan coding the 4-ary tree on the right. Both coding schemes group codes of immediate subtrees analogously to the way in which argument terms of a given binary, and, respectively, $\mathrm{m}$ -ary operation are successively listed when written in the so-called Polish notation. But the tree branchings are recorded in different ways: in the dyadic code, each $b$ stands for a dyadic branching node, in the Catalan coding each block of consecutive $b$ ’s followed by a single $a$ signals a branching node, with the number of consecutive $b$ ’s in the same block indicating the number of that node’s immediate descendants. Consequently, in the Catalan coding, the $a$ ’s in a given tree code count the nodes and the $b$ ’s the edges of the tree. Nonetheless, some basic information about the tree coded by the string—the number of branching nodes ( $=$ the number of blocks of consecutive $b$ ’s) and the number of terminal nodes ( $=$ the number of $a$ ’s in the dyadic case, and $=$ the number of $a$ ’s minus the number of blocks of consecutive $b$ ’s in the present scheme)—and, consequently, the total number of nodes in the tree ( $=$ the total number of digits and $=$ the total number of $a$ ’s, resp.) are read off the encoding string essentially in the same way in both codings.

The Catalan coding offers a practical and easy way to communicate descriptions of the immense variety of finite planar trees, allowing any number, including single, immediate descendants: for example,

are coded by ${\mathrm{b}}^3{\mathrm{a}}^2{\mathrm{b}}^2{\mathrm{a}}^4$ , ${\mathrm{b}}^2{\mathrm{a}\mathrm{b}}^2{\mathrm{a}}^3{\mathrm{b}}^2{\mathrm{a}}^3$ _, and ${\mathrm{babab}}^2{\mathrm{a}}^3$ , respectively. (Always ignore the first $a$ after a block of consecutive $b$ ’s.) Restricting attention to and strings allows us to consider in particular ${\le}{\mathrm{m}}$ - and $\mathrm{m}$ -, respectively, trees with branchings allowing no more than m and exactly $\mathrm{m}$ , respectively, immediate descendants, $\mathrm{m}\ge 1$ .

The fact that the strings work as codes just as well for the more general class of trees of arbitrary arity as they do for dyadic trees suggests that in the specific setting of concatenation theory there may be a way to systematically interpret statements about the former in a domain that consists exclusively of binary trees or their formal simulacra. We now proceed to develop this idea.

4 Interpreting ${\mathrm{T}}_{\le \mathrm{m}}$ in ${\mathrm{T}}_{\le 2}$

In contrast to ${\mathrm{T}}_2$ , the theory ${\mathrm{T}}_{\le 2}$ explicitly allows for trees having nodes with single immediate descendants. We exploit this feature to show that such ${\le}{2}$ -trees can encode information about multiple branchings. Consider, for example, the simple triple-branching tree ${\mathrm{b}}^3{\mathrm{a}}^4$ on the left, and the tree

${\mathrm{b}\mathrm{a}\mathrm{b}}^2\mathrm{a}({\mathrm{b}\mathrm{a}}^2){\mathrm{b}}^2\mathrm{a}({\mathrm{b}\mathrm{a}}^2){\mathrm{b}}^2\mathrm{a}({\mathrm{b}\mathrm{a}}^2)\mathrm{a}$ on the right. The latter has three binary branchings, and in each of these the left branch has a single node ${\mathrm{ba}}^2$ which in turn has a single terminal node as its sole immediate descendant. This is meant to capture the ternary connections of the root node of ${\mathrm{b}}^3{\mathrm{a}}^4$ . The right branchings of the ${\le}{2}$ -tree serve as the supporting “spine” to express this structure. So we are replacing an $\mathrm{m}$ -branching by $\mathrm{m}$ binary branchings with singletons branching to the left. Here is a slightly more complicated example:

$$\begin{align*} \begin{array}{l}{\mathrm{b}}^2{\mathrm{a}}^2{\mathrm{b}}^3{\mathrm{a}}^4\Rightarrow {\mathrm{b}\mathrm{a}\mathrm{b}}^2\mathrm{a}(({\mathrm{b}\mathrm{a}}^2){\mathrm{b}}^2\mathrm{a}({\mathrm{b}}^3{\mathrm{a}}^4))\mathrm{a}\Rightarrow \\ \qquad\qquad\Rightarrow {\mathrm{b}\mathrm{a}\mathrm{b}}^2\mathrm{a}({\mathrm{b}\mathrm{a}}^2){\mathrm{b}}^2\mathrm{a}({\mathrm{b}\mathrm{a}\mathrm{b}}^2\mathrm{a}({\mathrm{b}\mathrm{a}}^2){\mathrm{b}}^2\mathrm{a}({\mathrm{b}\mathrm{a}}^2){\mathrm{b}}^2\mathrm{a}({\mathrm{b}\mathrm{a}}^2)\mathrm{a})\mathrm{a}.\end{array}\end{align*}$$

(The parentheses serve to highlight the replacements—they are not essential to reading the tree code.). For this to work generally, the replacement procedure has to operate inductively, starting with the root of the $\le \mathrm{m}$ -tree systematically transforming it step-by-step by working down its branches until all of its branchings—single, binary, or multiple—are appropriately converted. The ultimate result will be a ${\le}{2}$ -tree resembling a funhouse chandelier heavily tilting to the left, with single drop crystals at all (and only) the left terminal nodes.

More formally, for fixed $\mathrm{m}$ , we define a map $\theta (\mathrm{x})$ on strings such that $\theta (\mathrm{a})=\mathrm{baa}$ and $\theta ({\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}})={\mathrm{b}\mathrm{ab}}^2\mathrm{a}\theta ({\mathrm{x}}_1){\mathrm{b}}^2\mathrm{a}\theta ({\mathrm{x}}_2)\dots {\mathrm{b}}^2\mathrm{a}\theta ({\mathrm{x}}_{\mathrm{k}})\mathrm{a}$ for $\mathrm{k}\le \mathrm{m}$ . The operation $\theta$ is defined by recursion, by letting $\mathrm{p}=\mathrm{baa}$ and ${\mathrm{G}}_{\mathrm{k}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{k}},\mathrm{y})$ be the ${{\mathcal{L}}}_{\mathrm{C}}$ -formulae

$$\begin{align*}\exists {\mathrm{z}}_1\dots {\mathrm{z}}_{\mathrm{k}}({\mathrm{z}}_1={\mathrm{b}}^2{\mathrm{ay}}_{\mathrm{k}}\ \&\ {\wedge}_{1\le \mathrm{j}<\mathrm{k}}{\mathrm{z}}_{\mathrm{j}+1}={\mathrm{b}}^2{\mathrm{ay}}_{\mathrm{k}-\mathrm{j}}{\mathrm{z}}_{\mathrm{j}}\ \&\ \mathrm{y}={\mathrm{b}\mathrm{a}\mathrm{z}}_{\mathrm{k}}\mathrm{a}).\end{align*}$$

Hence by Theorem 2.16 its graph is expressible in ${{\mathcal{L}}}_{\mathrm{C}}$ . Then

We say that the $\le 2$ -tree $\theta (\mathrm{x})$ is an SLS-code (singleton/left singleton) code of the ${\le} {\mathrm{m}}$ -tree $\mathrm{x}$ .

To show that ${\mathrm{T}}_{\le \mathrm{m}}$ is formally interpretable in ${\mathrm{T}}_{\le 2}$ we need to reformulate ${\mathrm{T}}_{\le \mathrm{m}}$ in relational vocabulary $\{\;0,{\mathrm{T}}_1,\dots, {\mathrm{T}}_{\mathrm{m}},\sqsubseteq \}$ where ${\mathrm{T}}_{\mathrm{k}}$ for $1\le \mathrm{k}\le \mathrm{m}$ are ( $\mathrm{k}+1$ )-place relational symbols. As axioms we take the universal closures of:

$$\begin{align*}&(\mathrm{T}{1}_{\mathrm{n}})\quad \neg {\mathrm{T}}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}},0)\quad \mathrm{for}\ \mathrm{each}\;\mathrm{n},1\le \mathrm{n}\le \mathrm{m},\\&(\mathrm{T}{2}_{\mathrm{k},\mathrm{n}})\quad {\mathrm{T}}_{\mathrm{k}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{k}},\mathrm{x})\ \&\ {\mathrm{T}}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}},\mathrm{y})\to \mathrm{x}\ne \mathrm{y}\quad \mathrm{for}\ \mathrm{each}\;\mathrm{k},\mathrm{n},1\le \mathrm{k}<\mathrm{n}\le \mathrm{m},\\&(\mathrm{T}{3}_{\mathrm{n}})\hspace{3pt}{\mathrm{T}}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}},\mathrm{x})\ \&\ {\mathrm{T}}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}},\mathrm{y})\ \&\ \mathrm{x}=\mathrm{y}\to {\wedge}_{1\le \mathrm{i}\le \mathrm{n}}\;{\mathrm{x}}_{\mathrm{i}}={\mathrm{y}}_{\mathrm{i}}\hspace{3pt}\mathrm{for}\ \mathrm{each}\;\mathrm{n},1\le \mathrm{n}\le \mathrm{m}.\\&(\mathrm{T}{4}_{\mathrm{n}})\quad {\mathrm{T}}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}},\mathrm{y})\to (\mathrm{x}\sqsubseteq \mathrm{y}\leftrightarrow \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}\le \mathrm{n}}\;\mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{i}})\quad \mathrm{for}\ \mathrm{each}\;\mathrm{n},1\le \mathrm{n}\le \mathrm{m},\\&(\mathrm{T}5)-(\mathrm{T}8),\\&(\mathrm{T}{9}_{\mathrm{n}})\quad \exists {\mathrm{x}\mathrm{T}}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}},\mathrm{x})\quad \mathrm{for}\ \mathrm{each}\;\mathrm{n},1\le \mathrm{n}\le \mathrm{m},\\&(\mathrm{T}1{0}_{\mathrm{n}})\quad {\mathrm{T}}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}},\mathrm{x})\ \&\ {\mathrm{T}}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}},\mathrm{y})\to \mathrm{x}=\mathrm{y}\quad \mathrm{for}\ \mathrm{each}\;\mathrm{n},1\le \mathrm{n}\le \mathrm{m}.\end{align*}$$

We define the domain of the formal interpretation so that the SSL codes of $\le \mathrm{m}$ -trees are guaranteed to be included in it:

$$\begin{align*}\mathrm{I}(\mathrm{x})\equiv \exists \mathrm{y}\;\mathrm{x}={\tau}_1(\mathrm{y}).\end{align*}$$

Let ${0}^{\tau}=: {\tau}_1(0)$ .

For each $\mathrm{n}$ , $1\le \mathrm{n}\le \mathrm{m}$ , let ${({\mathrm{T}}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}},\mathrm{y}))}^{\tau }$ be the formula

$$\begin{align*}\exists {\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{n}}({\mathrm{u}}_1={\tau}_2({\mathrm{y}}_{\mathrm{n}},0)\ \&\ {\wedge}_{1\le \mathrm{i}<\mathrm{n}}{\mathrm{u}}_{\mathrm{i}+1}={\tau}_2({\mathrm{y}}_{\mathrm{n}-\mathrm{i}},{\mathrm{u}}_{\mathrm{i}})\ \&\ \mathrm{y}={\tau}_1({\mathrm{u}}_{\mathrm{n}})),\end{align*}$$

and let ${(\mathrm{x}\sqsubseteq \mathrm{y})}^{\tau}\equiv \mathrm{x}\sqsubseteq \mathrm{y}$ . Throughout the rest of this section, we let $\mathrm{M}$ be an arbitrary model of ${\mathrm{T}}_{\le 2}$ .

4.1

(a) For each $\mathrm{n}$ , $1\le \mathrm{n}\le \mathrm{m}$ , $T_{\leq 2}\vdash (T1_n)^{\tau}$ .

(b) For each $\mathrm{k}$ and $\mathrm{n}$ , $1\le \mathrm{k}<\mathrm{n}\le \mathrm{m}$ , $T_{\leq 2}\vdash (T2_{k,n})^{\tau}.$

(c) For each $\mathrm{n}$ , $1\le \mathrm{n}\le \mathrm{m}$ , $T_{\leq 2}\vdash (T3_{n})^{\tau}.$

(d) For each $\mathrm{n}$ , $1\le \mathrm{n}\le \mathrm{m}$ , $T_{\leq 2}\vdash (T4_{n})^{\tau}.$

(e) For each $\mathrm{n}$ , $1\le \mathrm{n}\le \mathrm{m}$ , $T_{\leq 2}\vdash (T9_{n})^{\tau}.$

(f) For each $\mathrm{n}$ , $1\le \mathrm{n}\le \mathrm{m}$ , $T_{\leq 2}\vdash (T10_{n})^{\tau}.$

Proof (a) Assume $\mathrm{M}\models {({\mathrm{T}}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}},0))}^{\tau }$ where $\mathrm{M}{\models }\wedge_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{I}({\mathrm{y}}_{\mathrm{i}})$ . Then

$$\begin{align*}\mathrm{M}\models \exists {\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{n}}({\mathrm{u}}_1={\tau}_2({\mathrm{y}}_{\mathrm{n}},0)\ \&\ {\wedge}_{1\le \mathrm{i}<\mathrm{n}}{\mathrm{u}}_{\mathrm{i}+1}={\tau}_2({\mathrm{y}}_{\mathrm{n}-\mathrm{i}},{\mathrm{u}}_{\mathrm{i}})\ \&\ {\tau}_1(0)={\tau}_1({\mathrm{u}}_{\mathrm{n}})).\end{align*}$$

Suppose $\mathrm{n}>1$ . Then $\mathrm{M}\models {\tau}_1(0)={\tau}_1({\mathrm{u}}_{\mathrm{n}})\ \&\ {\mathrm{u}}_{\mathrm{n}}={\tau}_2({\mathrm{y}}_1,{\mathrm{u}}_{\mathrm{n}-1})$ . But then, by $(\mathrm{T}{3}_1)$ , we have $\mathrm{M}\models 0={\tau}_2({\mathrm{y}}_1,{\mathrm{u}}_{\mathrm{n}-1})$ , contradicting $(\mathrm{T}{1}_2)$ . If $\mathrm{n}=1$ , then $\mathrm{M}\models \exists {\mathrm{u}}_1({\mathrm{u}}_1={\tau}_2({\mathrm{y}}_1,0)\ \&\ {\tau}_1(0)={\tau}_1({\mathrm{u}}_1))$ . Then, by $(\mathrm{T}{3}_1)$ , $\mathrm{M}\models 0={\tau}_2({\mathrm{y}}_1,0)$ , contradicting $(\mathrm{T}{1}_2)$ . Hence $\mathrm{M}\models \neg {({\mathrm{T}}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}},0))}^{\tau }$ .

(b) Assume $\mathrm{M}\models {({\mathrm{T}}_{\mathrm{k}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{k}},\mathrm{x}))}^{\tau}\ \&\ {({\mathrm{T}}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}},\mathrm{y}))}^{\tau}\ \&\ \mathrm{x}=\mathrm{y}$ where $\mathrm{M}{\models }\wedge_{1\le \mathrm{i}\le \mathrm{k}}\mathrm{I}({\mathrm{x}}_{\mathrm{i}})\ \&\ {\wedge}_{1\le \mathrm{j}\le \mathrm{n}}\mathrm{I}({\mathrm{y}}_{\mathrm{j}})\ \&\ \mathrm{I}(\mathrm{x})\ \&\ \mathrm{I}(\mathrm{y})$ . Then $\mathrm{M}\models \exists {\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{k}}({\mathrm{u}}_1={\tau}_2({\mathrm{x}}_{\mathrm{k}},0)\ \&\ {\wedge}_{1\le \mathrm{i}<\mathrm{k}}{\mathrm{u}}_{\mathrm{i}+1}={\tau}_2({\mathrm{x}}_{\mathrm{k}-\mathrm{i}},{\mathrm{u}}_{\mathrm{i}})\ \&\ \mathrm{x}={\tau}_1({\mathrm{u}}_{\mathrm{k}}))$ and $\mathrm{M}\models \exists {\mathrm{v}}_1\dots {\mathrm{v}}_{\mathrm{n}}({\mathrm{v}}_1={\tau}_2({\mathrm{y}}_{\mathrm{n}},0)\ \&\ {\wedge}_{1\le \mathrm{j}<\mathrm{n}}{\mathrm{v}}_{\mathrm{j}+1}={\tau}_2({\mathrm{y}}_{\mathrm{n}-\mathrm{j}},{\mathrm{v}}_{\mathrm{j}})\ \&\ \mathrm{y}={\tau}_1({\mathrm{v}}_{\mathrm{n}}))$ , whence $\mathrm{M}\models {\tau}_1({\mathrm{u}}_{\mathrm{k}})=\mathrm{x}=\mathrm{y}={\tau}_1({\mathrm{v}}_{\mathrm{n}})$ , and further, by $(\mathrm{T}{3}_1)$ , $\mathrm{M}\models {\mathrm{u}}_{\mathrm{k}}={\mathrm{v}}_{\mathrm{n}}$ .

Let ${\mathrm{x}}_0=\mathrm{x}$ and ${\mathrm{y}}_0=\mathrm{y}$ . By hypothesis, we have that

(1) $$\begin{align}\mathrm{M}\models {\mathrm{x}}_0={\mathrm{y}}_0.\end{align}$$

Assume now that $\mathrm{M}\models {\mathrm{x}}_{\mathrm{j}}={\mathrm{y}}_{\mathrm{j}}\ \&\ {\mathrm{u}}_{\mathrm{k}-\mathrm{j}}={\mathrm{v}}_{\mathrm{n}-\mathrm{j}}$ , where $0\le \mathrm{j}<\mathrm{k}$ . Then $\mathrm{M}\models {\tau}_2({\mathrm{x}}_{\mathrm{j}+1},{\mathrm{u}}_{\mathrm{k}-(\mathrm{j}+1)})={\mathrm{u}}_{\mathrm{k}-\mathrm{j}}={\mathrm{v}}_{\mathrm{n}-\mathrm{j}}={\tau}_2({\mathrm{y}}_{\mathrm{j}+1},{\mathrm{v}}_{\mathrm{n}-(\mathrm{j}+1)})$ , whence, by $(\mathrm{T}{3}_2)$ , $\mathrm{M}\models {\mathrm{x}}_{\mathrm{j}+1}={\mathrm{y}}_{\mathrm{j}+1}\ \&\ {\mathrm{u}}_{\mathrm{k}-(\mathrm{j}+1)}={\mathrm{v}}_{\mathrm{n}-(\mathrm{j}+1)}$ . Thus, we have

(2) $$\begin{align}\mathrm{M}\models {\mathrm{x}}_{\mathrm{j}}={\mathrm{y}}_{\mathrm{j}}\ \&\ {\mathrm{u}}_{\mathrm{k}-\mathrm{j}}={\mathrm{v}}_{\mathrm{n}-\mathrm{j}}\to {\mathrm{x}}_{\mathrm{j}+1}={\mathrm{y}}_{\mathrm{j}+1}\ \&\ {\mathrm{u}}_{\mathrm{k}-(\mathrm{j}+1)}={\mathrm{v}}_{\mathrm{n}-(\mathrm{j}+1)}.\end{align}$$

From (1) after $\mathrm{k}$ applications of (2) we obtain

$$\begin{align*}\mathrm{M}\models {\mathrm{x}}_{\mathrm{k}}={\mathrm{y}}_{\mathrm{k}}\ \&\ {\mathrm{u}}_1={\mathrm{u}}_{\mathrm{k}-(\mathrm{k}-1)}={\mathrm{v}}_{\mathrm{n}-(\mathrm{k}-1)}={\mathrm{v}}_{\mathrm{n}-\mathrm{k}+1}.\end{align*}$$

But $\mathrm{M}\models {\mathrm{u}}_1={\tau}_2({\mathrm{x}}_{\mathrm{k}},0)$ and $\mathrm{M}\models {\mathrm{v}}_{\mathrm{n}-\mathrm{k}+1}={\tau}_2({\mathrm{y}}_{\mathrm{k}},{\mathrm{v}}_{\mathrm{n}-\mathrm{k}})$ where $\mathrm{n}\hbox{--} \mathrm{k}\ne 0$ . Hence $\mathrm{M}\models {\tau}_2({\mathrm{x}}_{\mathrm{k}},0)={\tau}_2({\mathrm{y}}_{\mathrm{k}},{\mathrm{v}}_{\mathrm{n}-\mathrm{k}})$ . But then, by $(\mathrm{T}{3}_2)$ , $\mathrm{M}\models 0={\mathrm{v}}_{\mathrm{n}-\mathrm{k}}={\tau}_2({\mathrm{y}}_{\mathrm{k}+1},{\mathrm{v}}_{\mathrm{n}-(\mathrm{k}+1)})$ , contradicting $(\mathrm{T}{1}_2)$ . Hence $\mathrm{M}\models \mathrm{x}\ne \mathrm{y}$ , and we obtain $\mathrm{M}\models {(\mathrm{T}{2}_{\mathrm{k},\mathrm{n}})}^{\tau }$ .

(c) Assume $\mathrm{M}\models {({\mathrm{T}}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}},\mathrm{x}))}^{\tau}\ \&\ {({\mathrm{T}}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}},\mathrm{y}))}^{\tau}\ \&\ \mathrm{x}=\mathrm{y}$ where $\mathrm{M}{\models }\wedge_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{I}({\mathrm{x}}_{\mathrm{i}})\ \&\ {\wedge}_{1\le \mathrm{j}\le \mathrm{n}}\mathrm{I}({\mathrm{y}}_{\mathrm{j}})\ \&\ \mathrm{I}(\mathrm{x})\ \&\ \mathrm{I}(\mathrm{y})$ . Then $\mathrm{M}\models \exists {\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{k}}({\mathrm{u}}_1={\tau}_2({\mathrm{x}}_{\mathrm{n}},0)\ \&\ {\wedge}_{1\le \mathrm{i}<\mathrm{n}}{\mathrm{u}}_{\mathrm{i}+1}={\tau}_2({\mathrm{x}}_{\mathrm{n}-\mathrm{i}},{\mathrm{u}}_{\mathrm{i}})\ \&\ \mathrm{x}={\tau}_1({\mathrm{u}}_{\mathrm{n}}))$ and $\mathrm{M}\models \exists {\mathrm{v}}_1\dots {\mathrm{v}}_{\mathrm{n}}({\mathrm{v}}_1={\tau}_2({\mathrm{y}}_{\mathrm{n}},0)\ \&\ {\wedge}_{1\le \mathrm{j}<\mathrm{n}}{\mathrm{v}}_{\mathrm{j}+1}={\tau}_2({\mathrm{y}}_{\mathrm{n}-\mathrm{j}},{\mathrm{v}}_{\mathrm{j}})\ \&\ \mathrm{y}={\tau}_1({\mathrm{v}}_{\mathrm{n}}))$ , whence $\mathrm{M}\models {\tau}_1({\mathrm{u}}_{\mathrm{n}})=\mathrm{x}=\mathrm{y}={\tau}_1({\mathrm{v}}_{\mathrm{n}})$ , and further, by $(\mathrm{T}{3}_1)$ , $\mathrm{M}\models {\mathrm{u}}_{\mathrm{n}}={\mathrm{v}}_{\mathrm{n}}$ . We now show, for $0\le \mathrm{j}<\mathrm{n}$ , that

(*) $$\begin{align}\kern0.36em \mathrm{M}\models {\mathrm{x}}_{\mathrm{j}}={\mathrm{y}}_{\mathrm{j}}\ \&\ {\mathrm{u}}_{\mathrm{n}-\mathrm{j}}={\mathrm{v}}_{\mathrm{n}-\mathrm{j}}\to {\mathrm{x}}_{\mathrm{j}+1}={\mathrm{y}}_{\mathrm{j}+1}\ \&\ {\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{v}}_{\mathrm{n}-(\mathrm{j}+1)}.\end{align}$$

Assume $\mathrm{M}\models {\mathrm{x}}_{\mathrm{j}}={\mathrm{y}}_{\mathrm{j}}\ \&\ {\mathrm{u}}_{\mathrm{n}-\mathrm{j}}={\mathrm{v}}_{\mathrm{n}-\mathrm{j}}$ . Then $\mathrm{M}\models {\tau}_2({\mathrm{x}}_{\mathrm{j}+1},{\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)})={\mathrm{u}}_{\mathrm{n}-\mathrm{j}}={\mathrm{v}}_{\mathrm{n}-\mathrm{j}}={\tau}_2({\mathrm{y}}_{\mathrm{j}+1},{\mathrm{v}}_{\mathrm{n}-(\mathrm{j}+1)})$ , whence, by $(\mathrm{T}{3}_2)$ , $\mathrm{M}\models {\mathrm{x}}_{\mathrm{j}+1}={\mathrm{y}}_{\mathrm{j}+1}\ \&\ {\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{v}}_{\mathrm{n}-(\mathrm{j}+1)}$ _, as claimed.

Letting ${\mathrm{x}}_0=\mathrm{x}$ and ${\mathrm{y}}_0=\mathrm{y}$ , after $\mathrm{n}$ applications of $({}^\ast )$ we obtain $\mathrm{M}\models {\mathrm{x}}_{\mathrm{n}}={\mathrm{y}}_{\mathrm{n}}$ . Hence $\mathrm{M}{\models }\wedge_{1\le \mathrm{i}\le \mathrm{n}}{\mathrm{x}}_{\mathrm{i}}={\mathrm{y}}_{\mathrm{i}}$ as needed.

(d) Assume $\mathrm{M}\models {({\mathrm{T}}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}},\mathrm{y}))}^{\tau }$ where $\mathrm{M}{\models }\wedge_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{I}({\mathrm{y}}_{\mathrm{i}})$ . Then

$$\begin{align*}\mathrm{M}\models \exists {\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{n}}({\mathrm{u}}_1={\tau}_2({\mathrm{y}}_{\mathrm{n}},0)\ \&\ {\wedge}_{1\le \mathrm{i}<\mathrm{n}}{\mathrm{u}}_{\mathrm{i}+1}={\tau}_2({\mathrm{y}}_{\mathrm{n}-\mathrm{i}},{\mathrm{u}}_{\mathrm{i}})\ \&\ \mathrm{y}={\tau}_1({\mathrm{u}}_{\mathrm{n}})).\end{align*}$$

Suppose further that $\mathrm{M}\models \mathrm{x}\sqsubseteq \mathrm{y}$ where $\mathrm{M}\models \mathrm{I}(\mathrm{x})$ . Then $\mathrm{M}\models \mathrm{x}\sqsubseteq {\tau}_1({\mathrm{u}}_{\mathrm{n}})$ , whence, by $(\mathrm{T}{4}_1)$ , $\mathrm{M}\models \mathrm{x}={\tau}_1({\mathrm{u}}_{\mathrm{n}})\;\mathrm{v}\;\mathrm{x}\sqsubseteq {\mathrm{u}}_{\mathrm{n}}$ , and further, $\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{x}\sqsubseteq {\mathrm{u}}_{\mathrm{n}}$ . We now show, for $0\le \mathrm{j}<\mathrm{n}$ , that

(**) $$\begin{align}\mathrm{M}\models \mathrm{x}\sqsubseteq {\mathrm{u}}_{\mathrm{n}-\mathrm{j}}\to \mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{j}+1}\ \mathrm{v}\ \mathrm{x}\sqsubseteq {\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)}.\end{align}$$

Assume that $\mathrm{M}\models \mathrm{x}\sqsubseteq {\mathrm{u}}_{\mathrm{n}-\mathrm{j}}$ . Then $\mathrm{M}\models \mathrm{x}\sqsubseteq {\tau}_2({\mathrm{y}}_{\mathrm{j}+1},{\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)})$ , whence, by $(\mathrm{T}{4}_2)$ , $\mathrm{M}\models \mathrm{x}={\mathrm{u}}_{\mathrm{n}-\mathrm{j}}\;\mathrm{v}\;\mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{j}+1}\;\mathrm{v}\;\mathrm{x}\sqsubseteq {\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)}$ . Suppose, for a reductio, that $\mathrm{M}\models \mathrm{x}={\mathrm{u}}_{\mathrm{n}-\mathrm{j}}$ . Then $\mathrm{M}\models \mathrm{x}={\tau}_2({\mathrm{y}}_{\mathrm{j}+1},{\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)})$ . But from $\mathrm{M}\models \mathrm{I}(\mathrm{x})$ we have that $\mathrm{M}\models \exists \mathrm{z}\;\mathrm{x}={\tau}_1(\mathrm{z})$ , whence $\mathrm{M}\models {\tau}_2({\mathrm{y}}_{\mathrm{j}+1},{\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)})={\tau}_1(\mathrm{z})$ , contradicting $(\mathrm{T}{2}_{1,2})$ . Hence $\mathrm{M}\models \mathrm{x}\ne {\mathrm{u}}_{\mathrm{n}-\mathrm{j}}$ . Therefore $\mathrm{M}\models \mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{j}+1}\;\mathrm{v}\;\mathrm{x}\sqsubseteq {\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)}$ , as claimed. After $\mathrm{n}\hbox{--} 1$ applications of $(^{\ast \ast} )$ we obtain from $\mathrm{M}\models \mathrm{x}=\mathrm{y}\;\mathrm{v}\;\mathrm{x}\sqsubseteq {\mathrm{u}}_{\mathrm{n}}$ that $\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}\le \mathrm{n}-1}\mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{i}}\; \mathrm{v}\;\mathrm{x}\sqsubseteq {\mathrm{u}}_1$ . If $\mathrm{M}\models \mathrm{x}\sqsubseteq {\mathrm{u}}_1$ , then $\mathrm{M}\models \mathrm{x}\sqsubseteq {\tau}_2({\mathrm{y}}_{\mathrm{n}},0)$ , whence by $(\mathrm{T}{4}_2)$ , we have $\mathrm{M}\models \mathrm{x}={\tau}_2({\mathrm{y}}_{\mathrm{n}},0)\kern0.24em \mathrm{v}\;\;\mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{n}}\;\mathrm{v}\;\mathrm{x}\sqsubseteq 0$ . But $\mathrm{M}\models \mathrm{x}={\tau}_2({\mathrm{y}}_{\mathrm{n}},0)$ contradicts $\mathrm{M}\models \mathrm{I}(\mathrm{x})$ by $(\mathrm{T}{2}_{1,2})$ . And from $\mathrm{M}\models \mathrm{x}\sqsubseteq 0$ by $(\mathrm{T}6)$ and $(\mathrm{T}7)$ we obtain $\mathrm{M}\models \mathrm{x}=0$ . But then from $\mathrm{M}\models \mathrm{I}(\mathrm{x})$ we have $\mathrm{M}\models \exists \mathrm{z}\;{\tau}_1(\mathrm{z})=\mathrm{x}=0$ , contradicting $(\mathrm{T}{1}_1)$ . Hence both $\mathrm{M}\models \mathrm{x}={\tau}_2({\mathrm{y}}_{\mathrm{n}},0)$ and $\mathrm{M}\models \mathrm{x}\sqsubseteq 0$ are ruled out, and we obtain $\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{i}}$ . But then

$$\begin{align*}\mathrm{M}\models \mathrm{x}\sqsubseteq \mathrm{y}\to \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{i}}.\end{align*}$$

Conversely, assume that $\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{i}}$ . Letting ${\mathrm{y}}_0=\mathrm{y}$ , we now show that the principal hypothesis $\mathrm{M}\models {({\mathrm{T}}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}},\mathrm{y}))}^{\tau }$ implies that

(†) $$\begin{align}\mathrm{M}\models\wedge_{1\le \mathrm{i}\le \mathrm{n}}{\mathrm{y}}_{\mathrm{i}}\sqsubseteq \mathrm{y}.\end{align}$$

By $(\mathrm{T}5)$ we have that $\mathrm{M}\models \mathrm{y}\sqsubseteq \mathrm{y}$ . Hence $\mathrm{M}\models {\mathrm{y}}_0\sqsubseteq \mathrm{y}$ . By $(\mathrm{T}{4}_1)$ we have that $\mathrm{M}\models {\mathrm{u}}_{\mathrm{n}}\sqsubseteq {\tau}_1({\mathrm{u}}_{\mathrm{n}})=\mathrm{y}$ . Next, we show, for $0\le \mathrm{j}<\mathrm{n}$ , that

(***) $$\begin{align}\mathrm{M}\models {\mathrm{y}}_{\mathrm{j}}\sqsubseteq \mathrm{y}\ \&\ {\mathrm{u}}_{\mathrm{n}-\mathrm{j}}\sqsubseteq \mathrm{y}\to {\mathrm{y}}_{\mathrm{j}+1}\sqsubseteq \mathrm{y}\ \&\ {\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)}\sqsubseteq \mathrm{y}.\end{align}$$

Assume that $\mathrm{M}\models {\mathrm{y}}_{\mathrm{j}}\sqsubseteq \mathrm{y}\ \&\ {\mathrm{u}}_{\mathrm{n}-\mathrm{j}}\sqsubseteq \mathrm{y}$ . Then, by $(\mathrm{T}{4}_2)$ , we have that

$\mathrm{M}\models {\mathrm{y}}_{\mathrm{j}+1}\sqsubseteq {\tau}_2({\mathrm{y}}_{\mathrm{j}+1},{\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)})={\mathrm{u}}_{\mathrm{n}-\mathrm{j}}\sqsubseteq \mathrm{y}$ and $\mathrm{M}\models {\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)}\sqsubseteq {\tau}_2({\mathrm{y}}_{\mathrm{j}},$ ${\mathrm{u}}_{\mathrm{n}-(\mathrm{j}+1)})={\mathrm{u}}_{\mathrm{n}-\mathrm{j}}\sqsubseteq \mathrm{y}$ .

This proves $(^{\ast \ast \ast} )$ .

After $\mathrm{n}$ applications of $(^{\ast \ast \ast} )$ we then obtain from $\mathrm{M}\models {\mathrm{y}}_0\sqsubseteq \mathrm{y}\ \&\ {\mathrm{u}}_{\mathrm{n}}\sqsubseteq \mathrm{y}$ that

$$\begin{align*}\mathrm{M}\models \wedge_{1\le \mathrm{i}<\mathrm{n}}{\mathrm{y}}_{\mathrm{i}}\sqsubseteq \mathrm{y}\ \&\ {\mathrm{u}}_1\sqsubseteq \mathrm{y}.\end{align*}$$

But then, by $(\mathrm{T}{4}_2)$ , $\mathrm{M}\models {\mathrm{y}}_{\mathrm{n}}\sqsubseteq {\tau}_2({\mathrm{y}}_{\mathrm{n}},0)={\mathrm{u}}_1\sqsubseteq \mathrm{y}$ . Hence by $(\mathrm{T}8)$ it follows that

$$\begin{align*}\mathrm{M} \models \wedge_{1\le \mathrm{i}\le \mathrm{n}}{\mathrm{y}}_{\mathrm{i}}\sqsubseteq \mathrm{y}.\end{align*}$$

This establishes $(\dagger )$ . But then from hypothesis $\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\vee {}_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{i}}$ and ${\mathrm{y}}_0=\mathrm{y}$ , we obtain, by $(\mathrm{T}8)$ , that $\mathrm{M}\models \mathrm{x}\sqsubseteq \mathrm{y}$ . Therefore also

$$\begin{align*}\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{x}\sqsubseteq {\mathrm{y}}_{\mathrm{i}}\to \mathrm{x}\sqsubseteq \mathrm{y},\end{align*}$$

as required.

(e) Assume $\mathrm{M}\models \wedge_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{I}({\mathrm{x}}_{\mathrm{i}})$ . We have that $\mathrm{M}\models \exists {\mathrm{u}}_1\kern0.24em {\mathrm{u}}_1={\tau}_2({\mathrm{x}}_{\mathrm{n}},0)$ .

Let ${\mathrm{u}}_0=0$ . We now argue that, for $0\le \mathrm{j} - 1<\mathrm{n}$ ,

(††) $$\begin{align}\mathrm{M}\models {\mathrm{u}}_{\mathrm{j}+1}={\tau}_2({\mathrm{x}}_{\mathrm{n}-\mathrm{j}},{\mathrm{u}}_{\mathrm{j}})\to \exists {\mathrm{u}}_{\mathrm{j}+2}{\mathrm{u}}_{\mathrm{j}+2}={\tau}_2({\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)},{\mathrm{u}}_{\mathrm{j}+1}).\end{align}$$

Assume that $\mathrm{M}\models {\mathrm{u}}_{\mathrm{j}+1}={\tau}_2({\mathrm{x}}_{\mathrm{n}-\mathrm{j}},{\mathrm{u}}_{\mathrm{j}})$ . Then, trivially in ${\mathrm{T}}_{\le 2}$ ,

$$\begin{align*}\mathrm{M}\models \exists {\mathrm{u}}_{\mathrm{j}+2}{\mathrm{u}}_{\mathrm{j}+2}={\tau}_2({\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)},{\mathrm{u}}_{\mathrm{j}+1}).\end{align*}$$

Hence $(\dagger \dagger )$ holds. After $\mathrm{n}\hbox{--} 1$ applications of $(\dagger \dagger )$ we obtain from $\mathrm{M}\models \exists {\mathrm{u}}_1{\mathrm{u}}_1={\tau}_2({\mathrm{x}}_{\mathrm{n}},0)$ that

$$\begin{align*}\mathrm{M}\models \exists {\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{n}}({\mathrm{u}}_1={\tau}_2({\mathrm{x}}_{\mathrm{n}},0)\ \&\ {\wedge}_{1\le \mathrm{i}<\mathrm{n}}{\mathrm{u}}_{\mathrm{i}+1}={\tau}_2({\mathrm{x}}_{\mathrm{n}-\mathrm{i}},{\mathrm{u}}_{\mathrm{i}})).\end{align*}$$

Now, we also have that $\mathrm{M}\models \exists \mathrm{x}\;\mathrm{x}={\tau}_1({\mathrm{u}}_{\mathrm{n}})$ . From the definition of $\mathrm{I}$ we have that $\mathrm{M}\models \exists \mathrm{x}\;(\mathrm{x}={\tau}_1({\mathrm{u}}_{\mathrm{n}})\ \&\ \mathrm{I}(\mathrm{x}))$ . Hence we have proved that $\mathrm{M}\models \exists \mathrm{x}\;(\mathrm{I}(\mathrm{x})\ \&\ {({\mathrm{T}}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}},\mathrm{x}))}^{\tau})$ , as required.

(f) Assume $\mathrm{M}\models {({\mathrm{T}}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}},\mathrm{x}))}^{\tau}\ \&\ {({\mathrm{T}}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}},\mathrm{y}))}^{\tau }$ where $\mathrm{M}\models \wedge_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{I}({\mathrm{x}}_{\mathrm{i}})\ \&\ \mathrm{I}(\mathrm{x})\ \&\ \mathrm{I}(\mathrm{y})$ . Then $\mathrm{M}\models \exists {\mathrm{u}}_1\dots {\mathrm{u}}_{\mathrm{n}}({\mathrm{u}}_1={\tau}_2({\mathrm{x}}_{\mathrm{n}},0)\ \& $ ${\wedge}_{1\le \mathrm{i}<\mathrm{n}}\ {\mathrm{u}}_{\mathrm{i}+1}={\tau}_2({\mathrm{x}}_{\mathrm{n}-\mathrm{i}},{\mathrm{u}}_{\mathrm{i}})\ \&\ \mathrm{x}={\tau}_1({\mathrm{u}}_{\mathrm{n}}))$ and $\mathrm{M}\models \exists {\mathrm{v}}_1\dots {\mathrm{v}}_{\mathrm{n}}({\mathrm{v}}_1={\tau}_2({\mathrm{x}}_{\mathrm{n}},0)\ \& $ ${\wedge}_{1\le \mathrm{i}<\mathrm{n}}\ {\mathrm{v}}_{\mathrm{i}+1}={\tau}_2({\mathrm{x}}_{\mathrm{n}-\mathrm{i}},{\mathrm{v}}_{\mathrm{i}})\ \&\ \mathrm{y}={\tau}_1({\mathrm{v}}_{\mathrm{n}}))$ . Hence $\mathrm{M}\models {\mathrm{u}}_1={\mathrm{v}}_1$ . Now, for $1\le \mathrm{j}<\mathrm{n}$ , we have that

(†††) $$\begin{align}\mathrm{M}\models {\mathrm{u}}_{\mathrm{j}}={\mathrm{v}}_{\mathrm{j}}\to {\mathrm{u}}_{\mathrm{j}+1}={\mathrm{v}}_{\mathrm{j}+1}.\end{align}$$

After $\mathrm{n}\hbox{--} 1$ applications of $(\dagger \dagger \dagger )$ we obtain from $\mathrm{M}\models {\mathrm{u}}_1={\mathrm{v}}_1$ that $\mathrm{M}\models {\mathrm{u}}_{\mathrm{n}}={\mathrm{v}}_{\mathrm{n}}$ . But then $\mathrm{M}\models \mathrm{x}={\tau}_1({\mathrm{u}}_{\mathrm{n}})={\tau}_1({\mathrm{v}}_{\mathrm{n}})=\mathrm{y}$ . So $\mathrm{M}\models \mathrm{x}=\mathrm{y}$ , as required.

From 4.1(a)–(f) we conclude:

Theorem 4.2. For each $\mathrm{m}\ge 1$ , ${\mathrm{T}}_{\le \mathrm{m}}$ is interpretable in ${\mathrm{T}}_{\le 2}$ .

Now, for fixed $\mathrm{n}\ge 1$ , the (relational form of) theory ${\mathrm{T}}_{\mathrm{n}}$ of full $\mathrm{n}$ -trees is formulated in the reduced vocabulary $\{0,{\mathrm{T}}_{\mathrm{n}},\sqsubseteq \}$ with $(\mathrm{T}{1}_{\mathrm{n}})$ , $(\mathrm{T}{3}_{\mathrm{n}})$ , $(\mathrm{T}{4}_{\mathrm{n}})$ , $(\mathrm{T}5)-(\mathrm{T}8)$ , $(\mathrm{T}{9}_{\mathrm{n}})$ , and $(\mathrm{T}1{0}_{\mathrm{n}})$ as axioms. So the argument for Theorem 4.2 also establishes:

Theorem 4.3. For each n ≥ 1, ${\mathrm{T}}_{\mathrm{n}}$ is interpretable in ${\mathrm{T}}_{\le 2}$ .

5 Interpreting ${\mathrm{T}}_{\le 2}$ in ${\mathrm{QT}}^{+}$

In [3] we have shown that the theory ${\mathrm{T}}_2$ of dyadic trees is interpretable in formal concatenation theory ${\mathrm{QT}}^{+}$ , a first-order theory formulated in vocabulary ${{\mathcal{L}}}_{\mathrm{C}}$ , with the (universal closures) of the following formulae as axioms:

(QT1) $$\begin{align}(\mathrm{x}^\ast \mathrm{y})^\ast \mathrm{z}=\mathrm{x}^\ast (\mathrm{y}^\ast \mathrm{z}).\end{align}$$

(QT2) $$\begin{align}\neg (\mathrm{x}^\ast \mathrm{y}=\mathrm{a})\ \&\ \neg (\mathrm{x}^\ast \mathrm{y}=\mathrm{b}).\end{align}$$

(QT3) $$\begin{align} \begin{array}{l}(\mathrm{x}^\ast \mathrm{a}=\mathrm{y}^\ast \mathrm{a}\to \mathrm{x}=\mathrm{y})\ \&\ (\mathrm{x}^\ast \mathrm{b}=\mathrm{y}^\ast \mathrm{b}\to \mathrm{x}=\mathrm{y})\ \&\ \\ {}\ \&\ (\mathrm{a}^\ast \mathrm{x}=\mathrm{a}^\ast \mathrm{y}\to \mathrm{x}=\mathrm{y})\ \&\ (\mathrm{b}^\ast \mathrm{x}=\mathrm{b}^\ast \mathrm{y}\to \mathrm{x}=\mathrm{y}).\end{array}\end{align}$$

(QT4) $$\begin{align}\neg (\mathrm{a}^\ast \mathrm{x}=\mathrm{b}^\ast \mathrm{y})\ \&\ \neg (\mathrm{x}^\ast \mathrm{a}=\mathrm{y}^\ast \mathrm{b}).\end{align}$$

(QT5) $$\begin{align}\mathrm{x}=\mathrm{a}\;\mathrm{v}\;\mathrm{x}=\mathrm{b}\;\mathrm{v}\kern0.24em (\exists \mathrm{y}(\mathrm{a}^\ast \mathrm{y}=\mathrm{x}\;\mathrm{v}\;\mathrm{b}^\ast \mathrm{y}=\mathrm{x})\ \&\ \exists \mathrm{z}(\mathrm{z}^\ast \mathrm{a}=\mathrm{x}\;\mathrm{v}\;\mathrm{z}^\ast \mathrm{b}=\mathrm{x})).\end{align}$$

It is convenient to have a function symbol for a successor operation on strings:

(QT6) $$\begin{align}\mathrm{Sx}=\mathrm{y}\leftrightarrow ((\mathrm{x}=\mathrm{a}\ \&\ \mathrm{y}=\mathrm{b})\;\mathrm{v}\;(\neg \mathrm{x}=\mathrm{a}\ \&\ \mathrm{x}^\ast \mathrm{b}=\mathrm{y})).\end{align}$$

Since the last axiom is basically a definition, adding it to the other five results in an inessential (i.e., conservative) extension.

The proof given in [3] of interpretability of ${\mathrm{T}}_2$ in ${\mathrm{QT}}^{+}$ relies on the binary representation of dyadic trees by strings but uses the coding scheme given there. Here we adapt the argument to the Catalan coding described in Section 3 to establish interpretability of theory ${\mathrm{T}}_{\le 2}$ of $\le 2$ -trees in ${\mathrm{QT}}^{+}$ . To define the domain of the interpretation we use the formula $\mathrm{I}^\ast (\mathrm{x})$ in the language of concatenation theory obtained in [3, Section 6], which defines the set of strings in ${\mathrm{QT}}^{+}$ . Let

$$\begin{align*}{\mathrm{I}}_{\le 2}(\mathrm{x})\equiv \mathrm{I}^\ast (\mathrm{x})\ \&\ \forall \mathrm{t}\;({\mathrm{Tally}}_{\mathrm{b}}(\mathrm{t})\ \&\ \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{x}\to \mathrm{t}=\mathrm{b}\;\mathrm{v}\;\mathrm{t}=\mathrm{b}\mathrm{b}).\end{align*}$$

We interpret $0$ by the digit $a$ , the function symbols ${\tau}_1$ and ${\tau}_2$ by setting

$$\begin{align*}{\tau}_1(\mathrm{x})=: \mathrm{bax}\quad {\tau}_2(\mathrm{x},\mathrm{y})=: \mathrm{bbaxy},\end{align*}$$

and let $\mathrm{x}\sqsubseteq \mathrm{y}$ be interpreted by the formula $\mathrm{x}=\mathrm{y}\;\mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}$ . Let ${\mathrm{A}}^{\kappa}$ be the corresponding ${{\mathcal{L}}}_{\mathrm{C}}$ -translation of a formula $\mathrm{A}$ of ${\mathrm{T}}_{\le 2}$ . Note that here, unlike in Section 2, we reason formally within the concatenation theory ${\mathrm{QT}}^{+}$ . Throughout this section we let $\mathrm{M}$ be an arbitrary model of ${\mathrm{QT}}^{+}$ .

First, some preliminaries.

5.1

(a) $\mathrm{QT}^{+}\vdash \forall \mathrm{x} \in \mathrm{I}^{\ast} \forall \mathrm{t,y,w,z}\; (\mathrm{Tally}_\mathrm{b}(\mathrm{t}) \ \&\ \mathrm{Tally}_\mathrm{a}(\mathrm{y}) \ \&\ \mathrm{x} = \mathrm{wyz} \ \&\ \mathrm{t} \subseteq_\mathrm{{p}} \mathrm{x} \rightarrow \mathrm{t}\subseteq_\mathrm{p} \mathrm{w\ v\ t} \subseteq_\mathrm{p} \mathrm{z}).$

(b) $\mathrm{QT}^{+}\vdash \mathrm{I}^{\ast}\mathrm{(x)} \ \&\ \mathrm{I}^{\ast}(\mathrm{y}) \ \&\ \mathrm{z} = \mathrm{bxy} \rightarrow \mathrm{I}^{\ast} (\mathrm{z}). $

(c) $\mathrm{QT}^{+}\vdash \mathrm{I}^{\ast}(\mathrm{x}) \ \&\ \mathrm{I}^{\ast}(\mathrm{y}) \rightarrow \neg \mathrm{xBy} \ \&\ \neg \mathrm{yBx}. $

(d) $\mathrm{QT}^{+}\vdash \mathrm{I}^{\ast}(\mathrm{x}) \ \&\ \mathrm{I}^{\ast}(\mathrm{y}) \rightarrow \neg \exists \mathrm{z} (\mathrm{zBx} \ \&\ \mathrm{zEy}). $

(e) $\mathrm{QT}^{+}\vdash \mathrm{I}^{\ast}(\mathrm{y}) \ \&\ \mathrm{I}^{\ast}(\mathrm{z}) \rightarrow \forall \mathrm{v,w} (\mathrm{v}\subseteq_\mathrm{p} \mathrm{z} \ \&\ \mathrm{wE} (\mathrm{bbayv}) \rightarrow \mathrm{wEv}\ \mathrm{v} \mathrm{w} = \mathrm{v\ v\ vEw}). $

(f) $\mathrm{QT}^{+}\vdash \mathrm{I}^{\ast}(\mathrm{z}) \rightarrow \forall \mathrm{u, v, w}\; (\mathrm{w}\subseteq_\mathrm{p} \mathrm{z} \ \&\ \mathrm{uw} = \mathrm{uw} \rightarrow \mathrm{u} = \mathrm{w}). $

(g) $\mathrm{QT}^{+}\vdash \mathrm{I}^{\ast}(\mathrm{x}) \rightarrow\neg (\mathrm{ax} \subseteq_\mathrm{p} \mathrm{x}). $

Proof For (a), see [2, 4.17(b)]; in [3] the formula $\mathrm{I}^\ast (\mathrm{x})$ is selected so as to ensure this property. Part (b) is proved as $(\mathrm{I}1)$ in [3, Section 6.1(c)]. Parts (c) and (d) are straightforwardly obtained from the definition of $\mathrm{I}^\ast$ in [3] (cf. 2.3(a) and (c)). For (e), assume $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{y})\ \&\ \mathrm{I}^\ast (\mathrm{z})$ . Then $\mathrm{M}\models \mathrm{J}^\ast (\mathrm{y})\ \&\ \mathrm{J}^\ast (\mathrm{z})$ , where $\mathrm{J}^\ast$ is the string form selected in [3, Section 6] that is closed under ${}^\ast$ and downward closed under ${\subseteq}_{\mathrm{p}}$ . Hence $\mathrm{M}\models \mathrm{J}^\ast (\mathrm{bbayz})$ . The claim follows from the fact that $\mathrm{J}^\ast$ was also selected to have the property described in (3.10) of [2]. The same proof for (f) and (g) taking into account (3.6) and (3.12) of [2].

5.2

(a) $\mathrm{QT}^{+}\vdash \mathrm{I}_{\leq 2}(\mathrm{x}) \ \&\ \mathrm{z} = \mathrm{bax} \rightarrow \mathrm{I}_{\leq 2} (\mathrm{z}).$

(b) $\mathrm{QT}^{+}\vdash \mathrm{I}_{\leq 2}(\mathrm{x}) \ \&\ \mathrm{I}_{\leq 2}(\mathrm{y})\ \&\ \mathrm{z} = \mathrm{bbaxy} \rightarrow \mathrm{I}_{\leq 2} (\mathrm{z}).$

Proof For (a), assume $\mathrm{M}\models {\mathrm{I}}_{\le 2}(\mathrm{x})\ \&\ \mathrm{z}=\mathrm{bax}$ . Then $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{x})$ . We have that $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{a})$ , by definition of $\mathrm{I}^\ast$ . By 5.1(b) we then have that $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{z})$ .

Assume now that $\mathrm{M}\models {\mathrm{Tally}}_{\mathrm{b}}(\mathrm{t})\ \&\ \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{z}$ . Then $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{bax}$ . But then, by 5.1(a) we have that $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{b}\;\mathrm{v}\;\mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{x}$ . Now, from $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{b}$ we have $\mathrm{M}\models \mathrm{t}=\mathrm{b}$ , and from $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{x}$ and hypothesis $\mathrm{M}\models {\mathrm{I}}_{\le 2}(\mathrm{x})$ we have $\mathrm{M}\models \mathrm{t}=\mathrm{b}\;\mathrm{v}\;\mathrm{t}=\mathrm{b}\mathrm{b}$ . Hence $\mathrm{M}\models \mathrm{t}=\mathrm{b}\;\mathrm{v}\;\mathrm{t}=\mathrm{b}\mathrm{b}$ , as required.

For (b), assume $\mathrm{M}\models {\mathrm{I}}_{\le 2}(\mathrm{x})\ \&\ {\mathrm{I}}_{\le 2}(\mathrm{y})\ \&\ \mathrm{z}=\mathrm{bbaxy}$ . Then $\mathrm{M}\models {\mathrm{I}}_{\le 2}(\mathrm{bax})$ by (a), so $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{bax})$ . From hypothesis $\mathrm{M}\models {\mathrm{I}}_{\le 2}(\mathrm{y})$ we have $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{y})$ . But then $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{z})$ by 5.1(b).

Assume now that $\mathrm{M}\models {\mathrm{Tally}}_{\mathrm{b}}(\mathrm{t})\ \&\ \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{z}$ . Then $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{bbaxy}$ . By 5.1(a), we have that $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{bb}\;\mathrm{v}\;\mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{xy}$ . If $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{bb}$ , then $\mathrm{M}\models \mathrm{t}=\mathrm{b}\;\mathrm{v}\;\mathrm{t}=\mathrm{b}\mathrm{b}$ . Suppose now that $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{xy}$ . From $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{x})$ we have that $\mathrm{M}\models \mathrm{x}=\mathrm{a}\;\mathrm{v}\;\mathrm{a}\mathrm{aEx}$ . If $\mathrm{M}\models \mathrm{x}=\mathrm{a}$ , then from $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{ay}$ we have $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{y}$ .

If $\mathrm{M}\models \mathrm{aaEx}$ , then $\mathrm{M}\models \exists {\mathrm{x}}_1\mathrm{x}={\mathrm{x}}_1\mathrm{aa}$ , so $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}({\mathrm{x}}_1\mathrm{aa})\mathrm{y}$ , whence $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_1\;\mathrm{v}\kern0.24em \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{y}$ . So from $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{xy}$ we have $\mathrm{M}\models \mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{x}\;\mathrm{v}\;\mathrm{t}{\subseteq}_{\mathrm{p}}\mathrm{y}$ , and thus from hypothesis $\mathrm{M}\models {\mathrm{I}}_{\le 2}(\mathrm{x})\ \&\ {\mathrm{I}}_{\le 2}(\mathrm{y})$ we obtain $\mathrm{M}\models \mathrm{t}=\mathrm{b}\;\mathrm{v}\;\mathrm{t}=\mathrm{b}\mathrm{b}$ , as required.

5.2 shows that the domain of the formal interpretation is closed under the concatenation operations chosen to interpret the tree-building functions ${\tau}_1$ and ${\tau}_2$ in ${\mathrm{T}}_{\le 2}$ . We next verify that the translations of the axioms of ${\mathrm{T}}_{\le 2}$ are derivable in ${\mathrm{QT}}^{+}$ . Here we have to make sure that the subtree relation in ${\mathrm{T}}_{\le 2}$ is adequately represented by the particular variant of subword relation between strings we chose above.

5.3.

(a) $\mathrm{QT}^{+}\vdash (\mathrm{T}4_1)^{\kappa}$ .

(b) $\mathrm{QT}^{+}\vdash (\mathrm{T}4_2)^{\kappa}$ .

(c) $\mathrm{QT}^{+}\vdash (\mathrm{T}6)^{\kappa}$ .

(d) $\mathrm{QT}^{+}\vdash (\mathrm{T}7)^{\kappa}$ .

(e) $\mathrm{QT}^{+}\vdash (\mathrm{T}8)^{\kappa}$ .

Proof (a) We show that

$\mathrm{QT}^+ {\kern-1.5pt}\vdash{\kern-1.5pt} \mathrm{I}_{\leq 2}(\mathrm{x}) \, \&\, \mathrm{I}_{\leq 2}(\mathrm{y}) {\kern-1.5pt}\rightarrow{\kern-1.5pt} (\mathrm{x}{\kern-1.5pt} ={\kern-1.5pt} \mathrm{bay}\, \mathrm{v}\, \mathrm{ax} \subseteq_\mathrm{p}\kern-3pt{\mathrm{bay}} \leftrightarrow \mathrm{x} = \mathrm{bay}\, \mathrm{v}\, \mathrm{x} {\kern-1.5pt}={\kern-1.5pt} \mathrm{y}\, \mathrm{v}\, \mathrm{ax}{\subseteq}_{\mathrm{p}}{\mathrm{y}}{\kern-1pt}). $ Assume $\mathrm{M}\models {\mathrm{I}}_{\le 2}(\mathrm{x})\ \&\ {\mathrm{I}}_{\le 2}(\mathrm{y})$ . Suppose that $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bay}$ . We can rule out $\mathrm{M}\models \mathrm{ax}=\mathrm{bay}\;\mathrm{v}\kern0.24em \mathrm{axBbay}$ immediately. Then we have $\mathrm{M}\models \mathrm{axEbay}\kern0.24em \mathrm{v}\ \exists {\mathrm{x}}_1,{\mathrm{x}}_2\;\mathrm{bay}={\mathrm{x}}_1(\mathrm{ax}){\mathrm{x}}_2$ , that is,

$$\begin{align*}\mathrm{M}\models \exists {\mathrm{x}}_1\mathrm{bay}={\mathrm{x}}_1(\mathrm{ax})\kern0.24em \mathrm{v}\ \exists {\mathrm{x}}_1,{\mathrm{x}}_2\;\mathrm{bay}={\mathrm{x}}_1(\mathrm{ax}){\mathrm{x}}_2.\end{align*}$$

Hence $\mathrm{M}\models \exists {\mathrm{x}}_1{\mathrm{x}}_1\mathrm{Bbay}$ . Now, we have that

$$\begin{align*}\mathrm{QT}^{+}\vdash \mathrm{zBbaw}\rightarrow \mathrm{z} = \mathrm{b\ v\ z} = \mathrm{ba\ v}\ \mathrm{baBz}\end{align*}$$

So $\mathrm{M}\models {\mathrm{x}}_1=\mathrm{b}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{x}}_1=\mathrm{b}\mathrm{a}\;\mathrm{v}\;{\mathrm{baBx}}_1$ . We distinguish the cases:

$$\begin{align*}\hspace{-136pt}(1)\hspace{136pt}\mathrm{M}\models {\mathrm{x}}_1=\mathrm{b}.\end{align*}$$

Then $\mathrm{M}\models \mathrm{bay}=\mathrm{b}\mathrm{ax}\kern0.24em \mathrm{v}\kern0.24em \mathrm{bay}=\mathrm{b}(\mathrm{ax}){\mathrm{x}}_2$ , whence $\mathrm{M}\models \mathrm{y}=\mathrm{x}\kern0.24em \mathrm{v}\kern0.24em \mathrm{y}={\mathrm{xx}}_2$ , so $\mathrm{M}\models \mathrm{y}=\mathrm{x}\;\mathrm{v}\;\mathrm{x}\mathrm{By}$ . But $\mathrm{M}\models \mathrm{xBy}$ is ruled out by $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{x})\ \&\ \mathrm{I}^\ast (\mathrm{y})$ and 5.1(c). Hence $\mathrm{M}\models \mathrm{x}=\mathrm{y}$ .

$$\begin{align*}\hspace{-135pt}(2)\hspace{135pt}\mathrm{M}\models {\mathrm{x}}_1=\mathrm{ba}.\end{align*}$$

Then $\mathrm{M}\models \mathrm{bay}=\mathrm{ba}(\mathrm{ax})\kern0.24em \mathrm{v}\;\;\mathrm{ba}\mathrm{y}=\mathrm{ba}(\mathrm{ax}){\mathrm{x}}_2$ , whence $\mathrm{M}\models \mathrm{y}=\mathrm{ax}\kern0.24em \mathrm{v}\kern0.24em \mathrm{y}={\mathrm{axx}}_2$ . But $\mathrm{M}\models \mathrm{aBy}$ contradicts $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{y})$ . So this case is ruled out.

$$\begin{align*}\hspace{-138.5pt}(3)\hspace{138.5pt}\mathrm{M}\models {\mathrm{baBx}}_1.\end{align*}$$

Then $\mathrm{M}\models \exists {\mathrm{x}}_3{\mathrm{x}}_1={\mathrm{bax}}_3$ , so $\mathrm{M}\models \mathrm{bay}={\mathrm{bax}}_3(\mathrm{ax})\kern0.24em \mathrm{v}\;\;\mathrm{bay}={\mathrm{bax}}_3(\mathrm{ax}){\mathrm{x}}_2$ , whence $\mathrm{M}\models \mathrm{y}={\mathrm{x}}_3(\mathrm{ax})\;\mathrm{v}\;\mathrm{y}={\mathrm{x}}_3(\mathrm{ax}){\mathrm{x}}_2$ . But then $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}$ .

Therefore, $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bay}\to \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}$ . Conversely, suppose $\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}$ . Then $\mathrm{M}\models \mathrm{ax}=\mathrm{ay}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}$ , whence $\mathrm{M}\models \mathrm{axEbay}\kern0.24em \mathrm{v} \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bay}$ , which yields $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bay}$ . Therefore we also have $\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}\to \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bay}$ . But then $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bay}\leftrightarrow \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}$ , and a fortiori, $\mathrm{M}\models \mathrm{x}=\mathrm{bay}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bay}\leftrightarrow \mathrm{x}=\mathrm{bay}\kern0.24em \mathrm{v}\kern0.24em \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}$ , as needed.

(b) We show that

$$\begin{align*}&\mathrm{QT}^{+}\vdash \mathrm{I}_{\leq2}(\mathrm{x}) \ \&\ \mathrm{I}_{\leq2} (\mathrm{y})\ \&\ \mathrm{I}_{\leq2} (\mathrm{z}) \rightarrow\\&\rightarrow (\mathrm{x} = \mathrm{bbayz}\ \mathrm{v}\ \mathrm{ax} \subseteq_{\mathrm{p}} \mathrm{bbayz} \leftrightarrow \mathrm{x} =\mathrm{bbayz}\ \mathrm{v}\\&\qquad \mathrm{v}\ (\mathrm{x} = \mathrm{y\ v\ ax} \subseteq_{\mathrm{p}} \mathrm{y}) \,\mathrm{v}\ (\mathrm{x} = \mathrm{z\ v\ ax}\subseteq_{\mathrm{p}} \mathrm{z})).\end{align*}$$

Assume $\mathrm{M}\models {\mathrm{I}}_{\le 2}(\mathrm{x})\ \&\ {\mathrm{I}}_{\le 2}(\mathrm{y})\ \&\ {\mathrm{I}}_{\le 2}(\mathrm{z})$ . Suppose that $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bbayz}$ . Again we can rule out $\mathrm{M}\models \mathrm{ax}=\mathrm{bbayz}\kern0.24em \mathrm{v}\kern0.24em \mathrm{axB}(\mathrm{bbayz})$ . So we are left with $\mathrm{M}\models \mathrm{axE}(\mathrm{bbayz})\kern0.24em \mathrm{v}\ \exists {\mathrm{x}}_1,{\mathrm{x}}_2\;\mathrm{bbayz}={\mathrm{x}}_1(\mathrm{ax}){\mathrm{x}}_2$ .

$$\begin{align*}\hspace{-125pt}(1)\hspace{125pt}\mathrm{M}\models \mathrm{axE}(\mathrm{bbayz}).\end{align*}$$

Then by 5.1(e), $\mathrm{M}\models \mathrm{axEz}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}=\mathrm{z}\kern0.24em \mathrm{v}\kern0.24em \mathrm{zEax}$ . If $\mathrm{M}\models \mathrm{axEz}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}=\mathrm{z}$ , then $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{z}$ , and we are done. So we may assume that $\mathrm{M}\models \mathrm{zEax}$ . Then $\mathrm{M}\models \exists {\mathrm{x}}_1\mathrm{ax}={\mathrm{x}}_1\mathrm{z}$ , whence $\mathrm{M}\models {\mathrm{x}}_1=\mathrm{a}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{aBx}}_1$ . If $\mathrm{M}\models {\mathrm{x}}_1=\mathrm{a}$ , then $\mathrm{M}\models \mathrm{ax}=\mathrm{az}$ , and we obtain $\mathrm{M}\models \mathrm{x}=\mathrm{z}$ , as needed. If $\mathrm{M}\models {\mathrm{aBx}}_1$ , then $\mathrm{M}\models \exists {\mathrm{x}}_2\ \mathrm{ax}={\mathrm{x}}_1\mathrm{z}=({\mathrm{ax}}_2)\mathrm{z}$ , whence $\mathrm{M}\models \mathrm{x}={\mathrm{x}}_2\mathrm{z}$ , and $\mathrm{M}\models {\mathrm{x}}_2\mathrm{Bx}$ .

From hypothesis $\mathrm{M}\models \mathrm{axE}(\mathrm{bbayz})$ , we have $\mathrm{M}\models \exists {\mathrm{z}}_1\;\mathrm{bbayz}={\mathrm{z}}_1\mathrm{a}\mathrm{x}={\mathrm{z}}_1\mathrm{a}({\mathrm{x}}_2\mathrm{z})$ .

By 5.1(f), we obtain $\mathrm{M}\models \mathrm{bbay}={\mathrm{z}}_1{\mathrm{ax}}_2$ , whence $\mathrm{M}\models {\mathrm{z}}_1=\mathrm{b}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{bBz}}_1$ . It follows that $\mathrm{M}\models \mathrm{bbay}={\mathrm{bax}}_2\;\mathrm{v}\kern0.24em \exists {\mathrm{z}}_2\;\mathrm{bbay}=({\mathrm{bz}}_2){\mathrm{ax}}_2$ , hence also $\mathrm{M}\models \mathrm{bay}={\mathrm{ax}}_2\;\mathrm{v}\kern0.24em \mathrm{bay}={\mathrm{z}}_2{\mathrm{ax}}_2$ . But $\mathrm{M}\models \mathrm{bay}={\mathrm{ax}}_2$ is ruled out. Hence $\mathrm{M}\models \mathrm{bay}={\mathrm{z}}_2{\mathrm{ax}}_2$ , and so $\mathrm{M}\models {\mathrm{x}}_2\mathrm{Ebay}$ . Now by 5.1(b), we have that $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{bay})$ since $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{a})\ \&\ \mathrm{I}^\ast (\mathrm{y})$ . But then $\mathrm{M}\models {\mathrm{x}}_2\mathrm{Bx}\ \&\ {\mathrm{x}}_2\mathrm{Ebay}$ contradicts $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{x})\ \&\ \mathrm{I}^\ast (\mathrm{y})$ by 5.1(d). Hence subcase $\mathrm{M}\models {\mathrm{aBx}}_1$ is ruled out.

$$\begin{align*}\hspace{-95pt}(2)\hspace{95pt}\mathrm{M}\models \exists {\mathrm{x}}_1,{\mathrm{x}}_2\;\mathrm{bbayz}={\mathrm{x}}_1(\mathrm{ax}){\mathrm{x}}_2.\end{align*}$$

Then by 5.1(e), $\mathrm{M}\models {\mathrm{x}}_2\mathrm{Ez}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{x}}_2=\mathrm{z}\;\mathrm{v}\;{\mathrm{zEx}}_2$ .

$$\begin{align*}\hspace{-120pt}(2\mathrm{a})\hspace{120pt}\mathrm{M}\models {\mathrm{zEx}}_2\mathrm{v}\;{\mathrm{x}}_2=\mathrm{z}.\end{align*}$$

Then $\mathrm{M}\models \exists {\mathrm{x}}_4{\mathrm{x}}_2={\mathrm{x}}_4\mathrm{z}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{x}}_2=\mathrm{z}$ , so $\mathrm{M}\models \mathrm{bbayz}={\mathrm{x}}_1\mathrm{ax}({\mathrm{x}}_4\mathrm{z})\kern0.24em \mathrm{v}\;\;\mathrm{bbayz}={\mathrm{x}}_1(\mathrm{ax})\mathrm{z}$ .

By 5.1(f), we have $\mathrm{M}\models \mathrm{bbay}={\mathrm{x}}_1{\mathrm{axx}}_4\;\mathrm{v}\kern0.24em \mathrm{bbay}={\mathrm{x}}_1(\mathrm{ax})$ , whence $\mathrm{M}\models {\mathrm{x}}_1=\mathrm{b}\;\mathrm{v}\;{\mathrm{bBx}}_1$ . It follows that

$$\begin{align*}\mathrm{M}\models \mathrm{bbay}={\mathrm{baxx}}_4\;\mathrm{v}\ \exists {\mathrm{x}}_3\mathrm{bbay}=({\mathrm{bx}}_3){\mathrm{axx}}_4\;\mathrm{v}\kern0.24em \mathrm{bbay}=\mathrm{b}(\mathrm{ax})\;\;\mathrm{v}\ \exists {\mathrm{x}}_3\mathrm{bbay}=({\mathrm{bx}}_3)\mathrm{ax},\end{align*}$$

Hence $\mathrm{M}\models \mathrm{bay}={\mathrm{axx}}_4\;\mathrm{v}\kern0.24em \mathrm{bay}={\mathrm{x}}_3{\mathrm{axx}}_4\;\mathrm{v}\kern0.24em \mathrm{bay}=\mathrm{ax}\kern0.24em \mathrm{v}\kern0.24em \mathrm{bay}={\mathrm{x}}_3\mathrm{ax}$ , whence $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bay}$ . Then $\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}$ follows as in 5.3(a).

$$\begin{align*}\hspace{-139pt}(2\mathrm{b})\hspace{139pt}\mathrm{M}\models {\mathrm{x}}_2\mathrm{Ez}.\end{align*}$$

Then $\mathrm{M}\models \exists {\mathrm{x}}_3\ \mathrm{z}={\mathrm{x}}_3{\mathrm{x}}_2$ ; thus $\mathrm{M}\models {\mathrm{x}}_3\mathrm{Bz}$ . Also, $\mathrm{M}\models \mathrm{bbay}({\mathrm{x}}_3{\mathrm{x}}_2)={\mathrm{x}}_1(\mathrm{ax}){\mathrm{x}}_2$ . Hence, by 5.1(f), $\mathrm{M}\models {\mathrm{bbayx}}_3={\mathrm{x}}_1(\mathrm{ax})$ . Then, by 5.1(e), $\mathrm{M}\models {\mathrm{x}}_3\mathrm{Ex}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{x}}_3=\mathrm{x}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{x}\mathrm{Ex}}_3$ .

$$\begin{align*}\hspace{-116pt}(2\mathrm{bi})\hspace{116pt}\mathrm{M}\models {\mathrm{x}}_3\mathrm{Ex}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{x}}_3=\mathrm{x}.\end{align*}$$

Then either way from $\mathrm{M}\models {\mathrm{x}}_3\mathrm{Bz}$ and $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{x})\ \&\ \mathrm{I}^\ast (\mathrm{z})$ we obtain a contradiction by 5.1(c) and 5.1(d). Hence subcase (2bi) is ruled out.

$$\begin{align*}\hspace{-134pt}(2\mathrm{bii})\hspace{134pt}\mathrm{M}\models {\mathrm{xEx}}_3.\end{align*}$$

Then $\mathrm{M}\models \exists {\mathrm{x}}_5\ {\mathrm{x}}_3={\mathrm{x}}_5\mathrm{x}$ , whence $\mathrm{M}\models {\mathrm{bbayx}}_5\mathrm{x}={\mathrm{x}}_1\mathrm{ax}$ . By 5.1(f), we have $\mathrm{M}\models {\mathrm{bbayx}}_5={\mathrm{x}}_1\mathrm{a}$ . Hence $\mathrm{M}\models {\mathrm{x}}_5=\mathrm{a}\;\mathrm{v}\;{\mathrm{aEx}}_5$ . Then from $\mathrm{M}\models {\mathrm{x}}_3={\mathrm{x}}_5\mathrm{x}$ , we obtain $\mathrm{M}\models {\mathrm{x}}_3=\mathrm{ax}\;\mathrm{v}\kern0.24em {\mathrm{axEx}}_3$ . From $\mathrm{M}\models {\mathrm{x}}_3\mathrm{Bz}$ , we obtain $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{z}$ , as needed.

This proves that $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bbayz}\to (\mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y})\;\mathrm{v}\;(\mathrm{x}=\mathrm{z}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{z})$ .

Conversely, suppose that $\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}$ . If $\mathrm{M}\models \mathrm{x}=\mathrm{y}$ , then $\mathrm{M}\models \mathrm{ax}=\mathrm{ay}$ , whence $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bb}(\mathrm{ay})\mathrm{z}$ . So $\mathrm{M}\models \mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}\to \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bbayz}$ . Likewise $\mathrm{M}\models \mathrm{x}=\mathrm{z}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{z}\to \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bbayz}$ . Therefore we also have

$$\begin{align*}\mathrm{M}\models (\mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y})\;\mathrm{v}\;(\mathrm{x}=\mathrm{z}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{z})\to \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bbayz}.\end{align*}$$

But then $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bbayz}\leftrightarrow (\mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y})\;\mathrm{v}\;(\mathrm{x}=\mathrm{z}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{z})$ , and finally $\mathrm{M}\models \mathrm{x}=\mathrm{bbayz}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{bbayz}\leftrightarrow \mathrm{x}=\mathrm{bbayz}\kern0.24em \mathrm{v}\;(\mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y})\;\mathrm{v} (\mathrm{x}=\mathrm{z}\;\mathrm{v}\;\mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{z}),$ as required.

(c) That $\mathrm{QT}^{+}\vdash \mathrm{I}_{\leq 2}(\mathrm{x}) \rightarrow \mathrm{x} = \mathrm{a\ v\ aa} \subseteq_\mathrm{p} \mathrm{x}$ is immediate from the definition of $\mathrm{I}^\ast (\mathrm{x})$ .

(d) We show that

$$\begin{align*}\mathrm{QT}^{+} \vdash \mathrm{I}_{\leq 2}(\mathrm{x}) \ \&\ \mathrm{I}_{\leq 2} (\mathrm{y}) \rightarrow ((\mathrm{x} = \mathrm{y\ v\ ax} \subseteq_\mathrm{p} \mathrm{y}) \ \&\ (\mathrm{y} = \mathrm{x\ v\ ay} \subseteq_\mathrm{p} \mathrm{x})\rightarrow \mathrm{x} = \mathrm{y})\end{align*}$$

Assume $\mathrm{M}\models {\mathrm{I}}_{\le 2}(\mathrm{x})\ \&\ {\mathrm{I}}_{\le 2}(\mathrm{y})$ , and suppose, for a reductio, that $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}\ \&\ \mathrm{ay}{\subseteq}_{\mathrm{p}}\mathrm{x}$ . Then $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}{\subseteq}_{\mathrm{p}}\mathrm{ay}{\subseteq}_{\mathrm{p}}\mathrm{x}$ . But this contradicts 5.1(g) since $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{x})$ . But then $\mathrm{M}\models (\mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y})\ \&\ (\mathrm{y}=\mathrm{x}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ay}{\subseteq}_{\mathrm{p}}\mathrm{x})\to \mathrm{x}=\mathrm{y}$ follows.

(e) We show that

$$\begin{align*}&\mathrm{QT}^{+}\vdash \mathrm{I}_{\leq2}(\mathrm{x}) \ \&\ \mathrm{I}_{\leq2} (\mathrm{y}) \ \&\ \mathrm{I}_{\leq2} (\mathrm{z}) \rightarrow\\&\rightarrow ((\mathrm{x} = \mathrm{y\ v\ ax} \subseteq_{\mathrm{p}} \mathrm{y}) \ \&\ (\mathrm{y} = \mathrm{z\ v\ ay} \subseteq_{\mathrm{p}} \mathrm{z}) \rightarrow (\mathrm{x} = \mathrm{z\ v\ ax} \subseteq_{\mathrm{p}} \mathrm{z})).\end{align*}$$

Assume $\mathrm{M}\models {\mathrm{I}}_{\le 2}(\mathrm{x})\ \&\ {\mathrm{I}}_{\le 2}(\mathrm{y})\ \&\ {\mathrm{I}}_{\le 2}(\mathrm{z})$ and suppose $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}\ \&\ \mathrm{ay}{\subseteq}_{\mathrm{p}}\mathrm{z}$ . Then $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}{\subseteq}_{\mathrm{p}}\mathrm{ay}{\subseteq}_{\mathrm{p}}\mathrm{z}$ , so $\mathrm{M}\models \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{z}$ . Then $\mathrm{M}\models (\mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y})\ \& (\mathrm{y}=\mathrm{z}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ay}{\subseteq}_{\mathrm{p}}\mathrm{z})\to (\mathrm{x}=\mathrm{z}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{z})$ , as needed.

From 5.2–5.3 we obtain:

Theorem 5.4. ${\mathrm{T}}_{\le 2}$ is interpretable in ${\mathrm{QT}}^{+}$ .

6 Mutual interpretability of finitely axiomatized tree theories

For each $\mathrm{m}\ge 2$ , we have that ${\mathrm{T}}_2$ is a subtheory of the theory of $\le \mathrm{m}$ -trees ${\mathrm{T}}_{\le \mathrm{m}}$ : so ${\mathrm{T}}_2{\le}_{\mathrm{I}}{\mathrm{T}}_{\le \mathrm{m}}$ . Now, ${\mathrm{T}}_{\le \mathrm{m}}$ allows any number $\le \mathrm{m}$ of immediate descendants. We wish to show that ${\mathrm{T}}_2{\le}_{\mathrm{I}}{\mathrm{T}}_{\mathrm{n}}$ for each $\mathrm{n}\ge 2$ , so that formal simulacra of dyadic trees can be systematically identified from among $\mathrm{n}$ -ary trees. Consider, for example, the dyadic trees ${\mathrm{b}}^2{\mathrm{a}}^2{\mathrm{b}}^2{\mathrm{a}\mathrm{b}}^2{\mathrm{a}}^4$ and ${\mathrm{b}}^2{\mathrm{a}\mathrm{b}}^2{\mathrm{a}}^3{\mathrm{b}}^2{\mathrm{a}}^2{\mathrm{b}}^2{\mathrm{a}}^3$ :

If we ignore the middle single-descendant branchings, we see that the ternary trees ${\mathrm{b}}^3{\mathrm{a}}^3{\mathrm{b}}^3{\mathrm{a}\mathrm{b}}^3{\mathrm{a}}^6$ and ${\mathrm{b}}^3{\mathrm{a}\mathrm{b}}^3{\mathrm{a}}^5{\mathrm{b}}^3{\mathrm{a}}^3{\mathrm{b}}^3{\mathrm{a}}^4$ reproduce their characteristic forms in the latters’ left and right branchings:

The same idea works with any $\mathrm{n}\ge 3$ , with $\mathrm{n}\hbox{--} 2$ singleton branchings instead. For fixed $\mathrm{n}\ge 2$ , we define a map on strings such that

$$\begin{align*}\xi(\mathrm{a})=\mathrm{a}\qquad \xi({\mathrm{b}}^2{\mathrm{a}\mathrm{x}}_1{\mathrm{x}}_2)={\mathrm{b}}^{\mathrm{n}}\mathrm{a}\xi ({\mathrm{x}}_1){\mathrm{a}}^{\mathrm{n}\hbox{--} 2}\xi ({\mathrm{x}}_2).\end{align*}$$

The operation is defined by recursion, by letting $\mathrm{p}=\mathrm{a}$ and $\mathrm{G}({\mathrm{y}}_1,{\mathrm{y}}_2,\mathrm{y})$ be the ${{\mathcal{L}}}_{\mathrm{C}}$ -formula $\exists {\mathrm{z}}_{1,}{\mathrm{z}}_2,{\mathrm{z}}_3(\mathrm{y}={\mathrm{b}}^{\mathrm{n}}{\mathrm{a}\mathrm{z}}_1\ \&\ {\mathrm{z}}_1={\mathrm{y}}_1{\mathrm{z}}_2\ \&\ {\mathrm{z}}_2= {\mathrm{a}}^{\mathrm{n}-2}{\mathrm{y}}_2)$ . Hence by Theorem 2.17 its graph is expressible in ${{\mathcal{L}}}_{\mathrm{C}}$ , and we have that

To define the formal interpretation of ${\mathrm{T}}_2$ in ${\mathrm{T}}_{\mathrm{n}}$ we let the domain be defined by the formula

$$\begin{align*}\mathrm{I}(\mathrm{x})\equiv \forall \mathrm{y}\;(\mathrm{y}\sqsubseteq \mathrm{x}\to \forall {\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}(\mathrm{y}={\tau}_{\mathrm{n}}({\mathrm{y}}_1,\dots, {\mathrm{y}}_{\mathrm{n}})\to {\wedge}_{1<\mathrm{i}<\mathrm{n}}\;{\mathrm{y}}_{\mathrm{i}}=0)),\end{align*}$$

and let $0$ be interpreted by $0$ , the binary operation ${\tau}_2(\mathrm{x},\mathrm{y})$ of ${\mathrm{T}}_2$ by ${\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y})$ , and the relational symbol $\sqsubseteq$ of ${\mathrm{T}}_2$ by $\sqsubseteq$ in ${\mathrm{T}}_{\mathrm{n}}$ . First we show that $\mathrm{I}(\mathrm{x})$ is closed, provably in ${\mathrm{T}}_{\mathrm{n}}$ , under the $\mathrm{n}$ -ary operation that is to serve as the interpretation of ${\tau}_2$ , and next we verify that the translations of the axioms of ${\mathrm{T}}_2$ are indeed deducible in ${\mathrm{T}}_{\mathrm{n}}$ . Throughout this section we let $\mathrm{M}$ be an arbitrary model of ${\mathrm{T}}_{\mathrm{n}}$ , for fixed $\mathrm{n}\ge 2$ .

6.1.

(a) For each $\mathrm{n}\ge 2$ , $\mathrm{T}_\mathrm{n} \vdash \mathrm{I}(\mathrm{x}) \ \&\ \mathrm{I}(\mathrm{y}) \ \&\ \mathrm{z} = \tau_\mathrm{n}(\mathrm{x}, 0,\ldots, 0,\mathrm{y})\rightarrow \mathrm{I}(\mathrm{z}). $ .

(b) For each $\mathrm{n}\ge 2$ ,

$$\begin{align*}\mathrm{T}_{\mathrm{n}}\vdash \mathrm{I}(\mathrm{x}) \ \&\ \mathrm{I}(\mathrm{y}) \ \&\ \mathrm{I}(\mathrm{z}) \rightarrow (\mathrm{z} \sqsubseteq \tau_{\mathrm{n}} (\mathrm{x}, 0,\ldots,0,\mathrm{y})\leftrightarrow \mathrm{z} = \tau_\mathrm{n} (\mathrm{x}, 0, \ldots, 0, \mathrm{y})\mathrm{v\ z} \sqsubseteq \mathrm{x\ v\ z} \sqsubseteq \mathrm{y}).\end{align*}$$

Proof (a) Assume that $\mathrm{M}\models \mathrm{z}={\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y})$ where $\mathrm{M}\models \mathrm{I}(\mathrm{x})\ \&\ \mathrm{I}(\mathrm{y})$ . Suppose $\mathrm{M}\models \mathrm{w}\sqsubseteq \mathrm{z}$ where $\mathrm{M}\models \mathrm{w}={\tau}_{\mathrm{n}}({\mathrm{w}}_1,{\mathrm{w}}_2,\dots, {\mathrm{w}}_{\mathrm{n}})$ . We need to show that $\mathrm{M}\models \wedge_{1<\mathrm{i}<\mathrm{n}}\;{\mathrm{w}}_{\mathrm{i}}=0$ . We have that $\mathrm{M}\models \mathrm{w}\sqsubseteq {\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y})$ . By $(\mathrm{T}{4}_{\mathrm{n}})$ , we get

$$\begin{align*}\mathrm{M}\models \mathrm{w}={\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y})\kern0.24em \mathrm{v}\;\;\mathrm{w}\sqsubseteq \mathrm{x}\;\;\mathrm{v}\;\;\mathrm{w}\sqsubseteq 0\;\mathrm{v}\dots \mathrm{v}\;\mathrm{w}\sqsubseteq 0\;\;\mathrm{v}\;\;\mathrm{w}\sqsubseteq \mathrm{y}).\end{align*}$$

We distinguish the cases:

(i) $\mathrm{M}\models \mathrm{w}={\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y}).$

Then from $\mathrm{M}\models \mathrm{w}={\tau}_{\mathrm{n}}({\mathrm{w}}_1,{\mathrm{w}}_2,\dots, {\mathrm{w}}_{\mathrm{n}})$ , by $(\mathrm{T}{3}_{\mathrm{n}})$ , we have $\mathrm{M}\models \wedge_{1<\mathrm{i}<\mathrm{n}}\;{\mathrm{w}}_{\mathrm{i}}=0$ .

(ii) $\mathrm{M}\models \mathrm{w}\sqsubseteq \mathrm{x}$ .

Then from $\mathrm{M}\models \mathrm{I}(\mathrm{x})\ \&\ \mathrm{w}={\tau}_{\mathrm{n}}({\mathrm{w}}_1,{\mathrm{w}}_2,\dots, {\mathrm{w}}_{\mathrm{n}})$ we have $\mathrm{M} \models \wedge_{1<\mathrm{i}<\mathrm{n}} {\mathrm{w}}_{\mathrm{i}}=0$ .

(iii) $\mathrm{M}\models \mathrm{w}\sqsubseteq 0$ .

Then from $(\mathrm{T}6)$ and $(\mathrm{T}7)$ , we have $\mathrm{M}\models \mathrm{w}=0$ . But this contradicts hypothesis $\mathrm{M}\models \mathrm{w}={\tau}_{\mathrm{n}}({\mathrm{w}}_1,{\mathrm{w}}_2,\dots, {\mathrm{w}}_{\mathrm{n}})$ by $(\mathrm{T}{1}_{\mathrm{n}})$ . Hence each of these $\mathrm{n}\hbox{--} 2$ cases is ruled out.

(iv) $\mathrm{M}\models \mathrm{w}\sqsubseteq \mathrm{y}$ .

Exactly analogous to (ii).

With (i)–(iv) we have that

$$\begin{align*}\mathrm{M}\models \forall \mathrm{w}\;(\mathrm{w}\sqsubseteq \mathrm{z}\to \forall {\mathrm{w}}_1\dots {\mathrm{w}}_{\mathrm{n}}(\mathrm{w}={\tau}_{\mathrm{n}}({\mathrm{w}}_1,\dots, {\mathrm{w}}_{\mathrm{n}})\to {\wedge}_{1<\mathrm{i}<\mathrm{n}}\;{\mathrm{w}}_{\mathrm{i}}=0)),\end{align*}$$

which means that $\mathrm{M}\models \mathrm{I}(\mathrm{z})$ .

(b) Assume $\mathrm{M}\models \mathrm{I}(\mathrm{x})\ \&\ \mathrm{I}(\mathrm{y})\ \&\ \mathrm{I}(\mathrm{z})$ , and let $\mathrm{M}\models \mathrm{z}\sqsubseteq {\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y})$ . Then we have, by $(\mathrm{T}{4}_{\mathrm{n}})$ , $\mathrm{M}\models \mathrm{z}={\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y})\kern0.24em \mathrm{v}\;\;\mathrm{z}\sqsubseteq \mathrm{x}\;\;\mathrm{v}\;\;\mathrm{z}\sqsubseteq 0\;\mathrm{v}\dots \mathrm{v}\;\;\mathrm{z}\sqsubseteq 0\;\;\mathrm{v}\;\;\mathrm{z}\sqsubseteq \mathrm{y}$ .

Now, suppose $\mathrm{M}\models \mathrm{z}\sqsubseteq 0$ . Then, by $(\mathrm{T}6)$ and $(\mathrm{T}7)$ , we have $\mathrm{M}\models \mathrm{z}=0$ . But then, again by $(\mathrm{T}6)$ , $\mathrm{M}\models \mathrm{z}\sqsubseteq \mathrm{x}$ . Hence $\mathrm{M}\models \mathrm{z}\sqsubseteq 0\to \mathrm{z}\sqsubseteq \mathrm{x}$ , and so we have, under hypothesis $\mathrm{M}\models \mathrm{z}\sqsubseteq {\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y})$ , that in fact

$$\begin{align*}\mathrm{M}\models \mathrm{z}={\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y})\;\mathrm{v}\;\mathrm{z}\sqsubseteq \mathrm{x}\;\mathrm{v}\;\mathrm{z}\sqsubseteq \mathrm{y}.\end{align*}$$

Therefore, $\mathrm{M}\models \mathrm{z}\sqsubseteq {\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y})\to \mathrm{z}={\tau}_{\mathrm{n}}(\mathrm{x},0,\dots, 0,\mathrm{y})\kern0.24em \mathrm{v}\;\;\mathrm{z}\sqsubseteq \mathrm{x}\;\;\mathrm{v} \mathrm{z}\sqsubseteq \mathrm{y}$ .

The converse follows from $(\mathrm{T}{4}_{\mathrm{n}})$ .⊣

We then obtain:

Theorem 6.2. For each $\mathrm{n}\ge 2$ , ${\mathrm{T}}_2{\le}_{\mathrm{I}}{\mathrm{T}}_{\mathrm{n}}$ .

On the other hand, since ${\mathrm{T}}_{\mathrm{n}}$ is a subtheory of ${\mathrm{T}}_{\le \mathrm{n}}$ , we have that ${\mathrm{T}}_{\mathrm{n}}{\le}_{\mathrm{I}}{\mathrm{T}}_{\le \mathrm{n}}$ . By Theorem 4.2, for each $\mathrm{n}\ge 2$ , also ${\mathrm{T}}_{\le \mathrm{n}}{\le}_{\mathrm{I}}{\mathrm{T}}_{\le 2}$ , and by Theorem 5.4 we have that ${\mathrm{T}}_{\le 2}{\le}_{\mathrm{I}}{\mathrm{QT}}^{+}$ .

In [3], we have established that the concatenation theory ${\mathrm{QT}}^{+}$ is formally interpretable in the theory of dyadic trees, so ${\mathrm{QT}}^{+}{\le}_{\mathrm{I}}{\mathrm{T}}_2$ . Putting all this together, we obtain:

Theorem 6.3. For each $\mathrm{n}\ge 2$ , ${\mathrm{T}}_{\le \mathrm{n}}{\equiv}_{\mathrm{I}}{\mathrm{T}}_{\le 2}{\equiv}_{\mathrm{I}}{\mathrm{T}}_2{\equiv}_{\mathrm{I}}{\mathrm{T}}_{\mathrm{n}}$ .

7 Interpreting $\mathrm{T}^\ast$ in ${\mathrm{QT}}^{+}$

We now let all strings into play and have $\mathrm{I}^\ast (\mathrm{x})$ define the domain of the interpretation. Again, $0$ is interpreted by the digit $a$ , and $\mathrm{x}\sqsubseteq \mathrm{y}$ by the formula $\mathrm{x}=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em \mathrm{ax}{\subseteq}_{\mathrm{p}}\mathrm{y}$ . We use the relational formulation of the axioms of $\mathrm{T}^\ast$ given in Section 4 and interpret the ( $\mathrm{n}+1$ )-place relational symbols ${\mathrm{T}}_{\mathrm{n}}$ for $\mathrm{n}\ge 1$ by setting ${\mathrm{T}}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}},\mathrm{x})\equiv {\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}=\mathrm{x}$ . Essentially, we are interpreting, for each fixed $\mathrm{n}$ , the function symbol for the $\mathrm{n}$ -ary tree-building operation ${\tau}_{\mathrm{n}}({\mathrm{x}}_1,\dots, {\mathrm{x}}_{\mathrm{n}})$ by the concatenation operation ${\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}$ . We let $\mathrm{M}$ be an arbitrary model of ${\mathrm{QT}}^{+}$ . Again, we’ll need some preliminaries:

7.1.

(a) $\mathrm{QT}^+ \vdash \mathrm{J}^{\ast} (\mathrm{z})\rightarrow \forall \mathrm{x,y}(\mathrm{xBz} \ \&\ \mathrm{yBz} \rightarrow \mathrm{xBy\ v\ x} = \mathrm{y\ v\ ybx}).$

(b) $\mathrm{QT}^+ \vdash \mathrm{J}^{\ast} (\mathrm{z})\rightarrow \forall \mathrm{x,y}(\mathrm{x}\mathrm{E}\mathrm{z} \ \&\ \mathrm{yEz} \rightarrow \mathrm{xEy\ v\ x} = \mathrm{y\ v\ yEx}).$

(c) $\mathrm{QT}^+ \vdash \mathrm{J}^{\ast} (\mathrm{y}) \ \&\ \mathrm{J}^{\ast} (\mathrm{z}) \rightarrow \forall \mathrm{x}(\mathrm{xByz} \leftrightarrow \mathrm{xBy\ v\ x} = \mathrm{y\ v}\ \exists \mathrm{w}(\mathrm{wBz} \ \&\ \mathrm{yw} = \mathrm{x})).$

(d) $\mathrm{QT}^+ \vdash \mathrm{J}^{\ast} (\mathrm{x}) \ \&\ \mathrm{J}^{\ast} (\mathrm{y}) \rightarrow \forall \mathrm{u}(\mathrm{uBb}(\mathrm{xy}) \rightarrow \mathrm{u} = \mathrm{b\ v\ uBbx\ v\ u} = \mathrm{bx\ v}\ \exists \mathrm{y}_1 (\mathrm{y}_1\mathrm{By} \ \&\ \mathrm{u} =\mathrm{bxy}_1) ).$

(e) For each $\mathrm{n}\ge 1$ ,

$$\begin{align*}\mathrm{QT}^{+}\vdash &\wedge_{1\leq \mathrm{i}\leq \mathrm{n}}\; \mathrm{J}^{\ast} (\mathrm{x}_\mathrm{i}) \rightarrow \forall \mathrm{w} (\mathrm{wBb}^\mathrm{n} \mathrm{ax}_{1}\ldots \mathrm{x}_\mathrm{n} \rightarrow \mathrm{wBb}^{\mathrm{n}} \mathrm{v\ w} = \mathrm{b}^\mathrm{n}\ \mathrm{v}\\&\mathrm{v\ w} = \mathrm{b}^\mathrm{n} \mathrm{a}\ \mathrm{v}\ \exists \mathrm{z}_1(\mathrm{z}_1 \mathrm{Bx}_1 \ \&\ \mathrm{w} = \mathrm{b}^\mathrm{n} \mathrm{az}_1)\ \mathrm{v} \vee_{1\leq \mathrm{i}\leq \mathrm{n}} \mathrm{w} = \mathrm{b}^\mathrm{n} \mathrm{ax}_1\ldots \mathrm{x}_\mathrm{i}\ \mathrm{v}\\&\quad \qquad\mathrm{v} \vee_{1\leq \mathrm{i}\leq \mathrm{n}} \exists \mathrm{z}_1(\mathrm{z}_\mathrm{i} \mathrm{Bx}_\mathrm{i} \ \&\ \mathrm{w} = \mathrm{b}^\mathrm{n} \mathrm{ax}_1 \ldots \mathrm{x}_{\mathrm{i}-1}\mathrm{z}_\mathrm{i})).\end{align*}$$

Proof For (a) and (b), see the proof of 5.1(e)–(g), this time with reference to (3.8) of [2] for (a) and (3.10) for (b). For (c) and (d), see [3, 3.7(b) and (c)]. We focus on (e), arguing by induction on $\mathrm{n}$ . Assume that $\mathrm{M} \models \wedge_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{J}^\ast ({\mathrm{x}}_{\mathrm{i}})$ . For $\mathrm{n}=1$ , we have from (d) that

$$\begin{align*}\mathrm{QT}^{+}\vdash \mathrm{wBbax}_1 \rightarrow \mathrm{w} = \mathrm{b\ v\ wBba\ v} = \mathrm{ba\ v}\ \exists \mathrm{z}_1 (\mathrm{z}_1 \mathrm{Bx}_1 \ \&\ \mathrm{w} = \mathrm{baz}_1).\end{align*}$$

Now, $\mathrm{QT}^{+} \vdash \mathrm{wBba} \rightarrow \mathrm{w} = \mathrm{b}$ and $\mathrm{QT}^{+} \vdash \neg \mathrm{wBba} $ , so in fact we have that

$$\begin{align*}\mathrm{QT}^{+}\vdash \mathrm{wBbax}_1 \rightarrow \mathrm{w} = \mathrm{b\ v\ w} = \mathrm{ba\ v}\ \exists \mathrm{z}_1 (\mathrm{z}_1 \mathrm{Bx}_1 \ \&\ \mathrm{w} = \mathrm{baz}_1),\end{align*}$$

as needed. Assume now that the claim holds for $\mathrm{k}$ . We then have that

$$\begin{align*} \begin{array}{l}\mathrm{M}\models {\mathrm{wBb}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}}\to {\mathrm{wBb}}^{\mathrm{k}}\kern0.24em \mathrm{v}\kern0.24em \mathrm{w}={\mathrm{b}}^{\mathrm{k}}\kern0.24em \mathrm{v}\kern0.24em \mathrm{w}={\mathrm{b}}^{\mathrm{k}}\mathrm{a}\kern0.24em \mathrm{v}\ \exists {\mathrm{z}}_1({\mathrm{z}}_1{\mathrm{Bx}}_1\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{k}}{\mathrm{az}}_1)\;\;\mathrm{v}\\ {}\mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}<\mathrm{k}}\mathrm{w}={\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}}\kern0.24em \mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}\le \mathrm{k}}\exists {\mathrm{z}}_{\mathrm{i}}({\mathrm{z}}_{\mathrm{i}}{\mathrm{Bx}}_{\mathrm{i}}\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}-1}{\mathrm{z}}_{\mathrm{i}}).\end{array}\end{align*}$$

Assume $\mathrm{M}\models \mathrm{wBb}(({\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}}){\mathrm{x}}_{\mathrm{k}+1})$ . By (d),

$$\begin{align*} \mathrm{M}\models \mathrm{w}&=\mathrm{b}\kern0.24em \mathrm{v}\kern0.24em \mathrm{w}\mathrm{Bb}({\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}})\;\;\mathrm{v}\kern0.24em \mathrm{w}=\mathrm{b}({\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}})\;\mathrm{v}\\ &\qquad\!\!\!\mathrm{v}\;\exists {\mathrm{z}}_{\mathrm{k}+1}({\mathrm{z}}_{\mathrm{k}+1}{\mathrm{Bx}}_{\mathrm{k}+1}\ \&\ \mathrm{w}=\mathrm{b}({\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}}){\mathrm{z}}_{\mathrm{k}+1}).\end{align*}$$

From $\mathrm{M}\models \mathrm{w}=\mathrm{b}$ , we have $\mathrm{M}\models \mathrm{wBb}({\mathrm{b}}^{\mathrm{k}})$ , i.e., $\mathrm{M}\models {\mathrm{wBb}}^{\mathrm{k}+1}$ .

Suppose that $\mathrm{M}\models \mathrm{wBb}({\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}})$ . By (c), then

$$\begin{align*}\mathrm{M}\models \mathrm{wBb}\kern0.24em \mathrm{v}\kern0.24em \mathrm{w}=\mathrm{b}\kern0.24em \mathrm{v}\;\exists \mathrm{z}({\mathrm{zBb}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}}\ \&\ \mathrm{bz}=\mathrm{w}).\end{align*}$$

But $\mathrm{QT}^{+}\vdash \neg \mathrm{wBb}$ , and we have $\mathrm{M}\models \mathrm{w}=\mathrm{b}\to {\mathrm{wBb}}^{\mathrm{k}+1}$ . Given the inductive hypothesis, we have from $\mathrm{M}\models {\mathrm{zBb}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}}\ \&\ \mathrm{bz}=\mathrm{w}$ that

$$\begin{align*} \begin{array}{l}\mathrm{M}\models {\mathrm{z}\mathrm{Bb}}^{\mathrm{k}}\kern0.24em \mathrm{v}\kern0.24em \mathrm{z}={\mathrm{b}}^{\mathrm{k}}\;\mathrm{v}\kern0.24em \mathrm{z}={\mathrm{b}}^{\mathrm{k}}\mathrm{a}\kern0.24em \mathrm{v}\;\exists {\mathrm{z}}_1({\mathrm{z}}_1{\mathrm{Bx}}_1\ \&\ \mathrm{z}={\mathrm{b}}^{\mathrm{k}}{\mathrm{az}}_1)\;\;\mathrm{v}\\ {}\mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}<\mathrm{k}}\mathrm{z}={\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}}\kern0.24em \mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}\le \mathrm{k}}\exists {\mathrm{z}}_{\mathrm{i}}({\mathrm{z}}_{\mathrm{i}}{\mathrm{Bx}}_{\mathrm{i}}\ \&\ \mathrm{z}={\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}-1}{\mathrm{z}}_{\mathrm{i}}).\end{array}\end{align*}$$

Now, it is easily seen that $\mathrm{M}\models \mathrm{bz}=\mathrm{w}\ \&\ {\mathrm{zBb}}^{\mathrm{k}}\to {\mathrm{wBb}}^{\mathrm{k}+1}\kern0.24em \mathrm{and}\kern0.24em \mathrm{M}\models \mathrm{bz}=\mathrm{w}\ \&\ \mathrm{z}={\mathrm{b}}^{\mathrm{k}}\to \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1},$ and also that $\mathrm{M}\models \mathrm{bz}=\mathrm{w}\ \&\ \mathrm{z}={\mathrm{b}}^{\mathrm{k}}\mathrm{a}\to \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1}\mathrm{a}.$

Furthermore, $\mathrm{M}\models \mathrm{bz}=\mathrm{w}\ \&\ \exists {\mathrm{z}}_1({\mathrm{z}}_1{\mathrm{Bx}}_1\ \&\ \mathrm{z}={\mathrm{b}}^{\mathrm{k}}{\mathrm{az}}_1)\to \exists {\mathrm{z}}_1({\mathrm{z}}_1{\mathrm{Bx}}_1\ \&\ \mathrm{w} ={\mathrm{b}}^{\mathrm{k}+1}{\mathrm{az}}_1)$ and $\mathrm{M}\models \mathrm{bz}=\mathrm{w}\ \&\ \mathrm{z}={\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\to \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1}{\mathrm{ax}}_1$ , and so on, plus $\mathrm{M}\models \mathrm{bz}=\mathrm{w}\ \&\ \exists {\mathrm{z}}_{\mathrm{k}}({\mathrm{z}}_{\mathrm{k}}{\mathrm{Bx}}_{\mathrm{k}}\ \&\ \mathrm{z}={\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}-1}{\mathrm{z}}_{\mathrm{k}})\to \exists {\mathrm{z}}_{\mathrm{k}}({\mathrm{z}}_{\mathrm{k}}{\mathrm{Bx}}_{\mathrm{k}}\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1} {\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}-1}{\mathrm{z}}_{\mathrm{k}}).$

Thus we have

$$\begin{align*} \begin{array}{l}\mathrm{M}\models \mathrm{wBb}({\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}})\to {\mathrm{wBb}}^{\mathrm{k}+1}\kern0.24em \mathrm{v}\kern0.24em \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1}\kern0.24em \mathrm{v}\kern0.24em \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1}\mathrm{a}\;\mathrm{v}\\ {}\mathrm{v}\;\exists {\mathrm{z}}_1({\mathrm{z}}_1{\mathrm{Bx}}_1\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1}{\mathrm{az}}_1)\;\;\mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}<\mathrm{k}}\mathrm{w}={\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}}\;\mathrm{v}\\ {}\mathrm{v}\;{\vee}_{1\le \mathrm{i}\le \mathrm{k}}\exists {\mathrm{z}}_{\mathrm{i}}({\mathrm{z}}_{\mathrm{i}}{\mathrm{Bx}}_{\mathrm{i}}\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}-1}{\mathrm{z}}_{\mathrm{i}}).\end{array}\end{align*}$$

But then

$$\begin{align*} \begin{array}{l}\mathrm{M}\models \mathrm{wBb}(({\mathrm{b}}^{\mathrm{k}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}}){\mathrm{x}}_{\mathrm{k}+1})\to {\mathrm{wBb}}^{\mathrm{k}+1}\kern0.24em \mathrm{v}\kern0.24em \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1}\kern0.24em \mathrm{v}\kern0.24em \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1}\mathrm{a}\;\mathrm{v}\\ {}\mathrm{v}\;\exists {\mathrm{z}}_1({\mathrm{z}}_1{\mathrm{Bx}}_1\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1}{\mathrm{az}}_1)\;\;\mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}<\mathrm{k}+1}\mathrm{w}={\mathrm{b}}^{\mathrm{k}+1}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}}\;\mathrm{v}\\ {}\mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}\le \mathrm{k}+1}\exists {\mathrm{z}}_{\mathrm{i}}({\mathrm{z}}_{\mathrm{i}}{\mathrm{Bx}}_{\mathrm{i}}\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{k}+1}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}-1}{\mathrm{z}}_{\mathrm{i}}).\end{array}\end{align*}$$

as required.

We then have:

7.2

(a) $\mathrm{QT}^{+}\vdash \neg (\mathrm{b}^\mathrm{n} \mathrm{ax}_1 \ldots \mathrm{x}_\mathrm{n} = \mathrm{a}) $ .

(b) For $1\le \mathrm{m}<\mathrm{n}$ , $\mathrm{QT}^{+}\vdash \neg (\mathrm{b}^\mathrm{m} \mathrm{ax}_1 \ldots \mathrm{x}_\mathrm{m} = \mathrm{b}^\mathrm{n} \mathrm{ay}_1\ldots \mathrm{y}_\mathrm{n}) $ .

(c) $\mathrm{QT}^{+}\vdash \wedge_{1\leq \mathrm{i}\leq \mathrm{n}} \mathrm{I}^{\ast}(\mathrm{x}_\mathrm{i})\ \&\ \wedge_{1\leq \mathrm{i}\leq \mathrm{n}} \mathrm{I}^{\ast} (\mathrm{y}_1) \rightarrow$ $\rightarrow (\mathrm{b}^\mathrm{n} \mathrm{ax}_1\ldots \mathrm{x}_\mathrm{n} = \mathrm{b}^\mathrm{n} \mathrm{ay}_1\ldots \mathrm{y}_\mathrm{n}\rightarrow \wedge_{1\leq \mathrm{i}\leq \mathrm{n}}\ \mathrm{x}_\mathrm{i} = \mathrm{y}_\mathrm{i}).$

(d) $\mathrm{QT}^{+}\vdash \wedge_{1\leq \mathrm{i}\leq \mathrm{n}} \mathrm{I}^{\ast}(\mathrm{x}_\mathrm{i})\ \&\ \mathrm{x} = \mathrm{b}^\mathrm{n} \mathrm{ax}_1\ldots \mathrm{x}_\mathrm{n}\rightarrow \mathrm{I}^{\ast}(\mathrm{x}).$

(e) $\mathrm{QT}^{+}\vdash \wedge_{1\leq \mathrm{i}\leq \mathrm{n}} \mathrm{I}^{\ast}(\mathrm{x}_\mathrm{i})\ \&\ \mathrm{I}^{\ast}(\mathrm{y}) \rightarrow (\mathrm{y} = \mathrm{b}^\mathrm{n} \mathrm{ax}_1 \ldots \mathrm{x}_\mathrm{n} \mathrm{v\ ay} \subseteq_\mathrm{p} \mathrm{b}^\mathrm{n} \mathrm{ax}_1 \ldots \mathrm{x}_\mathrm{n}$ $\leftrightarrow \mathrm{y} = \mathrm{b}^\mathrm{n} \mathrm{ax}_1 \ldots \mathrm{x}_\mathrm{n} \mathrm{v} \vee_{1\leq \mathrm{i}\leq \mathrm{n}}\ (\mathrm{y} = \mathrm{x}_\mathrm{i}\ \mathrm{v\ ay}\kern-3pt\subseteq_\mathrm{p} \mathrm{x}_\mathrm{i})).$

Proof (b) Suppose, for a reductio, that $\mathrm{M}\models {\mathrm{b}}^{\mathrm{m}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{m}}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ where $\mathrm{m}<\mathrm{n}$ . After m applications of $(\mathrm{QT}3)$ we obtain $\mathrm{M}\models {\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{m}}={\mathrm{b}}^{\mathrm{m}-\mathrm{n}}{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ contradicting $(\mathrm{QT}4)$ .

(c) Assume $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ay}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ where $\mathrm{M}\models \wedge_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{I}^\ast ({\mathrm{x}}_{\mathrm{i}})\ \& {\wedge}_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{I}^\ast ({\mathrm{y}}_{\mathrm{i}})$ . We formalize the reasoning of 2.4 in ${\mathrm{QT}}^{+}$ . After $\mathrm{n}+1$ applications of $(\mathrm{QT}3)$ we obtain $\mathrm{M}\models {\mathrm{x}}_1\dots {\mathrm{x}}_{\mathrm{n}}={\mathrm{y}}_1\dots {\mathrm{y}}_{\mathrm{n}}$ . We have that $\mathrm{M}\models \mathrm{J}^\ast ({\mathrm{x}}_1\dots {\mathrm{x}}_{\mathrm{n}})$ where $\mathrm{J}^\ast (\mathrm{x})$ is the string form constructed in [3, Section 6], and $\mathrm{M}\models {\mathrm{x}}_1\mathrm{B}({\mathrm{x}}_1\dots {\mathrm{x}}_{\mathrm{n}})\ \&\ {\mathrm{y}}_1\mathrm{B}({\mathrm{x}}_1\dots {\mathrm{x}}_{\mathrm{n}})$ . By 7.1(a), $\mathrm{M}\models {\mathrm{x}}_1{\mathrm{By}}_1\;\mathrm{v}\kern0.24em {\mathrm{x}}_1={\mathrm{y}}_1\;\mathrm{v}\kern0.24em {\mathrm{y}}_1{\mathrm{Bx}}_1$ . By 5.1(c), $\mathrm{M}\models \neg {\mathrm{x}}_1{\mathrm{By}}_1\ \&\ \neg {\mathrm{y}}_1{\mathrm{Bx}}_1$ . But then $\mathrm{M}\models {\mathrm{x}}_1={\mathrm{y}}_1$ . The rest of the proof follows the pattern of 2.4.

(d) For this we need to formalize the proof of 2.7 in ${\mathrm{QT}}^{+}$ . The proof has two parts: first we show in ${\mathrm{QT}}^{+}$ that under the hypothesis ${\wedge}_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{I}^\ast ({\mathrm{x}}_{\mathrm{i}})$ we have $(\mathrm{ci})\;\alpha (\mathrm{x})=\beta (\mathrm{x})+1$ , and, secondly, (cii) $\forall \mathrm{w}\big(\mathrm{w}\mathrm{Bx}\to \alpha (\mathrm{w})\le \beta (\mathrm{w})$ . In [3, Section 5], we have shown that the graphs of the counting functions $\alpha$ and $\beta$ are expressible by ${{\mathcal{L}}}_{\mathrm{C}}$ -formulae ${\mathrm{A}}^{\#}(\mathrm{x},\mathrm{y})$ and ${\mathrm{B}}^{\#}(\mathrm{x},\mathrm{y})$ , respectively, and that their fundamental properties, including additivity, are provable in ${\mathrm{QT}}^{+}$ modulo the method of formula selection explained there. These functions take finite strings as arguments and yield natural numbers as values. In the formal definition of their graphs in [3], the numerical values are represented by $\mathrm{b}$ -tallies, and a key role is played by the relation $\mathrm{Addtally}(\mathrm{x},\mathrm{y},\mathrm{z})$ between $\mathrm{b}$ -tallies that behaves like addition on natural numbers. (See [3, Section 3] for the relevant properties of Addtally and the associated relation $\le$ between $\mathrm{b}$ -tallies.) With this machinery in place, it is a straightforward exercise in proof formalization to show, following the computation in the first part of the proof of 2.7, that for each $\mathrm{n}\ge 1$ ,

$$\begin{align*}\mathrm{QT}^{+}\vdash \wedge_{1\leq \mathrm{i} \leq \mathrm{n}}\mathrm{I}^{\ast} (\mathrm{x}_\mathrm{i}) \& & \mathrm{x} = \mathrm{b}^\mathrm{n} \mathrm{ax}_1\ldots \mathrm{x}_\mathrm{n} \rightarrow (\mathrm{A}^{\#}(\mathrm{x},\mathrm{u}) \ \&\ \mathrm{B}^{\#} (\mathrm{x},\mathrm{v}) \rightarrow \mathrm{u} = \mathrm{Sv})\end{align*}$$

i.e., that (ci) holds. For (cii), assume that $\mathrm{M}\models \mathrm{wBx}\ \&\ {\mathrm{A}}^{\#}(\mathrm{x},\mathrm{u})\ \&\ {\mathrm{B}}^{\#}(\mathrm{x},\mathrm{v})$ ,

where $\mathrm{M}\models \wedge_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{I}^\ast ({\mathrm{x}}_{\mathrm{i}})\ \&\ \mathrm{x}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}$ . From 7.1(e) we have that

$$\begin{align*} \begin{array}{l}\mathrm{M}\models {\mathrm{wBb}}^{\mathrm{n}}\;\mathrm{v}\kern0.24em \mathrm{w}={\mathrm{b}}^{\mathrm{n}}\;\mathrm{v}\kern0.24em \mathrm{w}={\mathrm{b}}^{\mathrm{n}}\mathrm{a}\kern0.24em \mathrm{v}\exists {\mathrm{z}}_1({\mathrm{z}}_1{\mathrm{Bx}}_1\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{n}}{\mathrm{az}}_1)\;\;\mathrm{v}\\ {}\mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}<\mathrm{n}}\mathrm{w}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}}\kern0.24em \mathrm{v}\kern0.24em {\vee}_{1\le \mathrm{i}\le \mathrm{n}}\exists {\mathrm{z}}_{\mathrm{i}}({\mathrm{z}}_{\mathrm{i}}{\mathrm{Bx}}_{\mathrm{i}}\ \&\ \mathrm{w}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{i}-1}{\mathrm{z}}_{\mathrm{i}}).\end{array}\end{align*}$$

We then follow the pattern of the second part of the proof of 2.7, formalizing in each case the argument that $\mathrm{M}\models \mathrm{u}\le \mathrm{v}$ . We omit the details.

(e) Assume that $\mathrm{M}\models \wedge_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{I}^\ast ({\mathrm{x}}_{\mathrm{i}})\ \&\ \mathrm{I}^\ast (\mathrm{y})$ . Assume further that $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}$ . We show that for each $\mathrm{j}$ , $0\le \mathrm{j}<\mathrm{n}\hbox{--} 1$ ,

$$\begin{align*}(\$)\ \ \mathrm{M}\ \models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}\to \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}\;\mathrm{v}\kern0.24em \mathrm{y}={\mathrm{x}}_{\mathrm{n}-\mathrm{j}}\;\mathrm{v}\kern0.24em \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}.\end{align*}$$

Assume that $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}$ . Then

$$\begin{align*} \begin{array}{l}\mathrm{M}\models \mathrm{ay}={\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}\;\mathrm{v}\kern0.24em \mathrm{ayB}({\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}})\;\;\mathrm{v}\kern0.24em \mathrm{ayE}({\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}})\;\mathrm{v}\kern0.36em \\ {}\mathrm{v}\;\exists {\mathrm{y}}_1,{\mathrm{y}}_2{\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}={\mathrm{y}}_1(\mathrm{ay}){\mathrm{y}}_2.\end{array}\end{align*}$$

Now, $\mathrm{M}\models \mathrm{ay}={\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}\;\mathrm{v}\kern0.24em \mathrm{ayB}({\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}})$ is ruled out immediately by $(\mathrm{QT}4)$ .

Suppose that (1) $\mathrm{M}\models \mathrm{ayE}({\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}})$ . Then, from $\mathrm{M}\models {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}\mathrm{E}({\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1 \dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}})$ we have, by 7.1(b), $\mathrm{M}\models {\mathrm{ayEx}}_{\mathrm{n}-\mathrm{j}}\mathrm{v}\kern0.24em \mathrm{ay}={\mathrm{x}}_{\mathrm{n}-\mathrm{j}}\;\mathrm{v}\kern0.24em {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}\mathrm{Eay}$ . If $\mathrm{M}\models {\mathrm{ayEx}}_{\mathrm{n}-\mathrm{j}}\;\mathrm{v}\kern0.24em \mathrm{ay}={\mathrm{x}}_{\mathrm{n}-\mathrm{j}}$ , then $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}$ and we are done. So we may assume that $\mathrm{M}\models {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}\mathrm{Eay}$ .

Then $\mathrm{M}\models \exists {\mathrm{y}}_1\mathrm{ay}={\mathrm{y}}_1{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}$ , whence $\mathrm{M}\models {\mathrm{y}}_1=\mathrm{a}\;\mathrm{v}\kern0.24em {\mathrm{aBy}}_1$ . If $\mathrm{M}\models {\mathrm{y}}_1=\mathrm{a}$ , then $\mathrm{M}\models \mathrm{ay}={\mathrm{y}}_1{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}={\mathrm{ax}}_{\mathrm{n}-\mathrm{j}}$ ; hence $\mathrm{M}\models \mathrm{y}={\mathrm{x}}_{\mathrm{n}-\mathrm{j}}$ , as needed.

If $\mathrm{M}\models {\mathrm{aBy}}_1$ , then $\mathrm{M}\models \exists {\mathrm{y}}_2{\mathrm{y}}_1={\mathrm{ay}}_2$ . That is, $\mathrm{M}\models \mathrm{ay}={\mathrm{y}}_1{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}={\mathrm{ay}}_2{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}$ , whence $\mathrm{M}\models \mathrm{y}={\mathrm{y}}_2{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}$ . Then $\mathrm{M}\models {\mathrm{y}}_2\mathrm{By}$ . Now, from hypothesis $\mathrm{M}\models \mathrm{ayE}({\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}})$ we have

$$\begin{align*}\mathrm{M}\models \exists {\mathrm{z}}_1{\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}={\mathrm{z}}_1\mathrm{ay}={\mathrm{z}}_1{\mathrm{ay}}_2{\mathrm{x}}_{\mathrm{n}-\mathrm{j}},\end{align*}$$

whence, by 5.1(f), $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{z}}_1{\mathrm{ay}}_2$ . Then $\mathrm{M}\models {\mathrm{z}}_1=\mathrm{b}\;\mathrm{v}\;{\mathrm{bBz}}_1$ , so we have $\mathrm{M}\models {\mathrm{bb}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{bay}}_2\;\mathrm{v}\ \exists {\mathrm{z}}_2{\mathrm{bb}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}=({\mathrm{bz}}_2){\mathrm{ay}}_2$ , whence $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{ay}}_2\;\mathrm{v}\;{\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{z}}_2{\mathrm{ay}}_2$ . But $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{ay}}_2$ is ruled out. Hence $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{z}}_2{\mathrm{ay}}_2$ , and so $\mathrm{M}\models {\mathrm{y}}_2\mathrm{E}({\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)})$ . But by (d) from $\mathrm{M}\models \wedge_{1\le \mathrm{i}\le \mathrm{n}-(\mathrm{j}+1)}\mathrm{I}^\ast ({\mathrm{x}}_{\mathrm{i}})$ we have $\mathrm{M}\models \mathrm{I}^\ast ({\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)})$ . This, however, contradicts $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{y})\ \&\ {\mathrm{y}}_2\mathrm{By}$ by 5.1(d). Hence subcase $\mathrm{M}\models {\mathrm{aBy}}_1$ is ruled out.

Suppose that (2) $\mathrm{M}\models \exists {\mathrm{y}}_1,{\mathrm{y}}_2{\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}={\mathrm{y}}_1(\mathrm{ay}){\mathrm{y}}_2$ . Then $\mathrm{M}\models {\mathrm{y}}_2\mathrm{E}({\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-\mathrm{j}})$ , whence by 7.1(b), $\mathrm{M}\models {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}{\mathrm{Ey}}_2\ \mathrm{v}\;{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}={\mathrm{y}}_2\;\mathrm{v}\;{\mathrm{y}}_2{\mathrm{Ex}}_{\mathrm{n}-\mathrm{j}}$ . We distinguish the subcases:

$$\begin{align*}\hspace{-132.5pt}(2\mathrm{a})\hspace{132.5pt}\mathrm{M}\models {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}{\mathrm{Ey}}_2.\end{align*}$$

Then $\mathrm{M}\models \exists {\mathrm{y}}_4{\mathrm{y}}_2={\mathrm{y}}_4{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}$ , that is, $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}={\mathrm{y}}_1\mathrm{ay}({\mathrm{y}}_4{\mathrm{x}}_{\mathrm{n}-\mathrm{j}})$ . By 5.1(f), we get $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{y}}_1{\mathrm{ayy}}_4$ . Then $\mathrm{M}\models {\mathrm{y}}_1=\mathrm{b}\;\mathrm{v}\;{\mathrm{bBy}}_1$ ; hence

$\mathrm{M}\models {\mathrm{bb}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{bayy}}_4\;\mathrm{v}\;\exists {\mathrm{y}}_3{\mathrm{bb}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{by}}_3{\mathrm{ayy}}_4,$ and further, $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{ayy}}_4\;\mathrm{v}\ {\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{y}}_3{\mathrm{ayy}}_4$ . But $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{ayy}}_4$ is ruled out. Hence $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{y}}_3(\mathrm{ay}){\mathrm{y}}_4$ , and so we obtain $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}$ , as needed.

$$\begin{align*}\hspace{-129.5pt}(2\mathrm{b})\hspace{129.5pt}\mathrm{M}\models {\mathrm{x}}_{\mathrm{n}-\mathrm{j}}={\mathrm{y}}_2.\end{align*}$$

Then $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}={\mathrm{y}}_1{\mathrm{ayx}}_{\mathrm{n}-\mathrm{j}}$ , and by 5.1(f), $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{y}}_1\mathrm{ay}$ . But then $\mathrm{M}\models {\mathrm{y}}_1=\mathrm{b}\;\mathrm{v}\;{\mathrm{bBy}}_1$ . We proceed as in (2a) to show that $\mathrm{M}\models \exists {\mathrm{y}}_3{\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}={\mathrm{y}}_3\mathrm{ay}$ , whence $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}$ , as needed.

$$\begin{align*}\hspace{-133pt}(2\mathrm{c})\hspace{133pt}\mathrm{M}\models {\mathrm{y}}_2{\mathrm{Ex}}_{\mathrm{n}-\mathrm{j}}.\end{align*}$$

Then $\mathrm{M}\models \exists {\mathrm{y}}_3{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}={\mathrm{y}}_3{\mathrm{y}}_2$ , so $\mathrm{M}\models {\mathrm{y}}_3{\mathrm{Bx}}_{\mathrm{n}-\mathrm{j}}$ . Also, $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)} ({\mathrm{y}}_3{\mathrm{y}}_2)={\mathrm{y}}_1{\mathrm{ayy}}_2$ , and by 5.1(f), $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{y}}_3={\mathrm{y}}_1\mathrm{ay}$ .

So $\mathrm{M}\models {\mathrm{y}}_3\mathrm{E}({\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{y}}_3)\ \&\ \mathrm{yE}({\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{y}}_3)$ , whence by 7.1(b), $\mathrm{M}\models {\mathrm{y}}_3\mathrm{Ey}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{y}}_3=\mathrm{y}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{y}\mathrm{Ey}}_3$ .

$$\begin{align*}\hspace{-117pt}(2\mathrm{ci})\hspace{117pt}\mathrm{M}\models {\mathrm{y}}_3\mathrm{Ey}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{y}}_3=\mathrm{y}.\end{align*}$$

Then from $\mathrm{M}\models \mathrm{I}^\ast (\mathrm{y})$ and $\mathrm{M}\models \mathrm{I}^\ast ({\mathrm{x}}_{\mathrm{n}-\mathrm{j}})\ \&\ {\mathrm{y}}_3{\mathrm{Bx}}_{\mathrm{n}-\mathrm{j}}$ we obtain a contradiction, either by 5.1(d) or 5.1(c). Thus (2ci) is ruled out.

$$\begin{align*}\hspace{-135pt}(2\mathrm{cii})\hspace{135pt}\mathrm{M}\models {\mathrm{yEy}}_3.\end{align*}$$

Then $\mathrm{M}\models \exists {\mathrm{y}}_5{\mathrm{y}}_3={\mathrm{y}}_5\mathrm{y}$ , so $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}({\mathrm{y}}_5\mathrm{y})={\mathrm{y}}_1\mathrm{ay}$ . By 5.1(f), $\mathrm{M}\models {\mathrm{b}}^{\mathrm{n}-\mathrm{j}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}-(\mathrm{j}+1)}{\mathrm{y}}_5={\mathrm{y}}_1\mathrm{a}$ . Then $\mathrm{M}\models {\mathrm{y}}_5=\mathrm{a}\;\mathrm{v}\;{\mathrm{aEy}}_5$ . From $\mathrm{M}\models {\mathrm{y}}_3={\mathrm{y}}_5\mathrm{y}$ , we then have $\mathrm{M}\models {\mathrm{y}}_3=\mathrm{ay}\kern0.24em \mathrm{v}\kern0.24em {\mathrm{ayEy}}_3$ , whence from $\mathrm{M}\models {\mathrm{y}}_3{\mathrm{Bx}}_{\mathrm{n}-\mathrm{j}}$ , we obtain $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{n}-\mathrm{j}}$ , as needed.

This completes the proof of ($).

After $\mathrm{n}\hbox{--} 1$ applications of ($) we have from hypothesis $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}$ that

$$\begin{align*}\mathrm{M}\models {\vee}_{0\le \mathrm{i}\le \mathrm{n}-2}(\mathrm{y}={\mathrm{x}}_{\mathrm{n}-\mathrm{i}}\mathrm{v}\;\mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{n}-\mathrm{i}})\kern0.24em \mathrm{v}\;\;\mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{bax}}_1.\end{align*}$$

If $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{bax}}_1$ , we have exactly as in the proof of 5.3(a) that

$$\begin{align*}\mathrm{M}\models \mathrm{y}={\mathrm{x}}_1\;\mathrm{v}\;\mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_1.\end{align*}$$

Hence $\mathrm{M}\models {\vee}_{1\le \mathrm{i}\le \mathrm{n}}(\mathrm{y}={\mathrm{x}}_{\mathrm{i}}\mathrm{v}\;\mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{i}})$ .

But then $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}\to {\vee}_{1\le \mathrm{i}\le \mathrm{n}}(\mathrm{y}={\mathrm{x}}_{\mathrm{i}}\;\mathrm{v}\kern0.24em \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{i}})$ .

Conversely, suppose that $\mathrm{M}\models {\vee}_{1\le \mathrm{i}\le \mathrm{n}}(\mathrm{y}={\mathrm{x}}_{\mathrm{i}}\mathrm{v}\;\mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{i}})$ . If $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{j}}$ where $1\le \mathrm{j}\le \mathrm{n}$ , we immediately have that $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{j}}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}$ . Assume now that $\mathrm{M}\models {\vee}_{1\le \mathrm{i}\le \mathrm{n}}\mathrm{y}={\mathrm{x}}_{\mathrm{i}}$ . If $\mathrm{M}\models \mathrm{y}={\mathrm{x}}_1$ , then $\mathrm{M}\models \mathrm{ay}={\mathrm{ax}}_1{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}$ . If $\mathrm{j}=\mathrm{k}+1\le \mathrm{n}$ , we have from hypothesis $\mathrm{M}\models \mathrm{I}^\ast ({\mathrm{x}}_{\mathrm{k}})$ , that $\mathrm{M}\models {\mathrm{x}}_{\mathrm{k}}=\mathrm{a}\;\mathrm{v}\;{\mathrm{aEx}}_{\mathrm{k}}$ . But then if $\mathrm{M}\models \mathrm{y}={\mathrm{x}}_{\mathrm{j}}$ _, then $\mathrm{M}\models \mathrm{ay}={\mathrm{ax}}_{\mathrm{j}}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{k}}{\mathrm{x}}_{\mathrm{j}\dots }{\mathrm{x}}_{\mathrm{n}}$ , as required. Hence we also have

$$\begin{align*}\mathrm{M}\models {\vee}_{1\le \mathrm{i}\le \mathrm{n}}(\mathrm{y}={\mathrm{x}}_{\mathrm{i}}\;\mathrm{v}\kern0.24em \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{i}})\to \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}.\end{align*}$$

But then $\mathrm{M}\models \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}\leftrightarrow {\vee}_{1\le \mathrm{i}\le \mathrm{n}}(\mathrm{y}={\mathrm{x}}_{\mathrm{i}}\;\mathrm{v}\kern0.24em \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{i}})$ , whence $\mathrm{M} \models \mathrm{y}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}\;\mathrm{v}\kern0.24em \mathrm{ay}{\subseteq}_{\mathrm{p}}{\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}\leftrightarrow \mathrm{y}={\mathrm{b}}^{\mathrm{n}}{\mathrm{ax}}_1\dots {\mathrm{x}}_{\mathrm{n}}\;\mathrm{v}\;{\vee}_{1\le \mathrm{i}\le \mathrm{n}}(\mathrm{y}={\mathrm{x}}_{\mathrm{i}}\;\mathrm{v}\ \mathrm{ay} {\subseteq}_{\mathrm{p}}{\mathrm{x}}_{\mathrm{i}}),$ as required.⊣

We have dealt with $(\mathrm{T}5)-(\mathrm{T}8)$ in 5.3(c) and (d). Hence from 7.2 we have:

Theorem 7.3. $\mathrm{T}^\ast$ is interpretable in ${\mathrm{QT}}^{+}$ .

8 Some theories of dyadic trees

The theory $\mathrm{T}$ introduced by Kristiansen and Murwanashyaka in [4] is formulated in the vocabulary ${{\mathcal{L}}}_{\mathrm{T}}=\{0,\tau, \sqsubseteq \}$ , and has as its axioms:

(T1) $$\begin{align}\forall \mathrm{x},\mathrm{y}\neg \tau (\mathrm{x},\mathrm{y})=0\end{align}$$

(T2) $$\begin{align}\forall \mathrm{x},\mathrm{y},\mathrm{z},\mathrm{w}\;[\tau (\mathrm{x},\mathrm{y})=\tau (\mathrm{z},\mathrm{w})\to \mathrm{x}=\mathrm{z}\ \&\ \mathrm{y}=\mathrm{w}]\end{align}$$

(T3) $$\begin{align}\forall \mathrm{x}\;[\mathrm{x}\sqsubseteq 0\leftrightarrow \mathrm{x}=0]\end{align}$$

(T4) $$\begin{align}\forall \mathrm{x},\mathrm{y},\mathrm{z}\;[\mathrm{x}\sqsubseteq \tau (\mathrm{y},\mathrm{z})\leftrightarrow \mathrm{x}=\tau (\mathrm{y},\mathrm{z})\;\mathrm{v}\kern0.24em \mathrm{x}\sqsubseteq \mathrm{y}\;\mathrm{v}\;\mathrm{x}\sqsubseteq \mathrm{z}]\end{align}$$

Let $\mathrm{I}(\mathrm{x})$ be an ${{\mathcal{L}}}_{\mathrm{T}}$ -formula with $\mathrm{x}$ as sole free variable. We say that $\mathrm{I}(\mathrm{x})$ is a (dyadic) tree form if $\mathrm{T}\vdash \mathrm{I}(0)$ and $\mathrm{T}\vdash \forall \mathrm{x} (\mathrm{I}(\mathrm{x}) \ \&\ \mathrm{I}(\mathrm{y}) \rightarrow \mathrm{I}(\tau (\mathrm{x}, \mathrm{y}))).$

Note that if ${\mathrm{J}}_1$ and ${\mathrm{J}}_2$ are tree forms, then so is ${\mathrm{J}}_1\ \&\ {\mathrm{J}}_2$ .

Let ${\mathrm{I}}_{\mathrm{Z}}(\mathrm{x})\equiv 0\sqsubseteq \mathrm{x}$ , ${\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{x})\equiv \mathrm{x}\sqsubseteq \mathrm{x}\ \&\ \forall {\mathrm{x}}_1,{\mathrm{x}}_2(\mathrm{x}=\tau ({\mathrm{x}}_1,{\mathrm{x}}_2)\to {\mathrm{x}}_1\sqsubseteq {\mathrm{x}}_1\ \&\ {\mathrm{x}}_2\sqsubseteq {\mathrm{x}}_2),\mathrm{and}\ {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{x})\equiv \forall \mathrm{y},\mathrm{z}(\mathrm{y}\sqsubseteq \mathrm{z}\ \&\ \mathrm{z}\sqsubseteq \mathrm{x}\to \mathrm{y}\sqsubseteq \mathrm{x})$ .

Throughout this section we let $\mathrm{M}$ be any model of $\mathrm{T}$ . Then we have:

8.1

${\mathrm{I}}_{\mathrm{Z}}(\mathrm{x})$ , ${\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{x})$ , and ${\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{x})$ are tree forms.

Proof That ${\mathrm{I}}_{\mathrm{Z}}(\mathrm{x})$ is a tree form easily follows from $(\mathrm{T}3)$ and $(\mathrm{T}4)$ . For ${\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{x})$ , note that $\mathrm{T} \vdash \mathrm{I}_{\mathrm{REF} \sqsubseteq} (0)$ follows immediately from $(\mathrm{T}3)$ and $(\mathrm{T}1)$ . Assume $\mathrm{M}\models {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{u})\ \&\ {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{v})$ and consider $\mathrm{x}=\tau (\mathrm{u},\mathrm{v})$ . We have that $\mathrm{M}\models \tau (\mathrm{u},\mathrm{v})\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ by $(\mathrm{T}4)$ . On the other hand, assume $\mathrm{M}\models \tau (\mathrm{u},\mathrm{v})=\tau ({\mathrm{x}}_1,{\mathrm{x}}_2)$ . Then $\mathrm{M}\models \mathrm{u}={\mathrm{x}}_1\ \&\ \mathrm{v}={\mathrm{x}}_2$ by $(\mathrm{T}2)$ , whence from $\mathrm{M}\models {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{u})\ \&\ {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{v})$ we obtain $\mathrm{M}\models {\mathrm{x}}_1\sqsubseteq {\mathrm{x}}_1\ \&\ {\mathrm{x}}_2\sqsubseteq {\mathrm{x}}_2$ . Hence we have

$$\begin{align*}\mathrm{M}\models \forall {\mathrm{x}}_1,{\mathrm{x}}_2(\tau (\mathrm{u},\mathrm{v})=\tau ({\mathrm{x}}_1,{\mathrm{x}}_2)\to {\mathrm{x}}_1\sqsubseteq {\mathrm{x}}_1\ \&\ {\mathrm{x}}_2\sqsubseteq {\mathrm{x}}_2),\end{align*}$$

that is, $\mathrm{M}\models {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\tau (\mathrm{u},\mathrm{v}))$ . We now deal with ${\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{x})$ . Let $\mathrm{x}=0$ and assume $\mathrm{M}\models \mathrm{y}\sqsubseteq \mathrm{z}\ \&\ \mathrm{z}\sqsubseteq 0$ . Then $\mathrm{M}\models \mathrm{z}=0$ by $(\mathrm{T}3)$ , whence $\mathrm{M}\models \mathrm{y}\sqsubseteq 0$ , and we obtain $\mathrm{M}\models {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq }(0)$ . Assume now that $\mathrm{M}\models {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{u})\ \&\ {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{v})$ , and suppose $\mathrm{M}\models \mathrm{y}\sqsubseteq \mathrm{z}\ \&\ \mathrm{z}\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ . By $(\mathrm{T}4)$ we have that $\mathrm{M}\models \mathrm{z}=\tau (\mathrm{u},\mathrm{v})\;\mathrm{v}\;\mathrm{z}\sqsubseteq \mathrm{u}\;\mathrm{v}\;\mathrm{z}\sqsubseteq \mathrm{v}$ . If $\mathrm{M}\models \mathrm{z}=\tau (\mathrm{u},\mathrm{v})$ , then $\mathrm{M}\models \mathrm{y}\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ . If $\mathrm{M}\models \mathrm{z}\sqsubseteq \mathrm{u}$ , then $\mathrm{M}\models \mathrm{y}\sqsubseteq \mathrm{u}$ follows from $\mathrm{M}\models {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{u})$ . From $(\mathrm{T}4)$ we then obtain that $\mathrm{M}\models \mathrm{y}\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ . Analogously if $\mathrm{M}\models \mathrm{z}\sqsubseteq \mathrm{v}$ . Therefore, $\mathrm{M}\models \forall \mathrm{y},\mathrm{z}(\mathrm{y}\sqsubseteq \mathrm{z}\ \&\ \mathrm{z}\sqsubseteq \tau (\mathrm{u},\mathrm{v})\to \mathrm{y}\sqsubseteq \tau (\mathrm{u},\mathrm{v}))$ , that is, $\mathrm{M}\models {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\tau (\mathrm{u},\mathrm{v}))$ .⊣

If $\mathrm{I}(\mathrm{x})$ and $\mathrm{J}(\mathrm{x})$ are ${{\mathcal{L}}}_{\mathrm{T}}$ -formulae with $\mathrm{x}$ as sole free variable, we write $\mathrm{J}\subseteq \mathrm{I}$ if $\mathrm{T}\vdash \forall \mathrm{x}\;(\mathrm{J}(\mathrm{x})\to \mathrm{I}(\mathrm{x}))$ . And we write “ $\forall \mathrm{x}\in \mathrm{J}(\dots )$ ” for “ $\forall \mathrm{x}\;(\mathrm{J}(\mathrm{x})\to \dots )$ ” and “ $\forall \mathrm{x}\sqsubseteq \mathrm{t}(\dots )$ ” for “ $\forall \mathrm{x}\;(\mathrm{x}\sqsubseteq \mathrm{t}\to \dots )$ ” for an ${{\mathcal{L}}}_{\mathrm{T}}$ -term $\mathrm{t}$ .

8.2.

(a) For any tree form $\mathrm{I}$ there is a tree form $\mathrm{J}\subseteq \mathrm{I}$ such that

$$\begin{align*}\mathrm{T}\vdash \mathrm{J}(\mathrm{x})\ \&\ \mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{J}(\mathrm{y}).\end{align*}$$

(b) For any tree form $\mathrm{I}$ there is a tree form $\mathrm{J}\subseteq \mathrm{I}$ such that

$$\begin{align*}\mathrm{T}\vdash \forall \mathrm{x}\in \mathrm{J}\; \forall \mathrm{y}(\tau (\mathrm{x},\mathrm{y})\ne \mathrm{x}\ \&\ \tau (\mathrm{y},\mathrm{x})\ne \mathrm{x}).\end{align*}$$

(c) For any tree form $\mathrm{I}$ there is a tree form $\mathrm{J}\subseteq \mathrm{I}$ such that

$$\begin{align*}\mathrm{T}\vdash \forall \mathrm{y}\in \mathrm{J}\;(\forall \mathrm{z}(\mathrm{z}\sqsubseteq \mathrm{y}\to \mathrm{z}=\mathrm{y})\;\mathrm{v}\ \exists {\mathrm{y}}_1,{\mathrm{y}}_2\mathrm{y}=\tau ({\mathrm{y}}_1,{\mathrm{y}}_2)).\end{align*}$$

(d) For any tree form $\mathrm{I}$ there is a tree form $\mathrm{J}\subseteq \mathrm{I}$ such that

$$\begin{align*}\mathrm{T}\vdash \forall \mathrm{x}\in \mathrm{J}\;\forall \mathrm{y}\;(\mathrm{x}\sqsubseteq \mathrm{y}\ \&\ \mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{x}=\mathrm{y}).\end{align*}$$

(e) For any tree form $\mathrm{I}$ there is a tree form $\mathrm{J}\subseteq \mathrm{I}$ such that

$$\begin{align*}\mathrm{T}\vdash \forall \mathrm{x}\in \mathrm{J}\;\forall \mathrm{u},\mathrm{v}\;(\mathrm{x}\sqsubseteq \mathrm{u}\;\mathrm{v}\;\mathrm{x}\sqsubseteq \mathrm{v}\to \mathrm{x}\ne \tau (\mathrm{u},\mathrm{v})).\end{align*}$$

(f) For any tree form $\mathrm{I}$ there is a tree form $\mathrm{J}\subseteq \mathrm{I}$ such that

$$\begin{align*} \begin{array}{l}\mathrm{T}\vdash \forall \mathrm{x}\in \mathrm{J}\;(\mathrm{x}=0\;\mathrm{v}\ \exists \mathrm{y},\mathrm{z}\;(\mathrm{y}\sqsubseteq \mathrm{x}\ \&\ \mathrm{z}\sqsubseteq \mathrm{x}\ \&\ \mathrm{y}\ne \mathrm{x}\ \&\ \mathrm{z}\ne \mathrm{x}\ \&\ \\ {}\ \&\ (\mathrm{y}\sqsubseteq \mathrm{z}\;\mathrm{v}\;\forall \mathrm{w}(\mathrm{y}\sqsubseteq \mathrm{w}\sqsubseteq \mathrm{x}\to \mathrm{w}=\mathrm{x}\;\mathrm{v}\;\mathrm{w}=\mathrm{y}))\\ \&\ (\mathrm{z}\sqsubseteq \mathrm{y}\;\mathrm{v}\;\forall \mathrm{w}(\mathrm{z}\sqsubseteq \mathrm{w}\sqsubseteq \mathrm{x}\to \mathrm{w}=\mathrm{x}\;\mathrm{v}\;\mathrm{w}=\mathrm{z})))).\end{array}\end{align*}$$

Proof (a) Let $\mathrm{J}(\mathrm{x})\equiv {\mathrm{I}}_{\sqsubseteq}(\mathrm{x})\equiv \mathrm{I}(\mathrm{x})\ \&\ \forall \mathrm{z}\sqsubseteq \mathrm{x}\;\mathrm{I}(\mathrm{z})$ .

Assume $\mathrm{M}\models \mathrm{z}\sqsubseteq 0$ . Then $\mathrm{M}\models \mathrm{z}=0$ by $(\mathrm{T}3)$ and $\mathrm{M}\models \mathrm{I}(\mathrm{z})$ holds since $\mathrm{I}(\mathrm{x})$ is a tree form. Hence $\mathrm{M}\models {\mathrm{I}}_{\sqsubseteq }(0)$ . Assume now that $\mathrm{M}\models {\mathrm{I}}_{\sqsubseteq}(\mathrm{u})\ \&\ {\mathrm{I}}_{\sqsubseteq}(\mathrm{v})$ and suppose that $\mathrm{M}\models \mathrm{z}\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ . By $(\mathrm{T}4)$ we have that $\mathrm{M}\models \mathrm{z}=\tau (\mathrm{u},\mathrm{v})\;\mathrm{v}\;\mathrm{z}\sqsubseteq \mathrm{u}\;\mathrm{v}\;\mathrm{z}\sqsubseteq \mathrm{v}$ . If $\mathrm{M}\models \mathrm{z}\sqsubseteq \mathrm{u}\;\mathrm{v}\;\mathrm{z}\sqsubseteq \mathrm{v}$ we have that $\mathrm{M}\models \mathrm{I}(\mathrm{z})$ follows from hypothesis $\mathrm{M}\models {\mathrm{I}}_{\sqsubseteq}(\mathrm{u})\ \&\ {\mathrm{I}}_{\sqsubseteq}(\mathrm{v})$ . If $\mathrm{M}\models \mathrm{z}=\tau (\mathrm{u},\mathrm{v})$ then $\mathrm{M}\models \mathrm{I}(\mathrm{z})$ again from hypothesis $\mathrm{M}\models {\mathrm{I}}_{\sqsubseteq}(\mathrm{u})\ \&\ {\mathrm{I}}_{\sqsubseteq}(\mathrm{v})$ and the fact that $\mathrm{I}(\mathrm{x})$ is a tree form. Hence $\mathrm{M}\models {\mathrm{I}}_{\sqsubseteq}(\tau (\mathrm{u},\mathrm{v}))$ .

(b) Let $\mathrm{J}(\mathrm{x})\equiv \mathrm{I}(\mathrm{x})\ \&\ {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{x})\ \&\ \forall \mathrm{z}\sqsubseteq \mathrm{x}\forall \mathrm{y}(\tau (\mathrm{z},\mathrm{y})\ne \mathrm{z}\ \&\ \tau (\mathrm{y},\mathrm{z})\ne \mathrm{z})$ . Assume $\mathrm{M}\models \mathrm{z}\sqsubseteq 0$ . Then $\mathrm{M}\models \mathrm{z}=0$ by $(\mathrm{T}3)$ , and $\mathrm{M}\models \mathrm{J}(0)$ follows from $(\mathrm{T}1)$ and $\mathrm{M}\models {\mathrm{I}}_{\mathrm{REF}\sqsubseteq }(0)$ . Now, assume $\mathrm{M}\models \mathrm{J}(\mathrm{u})\ \&\ \mathrm{J}(\mathrm{v})$ , and let $\mathrm{M}\models \mathrm{z}\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ . Then $\mathrm{M}\models \mathrm{z}=\tau (\mathrm{u},\mathrm{v})\;\mathrm{v}\;\mathrm{z}\sqsubseteq \mathrm{u}\;\mathrm{v}\;\mathrm{z}\sqsubseteq \mathrm{v}$ by $(\mathrm{T}4)$ . Suppose (i) $\mathrm{M}\models \mathrm{z}=\tau (\mathrm{u},\mathrm{v})$ , and assume, for a reductio, that $\mathrm{M}\models \tau (\mathrm{z},\mathrm{y})=\mathrm{z}$ , that is, $\mathrm{M}\models \tau (\tau (\mathrm{u},\mathrm{v}),\mathrm{y})=\tau (\mathrm{u},\mathrm{v})$ . Then by $(\mathrm{T}2)$ we have $\mathrm{M}\models \tau (\mathrm{u},\mathrm{v})=\mathrm{u}$ , contradicting the hypothesis $\mathrm{M}\models \mathrm{J}(\mathrm{u})$ . Similarly if $\mathrm{M}\models \tau (\mathrm{y},\mathrm{z})=\mathrm{z}$ . Hence (i) is ruled out. Suppose (ii) $\mathrm{M}\models \mathrm{z}\sqsubseteq \mathrm{u}\;\mathrm{v}\;\mathrm{z}\sqsubseteq \mathrm{v}$ . Then from hypothesis $\mathrm{M}\models \mathrm{J}(\mathrm{u})\ \&\ \mathrm{J}(\mathrm{v})$ we have $\mathrm{M}\models \forall \mathrm{y}(\tau (\mathrm{z},\mathrm{y})\ne \mathrm{z}\ \&\ \tau (\mathrm{y},\mathrm{z})\ne \mathrm{z})$ . Therefore, $\mathrm{M}\models \forall \mathrm{z}\sqsubseteq \tau (\mathrm{u},\mathrm{v})(\forall \mathrm{y}(\tau (\mathrm{z},\mathrm{y})\ne \mathrm{z}\ \&\ \tau (\mathrm{y},\mathrm{z})\ne \mathrm{z}))$ . Given that ${\mathrm{I}}_{\mathrm{REF}\sqsubseteq }$ is a tree form, we thus have $\mathrm{M}\models \mathrm{J}(\tau (\mathrm{u},\mathrm{v}))$ . Hence $\mathrm{J}(\mathrm{x})$ is also a tree form.

(c) Let $\mathrm{J}(\mathrm{x})\equiv \mathrm{I}(\mathrm{x})\ \&\ (\forall \mathrm{y}(\mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{y}=\mathrm{x})\ \mathrm{v}\ \exists {\mathrm{x}}_1,{\mathrm{x}}_2\mathrm{x}=\tau ({\mathrm{x}}_1,{\mathrm{x}}_2))$ . That $\mathrm{J}(\mathrm{x})$ is a tree form follows from $(\mathrm{T}3)$ .

(d) Let $\mathrm{J}(\mathrm{x})\equiv {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{x})\ \&\ {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{x})\ \&\ {\mathrm{I}}_{8.2(\mathrm{b})}(\mathrm{x})\ \&\ \forall \mathrm{y}\;(\mathrm{x}\sqsubseteq \mathrm{y}\ \&\ \mathrm{y}\sqsubseteq \mathrm{x} \to \mathrm{x}=\mathrm{y})$ . Assume $\mathrm{M}\models 0\sqsubseteq \mathrm{y}\ \&\ \mathrm{y}\sqsubseteq 0$ . Then $\mathrm{M}\models \mathrm{y}=0$ , by $(\mathrm{T}3)$ . Hence for $\mathrm{x}=0$ , we have $\mathrm{M}\models \mathrm{x}\sqsubseteq \mathrm{y}\ \&\ \mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{x}=\mathrm{y}$ . Thus $\mathrm{M}\models \mathrm{J}(0)$ . Assume now that $\mathrm{M}\models \mathrm{J}(\mathrm{u})\ \&\ \mathrm{J}(\mathrm{v})$ , and let $\mathrm{x}=\tau (\mathrm{u},\mathrm{v})$ . Suppose $\mathrm{M}\models \tau (\mathrm{u},\mathrm{v})\sqsubseteq \mathrm{y}\ \&\ \mathrm{y}\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ . By $(\mathrm{T}4)$ we have that $\mathrm{M}\models \mathrm{y}=\tau (\mathrm{u},\mathrm{v})\;\mathrm{v}\;\mathrm{y}\sqsubseteq \mathrm{u}\;\mathrm{v}\;\mathrm{y}\sqsubseteq \mathrm{v}$ . If $\mathrm{M}\models \mathrm{y}=\tau (\mathrm{u},\mathrm{v})$ , then $\mathrm{M}\models \mathrm{x}=\mathrm{y}$ . Suppose, on the other hand, that $\mathrm{M}\models \mathrm{y}\sqsubseteq \mathrm{u}$ . From $\mathrm{M}\models \mathrm{J}(\mathrm{u})$ we have

$$\begin{align*}\mathrm{M}\models {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{u})\ \&\ {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{u})\ \&\ {\mathrm{I}}_{8.2(\mathrm{b})}(\mathrm{u}).\end{align*}$$

By $(\mathrm{T}4)$ we have that $\mathrm{M}\models \mathrm{u}\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ . And from hypothesis $\mathrm{M}\models \tau (\mathrm{u},\mathrm{v})\sqsubseteq \mathrm{y}$ and $\mathrm{M}\models \mathrm{y}\sqsubseteq \mathrm{u}$ we obtain $\mathrm{M}\models \tau (\mathrm{u},\mathrm{v})\sqsubseteq \mathrm{u}$ . Then $\mathrm{M}\models \mathrm{u}=\tau (\mathrm{u},\mathrm{v})$ follows from hypothesis $\mathrm{M}\models \mathrm{J}(\mathrm{u})$ . But this is a contradiction since also $\mathrm{M}\models {\mathrm{I}}_{8.2(\mathrm{b})}(\mathrm{u})$ . Hence $\mathrm{M}\models \mathrm{y}\sqsubseteq \mathrm{u}$ is ruled out. A completely analogous argument rules out $\mathrm{M}\models \mathrm{y}\sqsubseteq \mathrm{v}$ . Therefore, $\mathrm{M}\models \forall \mathrm{y}\;(\tau (\mathrm{u},\mathrm{v})\sqsubseteq \mathrm{y}\ \&\ \mathrm{y}\sqsubseteq \tau (\mathrm{u},\mathrm{v})\to \tau (\mathrm{u},\mathrm{v})=\mathrm{y})$ , and so $\mathrm{M}\models \mathrm{J}(\tau (\mathrm{u},\mathrm{v}))$ .

(e) Let $\mathrm{J}(\mathrm{x})\equiv {\mathrm{I}}_{8.2(\mathrm{d})}(\mathrm{x})\ \&\ \forall \mathrm{u},\mathrm{v}\;(\mathrm{x}\sqsubseteq \mathrm{u}\;\mathrm{v}\;\mathrm{x}\sqsubseteq \mathrm{v}\to \mathrm{x}\ne \tau (\mathrm{u},\mathrm{v}))$ . We have $\mathrm{M}\models \mathrm{J}(0)$ by $(\mathrm{T}1)$ . Assume $\mathrm{M}\models \mathrm{J}(\mathrm{y})\ \&\ \mathrm{J}(\mathrm{z})$ and consider $\mathrm{x}=\tau (\mathrm{y},\mathrm{z})$ . Suppose, for a reductio, that $\mathrm{M}\models \tau (\mathrm{y},\mathrm{z})\sqsubseteq \mathrm{u}\ \&\ \tau (\mathrm{y},\mathrm{z})=\tau (\mathrm{u},\mathrm{v})$ . Then $\mathrm{M}\models \mathrm{y}=\mathrm{u}\ \&\ \mathrm{z}=\mathrm{v}$ by $(\mathrm{T}2)$ _; hence $\mathrm{M}\models \mathrm{J}(\mathrm{u})$ , whence $\mathrm{M}\models {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{u})$ . By $(\mathrm{T}4)$ then $\mathrm{M}\models \mathrm{u}\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ . On the other hand, also $\mathrm{M}\models \tau (\mathrm{u},\mathrm{v})\sqsubseteq \mathrm{u}$ . Hence, again from $\mathrm{M}\models \mathrm{J}(\mathrm{u})$ , we obtain $\mathrm{M}\models \mathrm{u}=\tau (\mathrm{u},\mathrm{v})$ . But this contradicts $\mathrm{M}\models \mathrm{J}(\mathrm{u})$ . Thus, $\mathrm{M}\models \tau (\mathrm{y},\mathrm{z})\sqsubseteq \mathrm{u}\to \tau (\mathrm{y},\mathrm{z})\ne \tau (\mathrm{u},\mathrm{v})$ . Exactly analogously we derive $\mathrm{M}\models \tau (\mathrm{y},\mathrm{z})\sqsubseteq \mathrm{v}\to \tau (\mathrm{y},\mathrm{z})\ne \tau (\mathrm{u},\mathrm{v})$ . Therefore,

$$\begin{align*}\mathrm{M}\models \forall \mathrm{u},\mathrm{v}\;(\tau (\mathrm{y},\mathrm{z})\sqsubseteq \mathrm{u}\;\mathrm{v}\;\tau (\mathrm{y},\mathrm{z})\sqsubseteq \mathrm{v}\to \tau (\mathrm{y},\mathrm{z})\ne \tau (\mathrm{u},\mathrm{v})),\end{align*}$$

which suffices to show that $\mathrm{J}$ is a tree form.

(f) Let ${\displaystyle \begin{array}{l}\mathrm{J}(\mathrm{x})\equiv {\mathrm{I}}_{8.2(\mathrm{d})}(\mathrm{x})\ \&\ (\mathrm{x}=0\;\mathrm{v}\; \exists \mathrm{y},\mathrm{z}\;(\mathrm{y}\sqsubseteq \mathrm{x}\ \&\ \mathrm{z}\sqsubseteq \mathrm{x}\ \&\ \mathrm{y}\ne \mathrm{x}\ \&\ \mathrm{z}\ne \mathrm{x}\ \& \\ \&\ (\mathrm{y}\sqsubseteq \mathrm{z}\;\mathrm{v}\;\forall \mathrm{w}(\mathrm{y}\sqsubseteq \mathrm{w}\sqsubseteq \mathrm{x}\to \mathrm{w}=\mathrm{x}\;\mathrm{v}\;\mathrm{w}=\mathrm{y}))\ \&\ \\ (\mathrm{z}\sqsubseteq \mathrm{y}\;\mathrm{v}\;\forall \mathrm{w}(\mathrm{z}\sqsubseteq \mathrm{w}\sqsubseteq \mathrm{x}\to \mathrm{w}=\mathrm{x}\;\mathrm{v}\;\mathrm{w}=\mathrm{z})))).\end{array}}$ We clearly have $\mathrm{M}\models \mathrm{J}(0)$ . Assume $\mathrm{M}\models \mathrm{J}(\mathrm{u})\ \&\ \mathrm{J}(\mathrm{v})$ and consider $\mathrm{x}=\tau (\mathrm{u},\mathrm{v})$ . Then from $\mathrm{M}\models {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{u})\ \&\ {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{v})$ we have $\mathrm{M}\models \mathrm{u}\sqsubseteq \tau (\mathrm{u},\mathrm{v})\ \&\ \mathrm{v}\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ , and from $\mathrm{M}\models {\mathrm{I}}_{8.2(\mathrm{b})}(\mathrm{u})\ \&\ {\mathrm{I}}_{8.2(\mathrm{b})}(\mathrm{v})$ , that $\mathrm{M}\models \mathrm{u}\ne \tau (\mathrm{u},\mathrm{v})\ \&\ \mathrm{v}\ne \tau (\mathrm{u},\mathrm{v})$ . Suppose that $\mathrm{M}\models \neg \mathrm{u}\sqsubseteq \mathrm{v}$ , and assume $\mathrm{M}\models \mathrm{u}\sqsubseteq \mathrm{w}\sqsubseteq \mathrm{x}$ . Then $\mathrm{M}\models \mathrm{w}\sqsubseteq \tau (\mathrm{u},\mathrm{v})$ , and by $(\mathrm{T}4)$ we have $\mathrm{M}\models \mathrm{w}=\tau (\mathrm{u},\mathrm{v})\;\mathrm{v}\;\mathrm{w}\sqsubseteq \mathrm{u}\;\mathrm{v}\;\mathrm{w}\sqsubseteq \mathrm{v}$ . If $\mathrm{M}\models \mathrm{w}=\tau (\mathrm{u},\mathrm{v})=\mathrm{x}$ , we are done. So assume $\mathrm{M}\models \mathrm{w}\sqsubseteq \mathrm{u}$ . Then from hypothesis $\mathrm{M}\models \mathrm{u}\sqsubseteq \mathrm{w}$ we have $\mathrm{M}\models \mathrm{w}=\mathrm{u}$ since $\mathrm{M}\models {\mathrm{I}}_{8.2(\mathrm{d})}(\mathrm{u})$ . Suppose, on the other hand, that $\mathrm{M}\models \mathrm{w}\sqsubseteq \mathrm{v}$ . Then from hypothesis $\mathrm{M}\models \mathrm{u}\sqsubseteq \mathrm{w}$ we have $\mathrm{M}\models \mathrm{u}\sqsubseteq \mathrm{v}$ since $\mathrm{M}\models {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{v})$ . But this contradicts hypothesis $\mathrm{M}\models \neg \mathrm{u}\sqsubseteq \mathrm{v}$ . Therefore

$$\begin{align*}\mathrm{M}\models \mathrm{u}\sqsubseteq \mathrm{v}\;\mathrm{v}\;\forall \mathrm{w}\;(\mathrm{u}\sqsubseteq \mathrm{w}\sqsubseteq \tau (\mathrm{u},\mathrm{v})\to \mathrm{w}=\tau (\mathrm{u},\mathrm{v})\;\mathrm{v}\;\mathrm{w}=\mathrm{u}).\end{align*}$$

Exactly analogously we establish that

$$\begin{align*}\mathrm{M}\models \mathrm{v}\sqsubseteq \mathrm{u}\;\mathrm{v}\;\forall \mathrm{w}\;(\mathrm{v}\sqsubseteq \mathrm{w}\sqsubseteq \tau (\mathrm{u},\mathrm{v})\to \mathrm{w}=\tau (\mathrm{u},\mathrm{v})\;\mathrm{v}\;\mathrm{w}=\mathrm{v}).\end{align*}$$

Since ${\mathrm{I}}_{8.2(\mathrm{d})}(\mathrm{x})$ is a tree form this suffices to show that $\mathrm{M}\models \mathrm{J}(\tau (\mathrm{u},\mathrm{v}))$ . ⊣

We now consider several extensions of $\mathrm{T}$ postulating additional “natural” properties of dyadic trees. Let:

(T9) $$\begin{align}\forall \mathrm{x},\mathrm{y}\;(\tau (\mathrm{x},\mathrm{y})\ne \mathrm{x}\ \&\ \tau (\mathrm{y},\mathrm{x})\ne \mathrm{x}).\end{align}$$

(T10) $$\begin{align}\forall \mathrm{x}\;(\forall \mathrm{y}(\mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{y}=\mathrm{x})\;\mathrm{v}\;\exists \mathrm{y},\mathrm{z}\;\mathrm{x}=\tau (\mathrm{y},\mathrm{z})). \end{align}$$

(T11) $$\begin{align}\forall \mathrm{x},\mathrm{u},\mathrm{v}\;(\mathrm{x}\sqsubseteq \mathrm{u}\ \&\ \mathrm{x}\sqsubseteq \mathrm{v}\to \mathrm{x}\ne \tau (\mathrm{u},\mathrm{v})).\end{align}$$

(T12) $$\begin{align} \begin{array}{l}\forall \mathrm{x}\;(\mathrm{x}=0\;\mathrm{v}\;\exists \mathrm{y},\mathrm{z}\;(\mathrm{y}\sqsubseteq \mathrm{x}\ \&\ \mathrm{z}\sqsubseteq \mathrm{x}\ \&\ \mathrm{y}\ne \mathrm{x}\ \&\ \mathrm{z}\ne \mathrm{x}\ \&\ \\ {}\ \&\ (\mathrm{y}\sqsubseteq \mathrm{z}\;\mathrm{v}\;\forall \mathrm{w}(\mathrm{y}\sqsubseteq \mathrm{w}\sqsubseteq \mathrm{x}\to \mathrm{w}=\mathrm{x}\;\mathrm{v}\;\mathrm{w}=\mathrm{y}))\ \&\ \\ \& \ (\mathrm{z}\sqsubseteq \mathrm{y}\;\mathrm{v}\;\forall \mathrm{w}(\mathrm{z}\sqsubseteq \mathrm{w}\sqsubseteq \mathrm{x}\to \mathrm{w}=\mathrm{x}\;\mathrm{v}\;\mathrm{w}=\mathrm{z})))).\end{array}\end{align}$$

Let ${\mathrm{D}}_0$ stand for the theory $\mathrm{T}$ . (“ $\mathrm{D}$ ” is for “dyadic.”) Further, let:

$$\begin{align*}{\mathrm{D}}_1=: {\mathrm{D}}_0+(\mathrm{T}5),(\mathrm{T}8).\end{align*}$$

$$\begin{align*}{\mathrm{D}}_2=: {\mathrm{D}}_1+(\mathrm{T}6).\end{align*}$$

$$\begin{align*}{\mathrm{D}}_3=: {\mathrm{D}}_2+(\mathrm{T}7)(={\mathrm{T}}_2).\end{align*}$$

$$\begin{align*}{\mathrm{D}}_4=: {\mathrm{D}}_3+(\mathrm{T}9).\end{align*}$$

$$\begin{align*}{\mathrm{D}}_5=: {\mathrm{D}}_4+(\mathrm{T}10).\end{align*}$$

$$\begin{align*}{\mathrm{D}}_6=: {\mathrm{D}}_0+(\mathrm{T}5),(\mathrm{T}7),(\mathrm{T}11).\end{align*}$$

$$\begin{align*}{\mathrm{D}}_7=: {\mathrm{D}}_0+(\mathrm{T}5),(\mathrm{T}7),(\mathrm{T}8),(\mathrm{T}9),(\mathrm{T}12).\end{align*}$$

Then we have:

Theorem 8.3. ${\mathrm{D}}_0{\equiv}_{\mathrm{I}}{\mathrm{D}}_1{\equiv}_{\mathrm{I}}{\mathrm{D}}_2{\equiv}_{\mathrm{I}}{\mathrm{D}}_3{\equiv}_{\mathrm{I}}{\mathrm{D}}_4{\equiv}_{\mathrm{I}}{\mathrm{D}}_5{\equiv}_{\mathrm{I}}{\mathrm{D}}_6{\equiv}_{\mathrm{I}}{\mathrm{D}}_7.$

In particular, $\mathrm{T}{\equiv}_{\mathrm{I}}{\mathrm{T}}_2$ .

Proof Note that, with the exception of ${\mathrm{D}}_5$ and ${\mathrm{D}}_7$ , all of the theories considered are universal. We introduce a series of different translations ${\mathrm{A}}^{\varphi}$ of ${{\mathcal{L}}}_{\mathrm{T}}$ -formulae into ${{\mathcal{L}}}_{\mathrm{T}}$ -formulae where $\varphi (\mathrm{x})$ is a given ${{\mathcal{L}}}_{\mathrm{T}}$ -formula with $\mathrm{x}$ as sole free variable. In each case, the translation relativizes all free and bound variables in $\mathrm{A}$ to $\varphi (\mathrm{x})$ , otherwise leaving the formula unchanged. In the resulting interpretations, we generally let $0$ and $\tau$ be interpreted by themselves, and we let $\varphi (\mathrm{x})$ define the domain of the interpretation. The chosen formula will in each case be a tree form, ensuring that the domain of the interpretation contains $0$ and is closed under $\tau$ . In most cases, the validation of the axioms in $\mathrm{T}$ of the $\varphi$ -translations of the axioms of the interpreted theory is immediate given the choice of $\varphi$ .

1. (a) ${\mathrm{D}}_1\le_{\mathrm{I}}{\mathrm{D}}_0$ .Let $\varphi (\mathrm{x})\equiv {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{x})\ \&\ {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{x})$ . It suffices to note that $\mathrm{T}\vdash {(\mathrm{T}5)}^{\varphi}$ and $\mathrm{T}\vdash {(\mathrm{T}8)}^{\varphi}$ .

2. (b) ${\mathrm{D}}_2\le_{\mathrm{I}}{\mathrm{D}}_0$ .\\Let $\varphi (\mathrm{x})\equiv {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{x})\ \&\ {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{x})\ \&\ {\mathrm{I}}_{\mathrm{Z}}(\mathrm{x})$ . Then also $\mathrm{T}\vdash {(\mathrm{T}6)}^{\varphi}$ .

3. (c) ${\mathrm{D}}_3\le_{\mathrm{I}}{\mathrm{D}}_0$ .\\Let $\varphi (\mathrm{x})\equiv {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{x})\ \&\ {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{x})\ \&\ {\mathrm{I}}_{\mathrm{Z}}(\mathrm{x})\ \&\ {\mathrm{I}}_{8.2(\mathrm{b})}(\mathrm{x})\ \&\ \forall \mathrm{y}\;(\mathrm{x}\sqsubseteq \mathrm{y} \&$ $\mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{x}=\mathrm{y})$ . Then also $\mathrm{T}\vdash {(\mathrm{T}7)}^{\varphi}$ .

4. (d) ${\mathrm{D}}_4\le_{\mathrm{I}}{\mathrm{D}}_0$ .Let $\varphi (\mathrm{x})$ be as in (c). Then also $\mathrm{T}\vdash {(\mathrm{T}9)}^{\varphi}$ .

5. (e) ${\mathrm{D}}_5\le_{\mathrm{I}}{\mathrm{D}}_0$ .Let $\varphi (\mathrm{x})$ abbreviate

   $$\begin{align*}\hspace{-27pt} \begin{array}{l}{\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{x})\ \&\ {\mathrm{I}}_{\mathrm{TRANS}\sqsubseteq}(\mathrm{x})\ \&\ {\mathrm{I}}_{\mathrm{Z}}(\mathrm{x})\ \&\ {\mathrm{I}}_{8.2(\mathrm{b})}(\mathrm{x})\ \&\ \forall \mathrm{y}\;(\mathrm{x}\sqsubseteq \mathrm{y}\ \&\ \mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{x}=\mathrm{y})\ \&\ \\ {}\qquad\qquad \&\ (\forall \mathrm{y}(\mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{y}=\mathrm{x})\ \mathrm{v}\ \exists \mathrm{y},\mathrm{z}\;\mathrm{x}=\tau (\mathrm{y},\mathrm{z})).\end{array}\end{align*}$$
   Suppose $\mathrm{M}\models \varphi (\mathrm{x})$ . Then $\mathrm{M}{\kern-1.5pt}\models {\kern-1.5pt}\forall \mathrm{y}(\mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{y}=\mathrm{x})\ \mathrm{v}\ \exists {\mathrm{z}}_1,{\mathrm{z}}_2\mathrm{x}={\kern-1.5pt}\tau ({\mathrm{z}}_1,{\mathrm{z}}_2)\kern-1.5pt\Big)$ . If $\mathrm{M}\models \forall \mathrm{y}(\mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{y}=\mathrm{x})$ , then $\mathrm{M}\models \forall \mathrm{y}(\varphi (\mathrm{y})\to (\mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{y}=\mathrm{x}))$ . Suppose $\mathrm{M}\models \neg \forall \mathrm{y}(\mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{y}=\mathrm{x})$ . From $\mathrm{M}\models {\mathrm{I}}_{\mathrm{REF}\sqsubseteq}(\mathrm{x})$ we have\\ $\mathrm{M}\models \forall {\mathrm{x}}_1,{\mathrm{x}}_2(\mathrm{x}=\tau ({\mathrm{x}}_1,{\mathrm{x}}_2)\to {\mathrm{x}}_1\sqsubseteq {\mathrm{x}}_1\ \&\ {\mathrm{x}}_2\sqsubseteq {\mathrm{x}}_2)$ . Hence\\ $\mathrm{M}\models {\mathrm{z}}_1\sqsubseteq {\mathrm{z}}_1\ \&\ {\mathrm{z}}_2\sqsubseteq {\mathrm{z}}_2$ . But then, by $(\mathrm{T}4)$ , $\mathrm{M}\models {\mathrm{z}}_1\sqsubseteq \tau ({\mathrm{z}}_1,{\mathrm{z}}_2)=\mathrm{x}\ \&\ {\mathrm{z}}_2\sqsubseteq $ $\tau ({\mathrm{z}}_1,{\mathrm{z}}_2)=\mathrm{x}$ .Since by 8.2(a) we may assume that $\varphi (\mathrm{x})$ is downward closed with respect to $\sqsubseteq$ , it follows that $\mathrm{M}\models \varphi ({\mathrm{z}}_1)\ \&\ \varphi ({\mathrm{z}}_2)$ . Therefore,
   $$\begin{align*}\hspace{-27pt}\mathrm{M}\models \forall \mathrm{y}(\varphi (\mathrm{y})\to (\mathrm{y}\sqsubseteq \mathrm{x}\to \mathrm{y}=\mathrm{x}))\;\mathrm{v}\;\exists {\mathrm{z}}_1,{\mathrm{z}}_2(\varphi ({\mathrm{z}}_1)\ \&\ \varphi ({\mathrm{z}}_2)\ \&\ \mathrm{x}=\tau ({\mathrm{z}}_1,{\mathrm{z}}_2)),\end{align*}$$
   that is, $\mathrm{M}\models {(\mathrm{T}10)}^{\varphi}$ .
   $$\begin{align*}\hspace{-177pt}(\mathrm{f})\ {\mathrm{D}}_6{\le}_{\mathrm{I}}{\mathrm{D}}_0.\end{align*}$$
   Let $\varphi (\mathrm{x})\equiv {\mathrm{I}}_{8.2(\mathrm{e})}$ .
   $$\begin{align*}\hspace{-177pt}(\mathrm{g})\ {\mathrm{D}}_7{\le}_{\mathrm{I}}{\mathrm{D}}_0.\end{align*}$$
   Let $\varphi (\mathrm{x})\equiv {\mathrm{I}}_{8.2(\mathrm{f})}$ . By 8.2(a) we may assume that $\varphi (\mathrm{x})$ is downward closed under $\sqsubseteq$ . Then it is easily seen that we also have $\mathrm{T}\vdash {(\mathrm{T}12)}^{\varphi}$ .From (a)–(g) we have that ${\mathrm{D}}_{\mathrm{j}}{\le}_{\mathrm{I}}{\mathrm{D}}_0{\le}_{\mathrm{I}}{\mathrm{D}}_{\mathrm{k}}$ _, where $1\le \mathrm{j},\mathrm{k}\le 7$ . This completes the proof of the theorem.⊣

9 Right or left?

Some authors define binary trees more broadly so as to allow differentiating between left-hand and right-hand single branchings: a binary tree either consists of a null tree, $\mathrm{e}$ , or of a single vertex, $\mathrm{a}$ , or has as its “left child” a binary tree ${T}_1$ and as its “right child” a binary tree ${T}_2$ , in which case the tree is of the form $\tau ({T}_1,{T}_2)$ . This gives us, e.g., two $2$ -vertex and five $3$ -vertex binary trees:

We axiomatize the corresponding theory ${\mathrm{T}}_{\mathrm{e}}$ in the language ${{\mathcal{L}}}_{\mathrm{T},\mathrm{e}}=\{\mathrm{e},\mathrm{a},\tau, \sqsubseteq \}$ with two individual constants $e$ and $a$ , a single binary function symbol $\tau$ , and a $2$ -place relational symbol $\sqsubseteq$ :

(T0_e) $$\begin{align}\forall \mathrm{x},\mathrm{y}\neg \tau (\mathrm{x},\mathrm{y})=\mathrm{e}.\end{align}$$

(T1_e) $$\begin{align}\tau (\mathrm{e},\mathrm{e})=\mathrm{a}.\end{align}$$

(T2) $$\begin{align}\forall \mathrm{x},\mathrm{y},\mathrm{z},\mathrm{w}\;[\tau (\mathrm{x},\mathrm{y})=\tau (\mathrm{z},\mathrm{w})\to \mathrm{x}=\mathrm{z}\ \&\ \mathrm{y}=\mathrm{w}].\end{align}$$

(T3_e) $$\begin{align}\forall \mathrm{x}\;(\mathrm{x}\sqsubseteq \mathrm{e}\leftrightarrow \mathrm{x}=\mathrm{e}).\end{align}$$

(T4) $$\begin{align}\forall \mathrm{x},\mathrm{y},\mathrm{z}\;[\mathrm{x}\sqsubseteq \tau (\mathrm{y},\mathrm{z})\leftrightarrow \mathrm{x}=\tau (\mathrm{y},\mathrm{z})\;\mathrm{v}\;\mathrm{x}\sqsubseteq \mathrm{y}\;\mathrm{v}\;\mathrm{x}\sqsubseteq \mathrm{z}].\end{align}$$

Thinking of the null tree as an invisible branching to a “phantom” (or anti-node) $0$ as opposed to a “real” node $1$ , the trees

$$\begin{align*}\tau (\mathrm{e},\mathrm{a}),\tau (\mathrm{a},\mathrm{e}),\tau (\tau (\mathrm{a},\mathrm{e}),\mathrm{e}),\tau (\tau (\mathrm{e},\mathrm{a}),\mathrm{e}),\tau (\mathrm{e},\tau (\mathrm{a},\mathrm{e})),\tau (\mathrm{e},\tau (\mathrm{e},\mathrm{a})),\tau (\mathrm{a},\mathrm{a})\end{align*}$$

listed above may be described using the obvious parenthetical notation, omitting the outermost parentheses, as

$$\begin{align*}01,10,(10)0,(01)0,0(10),0(01),11,\end{align*}$$

respectively. We are in effect identifying these trees with $2$ -colored dyadic trees:

the red branches indicating the invisible branchings to a phantom node. Taking a bold step into abstraction and thinking of a single real node as the result of conjoining two anti-nodes into a single tree (or, alternatively, of collapsing two invisible branchings into a single point/vertex), we obtain the parenthetical notations

$$\begin{align*}0(00),(00)0,((00)0)0,(0(00))0,0((00)0),0(0(00)),(00)(00),\dots .\end{align*}$$

Each of these, on the other hand, represents an ordinary (monochromatic) dyadic tree:

Thus we obtain the following direct interpretation ${}^{\varepsilon}$ of ${\mathrm{T}}_{\mathrm{e}}$ in Kristiansen and Murwanashyaka’s $\mathrm{T}$ . Let

$$\begin{align*}{\mathrm{e}}^{\varepsilon}=: 0,\quad {\mathrm{a}}^{\varepsilon}=: {\tau}_2(0,0),{[\tau (\mathrm{x},\mathrm{y})]}^{\varepsilon}=: {\tau}_2(\mathrm{x},\mathrm{y})\kern0.36em \mathrm{and}\kern0.36em {[\mathrm{x}\sqsubseteq \mathrm{y}]}^{\varepsilon}\equiv :\mathrm{x}\sqsubseteq \mathrm{y}.\end{align*}$$

The $\varepsilon$ -translations of the axioms of ${\mathrm{T}}_{\mathrm{e}}$ are immediately derivable in $\mathrm{T}$ . Hence ${\mathrm{T}}_{\mathrm{e}}{\le}_{\mathrm{I}}\mathrm{T}$ . On the other hand, ${\mathrm{T}}_{\mathrm{e}}$ obviously extends $\mathrm{T}$ in the expanded vocabulary ${{\mathcal{L}}}_{\mathrm{T},\mathrm{e}}$ modulo relabeling $0$ in $\mathrm{T}$ as $\mathrm{e}$ . So we have

Theorem 9.1. ${\mathrm{T}}_{\mathrm{e}}{\equiv}_{\mathrm{I}}\mathrm{T}.$

We analogously obtain theories ${\mathrm{T}}_{\le \mathrm{n},\mathrm{e}}$ , for $\mathrm{n}\ge 2$ , and ${{\mathrm{T}}^{\ast}}_{\mathrm{e}}$ allowing for left-hand and right-hand single branchings in $\le \mathrm{n}$ -ary trees, by expanding the vocabularies of ${\mathrm{T}}_{\le \mathrm{n}}$ and ${\mathrm{T}}^{\ast }$ with an additional constant $\mathrm{e}$ , relabeling $0$ as $\mathrm{a}$ , and by adding axioms $(\mathrm{T}{0}_{\mathrm{e}})$ , $(\mathrm{T}{1}_{\mathrm{e}})$ , and $(\mathrm{T}{3}_{\mathrm{e}})$ , written with ${\tau}_2$ in place of $\tau$ , while omitting $(\mathrm{T}{1}_2)$ and replacing $(\mathrm{T}6)$ with $(\mathrm{T}{6}_{\mathrm{e}})$ : $\mathrm{e}\sqsubseteq \mathrm{x}$ . Then a slight variant of the above argument shows that

$$\begin{align*}{\mathrm{T}}_{\le \mathrm{n},\mathrm{e}}\;{\le}_{\mathrm{I}}{\mathrm{T}}_{\le \mathrm{n}}\kern0.36em \mathrm{and}\kern0.36em {{\mathrm{T}}^{\ast}}_{\mathrm{e}}{\le}_{\mathrm{I}}{\mathrm{T}}^{\ast }.\end{align*}$$

On the other hand, by Theorems 4.2, 8.3, and 9.1 we also have

$$\begin{align*}{\mathrm{T}}_{\le \mathrm{n}}{\le}_{\mathrm{I}}{\mathrm{T}}_2{\le}_{\mathrm{I}}\mathrm{T}{\le}_{\mathrm{I}}{\mathrm{T}}_{\mathrm{e}}{\le}_{\mathrm{I}}{\mathrm{T}}_{\le \mathrm{n},\mathrm{e}}.\end{align*}$$

Thus we also obtain

Theorem 9.2. For each $\mathrm{n}\ge 2$ , ${\mathrm{T}}_{\le \mathrm{n},\mathrm{e}}\;{\equiv}_{\mathrm{I}}{\mathrm{T}}_{\le \mathrm{n}}$ .

Taking into account Theorem 7.3 and [3], we also have

$$\begin{align*}\mathrm{T}^\ast {\le}_{\mathrm{I}}{\mathrm{QT}}^{+}{\le}_{\mathrm{I}}\mathrm{T}{\le}_{\mathrm{I}}{\mathrm{T}}_{\le 2,\mathrm{e}}{\le}_{\mathrm{I}}{{\mathrm{T}}^{\ast}}_{\mathrm{e}}\end{align*}$$

since ${{\mathrm{T}}^{\ast}}_{\mathrm{e}}$ extends ${\mathrm{T}}_{\le 2,\mathrm{e}}$ . Thus we have:

Theorem 9.3. ${\mathrm{T}}^{\ast}\;{\equiv}_{\mathrm{I}}{{\mathrm{T}}^{\ast}}_{\mathrm{e}}.$

10 The big picture

In [1] we used the concatenation theory ${\mathrm{QT}}^{+}$ as a linchpin to establish mutual interpretability of several well-known weak theories of numbers, sets, and strings. In [3], we added $\mathrm{T}$ to that list, in part relying on Kristiansen and Murwanashyaka’s interpretation of Robinson arithmetic $\mathrm{Q}$ in $\mathrm{T}$ . We are now in the position to expand the list to include the theories of trees considered in this paper.

From Theorem 7.3 and [3], we have that $\mathrm{T}^\ast {\le}_{\mathrm{I}}\;{\mathrm{QT}}^{+}{\le}_{\mathrm{I}}{\mathrm{T}}_2$ . Since ${\mathrm{T}}_2$ is a subtheory of $\mathrm{T}^\ast$ , we then obtain from Theorems 6.3, 8.3, 9.1, and 9.2:

Theorem 10.1. For each $\mathrm{n}\ge 2$ ,

$$\begin{align*}{\mathrm{T}}_{\le \mathrm{n},\mathrm{e}}\;{\equiv}_{\mathrm{I}}{\mathrm{T}}_{\le \mathrm{n}}{\equiv}_{\mathrm{I}}{\mathrm{T}}_{\le 2}{\equiv}_{\mathrm{I}}\mathrm{T}{\equiv}_{\mathrm{I}}{\mathrm{T}}_{\mathrm{e}}{\equiv}_{\mathrm{I}}{\mathrm{T}}_{\mathbf{2}}{\equiv}_{\mathrm{I}}{\mathrm{T}}_{\mathrm{n}}{\equiv}_{\mathrm{I}}\mathrm{T}^\ast {\equiv}_{\mathrm{I}}{{\mathrm{T}}^{\ast}}_{\mathrm{e}}{\equiv}_{\mathrm{I}}{\mathrm{QT}}^{+}{\equiv}_{\mathrm{I}}\mathrm{Q}{\equiv}_{\mathrm{I}}\mathrm{AST}+\mathrm{EXT}.\end{align*}$$

Here $\mathrm{AST}+\mathrm{EXT}$ is Adjunctive Set Theory with Extensionality described in [1]. See [1, 3] for more theories that belong in this chain. To summarize, even though on the surface these theories, in their intended interpretations, refer to objects of as diverse kinds as numbers, sets, strings, and finite trees of different arities, and to corresponding relations and operations associated with those objects, it turns out that each one of these theories contains expressive and deductive resources sufficient to allow it to formally simulate reasoning in any one of the other theories.