2.1 (a) 

1. (b)

2. (c)

Proof (a) Clearly, . Assume . Then ${\varSigma}^{\ast}\models \;\neg\; \mathrm{aBx}$ , by (c2). So ${\varSigma}^{\ast}\models \mathrm{bBx}$ . Note that .

Hence any x such that must have a (proper) end segment of length 2. Suppose ${\varSigma}^{\ast}\models \mathrm{x}={\mathrm{x}}_1\mathrm{ab}\;\mathrm{v}\;\mathrm{x}={\mathrm{x}}_1\mathrm{ba}\;\mathrm{v}\;\mathrm{x}={\mathrm{x}}_1\mathrm{bb}$ , that is, ${\varSigma}^{\ast}\models \mathrm{abEx}\;\mathrm{v}\;\mathrm{baEx}\;\mathrm{v}\;\mathrm{bbEx}$ . By (c1) and (c2), we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\beta\!\left(\mathrm{x}\right)+1$ , and also ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{x}}_1\right)\le \beta\!\left({\mathrm{x}}_1\right)$ . If ${\varSigma}^{\ast}\models \mathrm{abEx}$ or ${\varSigma}^{\ast}\models \mathrm{baEx}$ , then ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\alpha\!\left({\mathrm{x}}_1\right)+1$ and ${\varSigma}^{\ast}\models \beta\!\left(\mathrm{x}\right)=\beta\!\left({\mathrm{x}}_1\right)+1$ . But then

$$\begin{align*}{\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right) & =\beta\!\left(\mathrm{x}\right)+1=\left(\beta\!\left({\mathrm{x}}_1\right)+1\right)+1 \\ &=\beta\!\left({\mathrm{x}}_1\right)+2\ge \alpha\!\left({\mathrm{x}}_1\right)+2>\alpha\!\left({\mathrm{x}}_1\right)+1=\alpha\!\left(\mathrm{x}\right)\!,\end{align*}$$

a contradiction. On the other hand, if ${\varSigma}^{\ast}\models \mathrm{bbEx}$ , then ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\alpha\!\left({\mathrm{x}}_1\right)$ and ${\varSigma}^{\ast}\models \beta\!\left(\mathrm{x}\right)=\beta\!\left({\mathrm{x}}_1\right)+2$ . But then

$$\begin{align*}{\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right) &=\beta\!\left(\mathrm{x}\right)+1=\left(\beta\!\left({\mathrm{x}}_1\right)+2\right)+1 \\ &=\beta\!\left({\mathrm{x}}_1\right)+3\ge \alpha\!\left({\mathrm{x}}_1\right)+3=\alpha\!\left(\mathrm{x}\right)+3>\alpha\!\left(\mathrm{x}\right)\!,\end{align*}$$

a contradiction again. Hence ${\varSigma}^{\ast}\models \;\neg\; \mathrm{abEx}$ & ¬baEx & ¬bbEx. But then we must have ${\varSigma}^{\ast}\models \mathrm{aaEx}$ .

(b) Assume & ${\mathrm{x}}_2\mathrm{Ex}$ . Then ${\varSigma}^{\ast}\models\; \exists\; {\mathrm{x}}_1\mathrm{x}={\mathrm{x}}_1{\mathrm{x}}_2$ , hence ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{x}}_1\right)\le \beta\!\left({\mathrm{x}}_1\right)$ . But ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\beta\!\left(\mathrm{x}\right)+1$ and

$$\begin{align*}{\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\alpha\!\left({\mathrm{x}}_1{\mathrm{x}}_2\right)=\alpha\!\left({\mathrm{x}}_1\right)+\alpha\!\left({\mathrm{x}}_2\right)\!,\end{align*}$$

whereas ${\varSigma}^{\ast}\models \beta\!\left(\mathrm{x}\right)=\beta\!\left({\mathrm{x}}_1{\mathrm{x}}_2\right)=\beta\!\left({\mathrm{x}}_1\right)+\beta\!\left({\mathrm{x}}_2\right)$ . Then

$$\begin{align*}{\varSigma}^{\ast}\models \alpha\!\left({\mathrm{x}}_1\right)+\alpha\!\left({\mathrm{x}}_2\right)=\beta\!\left({\mathrm{x}}_1\right)+\beta\!\left({\mathrm{x}}_2\right)+1,\end{align*}$$

whence from ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{x}}_1\right)\le \beta\!\left({\mathrm{x}}_1\right)$ we have $\alpha\!\left({\mathrm{x}}_2\right)\ge \beta\!\left({\mathrm{x}}_2\right)+1$ , as claimed.

(c) Assume & & $\mathrm{xy}=\mathrm{uv}$ . We have that

$$\begin{align*}{\varSigma}^{\ast}\models \left(\mathrm{x}=\mathrm{u}\;\&\; \mathrm{y}=\mathrm{v}\right)\mathrm{v}\;\mathrm{xBu}\;\mathrm{v}\;\mathrm{u}\mathrm{Bx}.\end{align*}$$

Suppose ${\varSigma}^{\ast}\models \mathrm{xBu}$ . From , we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)\le \beta\!\left(\mathrm{x}\right)$ . From , we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\beta\!\left(\mathrm{x}\right)+1$ . But then ${\varSigma}^{\ast}\models \beta\!\left(\mathrm{x}\right)+1\le \beta\!\left(\mathrm{x}\right)$ , a contradiction. Likewise ${\varSigma}^{\ast}\models \mathrm{uBx}$ yields a contradiction. Hence ${\varSigma}^{\ast}\models \mathrm{x}= \mathrm{u}\;\&\; \mathrm{y}=\mathrm{v}.$

2.2

Proof (⇐) Assume . Then

$$\begin{align*}{\varSigma}^{\ast}\models \alpha\!\left(\mathrm{y}\right)=\beta\!\left(\mathrm{y}\right)+1\;\&\; \alpha\!\left(\mathrm{z}\right)=\beta\!\left(\mathrm{z}\right)+1.\end{align*}$$

Now, we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\alpha\!\left(\mathrm{byz}\right)=\alpha\!\left(\mathrm{y}\mathrm{z}\right)=\alpha\!\left(\mathrm{y}\right)+\alpha\!\left(\mathrm{z}\right)$ and further ${\varSigma}^{\ast}\models \beta\!\left(\mathrm{x}\right)=\beta\!\left(\mathrm{b}\mathrm{yz}\right)=\beta\!\left(\mathrm{b}\right)+\beta\!\left(\mathrm{y}\mathrm{z}\right)=\beta\!\left(\mathrm{y}\right)+\beta\!\left(\mathrm{z}\right)+1$ . Then

$$\begin{align*}{\varSigma}^{\ast} &\models \alpha\!\left(\mathrm{x}\right)=\alpha\!\left(\mathrm{y}\right)+\alpha\!\left(\mathrm{z}\right)=\left(\beta\!\left(\mathrm{y}\right)+1\right)+\left(\beta\!\left(\mathrm{z}\right)+1\right)\\&=\left(\beta\!\left(\mathrm{y}\right)+\beta\!\left(\mathrm{z}\right)+1\right)+1=\beta\!\left(\mathrm{x}\right)+1,\end{align*}$$

which verifies (c1). For (c2), assume ${\varSigma}^{\ast}\models \mathrm{uBx}$ , i.e., that ${\varSigma}^{\ast}\models \mathrm{uBbyz}$ .

Then ${\varSigma}^{\ast}\models \mathrm{u}=\mathrm{b}\;\mathrm{v}\;\mathrm{u}\mathrm{Bby}\;\mathrm{v}\;\mathrm{u}=\mathrm{b}\mathrm{y}\;\mathrm{v}\;\exists\; {\mathrm{z}}_1\left({\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{u}={\mathrm{byz}}_1\right)$ .

To illustrate the proof, we consider the case ${\varSigma}^{\ast}\models \exists\; {\mathrm{z}}_1\left({\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{u}={\mathrm{byz}}_1\right)$ .

Then from , we have ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{z}}_1\right)\le \beta\!\left({\mathrm{z}}_1\right)$ . From , we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{y}\right)=\beta\!\left(\mathrm{y}\right)+1$ . Then ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{u}\right)=\alpha\!\left({\mathrm{byz}}_1\right)=\alpha\!\left({\mathrm{yz}}_1\right)=\alpha\!\left(\mathrm{y}\right)+\alpha\!\left({\mathrm{z}}_1\right)$ whereas ${\varSigma}^{\ast}\models \beta\!\left(\mathrm{u}\right)=\beta\!\left({\mathrm{byz}}_1\right)=\beta\!\left(\mathrm{b}\right)+\beta\!\left({\mathrm{yz}}_1\right)=\beta\!\left(\mathrm{y}\right)+\beta\!\left({\mathrm{z}}_1\right)+1$ . It follows that

$$\begin{equation*}{\displaystyle \begin{array}{l}{\varSigma}^{\ast}\models \alpha\!\left(\mathrm{u}\right)=\alpha\!\left(\mathrm{y}\right)+\alpha\!\left({\mathrm{z}}_1\right)=\left(\beta\!\left(\mathrm{y}\right)+1\right)+\alpha\!\left({\mathrm{z}}_1\right) \\ {}\kern12em \le \left(\beta\!\left(\mathrm{y}\right)+1\right)+\beta\!\left({\mathrm{z}}_1\right)=\beta\!\left(\mathrm{y}\right)+\beta\!\left({\mathrm{z}}_1\right)+1=\beta\!\left(\mathrm{u}\right)\!.\end{array}}\end{equation*}$$

Thus ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{u}\right)\le \beta\!\left(\mathrm{u}\right)$ . This completes the proof of (c2). So .

(⇒) Assume & $\mathrm{x}\ne \mathrm{a}$ . Then, by 2.1(a), Σ* ⊧ bBx & aaEx, that is,

$$\begin{align*}{\varSigma}^{\ast}\models \exists\; {\mathrm{x}}_1\mathrm{x}={\mathrm{bx}}_1\;\&\; \exists\; {\mathrm{x}}_2\mathrm{x}={\mathrm{x}}_2\mathrm{aa}.\end{align*}$$

