
Gdel's completeness theorem is a fundamental theorem in mathematical logic proved by Kurt Gdel in 1929. It states, in its most familiar form, that in firstorder predicate calculus every universally valid formula can be proved.
The word "proved" above means, in effect: proved by a method whose validity can be checked algorithmically, for example, by a computer (although no such machines existed in 1929).
A logical formula is called universally valid if it is true in every possible domain and with every possible interpretation, inside that domain, of nonconstant symbols used in the formula. To say that it can be proved means that there exists a formal proof of that formula which uses only the logical axioms and rules of inference adopted in some particular formalisation of firstorder predicate calculus.
The theorem can be seen as a justification of the logical axioms and inference rules of firstorder logic. The rules are "complete" in the sense that they are strong enough to prove every universally valid statement. A converse to completeness is soundness, i.e., the fact that only universally valid statements can be proven in firstorder logic. (In fact, the axioms of firstorder logic are chosen in such a way that soundness is more or less obvious.)
To cleanly state Gdel's completeness theorem, one has to refer to an underlying set theory in order to clarify what the word "domain" in the definition of "universally valid" means.
The branch of mathematical logic that deals with what is true in different domains and under different interpretations is model theory; the branch that deals with what can be formally proved is proof theory. The completeness theorem, therefore, establishes a fundamental connection between what is (universally) true and what can be proved; between model theory and proof theory; between semantics and syntax in mathematical logic. It should not, however, be misinterpreted as obliterating the difference between these two concepts; in fact, another celebrated result by the same author, Gdel's incompleteness theorem, shows that there are inherent limitations in what can be achieved with formal proofs in mathematics.
Gdel's incompleteness theorem was the death knell of an attempt by the renowned mathematicians Alfred North Whitehead and Bertrand Russell to patch up set theories developed by Gottlob Frege and Georg Cantor, which attempted to avoid certain paradoxes derived more or less from an ancient one, Epimenides paradox, which, itself is resolvable as usually stated. The WhiteheadRussell proposal was, in very simple terms, to classify sets of sets at a higher level, or type, than the underlying sets of which they were composed. Type theory is a surviving descendant of their work, but their basic aim of allowing the creation of certain axiomatic systems was defeated by Gdel.
Proofs
For an explanation of Gdel's original proof of the theorem, see original proof.
In modern logic texts, Gdel's completeness theorem is usually proved with Henkin's proof rather than with Gdel's original proof.
Further reading
 Kurt Gdel, "ber die Vollstndigkeit des Logikkalkls", doctoral dissertation, University Of Vienna, 1929. This dissertation is the original source of the proof of the completeness theorem.
 Kurt Gdel, "Die Vollstndigkeit der Axiome des logischen Funktionenkalkls", Monatshefte fr Mathematik und Physik 37 (1930), 349360. 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.
External link
 Vilnis Detlovs and Karlis Podnieks, "Introduction to mathematical logic", http://www.ltn.lv/~podnieks/fr:Thorme de compltude