LARA

This is an old revision of the document!


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.

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