So ${\varSigma}^{\ast}\models {\mathrm{bx}}_1={\mathrm{x}}_2\mathrm{aa}$ . We may assume that ${\varSigma}^{\ast}\models {\mathrm{bBx}}_2$ , for if ${\varSigma}^{\ast}\models {\mathrm{x}}_2=\mathrm{b}$ , then ${{\varSigma}^{\ast}\models \mathrm{x}=\mathrm{b}\left(\mathrm{aa}\right)}$ and we may take y = a and z = a. So ${\varSigma}^{\ast}\models \exists\; {\mathrm{x}}_3{\mathrm{x}}_2={\mathrm{bx}}_3$ , and ${\varSigma}^{\ast}\models \mathrm{x}={\mathrm{bx}}_1={\mathrm{x}}_2\left(\mathrm{aa}\right)={\mathrm{bx}}_3\left(\mathrm{aa}\right)$ , whence ${\varSigma}^{\ast}\models {\mathrm{x}}_1={\mathrm{x}}_3\left(\mathrm{aa}\right)$ . Let y _j be a proper initial segment of x₁, and z _j the corresponding end segment of x₁ such that ${\varSigma}^{\ast}\models {\mathrm{y}}_j{\mathrm{z}}_j={\mathrm{x}}_1$ . At least one y _j has the property

(*) $$\begin{align}{\varSigma}^{\ast}\models \alpha\!\left({\mathrm{y}}_j\right)=\beta\!\left({\mathrm{y}}_j\right)+1.\end{align}$$

Consider, e.g., x₃a. From hypothesis we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\beta\!\left(\mathrm{x}\right)+1$ .

But ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\alpha\!\left(\mathrm{b}\left(\left({\mathrm{x}}_3\mathrm{a}\right)\mathrm{a}\right)\right)=\alpha\!\left(\mathrm{b}\right)+\alpha\!\left({\mathrm{x}}_3\mathrm{a}\right)+\alpha\!\left(\mathrm{a}\right)=\alpha\!\left({\mathrm{x}}_3\mathrm{a}\right)+1$ and

$$\begin{align*}{\varSigma}^{\ast}\models \beta\!\left(\mathrm{x}\right)=\beta\!\left(\mathrm{b}\left(\left({\mathrm{x}}_3\mathrm{a}\right)\mathrm{a}\right)\right)=\beta\!\left(\mathrm{b}\right)+\beta\!\left({\mathrm{x}}_3\mathrm{a}\right)+\beta\!\left(\mathrm{a}\right)=1+\beta\!\left({\mathrm{x}}_3\mathrm{a}\right)\!.\end{align*}$$

Then ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{x}}_3\mathrm{a}\right)=\alpha\!\left(\mathrm{x}\right)\hbox{--} 1=\beta\!\left(\mathrm{x}\right)=\beta\!\left({\mathrm{x}}_3\mathrm{a}\right)+1$ , as needed.

Let y _i be the shortest initial segment of x₁ with the property (*). Then

$$\begin{align*}{\varSigma}^{\ast}\models {\mathrm{x}}_1={\mathrm{y}}_i{\mathrm{z}}_i\;\&\; \alpha\!\left({\mathrm{y}}_i\right)=\beta\!\left({\mathrm{y}}_i\right)+1.\end{align*}$$

We claim that (i) ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{z}}_i\right)=\beta\!\left({\mathrm{z}}_i\right)+1$ , (ii) ${\varSigma}^{\ast}\models \forall\; \mathrm{u}\left({\mathrm{uBy}}_i\to \alpha\!\left(\mathrm{u}\right)\le \beta\!\left(\mathrm{u}\right)\right)$ , and (iii) ${\varSigma}^{\ast}\models \forall\; \mathrm{v}\left({\mathrm{vBz}}_i\to \alpha\!\left(\mathrm{v}\right)\le \beta\!\left(\mathrm{v}\right)\right)$ .

For (i) we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\alpha\!\left({\mathrm{bx}}_1\right)=\alpha\!\left({\mathrm{x}}_1\right)=\alpha\!\left({\mathrm{y}}_i{\mathrm{z}}_i\right)=\alpha\!\left({\mathrm{y}}_i\right)+\alpha\!\left({\mathrm{z}}_i\right)$ and ${\varSigma}^{\ast}\models \beta\!\left(\mathrm{x}\right)=\beta\!\left({\mathrm{bx}}_1\right)=1+\beta\!\left({\mathrm{x}}_1\right)=1+\beta\!\left({\mathrm{y}}_i{\mathrm{z}}_i\right)=1+\beta\!\left({\mathrm{y}}_i\right)+\beta\!\left({\mathrm{z}}_i\right)\!.$

Then ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{y}}_i\right)+\alpha\!\left({\mathrm{z}}_i\right)=\left(1+\beta\!\left({\mathrm{y}}_i\right)+\beta\!\left({\mathrm{z}}_i\right)\right)+1$ , and from ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{y}}_i\right)=\beta\!\left({\mathrm{y}}_i\right)+1$ we obtain ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{z}}_i\right)=\beta\!\left({\mathrm{z}}_i\right)+1$ .

For (ii), suppose ${\varSigma}^{\ast}\models {\mathrm{uBy}}_i$ . Since ${\varSigma}^{\ast}\models {\mathrm{x}}_1={\mathrm{y}}_{\mathrm{i}}{\mathrm{z}}_{\mathrm{i}}$ , we then have ${\varSigma}^{\ast}\models {\mathrm{uBx}}_1$ . But then, by the choice of y _i , ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{u}\right)\le \beta\!\left(\mathrm{u}\right)$ . For (iii), suppose ${\varSigma}^{\ast}\models {\mathrm{vBz}}_i$ . Then ${\varSigma}^{\ast}\models \exists\; \mathrm{w}\;{\mathrm{z}}_i=\mathrm{vw}$ , whence ${\varSigma}^{\ast}\models \mathrm{wEx}$ . From , by 2.1(b), ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{w}\right)\ge \beta\!\left(\mathrm{w}\right)+1$ . But ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{z}}_i\right)=\alpha\!\left(\mathrm{v}\right)+\alpha\!\left(\mathrm{w}\right)$ and ${\varSigma}^{\ast}\models \beta\!\left({\mathrm{z}}_i\right)=\beta\!\left(\mathrm{v}\right)+\beta\!\left(\mathrm{w}\right)$ . By (i), ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{v}\right)+\alpha\!\left(\mathrm{w}\right)=\beta\!\left(\mathrm{v}\right)+\beta\!\left(\mathrm{w}\right)+1$ .

Then from ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{w}\right)\ge \beta\!\left(\mathrm{w}\right)+1$ , we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{v}\right)\le \beta\!\left(\mathrm{v}\right)$ .

From (i)–(iii) we have that & . The uniqueness of y, z follows from 2.1(c).

2.3

Proof Assume ${\varSigma}^{\ast}\models \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{byz}$ where & Æ(y) & Æ(z). Now, we have that

$$\begin{align*}{\varSigma}^{\ast}\models \mathrm{x}=\mathrm{b}\mathrm{yz}\;\mathrm{v}\;\mathrm{x}=\mathrm{b}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{yz}\;\mathrm{v}\;\exists\; \mathrm{u}\left(\mathrm{uByz}\;\&\; \mathrm{x}=\mathrm{b}\mathrm{u}\right)\!. \end{align*}$$

Suppose that ${\varSigma}^{\ast}\models \exists\; \mathrm{u}\left(\mathrm{uByz}\;\&\; \mathrm{x}=\mathrm{bu}\right)$ . From & Æ(z), by 2.2, . From ${\varSigma}^{\ast}\models \mathrm{uByz}$ , we have ${\varSigma}^{\ast}\models \exists\; \mathrm{v}\;\mathrm{uv}=\mathrm{yz}$ , whence ${\varSigma}^{\ast}\models \mathrm{buBb}\left(\mathrm{yz}\right)$ . Thus ${\varSigma}^{\ast}\models \mathrm{xBb}\left(\mathrm{yz}\right)$ . But from , we also have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)\le \beta\!\left(\mathrm{x}\right)$ , which contradicts . So ${\varSigma}^{\ast}\models \exists\; \mathrm{u}\left(\mathrm{uByz}\;\&\; \mathrm{x}=\mathrm{bu}\right)$ is ruled out. By 2.1(a), so is ${\varSigma}^{\ast}\models \mathrm{x}=\mathrm{b}$ . So we are left with ${\varSigma}^{\ast}\models \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{byz}\to \mathrm{x}=\mathrm{byz}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{yz}$ . Supposing ${\varSigma}^{\ast}\models \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{yz}$ , we have that

$$\begin{equation*}{\displaystyle \begin{array}{l}{\varSigma}^{\ast}\models \mathrm{x}=\mathrm{yz}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}\;\mathrm{v}\;\exists\; {\mathrm{y}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; \mathrm{x}={\mathrm{y}}_1\mathrm{z}\right)\\[3pt] {}\kern8.24em \mathrm{v}\;\exists\; {\mathrm{z}}_1\left({\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}={\mathrm{y}\mathrm{z}}_1\right)\;\mathrm{v}\;\exists\; {\mathrm{y}}_1,{\mathrm{z}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; {\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}={\mathrm{y}}_1{\mathrm{z}}_1\right)\!.\end{array}}\end{equation*}$$

Assume ${\varSigma}^{\ast}\models \mathrm{x}=\mathrm{yz}$ . Then from & Æ(z), we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{y}\right)=\beta\!\left(\mathrm{y}\right)+1$ and $\alpha\!\left(\mathrm{z}\right)=\beta\!\left(\mathrm{z}\right)+1$ . But ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{y}\mathrm{z}\right)=\alpha\!\left(\mathrm{y}\right)+\alpha\!\left(\mathrm{z}\right)$ , so

$$\begin{align*}{\varSigma}^{\ast}\models \alpha\!\left(\mathrm{y}\mathrm{z}\right)=\left(\beta\!\left(\mathrm{y}\right)+1\right)+\left(\beta\!\left(\mathrm{z}\right)+1\right)=\beta\!\left(\mathrm{y}\right)+\beta\!\left(\mathrm{z}\right)+2.\end{align*}$$

