Recall, that the proof of Theorem 31G considers a formula $\exists x(\alpha_{0}\wedge\ldots\wedge\alpha_{q})$ where each $\alpha_{i}$ is atomic or the negation of an atomic formula, and provides a procedure to eliminate all quantifiers from it. We formalize this procedure (with a few more cases that we consider) and show the equivalence of the initial and resulting formulas under Axioms S1-S4 ($A_{S}$ ).

First, we argue that if for wffs $\alpha$ and $\beta$ there are wffs $\alpha'$ and $\beta'$ such that $\alpha'$ does not contain $x$ and $A_{S}\vDash\alpha\wedge\beta\leftrightarrow\alpha'\wedge\beta'$ , then $A_{S}\vDash\exists x(\alpha\wedge\beta)\leftrightarrow\alpha'\wedge\exists x\beta'$ . Indeed, for every structure $\mathfrak{A}$ and $s:V\rightarrow|\mathfrak{A}|$ such that $\vDash_{\mathfrak{A}}A_{S}$ , $\vDash_{\mathfrak{A}}\alpha\wedge\beta[s]$ iff $\vDash_{\mathfrak{A}}\alpha'\wedge\beta'[s]$ . Now, $\vDash_{\mathfrak{A}}\exists x(\alpha\wedge\beta)[s]$ iff for some $d\in|\mathfrak{A}|$ , $\vDash_{\mathfrak{A}}\alpha\wedge\beta[s(x|d)]$ iff for some $d\in|\mathfrak{A}|$ , $\vDash_{\mathfrak{A}}\alpha'\wedge\beta'[s(x|d)]$ iff for some $d\in|\mathfrak{A}|$ , $\vDash_{\mathfrak{A}}\alpha'[s(x|d)]$ and $\vDash_{\mathfrak{A}}\beta'[s(x|d)]$ iff for some $d\in|\mathfrak{A}|$ , $\vDash_{\mathfrak{A}}\alpha'[s]$ and $\vDash_{\mathfrak{A}}\beta'[s(x|d)]$ iff $\vDash_{\mathfrak{A}}\alpha'[s]$ and $\vDash_{\mathfrak{A}}\exists x\beta'[s]$ iff $\vDash_{\mathfrak{A}}\alpha'\wedge\exists x\beta'[s]$ .

(*) In particular, if $A_{S}\vDash\alpha\leftrightarrow\alpha'$ , then $A_{S}\vDash\exists x(\alpha\wedge\beta)\leftrightarrow\alpha'\wedge\exists x\beta$ , if $A_{S}\vDash\alpha$ , then $A_{S}\vDash\exists x(\alpha\wedge\beta)\leftrightarrow\exists x\beta$ , and if $A_{S}\vDash\neg\alpha$ , then $A_{S}\vDash\exists x(\alpha\wedge\beta)\leftrightarrow0\neq0$ .

Let us call $\alpha_{0}$ just $\alpha$ , for simplicity, and let $\phi=\alpha_{1}\wedge\ldots\wedge\alpha_{q}$ . $\alpha$ is either $\beta$ or $\neg\beta$ where $\beta=\mathbb{S}^{m}s=\mathbb{S}^{n}t$ , $m,n\ge0$ , and $s$ and $t$ can be a variable or a constant. We need to consider all possible cases for $\alpha$ . To simplify things, suppose $\alpha_{i}$ ’s are sorted in the following order: $s\neq x$ , $t\neq x$ ; $s=t=x$ ; $\alpha=\beta$ , $s=x$ , $t=0$ ; $\alpha=\beta$ , $s=x$ , $t=v_{k}$ ; $\alpha=\neg\beta$ (symmetrical cases such as $\alpha=\beta$ , $s=0$ , $t=x$ are equivalent to corresponding cases we consider).

