# 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.