On the other hand, ${\varSigma}^{\ast}\models \beta\!\left(\mathrm{y}\mathrm{z}\right)=\beta\!\left(\mathrm{y}\right)+\beta\!\left(\mathrm{z}\right)$ . Thus ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{yz}\right)=\beta\!\left(\mathrm{yz}\right)+2$ , whence from ${\varSigma}^{\ast}\models \mathrm{x}=\mathrm{yz}$ , we derive ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{x}\right)=\beta\!\left(\mathrm{x}\right)+2$ , contradicting . So ${\varSigma}^{\ast}\models \mathrm{x}=\mathrm{yz}$ is ruled out.

Suppose now that ${\varSigma}^{\ast}\models \exists\; {\mathrm{y}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; \mathrm{x}={\mathrm{y}}_1\mathrm{z}\right)$ , so ${\varSigma}^{\ast}\models {\mathrm{y}}_1\mathrm{Bx}$ . From , we have ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{y}}_1\right)\le \beta\!\left({\mathrm{y}}_1\right)$ . But from & y₁Ey, we also obtain, by 2.1(b), ${\varSigma}^{\ast}\models \alpha\!\left({\mathrm{y}}_1\right)\ge \beta\!\left({\mathrm{y}}_1\right)+1$ , a contradiction.

Suppose that ${\varSigma}^{\ast}\models \exists\; {\mathrm{z}}_1\left({\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}={\mathrm{yz}}_1\right)$ , so ${\varSigma}^{\ast}\models \mathrm{yBx}$ . But then from , we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{y}\right)\le \beta\!\left(\mathrm{y}\right)$ . From , we have ${\varSigma}^{\ast}\models \alpha\!\left(\mathrm{y}\right)= \beta\!\left(\mathrm{y}\right)+1$ , again a contradiction. If ${\varSigma}^{\ast}\models \exists\; {\mathrm{y}}_1,{\mathrm{z}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; {\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}={\mathrm{y}}_1{\mathrm{z}}_1\right)$ , we derive a contradiction by reasoning as in either of the two preceding cases. This proves that ${\varSigma}^{\ast}\models \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{byz}\to \mathrm{x}=\mathrm{byz}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}$ , as required.

If we take the domain to consists of Æ-strings, 2.1(c), 2.2, and 2.3 suffice to give the “first approximation” of our interpretation of T in concatenation theory: translations of (T1)–(T4) will be validated in Σ* if we model the term/tree-building operation x, $\mathrm{y}\mapsto \left(\mathrm{xy}\right)$ by bxy, the subterm/subtree relation ⊑ by the substring relation ${\subseteq}_{\mathrm{p}}$ between Æ-strings, and the digit a is taken to stand for the simple term 0. The entire project, however, hinges on definability of the counting functions α and β in concatenation theory. Showing that the latter contains resources needed to formally justify definitions by elementary recursion on strings requires, first, that we precisely formulate concatenation theory as a formal theory, and second, that we introduce codings for ordered pairs of strings, sequences of such, etc., and verify in that formal theory their properties relevant to the argument. We now turn to that task. In the process we shall make crucial use of the method of formula selection explained in [Reference Damnjanovic1].

3.1

(a) I₀(x) is a string form

1. (b) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \mathrm{J}\left(\mathrm{x}\right)\;\&\; \mathrm{J}\left(\mathrm{y}\right)\to \mathrm{J}\left(\mathrm{x}^\ast \mathrm{y}\right)\!.\end{align*}$$

2. (c) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form ${\mathrm{J}}_{\le}\subseteq {\mathrm{I}}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash {\mathrm{J}}_{\le}\left(\mathrm{x}\right)\;\&\; \mathrm{y}\le \mathrm{x}\to {\mathrm{J}}_{\le}\left(\mathrm{y}\right)\!.\end{align*}$$

3. (d) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in \mathrm{J}\left(\mathrm{y}\;{\subseteq}_{\mathrm{p}}\;\mathrm{x}\to \mathrm{J}\left(\mathrm{y}\right)\right)\!.\end{align*}$$

4. (e) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\equiv {\mathrm{I}}_{\mathrm{LC}}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{z}\in \mathrm{J}\left(\mathrm{z}^\ast \mathrm{x}=\mathrm{z}^\ast \mathrm{y}\to \mathrm{x}=\mathrm{y}\right)\!.\end{align*}$$

5. (f) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{z}\in \mathrm{J}\left(\mathrm{x}^\ast \mathrm{z}=\mathrm{y}^\ast \mathrm{z}\to \mathrm{x}=\mathrm{y}\right)\!.\end{align*}$$

For proofs, see [Reference Damnjanovic1], [Reference Damnjanovic2, (3.2), (3.3), (3.6), (3.7), and (3.13)].⊣

Parts (b–d) tell us that when establishing that a given string form I may be strengthened to a string form J with another property, we can always strengthen the string form J to one that is also closed with respect to * or downward closed with respect to ≤ or ${\subseteq}_{\mathrm{p}}$ .

We define ${\mathrm{Tally}}_{\mathrm{a}}\!\left(\mathrm{x}\right)\equiv \forall\; \mathrm{y}\;{\subseteq}_{\mathrm{p}}\;\mathrm{x}\left(\mathrm{Digit}\left(\mathrm{y}\right)\to \mathrm{y}=\mathrm{a}\right)$ and ${\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\equiv \forall\; \mathrm{y}\;{\subseteq}_{\mathrm{p}}\;\mathrm{x}\left(\mathrm{Digit}\left(\mathrm{y}\right)\to \mathrm{y}=\mathrm{b}\right)$ where $\mathrm{Digit}\left(\mathrm{x}\right)\equiv \mathrm{x}=\mathrm{a}\;\mathrm{v}\;\mathrm{x}=\mathrm{b}$ .

The following properties of tallies are easily established:

3.2

(a) ${\mathrm{QT}}^{+}\vdash {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\to {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{Sy}\right)$ .

1. (b) ${\mathrm{QT}}^{+}\vdash {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\leftrightarrow \mathrm{y}=\mathrm{b}\;\mathrm{v}\;\exists\; {\mathrm{y}}_1\left({\mathrm{Tally}}_{\mathrm{b}}\!\left({\mathrm{y}}_1\right)\;\&\; \mathrm{y}={\mathrm{Sy}}_1\right)\!.$

2. (c) ${\mathrm{QT}}^{+}\vdash {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{v}\right)\;\&\; \mathrm{u}<\mathrm{v}\to \mathrm{Su}\le \mathrm{v}.$

3. (d) ${\mathrm{QT}}^{+}\vdash {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\to \left(\mathrm{x}<\mathrm{y}\leftrightarrow \mathrm{Sx}<\mathrm{Sy}\right)\!.$

For some further properties we have to resort to string forms:

3.3

(a) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\equiv {\mathrm{I}}_{\mathrm{CTC}}\subseteq \mathrm{I}$ such that.

$$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{z}\in \mathrm{J}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{z}\right)\to {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}^\ast \mathrm{z}\right)\right)\!.\end{align*}$$

1. (b) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{z}\in \mathrm{J}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{z}\right)\to \mathrm{x}\le \mathrm{z}\;\mathrm{v}\;\mathrm{z}\le \mathrm{x}\right)\!.\end{align*}$$

2. (c) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\equiv {\mathrm{I}}_{3.3\left(\mathrm{c}\right)}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{u}\in \mathrm{J}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{u}\right)\to \mathrm{u}^\ast \mathrm{b}=\mathrm{b}^\ast \mathrm{u}\right)\!.\end{align*}$$

3. (d) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{y}\in \mathrm{J}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\to \mathrm{Sx}^\ast \mathrm{y}=\mathrm{x}^\ast \mathrm{Sy}=\mathrm{S}\left(\mathrm{x}^\ast \mathrm{y}\right)\right)\!.\end{align*}$$

4. (e) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_{3.3\left(\mathrm{c}\right)}$ there is a string form $\mathrm{J}\equiv {\mathrm{I}}_{\mathrm{COMM}}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{u},\mathrm{v}\in \mathrm{J}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{u}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{v}\right)\to \mathrm{u}^\ast \mathrm{v}=\mathrm{v}^\ast \mathrm{u}\right)\!.\end{align*}$$

For proofs, see [Reference Damnjanovic2, (4.5), (4.6), (4.8), and (4.10)].⊣

Let Addtally(x,y,z) abbreviate the formula

$$\begin{equation*}{\displaystyle \begin{array}{l}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\;\&\; \big(\left(\mathrm{x}=\mathrm{b}\;\&\; \mathrm{z}=\mathrm{y}\right)\;\mathrm{v}\;\left(\mathrm{y}=\mathrm{b}\;\&\; \mathrm{z}=\mathrm{x}\right)\right.\\ {}\kern3.8em \left.\mathrm{v}\;\exists\; {\mathrm{x}}_1,{\mathrm{y}}_1\left({\mathrm{Tally}}_{\mathrm{b}}\!\left({\mathrm{x}}_1\right)\;\&\; \mathrm{x}={\mathrm{Sx}}_1\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left({\mathrm{y}}_1\right)\;\&\; \mathrm{y}={\mathrm{Sy}}_1\;\&\; \mathrm{z}=\mathrm{x}^\ast {\mathrm{y}}_1\right)\right)\\ {}\kern17em \mathrm{v}\;\left(\left(\neg\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\mathrm{v}\;\neg\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\right)\;\&\; \mathrm{z}=\mathrm{b}\right)\!.\end{array}}\end{equation*}$$

We want to show that, provably in QT⁺, Addtally(x,y,z) behaves like the graph of addition function on natural numbers. The following are immediate consequences of definitions:

3.4

(a) ${\mathrm{QT}}^{+}\vdash \mathrm{Addtally}\left(\mathrm{x},\mathrm{y},\mathrm{v}\right)\;\&\; \mathrm{Addtally}\left(\mathrm{x},\mathrm{y},\mathrm{w}\right)\to \mathrm{v}=\mathrm{w}$ .

