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 equivalent statements of our target condition:
( 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. In other words, , 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.