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.
A formula is logically valid if it is true in every structure for the language of the formula. In order 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.
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 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 (see model theory - Using the compactness and completeness theorems). In particular, Gödel's completeness theorem deals with formulas that are logical consequences of a first-order theory, while the incompleteness theorem constructs formulas that are not logical consequences of certain theories.
An important consequence of the completeness theorem is that the set of logical consequences of an effective first-order theory is an enumerable set. The definition of logical consequence quantifies over all structures in a particular language, and thus does not give an immediate method for algorithmically testing whether a formula is logically valid. Moreover, a consequence of Gödel's incompleteness theorem is that the set of logically valid formulas is not decidable. But the completeness theorem implies that the set of consequences of an effective theory is enumerable; the algorithm is to first construct an enumeration of all formal deductions from the theory, and use this to produce an enumeration of their conclusions. The finitary, syntactic nature of formal deductions makes it possible to enumerate them.
The completeness theorem and the compactness theorem are two cornerstones of first-order logic. While neither of these theorems can be proven in a completely effective manner, each one can be effectively obtained from the other.
The compactness theorem says that if a formula φ is a logical consequence of a (possible infinite) set of formulas Γ then it is a logical consequence of a finite subset of Γ. This is an immediate consequence of the completeness theorem, because only a finite number of axioms from Γ can be mentioned in a formal deduction of φ, and the soundness of the deduction system then implies φ is a logical consequence of this finite set. This proof of the compactness theorem is originally due to Gödel.
Conversely, for many deductive systems, it is possible to prove the completeness theorem as an effective consequence of the compactness theorem.
The ineffectiveness of the completeness theorem can be measured in two ways, in set theory and in reverse mathematics. In set theory, the ultrafilter lemma is a weak form of the axiom of choice that is not provable in ZF, the system of Zermelo–Fraenkel set theory. ZF proves the completeness and compactness theorems are equivalent to each other, and to the ultrafilter lemma. Thus no theory extending ZF can prove either the completeness or compactness theorems without also proving the ultrafilter lemma. In reverse mathematics, only countable structures and countable theories are considered. In this context, the completeness and compactness theorems are equivalent to each other and to the axiom system WKL0, with the equivalence provable in RCA0. In particular, although every consistent first-order theory has a finite or countable model, as a consequence of the completeness theorem and the Löwenheim-Skolem theorem, it is known there are effective consistent first-order theories with no computable model.
Gödel's original proof of the theorem proceeded by reducing the problem to a special case for formulas in a certain syntactic form, and then handling this form with an ad hoc argument.
In modern logic texts, Gödel's completeness theorem is usually proved with Henkin's proof, rather than with Gödel's original proof. Henkin's proof directly constructs a term model for any consistent first-order theory. Other proofs are also known.