Undecidability of satisfiability of first-order formulas
From Learning Logic for Computer Science
The satisfiability problem for first-order formulas is undecidable.
Formal statement and proof
The proof is by reduction from the complement of the halting problem for deterministic TMs. Consider the function $g$ from the theorem on modeling computations. This is a reduction of the complement of the halting problem to the satisfiability problem for first-order logic.
Many variants of this problem can be considered, in particular, one can
- restrict the signatures and
- restrict the formulas allowed,
and one can combine the two. There are many results in this respect.