1. (b) ${\mathrm{QT}}^{+}\vdash {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\to \mathrm{Addtally}\left(\mathrm{x},\mathrm{b},\mathrm{x}\right)\!.\kern3.479999em \left("\mathrm{x}+0=\mathrm{x}"\right)$

2. (c) ${\mathrm{QT}}^{+}\vdash {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\to \mathrm{Addtally}\left(\mathrm{b},\mathrm{y},\mathrm{y}\right)\!.\kern3.239999em \ \left("0+\mathrm{y}=\mathrm{y}"\right)$

3. (d) ${\mathrm{QT}}^{+}\vdash {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\to \mathrm{Addtally}\left(\mathrm{x},\mathrm{bb},\mathrm{Sx}\right)\!.\kern2.639999em \left("\mathrm{x}+1=\mathrm{Sx}"\right)$

4. (e) $\!\!\!{\displaystyle \begin{array}[t]{l}{\mathrm{QT}}^{+}\vdash {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\to \left(\mathrm{Addtally}\left(\mathrm{x},\mathrm{y},\mathrm{z}\right)\to \mathrm{Addtally}\left(\mathrm{x},\mathrm{y}\mathrm{b},\mathrm{z}\mathrm{b}\right)\right)\!.\\ {}\left("\mathrm{x}+\mathrm{Sy}=\mathrm{S}\left(\mathrm{x}+\mathrm{y}\right)"\right)\end{array}}$

We also have:

3.5

(a) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\equiv {\mathrm{I}}_{\mathrm{Add}}\subseteq \mathrm{I}$ such that.

$$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x},\mathrm{y}\in \mathrm{J}\;\exists\; !\mathrm{z}\in \mathrm{J}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{z}\right)\;\&\; \mathrm{Addtally}\left(\mathrm{x},\mathrm{y},\mathrm{z}\right)\right)\!.\end{align*}$$

1. (b) ${\displaystyle \begin{array}[t]{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{z}\in {\mathrm{I}}_0\big({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{u}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{v}\right) \\ {}\kern6em \;\&\; \mathrm{Addtally}\left(\mathrm{x},\mathrm{u},\mathrm{y}\right)\;\&\; \mathrm{Addtally}\left(\mathrm{x},\mathrm{v},\mathrm{z}\right)\;\&\; \mathrm{u}\le \mathrm{v}\to \mathrm{y}\le \mathrm{z}\big).\\ {}\kern18.24em \left("\mathrm{u}\le \mathrm{v}\to \mathrm{x}+\mathrm{u}\le \mathrm{x}+\mathrm{v}"\right)\end{array}}$

2. (c) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{y}\in \mathrm{J}\;\big({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\to \mathrm{Addtally}\left(\mathrm{bb},\mathrm{y},\mathrm{Sy}\right)\!.\kern2.639999em \left("1+\mathrm{y}=\mathrm{Sy}"\right)\end{align*}$$

3. (d) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{equation*} \hspace{-2.2pc} {\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{y}\in \mathrm{J}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\;\&\; \mathrm{Addtally}\left(\mathrm{x},\mathrm{y},\mathrm{z}\right)\to \mathrm{Addtally}\left(\mathrm{x}\mathrm{b},\mathrm{y},\mathrm{z}\mathrm{b}\right)\right)\!.\\ {}\kern23em \left("\mathrm{Sx}+\mathrm{y}=\mathrm{S}\left(\mathrm{x}+\mathrm{y}\right)"\right)\end{array}}\end{equation*}$$

4. (e) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{equation*} {\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in \mathrm{J}\big({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{z}\right) \\ {}\kern9em \to \left(\mathrm{Addtally}\left(\mathrm{x},\mathrm{y},\mathrm{v}\right)\;\&\; \mathrm{Addtally}\left(\mathrm{x},\mathrm{z},\mathrm{v}\right)\to \mathrm{y}=\mathrm{z}\right)\big).\\ {}\kern20em \left("\mathrm{x}+\mathrm{y}=\mathrm{x}+\mathrm{z}\to \mathrm{y}=\mathrm{z}"\right)\end{array}}\end{equation*}$$

5. (f) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{equation*}{\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{y}\in \mathrm{J}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right) \right.\\ {}\kern10em \left.\to \left(\mathrm{x}\le \mathrm{y}\leftrightarrow \;\exists\; \mathrm{z}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{z}\right)\;\&\; \mathrm{Addtally}\left(\mathrm{z},\mathrm{x},\mathrm{y}\right)\right)\right)\right)\!.\\ {}\kern20em \left("\mathrm{x}\le \mathrm{y}\leftrightarrow \;\exists\; \mathrm{z}\;\mathrm{z}+\mathrm{x}=\mathrm{y}"\right)\end{array}}\end{equation*}$$

6. (g) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x},\mathrm{y}\in \mathrm{J}\left(\mathrm{Addtally}\left(\mathrm{x},\mathrm{y},\mathrm{z}\right)\to \mathrm{Addtally}\left(\mathrm{y},\mathrm{x},\mathrm{z}\right)\right)\!.\kern1.08em \left("\mathrm{x}+\mathrm{y}=\mathrm{y}+\mathrm{x}"\right)\end{align*}$$

7. (h) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{equation*}{\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x},\mathrm{y},\mathrm{z}\in \mathrm{J}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{y}\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{z}\right)\;\&\; \mathrm{Addtally}\left(\mathrm{x},\mathrm{y},\mathrm{u}\right) \right.\\ \left.\;\&\; \mathrm{Addtally}\left(\mathrm{u},\mathrm{z},{\mathrm{v}}_1\right)\;\&\; \mathrm{Addtally}\left(\mathrm{y},\mathrm{z},\mathrm{w}\right)\;\&\; \mathrm{Addtally}\left(\mathrm{x},\mathrm{w},{\mathrm{v}}_2\right)\to {\mathrm{v}}_1={\mathrm{v}}_2\right)\!.\\ {}\kern19em \left("\left(\mathrm{x}+\mathrm{y}\right)+\mathrm{z}=\mathrm{x}+\left(\mathrm{y}+\mathrm{z}\right)"\right)\end{array}}\end{equation*}$$

8. (i) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{equation*}{\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \;\forall\; {\mathrm{x}}_2,{\mathrm{y}}_1,{\mathrm{y}}_2\in \mathrm{J}\big({\mathrm{Tally}}_{\mathrm{b}}\!\left({\mathrm{x}}_2\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left({\mathrm{y}}_1\right)\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left({\mathrm{y}}_2\right) \\ {}\kern2em \;\&\; \mathrm{Addtally}\left({\mathrm{x}}_1,{\mathrm{x}}_2,{\mathrm{z}}_1\right)\;\&\; \mathrm{Addtally}\left({\mathrm{y}}_1,{\mathrm{y}}_2,{\mathrm{z}}_2\right)\;\&\; {\mathrm{x}}_1\le {\mathrm{y}}_1\;\&\; {\mathrm{z}}_1={\mathrm{Sz}}_2 \\ {}\kern25em \to {\mathrm{Sy}}_2\le {\mathrm{x}}_2\big).\\ {}\kern9em \left("{\mathrm{x}}_1+{\mathrm{x}}_2=\left({\mathrm{y}}_1+{\mathrm{y}}_2\right)+1\;\&\; {\mathrm{x}}_1\le {\mathrm{y}}_1\to {\mathrm{y}}_2+1\le {\mathrm{x}}_2"\right)\end{array}}\end{equation*}$$

We now turn to the part-of relation ${\subseteq}_{\mathrm{p}}$ between strings. To prevent unpleasant surprises, we want to make sure that this relation has natural properties we would normally expect it to have.

3.6

(a) ${\mathrm{QT}}^{+}\vdash \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\;\&\; \mathrm{y}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}\to \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}$ .

1. (b) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in \mathrm{J}\;\neg\; \mathrm{x}\mathrm{Ex}.\end{align*}$$

2. (c) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*} {\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in \mathrm{J}\;\neg \;\exists\; {\mathrm{x}}_1,{\mathrm{x}}_2\left({\mathrm{x}}_1{\mathrm{x}\mathrm{x}}_2=\mathrm{x}\right)\!.\end{align*}$$

3. (d) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in \mathrm{J}\left(\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\;\&\; \mathrm{y}\;{\subseteq}_{\mathrm{p}}\;\mathrm{x}\to \mathrm{x}=\mathrm{y}\right)\!.\end{align*}$$

4. (e) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in \mathrm{J}\left(\neg\; \mathrm{x}\mathrm{y}\;{\subseteq}_{\mathrm{p}}\;\mathrm{x}\;\&\; \neg\; \mathrm{yx}\;{\subseteq}_{\mathrm{p}}\;\mathrm{x}\right)\!.\end{align*}$$

We now specifically consider proper initial segments and end segments. The initial segments of arbitrary strings can be totally ordered by the initial-segment-of relation B, rendering the partial ordering < in which a is the least element tree-like:

3.7

(a) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\equiv {\mathrm{J}}_{\mathrm{LOIS}}\subseteq \mathrm{I}$ such that.

$$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in \mathrm{J}\left(\mathrm{uBx}\;\&\; \mathrm{vBx}\to \mathrm{u}=\mathrm{v}\;\mathrm{v}\;\mathrm{uBv}\;\mathrm{v}\;\mathrm{v}\mathrm{Bu}\right)\!.\end{align*}$$

1. (b) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{y},\mathrm{z}\in \mathrm{J}\left(\mathrm{xByz}\leftrightarrow \mathrm{xBy}\;\mathrm{v}\;\mathrm{x}=\mathrm{y}\;\mathrm{v}\;\exists\; \mathrm{w}\left(\mathrm{wBz}\;\&\; \mathrm{yw}=\mathrm{x}\right)\right)\!.\end{align*}$$

2. (c) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*} \hspace{-2pc} {\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x},\mathrm{y}\in \mathrm{J}\left(\mathrm{uBb}\left(\mathrm{xy}\right)\to \mathrm{u}=\mathrm{b}\;\mathrm{v}\;\mathrm{u}\mathrm{Bbx}\;\mathrm{v}\;\mathrm{u}=\mathrm{b}\mathrm{x}\;\mathrm{v}\;\exists\; {\mathrm{y}}_1\left({\mathrm{y}}_1\mathrm{By}\;\&\; \mathrm{u}={\mathrm{bxy}}_1\right)\right)\!.\end{align*}$$

