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 and an input , we given an algorithm for constructing a formula in first-order logic such that
- if is valid, then accepts
- if accepts , then is valid
Standard approach: accepts 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 equivalences:
is valid iff accepts
( is unsatisfiable) iff accepts
( is satisfiable) iff does not accept
(() is true in some Herbrand model) iff ( does not accept )
So, we work with formula denoting , 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.