Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929.
A first-order formula is called logically valid if it is true in every structure for its language. The completeness theorem shows that if a formula is logically valid then there is a finite deduction (a formal proof) of the formula. The deduction is a finite object that can be verified by hand or computer. This relationship between truth and provability establishes a close link between model theory and proof theory in mathematical logic.
An important consequence of the completeness theorem is that it is possible to enumerate the logical consequences of any effective first-order theory, by enumerating all the correct deductions using axioms from the theory.
Gödel's incompleteness theorem, referring to a different meaning of completeness, shows that if any sufficiently strong effective theory of arithmetic is consistent then there is a formula (depending on the theory) which can neither be proven nor disproven within the theory. Nevertheless the completeness theorem applies to these theories, showing that any logical consequence of such a theory is provable from the theory.
There are numerous deductive systems for first-order logic, including systems of natural deduction and Hilbert-style systems. Common to all deductive systems is the notion of a formal deduction. This is a sequence (or, in some cases, a finite tree) of formulas with a specially-designated conclusion. The definition of a deduction is such that it is finite and that it is possible to verify algorithmically (by a computer, for example, or by hand) that a given collection of formulas is indeed a deduction.
A formula is logically valid if it is true in every structure for the language of the formula. To formally state, and then prove, the completeness theorem, it is necessary to also define a deductive system. A deductive system is called complete if every logically valid formula is the conclusion of some formal deduction, and the completeness theorem for a particular deductive system is the theorem that it is complete in this sense. Thus, in a sense, there is a different completeness theorem for each deductive system.
Full article ▸