3. (d) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in \mathrm{J}\left(\mathrm{uEx}\;\&\; \mathrm{vEx}\to \mathrm{u}=\mathrm{v}\;\mathrm{v}\;\mathrm{uEv}\;\mathrm{v}\;\mathrm{v}\mathrm{Eu}\right)\!.\end{align*}$$

4. (e) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{y},\mathrm{z}\in \mathrm{J}\left(\mathrm{xEyz}\leftrightarrow \mathrm{xEz}\;\mathrm{v}\;\mathrm{x}=\mathrm{z}\;\mathrm{v}\;\exists\; \mathrm{w}\left(\mathrm{wEy}\;\&\; \mathrm{wz}=\mathrm{x}\right)\right)\!.\end{align*}$$

5. (f) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{equation*}{\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{y},\mathrm{z}\in \mathrm{J}\big({\mathrm{x}}_1{\mathrm{x}\mathrm{x}}_2=\mathrm{yz} \\ {}\kern7em \to \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}\;\mathrm{v}\;\exists\; {\mathrm{y}}_1,{\mathrm{z}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; {\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}={\mathrm{y}}_1{\mathrm{z}}_1\right)\big).\end{array}}\end{equation*}$$

6. (g) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{equation*} \hspace{-1.2pc} {\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{y},\mathrm{z}\in \mathrm{J}\;\big(\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\mathrm{z}\to \mathrm{x}=\mathrm{yz}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}\;\mathrm{v}\;\exists\; {\mathrm{y}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; \mathrm{x}={\mathrm{y}}_1\mathrm{z}\right) \\ {}\kern7em \mathrm{v}\;\exists\; {\mathrm{z}}_1\left({\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}={\mathrm{y}\mathrm{z}}_1\right)\;\mathrm{v}\;\exists\; {\mathrm{y}}_1,{\mathrm{z}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; {\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}={\mathrm{y}}_1{\mathrm{z}}_1\right)\big).\end{array}}\end{equation*}$$

7. (h) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

   $$\begin{equation*}{\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{y},\mathrm{z}\in \mathrm{J}\big(\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{b}\left(\mathrm{yz}\right) \\ {}\kern7em \to \mathrm{x}=\mathrm{b}\mathrm{yz}\;\mathrm{v}\;\mathrm{x}=\mathrm{b}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{yz}\;\mathrm{v}\;\exists\; {\mathrm{u}}_2\left({\mathrm{u}}_2\mathrm{Byz}\;\&\; \mathrm{x}={\mathrm{bu}}_2\right)\big).\end{array}}\end{equation*}$$

4.1

(a) Singleton Lemma. For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form ${\mathrm{I}}_{\mathrm{SNGL}}\subseteq \mathrm{I}$ such that.

$$\begin{equation*}{\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in {\mathrm{I}}_{\mathrm{SNGL}}\big(\mathrm{Set}\left(\mathrm{x}\right)\;\&\; \mathrm{Firstf}\left(\mathrm{x},{\mathrm{t}}_1,\mathrm{aua},{\mathrm{t}}_2\right)\;\&\;\mathrm{x}={\mathrm{t}}_1{\mathrm{auat}}_2 \\ {}\kern20em \to \forall\; \mathrm{w}\;\left(\mathrm{w}\;\varepsilon\;\mathrm{x}\leftrightarrow \mathrm{w}=\mathrm{u}\right)\big).\end{array}}\end{equation*}$$

1. (b) Appending Lemma. For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form ${\mathrm{I}}_{\mathrm{APP}}\subseteq \mathrm{I}$ such that

   $$\begin{equation*} \hspace{-2pc} {\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x},\mathrm{y}\in {\mathrm{I}}_{\mathrm{APP}}\big(\mathrm{Env}\left({\mathrm{t}}_2,\mathrm{x}\right)\;\&\; \mathrm{Env}\left(\mathrm{t},\mathrm{y}\right)\;\&\; \left({\mathrm{t}}_3\mathrm{a}\right)\mathrm{By}\;\&\; {\mathrm{Tally}}_{\mathrm{b}}\!\left({\mathrm{t}}_3\right)\;\&\; {\mathrm{t}}_2<{\mathrm{t}}_3 \\ \;\&\; \neg \;\exists\; \mathrm{u}\left(\mathrm{u}\;\varepsilon\; \mathrm{x}\;\&\; \mathrm{u}\;\varepsilon\; \mathrm{y}\right)\to \;\exists\; \mathrm{z}\in {\mathrm{I}}_{\mathrm{APP}}\left(\mathrm{Env}\left(\mathrm{t},\mathrm{z}\right)\;\&\; \forall\; \mathrm{u}\left(\mathrm{u}\;\varepsilon\;\mathrm{z}\leftrightarrow \mathrm{u}\;\varepsilon\;\mathrm{x}\;\mathrm{v}\;\mathrm{u}\;\varepsilon\;\mathrm{y}\right)\right)\!.\end{array}}\end{equation*}$$

2. (c) Doubleton Lemma. For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form ${\mathrm{I}}_{\mathrm{DBL}}\subseteq \mathrm{I}$ such that

   $$\begin{equation*} \hspace{-1pc} {\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in {\mathrm{I}}_{\mathrm{DBL}}\big(\mathrm{Pref}\left(\mathrm{aua},{\mathrm{t}}_1\right)\;\&\; \mathrm{Pref}\left(\mathrm{ava},{\mathrm{t}}_2\right)\;\&\; {\mathrm{t}}_1<{\mathrm{t}}_2\;\&\; {\mathrm{t}}_2={\mathrm{t}}_3\;\&\; \mathrm{u}\ne \mathrm{v} \\ {}\kern5em \;\&\; \mathrm{x}={\mathrm{t}}_1{\mathrm{auat}}_2{\mathrm{avat}}_3\to \mathrm{Set}\left(\mathrm{x}\right)\;\&\; \forall\; \mathrm{w}\left(\mathrm{w}\;\varepsilon\;\mathrm{x}\leftrightarrow \left(\mathrm{w}=\mathrm{u}\;\mathrm{v}\;\mathrm{w}=\mathrm{v}\right)\right)\!.\end{array}}\end{equation*}$$

To use the coding of sets to code sequences of strings, we need to populate the coded sets with ordered pairs of arbitrary strings.

Let $\mathrm{Pair}\left[\mathrm{x},\mathrm{y},\mathrm{z}\right]\equiv \;\exists\; \mathrm{t}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}\left(\mathrm{z}=\mathrm{taxatayat}\;\&\; {\mathrm{MinMax}}^{+}{\mathrm{T}}_{\mathrm{b}}\!\left(\mathrm{t},\mathrm{xay}\right)\right)\!,$

where ${\mathrm{MinMax}}^{+}{\mathrm{T}}_{\mathrm{b}}\!\left(\mathrm{t},\mathrm{u}\right)\equiv {\operatorname{Max}}^{+}{\mathrm{T}}_{\mathrm{b}}\!\left(\mathrm{t},\mathrm{u}\right)\;\&\; \forall\; \mathrm{t}'\left({\operatorname{Max}}^{+}{\mathrm{T}}_{\mathrm{b}}\!\left(\mathrm{t}',\mathrm{u}\right)\to \mathrm{t}\le \mathrm{t}'\right)$ .

We then have:

4.2

Pairing Lemma. (a) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_0$ there is a string form $\mathrm{J}\subseteq \mathrm{I}$ such that

$$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x},\mathrm{y}\in \mathrm{J}\;\exists\; \mathrm{z}\in \mathrm{J}\left(\mathrm{Pair}\left[\mathrm{x},\mathrm{y},\mathrm{z}\right]\;\&\; \forall\; \mathrm{z}'\left(\mathrm{Pair}\left[\mathrm{x},\mathrm{y},\mathrm{z}'\right]\to \mathrm{z}'=\mathrm{z}\right)\right)\!.\end{align*}$$

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

$$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{z}\in \mathrm{J}\left(\mathrm{Pair}\left[{\mathrm{x}}_1,{\mathrm{y}}_1,\mathrm{z}\right]\;\&\; \mathrm{Pair}\left[{\mathrm{x}}_2,{\mathrm{y}}_2,\mathrm{z}\right]\to {\mathrm{x}}_1={\mathrm{x}}_2\;\&\; {\mathrm{y}}_1={\mathrm{y}}_2\right)\!.\end{align*}$$

In (a), choose J as in [Reference Damnjanovic2, (6.8)]. For (b), referring to [Reference Damnjanovic2], let $\mathrm{J}\equiv {\mathrm{I}}_{3.6}$ & I_4.20 & I_4.23b.⊣

5.1

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

