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
Theorem The following problem is undecidable: given a signature $\mathcal S$ and a $\mathcal S$-formula, is $\varphi$ satisfiable?
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.
Variants
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.