Modeling computations in first-order logic

Whether a Turing machine has an infinite computation, starting from a given configuration, can be modeled in first-order logic in a straightforward fashion. As a consequence, satisfiability is undecidable for first-order formulas.

Turing machine model

The above statement is true regardless of which model of Turing machine is used. In the following, it is assumed that the tape is unbounded to the left and to the right and that a transition is of the form $q, a \to q', b', d$ where

• $q$ and $q'$ are states,
• $b$ and $b'$ are symbols from the working alphabet $B$, and
• $d$ is a head direction, one of $\text L$, $\text N$, and $\text R$.

The blank symbol is denoted $\_$.

A configuration of a Turing machine is given by:

• a state $q \in Q$,
• a tape content $u$, which is a function $\mathbf Z \to B$ where only a finite number of integers are mapped to a non-blank letter,
• a head position $j<|u|$.

When a transition is applicable to a given configuration, its application results in a new configuration (or the old one), depending on the concrete configuration and the concrete transition.

Example Suppose a Turing machine is in state $q_4$, its tape content is the function $\{\dots, -2 \mapsto \_, -1 \mapsto \_, 0 \mapsto a, 1 \mapsto b, 2 \mapsto a, 3 \mapsto a, 4 \mapsto d, 5 \mapsto b, 6 \mapsto a, 7 \mapsto a, 8 \mapsto \_, 9 \mapsto \_, \dots\}$, and the head is at position $3$. Then the transition $q_4, a \to q_2, c, \text R$ is applicable and the application of the transition results in the configuration where the Turing machine is in state $q_2$, the tape content is $\{\dots, -2 \mapsto \_, -1 \mapsto \_, 0 \mapsto a, 1 \mapsto b, 2 \mapsto a, 3 \mapsto c, 4 \mapsto d, 5 \mapsto b, 6 \mapsto a, 7 \mapsto a, 8 \mapsto \_, 9 \mapsto \_, \dots\}$, and the head position is $4$.

The objective is to model infinite computations starting from the start configuration for a given word.

Representing computations in grids and signature

The basic idea is to represent an infinite computation in the infinite grid $\mathbf Z \times \mathbf Z$ as follows.

Todo: picture.

Configurations are put on top of each other in the rows of the grid. The state of a configuration is stored at the point of the grid where the head is.

We somehow have to be able to move in the grid. For this, it is enough to have a unary function $\text{suc}/\!/1$, which goes from one index to the next one. But it will be easier for us if we can also go from one index to the previous one, so we add $\text{pred}/\!/1$.

We also need a way to say that there is a particular letter at a particular point in the grid: we choose a binary relation symbol, $L_b/2$, for each letter $b \in B$. In addition, we choose for each state $q \in Q$ a binary relation symbol $S_q/2$. We do not need to add a symbol for the position of the head, because our convention is that the head is in the position where the state is stored.

Overall, we have: \begin{align} \mathcal S = \{\text{suc}/\!/1, \text{pred}/\!/1\} \cup \{L_b \colon b \in B\} \cup \{S_q \colon q \in Q\} \enspace. \end{align}

The specification—a long formula

We want to develop an $\mathcal S$-formula which is satisfiable if, and only if, there is an infinite computation starting from the start configuration for a given word $u$.

First of all, we require \begin{align} \text{Domain} = \forall x_0 (\text{pred}(\text{suc}(x_0)) \doteq x_0 \wedge \text{suc}(\text{pred}(x_0)) \doteq x_0)\enspace, \end{align} that is, the two functions are inverses of each other.

In general, we want exactly one letter in each point and at most one state in each row of the grid: \begin{align} \text{LettersStates} = \forall x_0 \forall x_1 \left( \displaystyle{\dot\bigvee_{b \in B}} L_b(x_0, x_1) \wedge \bigwedge_{q \neq q'} \left( \neg S_q(x_0, x_1) \vee \neg S_{q'}(x_0, x_1)\right)\right) \wedge \forall x_0 \forall x_1 \forall x_2 \left(\bigvee_q S_q(x_0, x_1) \wedge \bigvee_q S_q(x_2, x_1) \rightarrow x_0 \doteq x_2\right)\enspace. \end{align}

When in a row there is a head on some position, then for each other position in this row it is true that this position and the position right above it store the same letter: \begin{align} \text{SameLetters} = \forall x_1 \left(\exists x_0 \bigvee_{q \in Q} S_q(x_0, x_1) \rightarrow \forall x_0 \left(\bigwedge_{q \in Q} \neg S_q(x_0, x_1) \rightarrow \bigwedge_{b \in B}(L_b(x_0, x_1) \leftrightarrow L_b(x_0, \text{suc}(x_1)))\right)\right) \enspace. \end{align}

All that is left (almost) is to describe that transitions are applied and how a transition is applied: \begin{align} \text{Transitions} & = \forall x_0 \forall x_1 \left(\bigvee_q S_q(x_0, x_1) \rightarrow \bigvee_{q,b \to q', b', d \in \delta} \text{Applies}[q, b, q', b', d] \right)\enspace. \end{align}

