Gödel's completeness theorem

From Wikipedia, the free encyclopedia

Gödel's completeness theorem is an important theorem in mathematical logic which was first proved by Kurt Gödel in 1929. It states, in its most familiar form, that in first-order predicate calculus every logically valid formula is provable.

The word "provable" above means that there is a formal deduction of the formula. Such a deduction is a finite list of steps in which each step either invokes an axiom or is obtained from previous steps by a basic inference rule. Given such a deduction, the correctness of each of its steps can be checked algorithmically (by a computer, for example, or by hand).

A formula is called logically valid if it is true in every model for the language of the formula. In order to formally state Gödel's completeness theorem, one has to define what the word model means in this context. This is a basic definition in model theory.

Put another way, Gödel's completeness theorem says that the inference rules of first-order predicate calculus are "complete" in the sense that no additional inference rule is required to prove all the logically valid formulas. A converse to completeness is soundness. The fact that first-order predicate calculus is sound, i.e., that only logically valid statements can be proven in first-order logic, is asserted by the soundness theorem.

The branch of mathematical logic that deals with what is true in different models is called model theory. The branch called proof theory studies what can be formally proved in particular formal systems. The completeness theorem establishes a fundamental connection between these two branches, giving a link between semantics and syntax. The completeness theorem should not, however, be misinterpreted as obliterating the difference between these two concepts; in fact Gödel's incompleteness theorem, another celebrated result, shows that there are inherent limitations in what can be achieved with formal proofs in mathematics. The name for the incompleteness theorem refers to another meaning of complete, as the article on model theory explains.

A more general version of Gödel's completeness theorem holds. It says that for any first-order theory T and any sentence S in the language of the theory, there is a formal deduction of S from T if and only if S is satisfied by every model of T. This more general theorem is used implicitly, for example, when a sentence is shown to be provable from the axioms of group theory by considering an arbitrary group and showing that the sentence is satisfied by that group.

The completeness theorem is a central property of first-order logic that does not hold for all logics. Second-order logic, for example, does not have a completeness theorem.

The completeness theorem is equivalent to the ultrafilter lemma, a weak form of the axiom of choice, with the equivalence provable in Zermelo–Fraenkel set theory without the axiom of choice.

1 Proofs
2 See also
3 Further reading
4 External links

[edit] Proofs

For an explanation of Gödel's original proof of the theorem, see Original proof of Gödel's completeness theorem.

In modern logic texts, Gödel's completeness theorem is usually proved with Henkin's proof rather than with Gödel's original proof.

[edit] See also

Gödel's incompleteness theorems

[edit] Further reading

Kurt Gödel, "Über die Vollständigkeit des Logikkalküls", doctoral dissertation, University Of Vienna, 1929. This dissertation is the original source of the proof of the completeness theorem.
Kurt Gödel, "Die Vollständigkeit der Axiome des logischen Funktionen-kalküls", Monatshefte für Mathematik und Physik 37 (1930), 349-360. This article contains the same material as the doctoral dissertation, in a rewritten and shortened form. The proofs are more brief, the explanations more succinct, and the lengthy introduction has been omitted.