Doubt in the Proof of the Theorem on the Undecidability of First-Order Logic

Question

I am studying Ebbinghauss's book Mathematical Logic and I wanted your help in checking that a given condition that the author says it holds really holds. The theorem is about undecidability of first-order logic.

The theorem is:

4.1 Theorem on the Undecidability of First Order Language The set $\{ \phi \in L_{0}^{S_{\infty}} \ | \vDash \phi \} $ of valid $S_{\infty}$-sentences is not $R$-decidable.

Proof (only the relevant parts for the condition I am trying to check):

We work with the alphabet $\mathcal{A} = \{ | \}$ and we consider $\square$ the empty word.

Let $P$ be a program with instructions $\alpha_0, \ldots, \alpha_k$. We say that $(L, m_0, \ldots, m_n)$ is the configuration of P after $s$ steps if $P$, started with $\square$, runs for at least $s$ steps and after this $s$ steps, instruction $L$ is to be executed next, with the numbers $m_0, \ldots, m_n$ in the registers $R_0, \ldots, R_n$. In particular, $(0, 0, \ldots, 0)$ is the initial configuration of $P$.

Choose symbols $R$ (($n$ + 3)-ary), $<$ (binary), $f$ (unary), and $c \in S_{\infty}$ and set $S = \{R, <, f, c\}$. To each program $P$, we associate an $S$-structure $\mathcal{A}_p$ according to whether $P$ halts or not:

Case P doesn't halt, i.e., $P: \square \to \infty$. Set $A_{P} = \mathbb{N}$, and interpret $<$ by the usual ordering on $\mathbb{N}$, $c$ by 0, $R$ by $\{(s, L, m_0, \ldots, m_n) \ | \ (L, m_0, \ldots, m_n) \text{ is the configuration of $P$ after $s$ steps}\}$ and $f$ by the successor function.

Case P halts, i.e., $P: \square \to \text{halt}$. Let $s_P$ be the number of steps carried out by $P$ until it arrives at the halt instruction. Set $e = \text{max}\{k, s_P\}$ and $A_{p} = \{0, \ldots, e\}$ and interpret $<$ by the usual ordering on $A_{p}$ and $c$ by 0.

Next the author provides an $S$-sentence $\psi_P$ that will describe, in a suitable way, the operations of $P$ on $\square$. In reading $\psi_{P}$ I am trying to check that the following holds:

(a) - $\mathcal{A_P} \vDash \psi_P$

(b) - If $\mathcal{A}$ is an $S$-structure with $\mathcal{A} \vDash \psi_P$ and $(L, m_0, \ldots, m_n)$ is the configuration of $P$ after $s$ steps, then the elements $0^\mathcal{A}, 1^\mathcal{A}, \ldots, s^\mathcal{A}$ are pairwise distinct and $\mathcal{A} \vDash RsLm_0,\ldots, m_n$

where we set $\psi_P$ to be:

$\psi_P = \psi_0 \land R0,\ldots,0 \land \psi_{\alpha_0} \land \ldots \land \psi_{\alpha_{k-1}}$

The sentence $\psi_0$ says that $<$ is an ordering whose first element is $c$, that $x < fx$ holds for every $x$ and that $fx$ is the immediate successor of $x$ in case $x$ is not the last element:

$\psi_0 = \ $ " $<$ is an ordering" $\land \forall x (c < x \lor c \equiv x) \land \forall x (x < f x \lor x \equiv fx) \land \forall x(\exists y \ x < y \to (x < fx \land \forall z (x < z \to (fx < z \ \lor fx \equiv z))))$

For $\alpha = \alpha_0, \ldots, \alpha_{k-1}$, the sentence $\psi_{\alpha}$ describes the operation corresponding to instruction $\alpha$. $\psi_{\alpha}$ is defined as follows:

If $\alpha$ is an add instruction, say $L \text{ LET } R_i = R_i + \{ | \}$:

