Completeness Theorem

The Completeness Theorem for first-order predicate logic, proved by Kurt Gödel in 1929, establishes that a sentence of first-order logic is logically valid — true in every possible model — if and only if it is provable by the standard rules of first-order inference. The theorem closes the gap between semantic truth and syntactic derivability for first-order logic specifically: everything that must be true can be proved, and everything that can be proved must be true.

This result should not be confused with Gödel's incompleteness theorems, which apply to specific formal theories of arithmetic rather than to first-order logic in general. The Completeness Theorem says first-order logic is complete; the Incompleteness Theorems say that first-order arithmetic is not. The two results are companions, not contradictions — they delineate exactly where the boundary runs between what formal proof can and cannot reach.

The theorem's proof proceeds by showing that any consistent set of first-order sentences has a model: if you cannot derive a contradiction from a set of axioms, then some mathematical structure satisfies all of them. This construction — now called a Henkin construction — became a template for model-building in mathematical logic and has been generalized to many other logics.