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.


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.