First-Order Logic is Undecidable

Sketch of One Possible Proof

Idea: we know that halting problem is undecidable.

We show that, if there were a terminating algorithm for checking validity of first-order logic formulas, then we could solve the halting problem.

Given a Turing machine description $M$ and an input $w$ , we given an algorithm for constructing a formula $F$ in first-order logic such that

if $F$ is valid, then $M$ accepts $w$
if $M$ accepts $w$ , then $F$ is valid

Standard approach: $M$ accepts $w$ iff there exists a sequence of configurations from the initial state to final state.

Encode existence of accepting configuration as formula validity.

Technical difficulty: no simple way to express sequences, reachability, or finiteness in first order logic.

Note the following equivalent statements of our target condition:

( $F$ is valid) iff ( $M$ accepts $w$ )

(( $\lnot F$ ) is unsatisfiable) iff ( $M$ accepts $w$ )

(( $\lnot F$ ) is satisfiable) iff ( $M$ does not accept $w$ )

(( $\lnot F$ ) is true in some Herbrand model) iff ( $M$ does not accept $w$ )

So, we work with formula $G$ denoting $\lnot F$ , interpreted over Herbrand model, and we express the condition that all Turing machine computation histories are non-accepting. In other words, $F$ , when interpreted over Herbrand interpretations, says that there exists an accepting Turing computation history.

The fact that we work over Herbrand models helps us talk about computation histories, because we can encode strings and reachability.