Namespaces
Variants
Actions

Difference between revisions of "Gödel completeness theorem"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (→‎References: zbl link)
 
(3 intermediate revisions by one other user not shown)
Line 1: Line 1:
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.
+
<!--
 +
g0445101.png
 +
$#A+1 = 15 n = 0
 +
$#C+1 = 15 : ~/encyclopedia/old_files/data/G044/G.0404510 G\AGodel completeness theorem
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
 +
 
 +
{{TEX|auto}}
 +
{{TEX|done}}
 +
 
 +
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 $  A $
 +
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 $  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|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.
 
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.
Line 6: Line 33:
  
 
====References====
 
====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>
+
<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 {{ZBL|56.0046.04}}</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>

Latest revision as of 14:27, 19 March 2023


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)
How to Cite This Entry:
Gödel completeness theorem. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=G%C3%B6del_completeness_theorem&oldid=14942
This article was adapted from an original article by G.E. Mints (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article