1. $\beta=\mathbb{S}^{m}s=\mathbb{S}^{n}t$ where $s\neq x$ , $t\neq x$ . Then, $\alpha$ does not contain $x$ , and we can simply take $\alpha'=\alpha$ to obtain $A_{S}\vDash\exists x(\alpha\wedge\phi)\leftrightarrow\alpha\wedge\exists x\phi$ . We can now proceed with $\alpha$ being the first formula in $\phi$ .
2. $\beta=\mathbb{S}^{m}x=\mathbb{S}^{n}x$ .
   1. If $m=n$ , then, obviously, $\beta$ is true in any structure with any assignment of $x$ , so that, according to (*), $A_{S}\vDash\exists x(\beta\wedge\phi)\leftrightarrow\exists x\phi$ (and we can proceed with $\alpha$ being the first formula in $\phi$ ), and $A_{S}\vDash\exists x(\neg\beta\wedge\phi)\leftrightarrow0\neq0$ (and we stop here).
   2. If $m\neq n$ , without loss of generality, suppose $m>n$ . Using deduction axiom group 2 (A2) for S4, $A_{S}\vdash\mathbb{S}^{m-n}x\neq x$ . Using A2 and contraposition for S2, we further obtain $A_{S}\vdash x\neq y\rightarrow\mathbb{S}x\neq\mathbb{S}y$ . From here, using all the standard techniques for substitution, we obtain $A_{S}\vdash x\neq y\rightarrow\mathbb{S}^{n}x\neq\mathbb{S}^{n}y$ , and further $A_{S}\vdash\mathbb{S}^{m-n}x\neq x\rightarrow\mathbb{S}^{m}x\neq\mathbb{S}^{n}x$ . Overall, we see that $A_{S}\vdash\mathbb{S}^{m}x\neq\mathbb{S}^{n}x$ , i.e. $A_{S}\vDash\neg\beta$ . Similarly, according to (*), $A_{S}\vDash\exists x(\beta\wedge\phi)\leftrightarrow0\neq0$ (and we stop here), and $A_{S}\vDash\exists x(\neg\beta\wedge\phi)\leftrightarrow\exists x\phi$ (and we proceed with the new $\alpha$ ).
3. $\alpha=\beta=\mathbb{S}^{m}x=\mathbb{S}^{n}0$ .
   1. If $m>n$ , by using A2 for S1 and S2 and contraposition for S2, $A_{S}\vdash\mathbb{S}x\neq0;x\neq y\rightarrow\mathbb{S}x\neq\mathbb{S}y$ , and by using generalization and A2 $m-n-1$ and then $n$ times (as well as other substitution techniques), we obtain $A_{s}\vdash\mathbb{S}^{n}\mathbb{S}^{m-n}x\neq\mathbb{S}^{n}0$ , i.e. $A_{S}\vDash\neg\beta$ , and, as before, according to (*), $A_{S}\vDash\exists x(\beta\wedge\phi)\leftrightarrow0\neq0$ (stop).
   2. If $m\le n$ , by S2 and A2, $A_{S}\vdash\mathbb{S}^{m}x=\mathbb{S}^{n}0\rightarrow\mathbb{S}^{m-1}x=\mathbb{S}^{n-1}0$ , and by applying this rule $m$ times, $A_{S}\vdash\mathbb{S}^{m}x=\mathbb{S}^{n}0\rightarrow x=\mathbb{S}^{n-m}0$ . Moreover, $\vdash x=\mathbb{S}^{n-m}0\rightarrow\mathbb{S}^{m}x=\mathbb{S}^{n}0$ (see Example Eq5, page 122, for the idea of the proof). Hence, $A_{S}\vDash\beta\leftrightarrow x=\mathbb{S}^{n-m}0$ . Then, $A_{S}\vDash\exists x(\beta\wedge\phi)\leftrightarrow\exists x(x=\mathbb{S}^{n-m}0\wedge\phi)$ , and $A_{S}\vDash\exists x(x=\mathbb{S}^{n-m}0\wedge\phi)\leftrightarrow\phi_{\mathbb{S}^{n-m}0}^{x}$ (stop). Indeed, for every structure $\mathfrak{A}$ and $s:V\rightarrow|\mathfrak{A}|$ such that $\vDash_{\mathfrak{A}}A_{S}$ , $\vDash_{\mathfrak{A}}\exists x(x=\mathbb{S}^{n-m}0\wedge\phi)[s]$ iff for some $d\in|\mathfrak{A}|$ , $d=(\mathbb{S}^{\mathfrak{A}})^{n-m}(s(0))$ and $\vDash_{\mathfrak{A}}\phi[s(x|d)]$ iff $\vDash_{\mathfrak{A}}\phi[s(x|(\mathbb{S}^{\mathfrak{A}})^{n-m}(s(0)))]$ iff $\vDash_{\mathfrak{A}}\phi_{\mathbb{S}^{n-m}0}^{x}[s]$ (we used S2 at some point).