$\psi_{\alpha} = \forall x \forall y_0 \ldots \forall y_n(R x L y_0 \ldots y_n \to (x < fx \land R fx L+1 y_0 \ldots y_{i-1} fy_i y_{i+1} \ldots y_n)) $

If $\alpha$ is the instruction $L \text{ LET } R_i = R_i - \{ | \}$:

$\psi_{\alpha} = \forall x \forall y_0 \ldots \forall y_n(R x L y_0 \ldots y_n \to (x < fx \land ((y_i \equiv 0 \land R fx L+1 y_0 \ldots y_n) \lor \\ \hspace{15mm} (\lnot y_i \equiv 0 \land \exists u (f u \equiv y_i \land R fx L+1 y_0 \ldots y_{i-1} u y_{i+1} \ldots y_{n})))))$

If $\alpha$ is the instruction $L \text{ IF } R_i = \square \text{ THEN } L' \text{ ELSE } L_0$:

$\psi_{\alpha} = \forall x \forall y_0 \ldots \forall y_n(R x L y_0 \ldots y_n \to (x < fx \land ((y_i \equiv 0 \land R fx L' y_0 \ldots y_n) \lor \\ \hspace{15mm} (\lnot y_i \equiv 0 \land R fx L_0 y_0 \ldots y_n))))$

Finally for $\alpha = L \text{ PRINT }$ let:

$\psi_{\alpha} = \forall x \forall y_0 \ldots \forall y_n(R x L y_0 \ldots y_n \to (x < fx \ \land \ R fx L+1 y_0 \ldots y_n))$

Answer 1

2.a. $\mathcal{A_P} \vDash \psi_P$

Notice that $\mathcal{A_P} \vDash \psi_0$, in both cases. This is because, as commented, $\psi_0$ says that $<$ is an ordering whose first element is $c$ (indeed, we interpret $<$ by the usual ordering - whether we are in $\mathbb{N}$ or in $A_P$ - and we interpret $c$ as 0), that $x \le fx$ holds for every $x$ and that every $fx$ is the immediate successor of $x$ in case $x$ is not the last element (this holds when we interpret $fx$ as the successor of $x$ and this also holds when $P$ halts and $x$ is equal to $e$ - in this case we have $x = fx$).

Notice that $\mathcal{A_P} \vDash R0\ldots0$. That's because $(0, \ldots, 0)$ is the configuration of $P$ after 0 steps and, therefore, $(0, \ldots, 0) \in R^{A_P}$.

Finally, for the sentences that describe the operation corresponding to instruction $\alpha$. Notice that the formula $\psi_{\alpha}$, when interpreted under $\mathcal{A_P}$, corresponds precisely to instruction $\alpha$ and we will have $\mathcal{A_P} \vDash \psi_{\alpha}$ in any of the cases below:

If $\alpha$ is an add instruction, $\psi_{\alpha}$ says (when interpreted under $\mathcal{A_p}$) that if you are in the configuration $(L, y_0, \ldots, y_n)$ after $x$ steps, then we are not in the last instruction and after $x+1$ steps we are now in the configuration $(L+1, y_0, \ldots, y_{i-1}, fy_i, y_{i+1}, \ldots, y_n)$. Therefore, in this case, $\mathcal{A_P} \vDash \psi_{\alpha}$.

If $\alpha$ is the instruction $L \text{ LET } R_i = R_i - |$, $\psi_{\alpha}$ says (when interpreted under $\mathcal{A_P}$) that if you are in the configuration $(L, y_0, \ldots, y_n)$ after $x$ steps, then we are not in the last instruction(i.e. $x \le fx$) and we have either:

1. register $y_i$ is empty and in this case after step $x+1$ we are in configuration $(L+1, y_0, \ldots, y_n)$ - the values on all the registers are the same in relation to the previous configuration.

2. or register $y_i$ is not empty and in this case, there exists some element $u$, which is the antecessor of $y_i$ such that after $x+1$ steps we are in configuration $(L+1, y_0, \ldots, y_{i-1}, u, y_{i+1} \ldots y_{n})$. Therefore, in any case, $\mathcal{A_P} \vDash \psi_{\alpha}$.

If $\alpha$ is the instruction $L \text{ IF } R_{i} = \square \text{ THEN } L' \text{ ELSE } L_{0}$, then $\mathcal{A_P}$ interprets $\psi_{\alpha}$ as saying that if you are in the configuration $(L, y_0, \ldots, y_n)$ after $x$ steps, then you are not in the last instruction (i.e. $x \le fx$) and:

1. There is the empty word in register $R_i$ and after $x+1$ steps we are in configuration $(L', y_0, \ldots, y_n)$.
2. or the word in register $R_i$ is not empty and after $x+1$ steps we are in configuration $(L_0, y_0, \ldots, y_n)$.

If $\alpha$ is a print instruction, $\psi_{\alpha}$ says (when interpreted under $\mathcal{A_p}$) that if you are in the configuration $(L, y_0, \ldots, y_n)$ after $x$ steps, then we are not in the last instruction and after $x+1$ steps we are now in the configuration $(L+1, y_0, \ldots, y_n)$.

This concludes the proof of item 2.a.

2.b. If $\mathcal{A}$ is an $S$-structure with $\mathcal{A} \vDash \psi_P$ and $(L, m_0, \ldots, m_n)$ is the configuration of $P$ after $s$ steps, then the elements $0^\mathcal{A}, 1^\mathcal{A}, \ldots, s^\mathcal{A}$ are pairwise distinct and $\mathcal{A} \vDash RsLm_0,\ldots, m_n$

Following the book suggestion, we prove by induction on $s$.

For $s = 0$, there is only the element 0 (so all the elements are pairwise distinct) and $(0, 0, \ldots, 0)$ is the configuration of $P$ after 0 steps. Since $\mathcal{A} \vDash \psi_{P}$ we also have $\mathcal{A} \vDash R 0 \ldots 0$.

For $s+1$, let $(L, m_0, \ldots, m_n)$ be the configuration of $P$ after $s$ steps. By inductive hypothesis, we have $\mathcal{A} \vDash R s L m_0, \ldots, m_n$ and we must prove $\mathcal{A} \vDash R s+1 L' m'_0, \ldots m'_n$ where $(L', m'_0, \ldots, m'_n)$ is the configuration of $P$ after $s+1$ steps. We must also prove that $0, \ldots, s+1$ are pairwise distinct.

Let's start by proving that $0, \ldots, s+1$ are pairwise distinct. We do that by proving that $0 < \ldots < s+1$ and this require us to strengthen the induction hypothesis slightly. Notice that $\mathcal{A} \vDash \psi_{\alpha}$. Then, for every instruction at label $L$ we atribute to variable $x$ the value $s$ and we attribute to the variables $y_0, \ldots, y_n$ the values $m_0, \ldots, m_n$. Then, in all of the cases, we can use that $\mathcal{A} \vDash R s L m_0 \ldots m_n$ (this holds by inductive hypothesis) to conclude that $s < fs \equiv s+1$. This, together with the fact that $0 < \ldots < s$ (this is our strengthened inductive hypothesis and can be verified to hold in the base case) lets us conclude that $0 < \ldots < s+1$. Therefore, we conclude that $0, \ldots, s+1$ are pairwise distinct.

Let's prove that $\mathcal{A} \vDash R s+1 L' m'_0, \ldots m'_n$. Notice that $\mathcal{A} \vDash \psi_{\alpha}$. Then, by instantiating variables $x$ and $y_0, \ldots, y_n$ as described in the preceding paragraph, and using the fact that $\mathcal{A} \vDash R s L m_0 \ldots m_n$ (this holds by inductive hypothesis) we conclude (examine the structure of the formula $\psi_{\alpha}$ for every instruction - add, subs, jump and print) that $\mathcal{A} \vDash R s+1 L' m'_0, \ldots m'_n$ where $(L', m'_0, \ldots, m'_n)$ is precisely the configuration of $P$ after $s+1$ steps.