View source for Gödel completeness theorem

The following statement on the completeness of classical predicate calculus: Any predicate formula that is true in all models is deducible (by formal rules of classical predicate calculus). The theorem proves that the set of deducible formulas of this calculus is, in a certain sense, maximal: it contains all purely-logical laws of set-theoretic mathematics. K. Gödel's proof [[#References|[1]]] yields a means of constructing a countermodel (i.e. model for the negation) of any formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g0445101.png" /> that is not-deducible in the [[Gentzen formal system|Gentzen formal system]] without cut-rule. There are also proofs based on extensions of the system of formulas to a maximal system, and also proofs involving the use of algebraic methods. The theorem together with the proof has been generalized to include calculi with equality. Another direction is a generalization to arbitrary sets of formulas: Any consistent set of formulas has a model (a set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g0445102.png" /> is called consistent if for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g0445103.png" /> it is not possible to deduce <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g0445104.png" />). Gödel's proof yields a model, with terms as its elements, for a consistent set of formulas. Such models constitute a starting point in many meta-mathematical studies on set theory. Another application of models of terms is the Löwenheim–Skolem theorem: If a denumerable set of formulas has a model, then it has a denumerable model. Gödel's proof itself can be carried out in set theory without the axiom of infinity, i.e. by arithmetical means. One obtains thus a constructive form of Gödel's completeness theorem (Bernays' lemma): For each predicate formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g0445105.png" /> it is possible to find a substitution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g0445106.png" /> of arithmetical predicates for predicate variables such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g0445107.png" /> is deducible in formal arithmetic. Here <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g0445108.png" /> is the arithmetical formula that says that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g0445109.png" /> is deducible. Thus, for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g04451010.png" /> to be deducible it is sufficient for it to be true in the model defined by the substitution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g04451011.png" />. Bernays' lemma is used to construct models of a formal system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g04451012.png" /> in a system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g04451013.png" /> if in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g04451014.png" /> the consistency of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044510/g04451015.png" /> has been proved.

From Gödel's completeness theorem one may deduce the cut-elimination theorem (see [[Gentzen formal system|Gentzen formal system]]) and various separation theorems, e.g.: If a formula not containing the equality sign is deducible in predicate calculus with equality, then it is also deducible by pure predicate calculus; if a predicate formula is deducible in arithmetic with free predicate variables, then it is deducible in predicate calculus.

Gödel's completeness theorem may be generalized (if the concept of a model is suitably generalized as well) to non-classical calculi: intuitionistic, modal, etc., as well as to infinitary languages.

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  K. Gödel,   "Die Vollstandigkeit der Axiomen des logischen Funktionalkalküls"  ''Monatsh. Math. Physik'' , '''37'''  (1930)  pp. 349–360</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  P.S. Novikov,   "Elements of mathematical logic" , Oliver &amp; Boyd and Acad. Press  (1964)  (Translated from Russian)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  S.C. Kleene,   "Introduction to metamathematics" , North-Holland  (1951)</TD></TR></table>