4. $\alpha=\beta=\mathbb{S}^{m}x=\mathbb{S}^{n}v_{k}$ .
   1. If $m>n$ , then, similar to 3(b), we, first, conclude that $A_{S}\vdash\beta\leftrightarrow\mathbb{S}^{m-n}x=v_{k}$ . Then, for every structure $\mathfrak{A}$ and assignment $s:V\rightarrow|\mathfrak{A}|$ such that $\vDash_{\mathfrak{A}}A_{S}$ , $\vDash_{\mathfrak{A}}\exists x(\mathbb{S}^{m-n}x=v_{k}\wedge\phi)$ iff for some $d\in|\mathfrak{A}|$ , $(\mathbb{S}^{\mathfrak{A}})^{m-n}(d)=s(v_{k})$ and $\vDash_{\mathfrak{A}}\phi[s(x|d)]$ . Similar to 3(b), we argue that for any term in $\phi$ , $A_{S}\vDash\mathbb{S}^{a}x=\mathbb{S}^{b}t\leftrightarrow\mathbb{S}^{a+c}x=\mathbb{S}^{b+c}t$ and $A_{S}\vDash\neg(\mathbb{S}^{a}x=\mathbb{S}^{b}t)\leftrightarrow\neg(\mathbb{S}^{a+c}x=\mathbb{S}^{b+c}t)$ . So, let $\phi'$ be $\phi$ in which we apply $\mathbb{S}^{m-n}$ to each side of the equality of each term of $\phi$ . Then, in $\phi'$ , all occurrences of $x$ can be represented as $\mathbb{S}^{k}\mathbb{S}^{m-n}x$ . Now we can proceed, iff for some $d\in|\mathfrak{A}|$ , $(\mathbb{S}^{\mathfrak{A}})^{m-n}(d)=s(v_{k})$ and $\vDash_{\mathfrak{A}}(\phi')_{v_{k}}^{\mathbb{S}^{m-n}x}[s]$ iff for some $d\in|\mathfrak{A}|$ , $(\mathbb{S}^{\mathfrak{A}})^{m-n}(d)=s(v_{k})$ and $\vDash_{\mathfrak{A}}v_{k}\neq\mathbb{S}0\wedge\ldots\wedge v_{k}\neq\mathbb{S}^{m-n-1}0\wedge(\phi')_{v_{k}}^{\mathbb{S}^{m-n}x}[s]$ (we used S1 and S3). Therefore, $A_{S}\vDash\exists x(\beta\wedge\phi)\leftrightarrow v_{k}\neq\mathbb{S}0\wedge\ldots\wedge v_{k}\neq\mathbb{S}^{m-n-1}0\wedge(\phi')_{v_{k}}^{\mathbb{S}^{m-n}x}$ (stop).
   2. If $m\le n$ , then, similar to 3(b), we, first, conclude that $A_{S}\vDash\beta\leftrightarrow x=\mathbb{S}^{n-m}v_{k}$ , and, then $A_{S}\vDash\exists x(\beta\wedge\phi)\leftrightarrow\phi_{\mathbb{S}^{n-m}v_{k}}^{x}$ (stop). Indeed, for every structure $\mathfrak{A}$ and assignment $s:V\rightarrow|\mathfrak{A}|$ such that $\vDash_{\mathfrak{A}}A_{S}$ , $\vDash_{\mathfrak{A}}\exists x(x=\mathbb{S}^{n-m}v_{k}\wedge\phi)$ iff for some $d\in|\mathfrak{A}|$ , $d=(\mathbb{S}^{\mathfrak{A}})^{n-m}(s(v_{k}))$ and $\vDash_{\mathfrak{A}}\phi[s(x|d)]$ iff $\vDash_{\mathfrak{A}}\phi[s(x|(\mathbb{S}^{\mathfrak{A}})^{n-m}(s(v_{k})))]$ iff $\vDash_{\mathfrak{A}}\phi_{\mathbb{S}^{n-m}v_{k}}^{x}[s]$ (we used S2 at some point).
5. $\alpha=\neg\beta$ . All that we have left now, is terms that are negations of atomic formulas $\mathbb{S}^{a}x=\mathbb{S}^{b}t$ , $t\neq x$ . Consider any structure $\mathfrak{A}$ and $s:V\rightarrow|\mathfrak{A}|$ such that $\vDash_{\mathfrak{A}}A_{S}$ . For every term $\neg(\mathbb{S}^{a}x=\mathbb{S}^{b}t)$ , using S3, we can find $k$ such that $s(t)=(\mathbb{S}^{\mathfrak{A}})^{k}(s(0))$ , then let $p$ be greater than any $b+k$ for any such term, and let $d=(\mathbb{S}^{\mathfrak{A}})^{p}(s(0))$ . Then, if we let $s(x)=d$ , then, using S4, $(\mathbb{S}^{\mathfrak{A}})^{a}(s(x))=(\mathbb{S}^{\mathfrak{A}})^{a+p}(s(0))\neq(\mathbb{S}^{\mathfrak{A}})^{b+k}(s(0))=(\mathbb{S}^{\mathfrak{A}})^{b}(s(t))$ , i.e. $\vDash_{\mathfrak{A}}\neg(\mathbb{S}^{a}x=\mathbb{S}^{b}t)[s(x|d)]$ . Since $d$ does not depend on the term, we conclude that the rest of the formula is satisfied in any structure $\mathfrak{A}$ that satisfies $A_{S}$ with any $s:V\rightarrow|\mathfrak{A}|$ , and $A_{S}\vDash(\alpha\wedge\phi)\leftrightarrow0=0$ .

To conclude, we note that in our procedure, we did a few more steps compared to the proof in the text, and modified the formula in a slightly way in some common steps. Same as in the proof, we first move all formulas not containing $x$ out from the quantified expression (step 1). Then, similar to the text, we consider the case when a term contains $x$ on both sides (step 2). If $m=n$ , then, unlike the proof, we do not replace the term with $0=0$ or $\neg(0=0)$ , but, equivalently, either remove it at all (instead of replacing with $0=0$ ) or conclude that the whole expression is equivalent to $0\neq0$ (instead of replacing just one term by $\neg(0=0)$ ). If $m\neq n$ , then, similarly, we either conclude that the whole expression is equivalent to $0\neq0$ (instead of replacing a term by $0\neq0$ ) or remove the term (instead of replacing it by $\neg(0\neq0)$ ). In steps 3 and 4, we, as in the proof, consider terms which are atomic formulas (not negations). Similar to the text, if there is at least one such term left, then we are going to obtain a quantifier-free formula right after this step. However, we consider four separate subcases here, which, of course, can be put together to form the one step in the proof. However, by doing this, we avoid unnecessary substitutions and new terms that are either always false or always true. For example, in step 3(a) we conclude that the whole formula is equivalent to $0\neq0$ instead of substituting it with a series of terms one of which would be $\mathbb{S}^{n}0\neq\mathbb{S}^{n}0$ . Similarly, in 3(b) we avoid unnecessary terms of the form $\mathbb{S}^{n}0\neq\mathbb{S}^{k}0$ for $0\le k\le m-1<n$ , as well as transformations of the remaining terms. In 4, we also consider two subcases, in one of which there is no need to check $\mathbb{S}^{n}v_{k}$ against $\mathbb{S}^{k}0$ for $k<n$ or transform the remaining terms. Finally, same as in the proof, we get to step 5 only if there were no terms in steps 3 or 4, i.e. if after steps 1 and 2 all remaining terms are negations.