The Undecidability of First-Order Logic

To say that first-order logic is undecidable is to say that there is no Turing machine (or equivalent formalism) that can decide whether or not a formula $\phi$ in a given first-order language is valid. Our approach to establishing that there is no such Turing machine will be to show that given a Turing machine M and input n to this machine (where n is a natural number represented by a string of n 1's), there is a set $\Delta$ of first-order formulas, and a first-order formula $\phi_h$, such that

$$\Delta \vdash \phi_h.$$

In order to produce $\Delta$ and $\phi_h$ given a Turing machine M, we begin by assuming that this machine's tape has had all its squares numbered, as in

$\cdots$

-2

-1

0

1

2

$\cdots$

We assume that our Turing machines begin operation at time 0, and march on, step by step for each operation, with time incremented by one unit for each step. We thus model time on N. Next, we need three predicates, Q, S, and <, defined as follows.

• Q(q_i,t,x) iff at time t the machine is in state q_i scanning square number x.
• S(s_j,t,x) iff at time t the symbol s_j is in square number x.
• x < y iff x is less than y.

We assume that the alphabet of our the Turing machine we are capturing in first-order logic is $\{s_0, s_1, \ldots, s_r\}$, where s₀ is 0 and s₁ is 1. Given all this we show how to recast all the kinds of arcs that can exist in a flow diagrammatic representation of Turing machines.

The first type of arc we consider goes from state q_i to q_m and is labelled with a pair s_j s_k. Here is the formula corresponding to this arc (where t ranges over times, and x and y over square numbers, and where n' is the successor of n):

$$\begin{eqnarray*} \forall t \forall x \forall y \{[Q(q_i,t,x) \wedge S(s_j,t,x)]... ...y)) \wedge \ldots \wedge (S(s_r,t,y) \rightarrow S(s_r,t',y))]\} \end{eqnarray*}$$

Now for those arcs that indicate movement, either to the right (denoted here by R) or to the left (L). The former, with the arc from state q_i to q_m having the label s_j R, is represented as follows in first-order logic.

$$\begin{eqnarray*} \forall t \forall x \forall y \{[Q(q_i,t',x') \wedge S(s_j,t,x... ...y)) \wedge \ldots \wedge (S(s_r,t,y) \rightarrow S(s_r,t',y))]\} \end{eqnarray*}$$

It should be obvious from this how to symbolize the operation of moving to the left.

Here, now, is how the initial configuration of the machine M can be captured:

$$\begin{eqnarray*} Q(q_1,0,0) \wedge S(s_1,0,0) \wedge S(s_1,0,0') \wedge \ldots ... ...0' \wedge \ldots \wedge y \not= 0^{n-1}) \rightarrow S(s_0,0,y)] \end{eqnarray*}$$

We also need for make sure that the function ' works as desired, so we need the following formulas.

$$\forall z \exists x z = x' \wedge \forall z \forall x \forall y ((z = x' \wedge z = y') \rightarrow x = y)$$ (5.1)

$$\forall x \forall y \forall z ((x<y \wedge y<z) \rightarrow ... ...ow x <y) \wedge \forall x \forall y (x<y \rightarrow x \not=y)$$ (5.2)

Finally, what is $\phi_h$? This formula is the disjunction of all symbolizations of parts of flow diagrams where there is no entry in the left of a label for an arc, for symbol s_j. So $\phi_h$ will be a disjunction of formulas having this form:

$$\exists t \exists x [Q(q_i,t,x) \wedge S(s_j,t,x)]$$ (5.3)