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 [1] yields a means of constructing a countermodel (i.e. model for the negation) of any formula $ A $ that is not-deducible in the 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 $ M $ is called consistent if for any $ A _ {1} \dots A _ {k} \subset M $ it is not possible to deduce $ \neg ( A _ {1} \wedge \dots \wedge A _ {k} ) $). 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 $ A $ it is possible to find a substitution $ \xi $ of arithmetical predicates for predicate variables such that $ \xi A \rightarrow \mathop{\rm Pr} ( A) $ is deducible in formal arithmetic. Here $ \mathop{\rm Pr} ( A) $ is the arithmetical formula that says that $ A $ is deducible. Thus, for $ A $ to be deducible it is sufficient for it to be true in the model defined by the substitution $ \xi $. Bernays' lemma is used to construct models of a formal system $ S $ in a system $ S ^ \prime $ if in $ S ^ \prime $ the consistency of $ S $ has been proved.

From Gödel's completeness theorem one may deduce the cut-elimination theorem (see 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

[1]	K. Gödel, "Die Vollstandigkeit der Axiomen des logischen Funktionalkalküls" Monatsh. Math. Physik , 37 (1930) pp. 349–360 Zbl 56.0046.04
[2]	P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd and Acad. Press (1964) (Translated from Russian)
[3]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)