[proofplan] We reduce [the halting problem](/theorems/1823) to first-order validity. Given a Turing machine index $e$ and input word $x$, we effectively build a first-order sentence $\theta_{e,x}$ whose models are non-halting computation histories for machine $e$ on input $x$. Thus $\theta_{e,x}$ is satisfiable exactly when the computation does not halt, so $\neg \theta_{e,x}$ is valid exactly when the computation halts. A decision procedure for first-order validity would therefore decide the halting problem, contradicting its undecidability. [/proofplan]

[step:Encode computation histories in a finite first-order language]Fix a deterministic one-tape Turing machine $M_e$ with finite state set $Q$, tape alphabet $\Gamma$, initial state $q_{\mathrm{init}} \in Q$, and halting state $q_{\mathrm{halt}} \in Q$. For the input word $x = x_0 \cdots x_{m-1} \in \Gamma^m$, we construct a many-sorted first-order signature $\mathcal{L}_{e,x}$ with a time sort $T$ and a tape-position sort $P$. The time sort has a constant $0_T$ and a unary function symbol \begin{align*} S_T : T \to T. \end{align*} The tape-position sort has a constant $0_P$ and unary function symbols \begin{align*} R &: P \to P, \\ L &: P \to P, \end{align*} intended to denote the right and left tape-neighbour maps. For each state $q \in Q$ we introduce a unary predicate \begin{align*} \operatorname{State}_q \subseteq T, \end{align*} for each tape symbol $a \in \Gamma$ a binary predicate \begin{align*} \operatorname{Sym}_a \subseteq T \times P, \end{align*} and a binary predicate \begin{align*} \operatorname{Head} \subseteq T \times P. \end{align*} The sentence $\theta_{e,x}$ is the conjunction of the following first-order assertions. First, the tape-position successor maps are inverse to each other: \begin{align*} \forall p \in P \, \bigl(L(R(p)) = p \wedge R(L(p)) = p\bigr). \end{align*} Second, at every time there is exactly one state: \begin{align*} \forall t \in T \, \bigvee_{q \in Q} \operatorname{State}_q(t), \end{align*} together with, for all distinct $q,r \in Q$, \begin{align*} \forall t \in T \, \neg\bigl(\operatorname{State}_q(t) \wedge \operatorname{State}_r(t)\bigr). \end{align*} Third, at every time and tape position there is exactly one tape symbol: \begin{align*} \forall t \in T \, \forall p \in P \, \bigvee_{a \in \Gamma} \operatorname{Sym}_a(t,p), \end{align*} together with, for all distinct $a,b \in \Gamma$, \begin{align*} \forall t \in T \, \forall p \in P \, \neg\bigl(\operatorname{Sym}_a(t,p) \wedge \operatorname{Sym}_b(t,p)\bigr). \end{align*} Fourth, at every time there is exactly one head position: \begin{align*} \forall t \in T \, \exists p \in P \, \operatorname{Head}(t,p), \end{align*} and \begin{align*} \forall t \in T \, \forall p \in P \, \forall r \in P \, \bigl(\operatorname{Head}(t,p) \wedge \operatorname{Head}(t,r) \implies p = r\bigr). \end{align*} Fifth, the initial configuration is imposed. We require \begin{align*} \operatorname{State}_{q_{\mathrm{init}}}(0_T) \wedge \operatorname{Head}(0_T,0_P). \end{align*} For each $i \in \{0,\dots,m-1\}$, let $R^i(0_P)$ denote the term obtained by applying $R$ exactly $i$ times to $0_P$; we require \begin{align*} \operatorname{Sym}_{x_i}(0_T,R^i(0_P)). \end{align*} Writing $\sqcup \in \Gamma$ for the blank symbol, we also require all other tape cells to be blank at time $0_T$: \begin{align*} \forall p \in P \, \left( \bigwedge_{i=0}^{m-1} p \neq R^i(0_P) \implies \operatorname{Sym}_{\sqcup}(0_T,p) \right). \end{align*} Sixth, for each non-halting transition \begin{align*} \delta(q,a) = (q',b,\mathrm{R}) \end{align*} of $M_e$, we include the local update axiom \begin{align*} \forall t \in T \, \forall p \in P \, \Bigl( \operatorname{State}_q(t) \wedge \operatorname{Head}(t,p) \wedge \operatorname{Sym}_a(t,p) \implies \operatorname{State}_{q'}(S_T(t)) \wedge \operatorname{Head}(S_T(t),R(p)) \wedge \operatorname{Sym}_b(S_T(t),p) \Bigr), \end{align*} and, for each tape symbol $c \in \Gamma$, \begin{align*} \forall t \in T \, \forall p \in P \, \forall r \in P \, \Bigl( \operatorname{State}_q(t) \wedge \operatorname{Head}(t,p) \wedge \operatorname{Sym}_a(t,p) \wedge r \neq p \implies \bigl(\operatorname{Sym}_c(t,r) \iff \operatorname{Sym}_c(S_T(t),r)\bigr) \Bigr). \end{align*} For a transition \begin{align*} \delta(q,a) = (q',b,\mathrm{L}), \end{align*} the same axiom is used with $\operatorname{Head}(S_T(t),L(p))$ in place of $\operatorname{Head}(S_T(t),R(p))$. Finally, $\theta_{e,x}$ asserts that no halting state ever occurs: \begin{align*} \forall t \in T \, \neg \operatorname{State}_{q_{\mathrm{halt}}}(t). \end{align*} This construction is effective in the pair $(e,x)$, because $Q$, $\Gamma$, $\delta$, and the finite word $x$ are computably obtained from the machine index and input.[/step]

[guided]The purpose of $\theta_{e,x}$ is not to describe an arbitrary computation loosely, but to force every model to behave like a complete non-halting run of $M_e$ on $x$. The sort $T$ carries formal times, with $S_T(t)$ representing the next time. The sort $P$ carries tape positions, with $R$ and $L$ representing right and left movement. The predicates $\operatorname{State}_q(t)$, $\operatorname{Head}(t,p)$, and $\operatorname{Sym}_a(t,p)$ record, respectively, the machine state at time $t$, the head position at time $t$, and the tape symbol at position $p$ at time $t$. The uniqueness axioms are needed because the transition rules only make sense for genuine configurations. At each time, exactly one state holds; at each time and tape position, exactly one symbol holds; and at each time, exactly one tape position is the head position. The initial-configuration axioms then force time $0_T$ to encode the input word $x$ with the head at the origin and all other cells blank. The transition axioms are local first-order formulas. If at time $t$ the state is $q$, the head is at $p$, and the scanned symbol is $a$, then at time $S_T(t)$ the new state, new head position, and overwritten symbol agree with $\delta(q,a)$. The additional equivalence \begin{align*} \operatorname{Sym}_c(t,r) \iff \operatorname{Sym}_c(S_T(t),r) \end{align*} for $r \neq p$ says that every tape cell not under the head keeps its old symbol. Because the machine has finitely many states, finitely many symbols, and finitely many transition instructions, all these requirements form one finite first-order sentence. The last conjunct, \begin{align*} \forall t \in T \, \neg \operatorname{State}_{q_{\mathrm{halt}}}(t), \end{align*} is what makes $\theta_{e,x}$ a sentence for non-halting histories. It says that the computation described by the model never reaches the halting state.[/guided]

[step:Show that the computation does not halt exactly when the history sentence is satisfiable]We prove \begin{align*} \theta_{e,x} \text{ is satisfiable} \iff M_e \text{ does not halt on input } x. \end{align*} Suppose first that $M_e$ does not halt on input $x$. Define an $\mathcal{L}_{e,x}$-structure $\mathcal{A}$ as follows. Let the time domain be $\mathbb{N}$ with $0_T^{\mathcal{A}} = 0$ and \begin{align*} S_T^{\mathcal{A}} : \mathbb{N} &\to \mathbb{N} \\ n &\mapsto n+1. \end{align*} Let the tape-position domain be $\mathbb{Z}$ with $0_P^{\mathcal{A}} = 0$ and \begin{align*} R^{\mathcal{A}} : \mathbb{Z} &\to \mathbb{Z} \\ k &\mapsto k+1, \end{align*} \begin{align*} L^{\mathcal{A}} : \mathbb{Z} &\to \mathbb{Z} \\ k &\mapsto k-1. \end{align*} For each $n \in \mathbb{N}$, interpret $\operatorname{State}_q(n)$, $\operatorname{Head}(n,k)$, and $\operatorname{Sym}_a(n,k)$ according to the actual configuration of $M_e$ after $n$ steps on input $x$. Since the computation never halts, $\operatorname{State}_{q_{\mathrm{halt}}}(n)$ is false for every $n \in \mathbb{N}$. The initial, uniqueness, tape-neighbour, transition, and non-halting axioms are therefore all satisfied, so $\mathcal{A} \models \theta_{e,x}$. Conversely, suppose that $M_e$ halts on input $x$ after exactly $N \in \mathbb{N}$ transition steps. Let $\mathcal{B}$ be any $\mathcal{L}_{e,x}$-structure satisfying all conjuncts of $\theta_{e,x}$ except possibly the final non-halting conjunct. By induction on $n \in \{0,\dots,N\}$, the axioms force the predicates at the time term $S_T^n(0_T)$ to agree with the actual $n$-step configuration of $M_e$ on input $x$. The base case is the initial-configuration conjunct. The induction step follows from the unique state, unique head position, unique tape symbol, and the transition axiom corresponding to the actual instruction used by $M_e$ at step $n$. At $n=N$, the actual state is $q_{\mathrm{halt}}$, hence the axioms force \begin{align*} \operatorname{State}_{q_{\mathrm{halt}}}(S_T^N(0_T)). \end{align*} But $\theta_{e,x}$ also contains \begin{align*} \forall t \in T \, \neg \operatorname{State}_{q_{\mathrm{halt}}}(t), \end{align*} and applying this universal sentence to $t = S_T^N(0_T)$ gives a contradiction. Thus no model of $\theta_{e,x}$ exists when $M_e$ halts on $x$.[/step]

[guided]We must prove both directions because satisfiability is a semantic property, while halting is a computational property. First assume the computation never halts. Then there is an actual infinite run of $M_e$ on $x$. We turn that run into a structure. The time domain is $\mathbb{N}$, with successor $n \mapsto n+1$. The tape domain is $\mathbb{Z}$, with right and left neighbours $k \mapsto k+1$ and $k \mapsto k-1$. At each time $n$, the predicates record the actual machine configuration after $n$ steps. Since the machine never halts, the predicate $\operatorname{State}_{q_{\mathrm{halt}}}(n)$ is false for every time $n$. The axioms were written precisely to match the initial configuration and the transition function, so this structure satisfies $\theta_{e,x}$. Now assume the computation halts after exactly $N$ steps. We show that no structure can satisfy $\theta_{e,x}$. The point is that only finitely many transition steps are needed to reach the contradiction. Starting from the initial-configuration axioms, the transition axiom for the first actual instruction forces the correct configuration at $S_T(0_T)$. Applying the next transition axiom forces the correct configuration at $S_T^2(0_T)$, and continuing in this way gives a finite induction. Formally, for each $n \in \{0,\dots,N\}$, the predicates at the time term $S_T^n(0_T)$ agree with the actual $n$-step configuration. The base case $n=0$ is exactly the initial-configuration part of $\theta_{e,x}$. For the induction step, uniqueness of the state, head position, and tape symbol ensures that the relevant transition rule is the one dictated by the actual computation. The transition axiom then forces the next state, next head position, overwritten symbol, and unchanged symbols at time $S_T^{n+1}(0_T)$. At time $S_T^N(0_T)$, the actual computation is in state $q_{\mathrm{halt}}$, so the axioms force \begin{align*} \operatorname{State}_{q_{\mathrm{halt}}}(S_T^N(0_T)). \end{align*} But the final conjunct of $\theta_{e,x}$ says that no time is a halting time: \begin{align*} \forall t \in T \, \neg \operatorname{State}_{q_{\mathrm{halt}}}(t). \end{align*} Substituting $S_T^N(0_T)$ for $t$ gives the negation of the displayed formula. Hence $\theta_{e,x}$ is unsatisfiable whenever $M_e$ halts on $x$.[/guided]

[step:Pass from satisfiability of non-halting histories to validity]For every first-order sentence $\varphi$, the sentence $\neg \varphi$ is logically valid if and only if $\varphi$ is unsatisfiable. Applying this to $\varphi = \theta_{e,x}$ gives \begin{align*} \neg \theta_{e,x} \text{ is valid} &\iff \theta_{e,x} \text{ is unsatisfiable} \\ &\iff M_e \text{ halts on input } x. \end{align*} The first equivalence is the semantic definition of validity and satisfiability, and the second equivalence is the computation-history equivalence proved above.[/step]

[guided]Validity and satisfiability are dual under negation. A sentence $\neg\varphi$ is valid exactly when every structure satisfies $\neg\varphi$. That is equivalent to saying that no structure satisfies $\varphi$, which is exactly unsatisfiability of $\varphi$. Using the sentence $\theta_{e,x}$ constructed above, we therefore have \begin{align*} \neg \theta_{e,x} \text{ is valid} &\iff \theta_{e,x} \text{ has no model} \\ &\iff M_e \text{ halts on input } x. \end{align*} Thus the halting question for $(e,x)$ has been converted effectively into the validity question for the single first-order sentence $\neg\theta_{e,x}$.[/guided]

[step:Derive a contradiction from a hypothetical validity decision procedure] Assume, for contradiction, that first-order validity is decidable. Then there exists an algorithm \begin{align*} D : \mathbb{N} \to \{0,1\} \end{align*} such that, for every Gödel code $n$ of a first-order sentence $\varphi_n$, \begin{align*} D(n) = 1 \iff \varphi_n \text{ is logically valid}. \end{align*} Given a Turing machine index $e$ and input $x$, compute the Gödel code of $\neg\theta_{e,x}$ and run $D$ on that code. By the previous step, \begin{align*} D(\ulcorner \neg\theta_{e,x}\urcorner) = 1 \iff M_e \text{ halts on input } x. \end{align*} Hence $D$ would decide the halting problem. This contradicts the undecidability of the halting problem (citing a result not yet in the wiki: Undecidability of the Halting Problem). Therefore no decision procedure for first-order validity exists. Since many-sorted first-order logic over a finite many-sorted signature can be effectively translated into ordinary one-sorted first-order logic by adding unary sort predicates and relativizing quantifiers, the argument applies to the usual one-sorted formulation of first-order validity. Thus $\operatorname{Val}_{\mathrm{FOL}}$ is not decidable. [/step]