Depending on $d$, there are three different types of formulas $\text{Applies}[q, b, q', b', d]$. For instance, when $d = \text L$, then \begin{align} \text{Applies}[q, b, q', b, d] = S_q(x_0,x_1) \wedge L_b(x_0,x_1) \wedge L_{b'}(x_0, \text{suc}(x_1)) \wedge S_{q'}(\text{pred}(x_0), \text{suc}(x_1)) \enspace. \end{align}

Finally, to describe the start configuration for $u$ with $|u| = n$, we use \begin{align} \text{FirstConfig}[u] = S_{q_\text{init}}(x_0, x_0) \wedge \bigwedge_{i<n} L_{u(i)}(\text{suc}^i(x_0), x_0) \wedge \forall x_1 \left(\bigvee_{i<n} \neg x_1 \doteq \text{suc}^i(x_0) \rightarrow L_\underline{\ }(x_1, x_0)\right) \enspace. \end{align} Here, $\text{suc}^i$ stands for $i$ applications of $\text{suc}$.

The overall formula is $\text{InfComputation}[u]$, which is defined by \begin{align} \text{InfComputation}[u] = \text{FirstConfig}[u] \wedge \text{Domain} \wedge \text{LettersStates} \wedge \text{SameLetters} \wedge \text{Transitions} \enspace. \end{align}

To indicate that $\text{InfComputation}[u]$ depends on the given TM, say $M$, we also write $\text{InfComputation}_M[u]$.

From computations to models

Assume we are given a word $u$ such that the given TM has an infinite computation for this word. This means we have configurations

• $q_0 \in Q$, $c_0 \colon \mathbf Z \to B$, $p_0 \in \mathbf Z$,
• $q_1 \in Q$, $c_1 \colon \mathbf Z \to B$, $p_1 \in \mathbf Z$,
• ...

where the first configuration is the start configuration for $u$ and configuration $i+1$ is a successor of the configuration $i$, for every $i \in \mathbf N$.

Our task is to turn this sequence of configurations into a model $\mathcal A, \beta$ of $\text{InfComputation}[u]$. We can use the above picture, that is, we set: \begin{align} A & = \mathbf Z \enspace,\\ \text{succ}^\mathcal A(j) & = j+1 && \text{for every $j \in \mathbf Z$}\enspace,\\ \text{pred}^\mathcal A(j) & = j-1 && \text{for every $j \in \mathbf Z$}\enspace,\\ S_q^\mathcal A & = \{\langle p_j, j\rangle \colon j \in \mathbf N \text{ and } q_j = q\}\enspace,\\ L_b^\mathcal A & = \{\langle i,j \rangle \colon i \in \mathbf N \text{ and } c_j(i) = b\} && \text{for every $b \in B$ with $b \neq \_$} \enspace,\\ L_{\_}^\mathcal A & = \{\langle i,j \rangle \colon i \in \mathbf N \text{ and } c_j(i) = \_\} \cup \{\langle i, -j-1\rangle \colon i \in \mathbf Z \text{ and } j \in \mathbf N\}\enspace. \end{align} Note that the last equation stipulates that all points in the lower half of the grid carry the blank symbol.

Now it is easy to check that $\mathcal A, \{x_0 \mapsto 0, x_1 \mapsto 0\} \mymodels \text{InfComputation}[u]$ holds.

From models to computations

Assume we are given a word $u$ and an $\mathcal S$-structure $\mathcal A$ and an $A$-assignment $\beta$ such that $\mathcal A, \beta \mymodels \text{InfComputation}[u]$. Then we can construct an infinite computation of the given TM on $u$ as follows.

In the first step, we reconstruct the integers: we set $f(i) = \llbracket \text{suc}^i(x_0) \rrbracket_\beta^\mathcal A$ for every $i \geq 0$ and $f(-i) = \llbracket \text{pred}^i(x_0)\rrbracket_{\beta}^\mathcal A$ for every $i>0$.

The formula $\text{Domain}$ makes sure that, for instance, $\llbracket \text{pred}(x_i)\rrbracket_{x_0 \mapsto f(i)}^\mathcal A = f(i-1)$. This is trivially true for $i \leq 0$, but $\text{Domain}$ is needed for $i>0$.

Because of $\mathcal A \mymodels \text{LettersStates}$, the following is true:

• For every $i$ and every $j$ there is exactly one $b \in B$ such that $\mathcal A, \{x_0 \mapsto f(i), x_1 \mapsto f(j)\} \mymodels L_b(x_0, x_1)$. We set $c_j(i) = b$ for this $b \in B$.
• For every $j$ there is at most one $i$ and one $q \in Q$ such that $\mathcal A, \{x_0 \mapsto f(i), x_1 \mapsto f(j)\} \mymodels S_q(x_0, x_1)$. If this $i$ exists, we write $p_j$ for it and set $q_j = q$.

The desired sequence of computations is reconstructed as follows. From $\mathcal A \mymodels \text{InfComputation}[u]$, we can conclude that

• $p_0$ is defined and equals $0$,
• $c_0$ describes the content of the tape at the beginning of the computation on $u$, and
• $q_0$ is defined and equals $q_\text{init}$.

In other words, $q_0$, $c_0$, $p_0$ is the start configuration of the TM on $u$. By induction, one can now define $c_{j+1}$ for every $j\geq 0$ and show that $p_{j+1}$ and $q_{j+1}$ are well-defined and such that $q_{j+1}$, $c_{j+1}$, and $p_{j+1}$ is a successor of the configuration $q_i$, $c_i$, and $p_i$. In this inductive prove one uses that $\mathcal A \mymodels \text{SameLetters}$ and $\mathcal A \mymodels \text{Transitions}$ hold.

Reduction

The overall result is:

Theorem

1. Let $M$ be an arbitrary TM over some alphabet $A$. Then $M$ has an infinite computation on $u$ if, and only if, $\text{InfComputation}_M[u]$ is satisfiable.
2. The function $g$, which maps every encoding of a TM $M$ and a given input $u$ for this TM to $\text{InfComputation}[u]_m$, is computable.

Undecidability of satisfiability

The above result implies immediately the undecidability of the satisfiability problem for first-order formulas.