$$\begin{align*}{\mathrm{QT}}^{+}\vdash {\mathrm{A}}^{\#}\left(\mathrm{a},\mathrm{Sb}\right)\;\&\; \forall\; \mathrm{x}\in \mathrm{J}\;\forall\; \mathrm{y}\in \mathrm{I}\;\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{A}}^{\#}\left(\mathrm{x},\mathrm{y}\right)\to \mathrm{y}=\mathrm{b}\right)\kern0.6em \mathrm{and}\end{align*}$$

$$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in \mathrm{J}\;\forall\; \mathrm{y}\in \mathrm{I}\left({\mathrm{Tally}}_{\mathrm{a}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{B}}^{\#}\left(\mathrm{x},\mathrm{y}\right)\to \mathrm{y}=\mathrm{b}\right)\!.\end{align*}$$

(That is, “α(a)=1” and “ ${\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\to \alpha\!\left(\mathrm{x}\right)=0$ ,” and “ ${\mathrm{Tally}}_{\mathrm{a}}\!\left(\mathrm{x}\right)\to \beta\!\left(\mathrm{x}\right)=0$ .”)

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

$$\begin{align*}{\mathrm{QT}}^{+}\vdash \forall\; \mathrm{x}\in \mathrm{J}\;\forall\; \mathrm{y}\in \mathrm{I}\left({\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\;\&\; {\mathrm{B}}^{\#}\left(\mathrm{x},\mathrm{y}\right)\to \mathrm{y}=\mathrm{x}^\ast \mathrm{b}\right)\!.\end{align*}$$

Informally, ${\mathrm{Tally}}_{\mathrm{b}}\!\left(\mathrm{x}\right)\to \beta\!\left(\mathrm{x}\right)=\mathrm{length}\left(\mathrm{x}\right)$ .

We now verify that the functions α and β are indeed additive. Let I_Add be as in 3.5(a).

5.2

(a) For any string form I such that $\mathrm{I}\subseteq {\mathrm{I}}_{\alpha}$ and $\mathrm{I}\subseteq {\mathrm{I}}_{\mathrm{Add}}$ there is a string form $\mathrm{J}\equiv {\mathrm{I}}_{\mathrm{Add}\alpha}\subseteq \mathrm{I}$ such that

$$\begin{equation*} \hspace{-0.4pc} {\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\, \mathrm{x},\mathrm{y} {{\kern-2pt}\in{\kern-2pt}} \mathrm{J}\,\forall\, \mathrm{u},\mathrm{v},\mathrm{w}\left({\mathrm{A}}^{\#}\left(\mathrm{x},\mathrm{u}\right)\,\&\, {\mathrm{A}}^{\#}\left(\mathrm{y},\mathrm{v}\right)\,\&\, \mathrm{AddTally}\left(\mathrm{u},\mathrm{v},\mathrm{w}\right) {{\kern-2pt}\to{\kern-2pt}} {\mathrm{A}}^{\#}\left(\mathrm{x}^\ast \mathrm{y},\mathrm{w}\right)\right)\!.\\ {}\kern22em \left(“\alpha\!\left(\mathrm{x}^\ast \mathrm{y}\right)=\alpha\!\left(\mathrm{x}\right)+\alpha\!\left(\mathrm{y}\right)”\right)\end{array}}\end{equation*}$$

(b) For any string form $\mathrm{I}\subseteq {\mathrm{I}}_{\beta}$ and $\mathrm{I}\subseteq {\mathrm{I}}_{\mathrm{Add}}$ there is a string form $\mathrm{J}\equiv {\mathrm{I}}_{\mathrm{Add}\beta}\subseteq \mathrm{I}$ such that

$$\begin{equation*} \hspace{-0.4pc} {\displaystyle \begin{array}{l}{\mathrm{QT}}^{+}\vdash \forall\, \mathrm{x},\mathrm{y} {{\kern-2pt}\in{\kern-2pt}} \mathrm{J}\,\forall\, \mathrm{u},\mathrm{v},\mathrm{w}\left({\mathrm{B}}^{\#}\left(\mathrm{x},\mathrm{u}\right)\,\&\, {\mathrm{B}}^{\#}\left(\mathrm{y},\mathrm{v}\right)\,\&\, \mathrm{AddTally}\left(\mathrm{u},\mathrm{v},\mathrm{w}\right)\to {\mathrm{B}}^{\#}\left(\mathrm{x}^\ast \mathrm{y},\mathrm{w}\right)\right)\!.\\ {}\kern22em \left(“\beta\!\left(\mathrm{x}^\ast \mathrm{y}\right)=\beta\!\left(\mathrm{x}\right)+\beta\!\left(\mathrm{y}\right)”\right)\end{array}}\end{equation*}$$

6.1

(a) ${\mathrm{QT}}^{+}\vdash \mathrm{I}^\ast \left(\mathrm{x}\right)\to \mathrm{x}=\mathrm{a}\;\mathrm{v}\left(\mathrm{bBx}\;\&\; \mathrm{aaEx}\right)\!$ .

1. (b) ${\mathrm{QT}}^{+}\vdash \mathrm{I}^\ast \left(\mathrm{x}\right)\;\&\; {\mathrm{x}}_2\mathrm{Ex}\to \forall\; \mathrm{u},\mathrm{v}\left({\mathrm{A}}^{\#}\left({\mathrm{x}}_2,\mathrm{u}\right)\;\&\; {\mathrm{B}}^{\#}\left({\mathrm{x}}_2,\mathrm{v}\right)\to \mathrm{Sv}\le \mathrm{u}\right)\!.$

2. (c) ${\mathrm{QT}}^{+}\vdash \mathrm{I}^\ast \left(\mathrm{x}\right)\;\&\; \mathrm{I}^\ast \left(\mathrm{y}\right)\;\&\; \mathrm{z}=\mathrm{bxy}\to \mathrm{I}^\ast \left(\mathrm{z}\right)\!.$

3. (d) ${\mathrm{QT}}^{+}\vdash \mathrm{I}^\ast \left(\mathrm{x}\right)\;\&\; \mathrm{I}^\ast \left(\mathrm{u}\right)\;\&\; \mathrm{bxy}=\mathrm{buv}\to \mathrm{x}=\mathrm{u}\;\&\; \mathrm{y}=\mathrm{v}.$

4. (e) ${\mathrm{QT}}^{+}\vdash \mathrm{I}^\ast \left(\mathrm{x}\right)\to \left(\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{a}\leftrightarrow \mathrm{x}=\mathrm{a}\right)\!.$

5. (f) ${\mathrm{QT}}^{+}\vdash \mathrm{I}^\ast \left(\mathrm{x}\right)\;\&\; \mathrm{I}^\ast \left(\mathrm{y}\right)\;\&\; \mathrm{I}^\ast \left(\mathrm{z}\right)\to \left(\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{byz}\leftrightarrow \mathrm{x}=\mathrm{byz}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}\right)\!.$

Proof See [Reference Damnjanovic3]. We give some details of the proof of (f) to illustrate the flavor of the type of formal argument used. Let M be an arbitrary model of QT⁺. Assume $\mathrm{M}\models \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{byz}$ where $\mathrm{M}\models$ I* ({x}) & I*(y) & I*(z).

Then $\mathrm{M}\models$ J* (x) & J*(y) & J*(z) and also & Æ(y) & Æ(z).

By (i^α) and (i^β), $\mathrm{M}\models \exists\; !{\mathrm{x}}_1\in \mathrm{J}^\ast {\mathrm{A}}^{\#}\left(\mathrm{x},{\mathrm{x}}_1\right)\;\&\; \exists\; !{\mathrm{x}}_2\in \mathrm{J}^\ast {\mathrm{B}}^{\#}\left(\mathrm{x},{\mathrm{x}}_2\right)$ .

From $\mathrm{M}\models \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{byz}$ by 3.7(h) we have that

$$\begin{align*}\mathrm{M}\models \mathrm{x}=\mathrm{b}\mathrm{yz}\;\mathrm{v}\;\mathrm{x}=\mathrm{b}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{yz}\;\mathrm{v}\;\exists\; \mathrm{u}\left(\mathrm{uByz}\;\&\; \mathrm{x}=\mathrm{b}\mathrm{u}\right)\!. \\[-38pt] \end{align*}$$

We distinguish the cases:

(1) $\mathrm{M}\models \exists\; \mathrm{u}\left(\mathrm{uByz}\;\&\; \mathrm{x}=\mathrm{bu}\right)\!.$

Then by (QT2), $\mathrm{M}\models \mathrm{x}\ne \mathrm{a}$ . From $\mathrm{M}\models \mathrm{I}^\ast \left(\mathrm{y}\right)$ & I*(z), by 6.1(c), $\mathrm{M}\models \mathrm{I}^\ast \left(\mathrm{byz}\right)$ .

From $\mathrm{M}\models \mathrm{uByz}$ , we have $\mathrm{M}\models \exists\; \mathrm{v}\;\mathrm{uv}=\mathrm{yz}$ , hence $\mathrm{M}\models \mathrm{b}\left(\mathrm{uv}\right)=\mathrm{b}\left(\mathrm{yz}\right)$ , and therefore $\mathrm{M}\models \left(\mathrm{bu}\right)\mathrm{v}=\mathrm{b}\left(\mathrm{yz}\right)$ . Thus $\mathrm{M}\models \mathrm{buBb}\left(\mathrm{yz}\right)$ , hence $\mathrm{M}\models \mathrm{xBb}\left(\mathrm{yz}\right)$ . Now, from $\mathrm{M}\models \mathrm{I}^\ast \left(\mathrm{byz}\right)$ , we have , whence $\mathrm{M}\models {\mathrm{x}}_1\le {\mathrm{x}}_2$ . But from , we obtain $\mathrm{M}\models {\mathrm{x}}_1={\mathrm{Sx}}_2$ , and thus $\mathrm{M}\models {\mathrm{x}}_1\le {\mathrm{x}}_2<{\mathrm{Sx}}_2={\mathrm{x}}_1$ , contradicting $\mathrm{M}\models {\mathrm{I}}_0\left({\mathrm{x}}_1\right)$ . Hence (1) is ruled out.

(2) $\mathrm{M}\models \mathrm{x}=\mathrm{b}$ .

Then by (QT4), $\mathrm{M}\models \mathrm{x}\ne \mathrm{a}$ , and from , we have, by 6.1(a), $\mathrm{M}\models \mathrm{bBx}$ .

But then M ⊧ bBb, contradicting (QT2). Hence (2) is also ruled out.

(3) $\mathrm{M}\models \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{yz}$ .

By 3.7(g), ${\displaystyle \begin{array}[t]{l}\mathrm{M}\models \mathrm{x}=\mathrm{yz}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}\;\mathrm{v}\;\exists\; {\mathrm{y}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; \mathrm{x}={\mathrm{y}}_1\mathrm{z}\right) \\ {}\kern2em \mathrm{v}\;\exists\; {\mathrm{z}}_1\left({\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}={\mathrm{y}\mathrm{z}}_1\right)\;\mathrm{v}\;\exists\; {\mathrm{y}}_1,{\mathrm{z}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; {\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}={\mathrm{y}}_1{\mathrm{z}}_1\right)\!.\end{array}}$

(3i) $\mathrm{M}\models \mathrm{x}=\mathrm{yz}$ .

By (i^α) and (i^β), $\mathrm{M}\models \exists\; !{\mathrm{y}}_1\in \mathrm{J}^\ast {\mathrm{A}}^{\#}\left(\mathrm{y},{\mathrm{y}}_1\right)\;\&\; \exists\; !{\mathrm{y}}_2\in \mathrm{J}^\ast {\mathrm{B}}^{\#}\left(\mathrm{y},{\mathrm{y}}_2\right)$ and further $\mathrm{M}\models \exists\; !{\mathrm{z}}_1\in \mathrm{J}^\ast {\mathrm{A}}^{\#}\left(\mathrm{z},{\mathrm{z}}_1\right)\;\&\; \exists\; !{\mathrm{z}}_2\in \mathrm{J}^\ast {\mathrm{B}}^{\#}\left(\mathrm{z},{\mathrm{z}}_2\right)$ .

From , we have $\mathrm{M}\models {\mathrm{y}}_1={\mathrm{Sy}}_2$ , and from , we have $\mathrm{M}\models {\mathrm{z}}_1={\mathrm{Sz}}_2$ . By 3.5(a), $\mathrm{M}\models \exists\; !{\mathrm{p}}_1\in \mathrm{J}^\ast \big({\mathrm{Tally}}_{\mathrm{b}}\!\left({\mathrm{p}}_1\right)$ & Addtally(y₁,z₁,p₁)) and $\mathrm{M}\models \exists\; !{\mathrm{p}}_2\in \mathrm{J}^\ast \big({\mathrm{Tally}}_{\mathrm{b}}\!\left({\mathrm{p}}_2\right)$ & Addtally(y₂,z₂,p₂)). Then from $\mathrm{M}\models {\mathrm{A}}^{\#}\left(\mathrm{y},{\mathrm{y}}_1\right)$ & A^#(z,z₁), by 5.2(a), $\mathrm{M}\models {\mathrm{A}}^{\#}\left(\mathrm{y}^\ast \mathrm{z},{\mathrm{p}}_1\right)$ , and from $\mathrm{M}\models {\mathrm{B}}^{\#}\left(\mathrm{y},{\mathrm{y}}_2\right)$ & B^#(z,z₂), by 5.2(b), $\mathrm{M}\models {\mathrm{B}}^{\#}\left(\mathrm{y}^\ast \mathrm{z},{\mathrm{p}}_2\right)$ . Thus, from $\mathrm{M}\models {\mathrm{y}}_1={\mathrm{Sy}}_2$ & z₁=Sz₂, we obtain M ⊧ Addtally(Sy₂,Sz₂,p₁).

On the other hand, from M ⊧ Addtally(y₂,z₂,p₂), by 3.4(e), M ⊧ Addtally(y₂,Sz₂,Sp₂), whence by 3.5(d), M ⊧ Addtally(Sy₂,Sz₂,SSp₂). By single-valuedness of Addtally, we then have $\mathrm{M}\models {\mathrm{p}}_1={\mathrm{SSp}}_2$ .

From hypothesis $\mathrm{M}\models \mathrm{x}=\mathrm{y}$ *z & A^#(y*z,p₁) & B^#(y*z,p₂), we have

$$\begin{align*}\mathrm{M}\models {\mathrm{A}}^{\#}\left(\mathrm{x},{\mathrm{p}}_1\right)\;\&\; {\mathrm{B}}^{\#}\left(\mathrm{x},{\mathrm{p}}_2\right)\!.\end{align*}$$

Hence from $\mathrm{M}\models {\mathrm{A}}^{\#}\left(\mathrm{x},{\mathrm{x}}_1\right)$ & B^#(x,x₂), by single-valuedness of A^# and B^#,

$$\begin{align*}\mathrm{M}\models {\mathrm{p}}_1={\mathrm{x}}_1\;\&\; {\mathrm{p}}_2={\mathrm{x}}_2.\end{align*}$$

Thus from $\mathrm{M}\models {\mathrm{p}}_1={\mathrm{SSp}}_2$ , we have $\mathrm{M}\models {\mathrm{x}}_1={\mathrm{SSx}}_2$ . But from we have $\mathrm{M}\models {\mathrm{x}}_1={\mathrm{Sx}}_2$ , whence $\mathrm{M}\models {\mathrm{x}}_1={\mathrm{Sx}}_1$ . But then from $\mathrm{M}\models {\mathrm{x}}_1<{\mathrm{Sx}}_1$ we obtain $\mathrm{M}\models {\mathrm{x}}_1<{\mathrm{x}}_1$ , contradicting $\mathrm{M}\models {\mathrm{I}}_0\left({\mathrm{x}}_1\right)$ . Hence (3i) is ruled out.

(3ii) $\mathrm{M}\models \exists\; {\mathrm{y}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; \mathrm{x}={\mathrm{y}}_1\mathrm{z}\right)\!.$

Then $\mathrm{M}\models {\mathrm{y}}_1\mathrm{Bx}$ . By (i^α) and (i^β),

$$\begin{align*}\mathrm{M}\models \exists\; !{\mathrm{u}}_1\in \mathrm{J}^\ast {\mathrm{A}}^{\#}\left({\mathrm{y}}_1,{\mathrm{u}}_1\right) & \exists\; !{\mathrm{u}}_2\in \mathrm{J}^\ast {\mathrm{B}}^{\#}\left({\mathrm{y}}_2,{\mathrm{u}}_2\right)\!.\end{align*}$$

From & y₁Bx, we have $\mathrm{M}\models {\mathrm{u}}_1\le {\mathrm{u}}_2$ , whereas from $\mathrm{M}\models \mathrm{I}^\ast \left(\mathrm{y}\right)$ & y₁Ey, by 6.1(b), we also have $\mathrm{M}\models {\mathrm{Su}}_2\le {\mathrm{u}}_1$ . But then $\mathrm{M}\models {\mathrm{u}}_2<{\mathrm{Su}}_2\le {\mathrm{u}}_2$ , contradicting $\mathrm{M}\models {\mathrm{I}}_0\left({\mathrm{u}}_2\right)$ . This rules out (3ii). Similar formalized calculations rule out

(3iii) $\mathrm{M}\models \exists\; {\mathrm{z}}_1\left({\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}= {\mathrm{yz}}_1\right)$ , and (3iv) $\mathrm{M}\models \exists\; {\mathrm{y}}_1,{\mathrm{z}}_1\left({\mathrm{y}}_1\mathrm{Ey}\;\&\; {\mathrm{z}}_1\mathrm{Bz}\;\&\; \mathrm{x}=\right. \left. {\mathrm{y}}_1{\mathrm{z}}_1\right)$ .

(See [Reference Damnjanovic3].) We conclude that

$$\begin{align*}\mathrm{M}\models \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\mathrm{z}\to \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}\end{align*}$$

and further that $\mathrm{M}\models \mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{byz}\to \mathrm{x}=\mathrm{byz}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{y}\;\mathrm{v}\;\mathrm{x}\;{\subseteq}_{\mathrm{p}}\;\mathrm{z}$ .

The converse is immediate from the definition of ${\subseteq}_{\mathrm{p}}$ .⊣

Taking the formula Æ(x) from Section 6 to define the domain, and interpreting the non-logical vocabulary ${\mathrm{\mathcal{L}}}_{\mathrm{T}}=\left\{0,\left(\, \right)\!,\sqsubseteq \right\}$ of T by a, bxy, and ${\subseteq}_{\mathrm{p}}$ , resp., as explained in Section 2, we have that 6.1(c)–(f), along with the fact that ${\mathrm{QT}}^{+}\vdash \mathrm{bxy}\ne \mathrm{a}$ , suffice to establish formal interpretability of T in QT⁺. On the other hand, from [Reference Damnjanovic1], building on previous work of Halpern and Collins, Wilkie, Visser, Grzegorczyk, and Ganea, we have that

$$\begin{align*}\mathrm{TC}{\equiv}_{\mathrm{I}}{\mathrm{QT}}^{+}{\equiv}_{\mathrm{I}}\mathrm{AST}{\equiv}_{\mathrm{I}}\mathrm{AST}+\mathrm{EXT}{\equiv}_{\mathrm{I}}\mathrm{Q}.\end{align*}$$

Since, by [Reference Kristiansen, Murwanashyaka, Anselmo, Vedova, Manea and Pauly6], Q ≤_I T, this suffices to establish

Weak Essentially Undecidable Theories: First Mutual Interpretability Theorem.

$$\begin{align*}\mathrm{T}\;{\equiv}_{\mathrm{I}}{\mathrm{QT}}^{+}{\equiv}_{\mathrm{I}}\mathrm{TC}\;{\equiv}_{\mathrm{I}}\mathrm{Q}\;{\equiv}_{\mathrm{I}}\mathrm{AST}.\end{align*}$$

In addition, each of the theories above is mutually interpretable with AST+EXT, and Buss’s theory ${S}_2^1$ (for the latter see [Reference Ferreira and Ferreira4]).

7.1 $\mathrm{WT}{\le}_{\mathrm{I}}\mathrm{WQT}$

The theory WQT is not recognizably a concatenation theory: the axioms make no substantive assumptions about the binary operation *, not even associativity. On that account, it might be considered at best as a “pseudo-concatenation” notational variant of WT. We now consider another first-order theory, WQT*, formulated in the same vocabulary ${\mathrm{\mathcal{L}}}_{\mathrm{C},\sqsubseteq \ast}=\left\{\mathrm{a},\mathrm{b},\ast, {\sqsubseteq}^{\ast}\right\}$ as WQT, with the following axioms: for each variable-free term t of ${\mathrm{\mathcal{L}}}_{\mathrm{C},\sqsubseteq \ast }$ ,

1. (WQT*1) $\forall\; \mathrm{x},\mathrm{y},\mathrm{z}\;\left(\mathrm{x}^\ast \left(\mathrm{y}^\ast \mathrm{z}\right){\sqsubseteq}_{\mathrm{p}}\mathrm{t}\;\mathrm{v}\;\left(\mathrm{x}^\ast \mathrm{y}\right)\ast \mathrm{z}{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\to \mathrm{x}^\ast \left(\mathrm{y}^\ast \mathrm{z}\right)=\left(\mathrm{x}^\ast \mathrm{y}\right)\ast \mathrm{z}\right)\!,$

2. (WQT*2) $\forall\; \mathrm{x},\mathrm{y}\;\left(\mathrm{x}^\ast \mathrm{y}{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\to \;\neg\; \left(\mathrm{x}^\ast \mathrm{y}=\mathrm{a}\right)\;\&\; \neg\; \left(\mathrm{x}^\ast \mathrm{y}=\mathrm{b}\right)\right)\!,$

3. (WQT*3) ${\displaystyle \begin{array}[t]{l} \forall\; \mathrm{x},\mathrm{y}\;\left(\left(\mathrm{a}^\ast \mathrm{x}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\;\&\; \mathrm{a}^\ast \mathrm{y}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\to \left(\mathrm{a}^\ast \mathrm{x}=\mathrm{a}^\ast \mathrm{y}\to \mathrm{x}=\mathrm{y}\right)\right) \right.\\ {}\kern3em \;\&\; \left(\mathrm{b}^\ast \mathrm{x}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\;\&\; \mathrm{b}^\ast \mathrm{y}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\to \left(\mathrm{b}^\ast \mathrm{x}=\mathrm{b}^\ast \mathrm{y}\to \mathrm{x}=\mathrm{y}\right)\right) \\ {}\kern3em \;\&\; \left(\mathrm{x}^\ast \mathrm{a}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\;\&\; \mathrm{y}^\ast \mathrm{a}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\to \left(\mathrm{x}^\ast \mathrm{a}=\mathrm{y}^\ast \mathrm{a}\to \mathrm{x}=\mathrm{y}\right)\right)\\ {}\kern3em \;\&\; \left.\left(\mathrm{x}^\ast \mathrm{b}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\;\&\; \mathrm{x}^\ast \mathrm{y}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\to \left(\mathrm{x}^\ast \mathrm{b}=\mathrm{y}^\ast \mathrm{b}\to \mathrm{x}=\mathrm{y}\right)\right)\right)\!,\end{array}}$

4. (WQT*4) ${\displaystyle \begin{array}[t]{l} \forall\; \mathrm{x},\mathrm{y}\;\left(\left(\mathrm{a}^\ast \mathrm{x}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\;\&\; \mathrm{b}^\ast \mathrm{y}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\to \;\neg\; \left(\mathrm{a}^\ast \mathrm{x}=\mathrm{b}^\ast \mathrm{y}\right)\right) \right.\\ {}\left.\kern3em \;\&\; \left(\mathrm{x}^\ast \mathrm{a}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\;\&\; \mathrm{y}^\ast \mathrm{b}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\to \;\neg\; \left(\mathrm{x}^\ast \mathrm{a}=\mathrm{y}^\ast \mathrm{b}\right)\right)\right)\!,\end{array}}$

5. (WQT*5) $\forall\; \mathrm{x}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{t}\left(\mathrm{x}=\mathrm{a}\;\mathrm{v}\;\mathrm{x}=\mathrm{b}\;\mathrm{v}\;\left(\left(\mathrm{aBx}\;\mathrm{v}\;\mathrm{b}\mathrm{Bx}\right)\;\&\; \left(\mathrm{aEx}\;\mathrm{v}\;\mathrm{b}\mathrm{Ex}\right)\right)\right)\!,$

6. (WQT*6) ${\displaystyle \begin{array}[t]{l} \forall\; \mathrm{y},\mathrm{z}\;\left(\mathrm{b}^\ast \left(\mathrm{y}^\ast \mathrm{z}\right){\sqsubseteq}^{\ast}\mathrm{t} \right.\\ {}\kern4em \to \left.\forall\; \mathrm{x}\;\left(\mathrm{x}{\sqsubseteq}^{\ast}\mathrm{b}^\ast \left(\mathrm{y}^\ast \mathrm{z}\right)\leftrightarrow \mathrm{x}=\mathrm{b}^\ast \left(\mathrm{y}^\ast \mathrm{z}\right)\;\mathrm{v}\;\mathrm{x}{\sqsubseteq}^{\ast}\mathrm{y}\;\mathrm{v}\;\mathrm{x}{\sqsubseteq}^{\ast}\mathrm{z}\right)\right)\!,\end{array}}$

7. (WQT*7) $\forall\; \mathrm{z}\;\left(\mathrm{z}{\sqsubseteq}^{\ast}\mathrm{a}\leftrightarrow \mathrm{z}=\mathrm{a}\right)\!,$

8. (WQT*8) $\forall\; \mathrm{x},\mathrm{y}\;\left(\mathrm{x}{\sqsubseteq}^{\ast}\mathrm{y}\;\&\; \mathrm{y}{\sqsubseteq}^{\ast}\mathrm{x}\to \mathrm{x}=\mathrm{y}\right)\!,$

9. (WQT*9) $\forall\; \mathrm{x},\mathrm{y}\;\left(\mathrm{x}{\sqsubseteq}^{\ast}\mathrm{y}\;\&\; \mathrm{y}{\sqsubseteq}^{\ast}\mathrm{z}\to \mathrm{y}{\sqsubseteq}^{\ast}\mathrm{z}\right)\!.$

Here we use the following abbreviations:

$$\begin{align*}\mathrm{x}\mathrm{By}\equiv \;\exists\; \mathrm{z}\;\mathrm{y}=\mathrm{x}^\ast \mathrm{z},\kern1.92em \mathrm{xEy}\equiv \;\exists\; \mathrm{z}\;\mathrm{y}=\mathrm{z}^\ast \mathrm{x},\end{align*}$$

and ${\mathrm{x}{\sqsubseteq}_{\mathrm{p}}\mathrm{y}\equiv \mathrm{x}=\mathrm{y}\,\mathrm{v}\,\mathrm{xBy}\,\mathrm{v}\,\mathrm{xEy}\,\mathrm{v}\;\exists\; {\mathrm{z}}_1,{\mathrm{z}}_2\,\mathrm{y}={\mathrm{z}}_1\ast \left(\mathrm{x}^\ast {\mathrm{z}}_2\right)\,\mathrm{v}\;\exists\; {\mathrm{z}}_1,{\mathrm{z}}_2\,\mathrm{y}=\left({\mathrm{z}}_1\ast \mathrm{x}\right)\ast {\mathrm{z}}_2.}$

Then $\forall\; \mathrm{x}\;{\sqsubseteq}_{\mathrm{p}}\mathrm{u}\;\varphi \equiv \forall\; \mathrm{x}\;\left(\mathrm{x}{\sqsubseteq}_{\mathrm{p}}\mathrm{u}\to \varphi \right)$ , where x does not occur in the term u.

Also, $\forall\; \mathrm{x}\;{\sqsubseteq}^{\ast}\mathrm{u}\;\varphi \equiv \forall\; \mathrm{x}\;\left(\mathrm{x}{\sqsubseteq}^{\ast}\mathrm{u}\to \varphi \right)$ .

(WQT*1)–(WQT*6) are axiom schemas with infinitely many instances, one for each variable-free term t. The schemas (WQT*1)–(WQT*5) are “bounded” versions of the axioms (QT1)–(QT5) of QT⁺. Schema (WQT*6) is a “bounded” generalization of schema (WQT2) of WQT. In light of that, WQT* may be naturally interpreted as a hybrid basic theory of finite strings and trees: the intended domain are the finite non-empty strings over the alphabet {a, b}, the binary operation symbol * is interpreted as the concatenation operation, and ${\sqsubseteq}^{\ast }$ as the substring relation between Æ-strings.

Now, WQT* is an extension of WQT. First, note the following:

7.2

For any distinct terms s, $\mathrm{t}\in {\Sigma}^{\tau }$ , WQT* $\vdash \;\neg\; \left(\mathrm{s}=\mathrm{t}\right)$ .

Hence in particular all instances of schema (WQT1) are provable in WQT*. Consider an instance of (WQT2) for terms s, $\mathrm{t}\in {\Sigma}^{\tau }$ ,

$$\begin{align*}\forall\; \mathrm{z}\;\left(\mathrm{z}{\sqsubseteq}^{\ast}\mathrm{b}^\ast \left(\mathrm{s}^\ast \mathrm{t}\right)\leftrightarrow \mathrm{z}=\mathrm{b}^\ast \left(\mathrm{s}^\ast \mathrm{t}\right)\;\mathrm{v}\;\mathrm{z}{\sqsubseteq}^{\ast}\mathrm{s}\;\mathrm{v}\;\mathrm{z}{\sqsubseteq}^{\ast}\mathrm{t}\right)\!.\end{align*}$$

Now, we have WQT* $\vdash \mathrm{b}^\ast \left(\mathrm{s}^\ast \mathrm{t}\right)=\mathrm{b}^\ast \left(\mathrm{s}^\ast \mathrm{t}\right)$ , so WQT* $\vdash \mathrm{b}^\ast \left(\mathrm{s}^\ast \mathrm{t}\right){\sqsubseteq}_{\mathrm{p}}\mathrm{b}^\ast \left(\mathrm{s}^\ast \mathrm{t}\right)$ . From (WQT*6), we have

$$\begin{align*}{\mathrm{WQT}}^{\ast}\vdash \forall\; \mathrm{x}\;\left(\mathrm{x}{\sqsubseteq}^{\ast}\mathrm{b}^\ast \left(\mathrm{s}^\ast \mathrm{t}\right)\leftrightarrow \mathrm{x}=\mathrm{b}^\ast \left(\mathrm{s}^\ast \mathrm{t}\right)\;\mathrm{v}\;\mathrm{x}{\sqsubseteq}^{\ast}\mathrm{s}\;\mathrm{v}\;\mathrm{x}{\sqsubseteq}^{\ast}\mathrm{t}\right)\!.\end{align*}$$

Hence each instance of (WQT2) is provable in WQT*. Given that (WQT3) is (WQT*7), this is enough to establish that WQT* is an extension of WQT.

On the other hand, we also have:

7.3

WQT* is locally finitely satisfiable.

That is, each finite subset of its non-logical axioms has a finite model.

By Visser’s Theorem, it follows that WQT* is interpretable in R.

Since by [Reference Kristiansen, Murwanashyaka, Anselmo, Vedova, Manea and Pauly6], R ≤_I WT, we then have

Weak Essentially Undecidable Theories: Second Mutual Interpretability Theorem. $\mathrm{R}{\equiv}_{\mathrm{I}}\;{\mathrm{WTC}}^{- \varepsilon }{\equiv}_{\mathrm{I}}\;\mathrm{WT}{\equiv}_{\mathrm{I}}\mathrm{WQT}{\equiv}_{\mathrm{I}}{\mathrm{WQT}}^{\ast }$ .

For definition of the theory WTC^–ε, see [Reference Higuchi and Horihata5].