Namespaces
Variants
Actions

Difference between revisions of "Gödel incompleteness theorem"

From Encyclopedia of Mathematics
Jump to: navigation, search
m (moved Goedel incompleteness theorem to Gödel incompleteness theorem over redirect: accented title)
(TeX)
 
Line 1: Line 1:
A common name given to two theorems established by K. Gödel [[#References|[1]]]. Gödel's first incompleteness theorem states that in any consistent [[Formal system|formal system]] containing a minimum of arithmetic (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g0445301.png" />, the symbols <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g0445302.png" />, and the usual rules for handling them) a formally-undecidable proposition can be found, i.e. a closed formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g0445303.png" /> such that neither <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g0445304.png" /> nor <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g0445305.png" /> can be deduced within the system. Gödel's second incompleteness theorem states that if certain natural completeness conditions are met, one can take this formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g0445306.png" /> to be the formula which expresses the consistency of the system. These theorems indicated the failure of Hilbert's program on the foundations of mathematics, which expected a full formalization of all existing mathematics, or at least of a substantial part of it (Gödel's first incompleteness theorem proved that this is not possible), and attempted to justify the resulting formal system by a finite demonstration of its consistency (Gödel's second incompleteness theorem showed that even if all the tools of formalized arithmetic are considered to be finitary, this is still insufficient to prove the consistency of arithmetic).
+
{{TEX|done}}
 +
A common name given to two theorems established by K. Gödel [[#References|[1]]]. Gödel's first incompleteness theorem states that in any consistent [[Formal system|formal system]] containing a minimum of arithmetic ($+,\cdot$, the symbols $\forall,\exists$, and the usual rules for handling them) a formally-undecidable proposition can be found, i.e. a closed formula $A$ such that neither $A$ nor $\lnot A$ can be deduced within the system. Gödel's second incompleteness theorem states that if certain natural completeness conditions are met, one can take this formula $A$ to be the formula which expresses the consistency of the system. These theorems indicated the failure of Hilbert's program on the foundations of mathematics, which expected a full formalization of all existing mathematics, or at least of a substantial part of it (Gödel's first incompleteness theorem proved that this is not possible), and attempted to justify the resulting formal system by a finite demonstration of its consistency (Gödel's second incompleteness theorem showed that even if all the tools of formalized arithmetic are considered to be finitary, this is still insufficient to prove the consistency of arithmetic).
  
 
The formally-undecidable proposition is constructed by arithmetization (or Gödel numbering); this has now become one of the principal methods of proof theory (meta-mathematics); it is described below.
 
The formally-undecidable proposition is constructed by arithmetization (or Gödel numbering); this has now become one of the principal methods of proof theory (meta-mathematics); it is described below.
  
One fixes a numbering (encoding) of the basic formal objects (formulas, finite sequences of formulas, etc.) by natural numbers so that the principal properties of these objects (to be an [[Axiom|axiom]] or a logical derivation (cf. [[Derivation, logical|Derivation, logical]]) in accordance with the rules of the system, etc.) can be expressed by simple numbers. The calculation of the codes of results of combinatory transformations (e.g. substitution of a term for a variable in a formula) from the codes of the initial data are just as simple. It is possible, in this way, to write down an arithmetical formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g0445307.png" /> of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g0445308.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g0445309.png" /> is a primitive recursive function, in order to express the following condition: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453010.png" /> is the code of the formula which is obtained from the formula with the code <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453011.png" /> by substitution of the natural number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453012.png" /> for the variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453013.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453014.png" /> is the code of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453015.png" />, the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453016.png" /> denotes its own non-deducibility. It is thus formally undecidable. It follows that any consistent system with minimal arithmetical possibilities contains a true, but non-deducible statement of this type.
+
One fixes a numbering (encoding) of the basic formal objects (formulas, finite sequences of formulas, etc.) by natural numbers so that the principal properties of these objects (to be an [[Axiom|axiom]] or a logical derivation (cf. [[Derivation, logical|Derivation, logical]]) in accordance with the rules of the system, etc.) can be expressed by simple numbers. The calculation of the codes of results of combinatory transformations (e.g. substitution of a term for a variable in a formula) from the codes of the initial data are just as simple. It is possible, in this way, to write down an arithmetical formula $B(a,b)$ of the form $f(a,b)=0$, where $f$ is a primitive recursive function, in order to express the following condition: $b$ is the code of the formula which is obtained from the formula with the code $a$ by substitution of the natural number $a$ for the variable $x$. If $p$ is the code of the formula $\forall b\,\lnot B(x,b)$, the formula $\forall b\,\lnot B(p,b)$ denotes its own non-deducibility. It is thus formally undecidable. It follows that any consistent system with minimal arithmetical possibilities contains a true, but non-deducible statement of this type.
  
Gödel's second incompleteness theorem is obtained by formalizing the proof of Gödel's first incompleteness theorem. This proof involves a substantial use of the properties of the arithmetization of the syntax of the system under consideration, in that formulas expressing the following statements must be deducible: 1) the system is closed with respect to the rule of contraction of the argument ([[Modus ponens|modus ponens]]); 2) the system is closed under substitution of terms for individual variables; and 3) the truth of a formula of a form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453017.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453018.png" /> is a natural number and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453019.png" /> is a primitive recursive function, implies its deducibility. These conditions are met for natural arithmetization, but it is possible, without altering the algorithmic features of the arithmetization (all functions and predicates remain primitive recursive), to alter it so that the formula expressing the consistency of the system (with respect to the new arithmetization) becomes deducible. In the new arithmetization, condition 1) is violated.
+
Gödel's second incompleteness theorem is obtained by formalizing the proof of Gödel's first incompleteness theorem. This proof involves a substantial use of the properties of the arithmetization of the syntax of the system under consideration, in that formulas expressing the following statements must be deducible: 1) the system is closed with respect to the rule of contraction of the argument ([[Modus ponens|modus ponens]]); 2) the system is closed under substitution of terms for individual variables; and 3) the truth of a formula of a form $f(N)=0$, where $N$ is a natural number and $f$ is a primitive recursive function, implies its deducibility. These conditions are met for natural arithmetization, but it is possible, without altering the algorithmic features of the arithmetization (all functions and predicates remain primitive recursive), to alter it so that the formula expressing the consistency of the system (with respect to the new arithmetization) becomes deducible. In the new arithmetization, condition 1) is violated.
  
Gödel's second incompleteness theorem gives a criterion for the comparison of formal systems: If it is possible to prove the consistency of a system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453020.png" /> in a system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453021.png" />, then the latter system cannot be interpreted in the former. It can thus be proved that [[Formal mathematical analysis|formal mathematical analysis]] is not interpretable in arithmetic, the theory of types is not interpretable in analysis (cf. [[Types, theory of|Types, theory of]]), and set theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044530/g04453022.png" /> is not interpretable in the theory of types.
+
Gödel's second incompleteness theorem gives a criterion for the comparison of formal systems: If it is possible to prove the consistency of a system $T$ in a system $S$, then the latter system cannot be interpreted in the former. It can thus be proved that [[Formal mathematical analysis|formal mathematical analysis]] is not interpretable in arithmetic, the theory of types is not interpretable in analysis (cf. [[Types, theory of|Types, theory of]]), and set theory $Z$ is not interpretable in the theory of types.
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  K. Gödel,  "Ueber formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I"  ''Monatsh. Math. Physik'' , '''38'''  (1931)  pp. 178–198</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  D. Hilbert,  P. Bernays,  "Grundlagen der Mathematik" , '''1–2''' , Springer  (1968–1970)</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,  "Ueber formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I"  ''Monatsh. Math. Physik'' , '''38'''  (1931)  pp. 178–198</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  D. Hilbert,  P. Bernays,  "Grundlagen der Mathematik" , '''1–2''' , Springer  (1968–1970)</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 18:30, 18 November 2018

A common name given to two theorems established by K. Gödel [1]. Gödel's first incompleteness theorem states that in any consistent formal system containing a minimum of arithmetic ($+,\cdot$, the symbols $\forall,\exists$, and the usual rules for handling them) a formally-undecidable proposition can be found, i.e. a closed formula $A$ such that neither $A$ nor $\lnot A$ can be deduced within the system. Gödel's second incompleteness theorem states that if certain natural completeness conditions are met, one can take this formula $A$ to be the formula which expresses the consistency of the system. These theorems indicated the failure of Hilbert's program on the foundations of mathematics, which expected a full formalization of all existing mathematics, or at least of a substantial part of it (Gödel's first incompleteness theorem proved that this is not possible), and attempted to justify the resulting formal system by a finite demonstration of its consistency (Gödel's second incompleteness theorem showed that even if all the tools of formalized arithmetic are considered to be finitary, this is still insufficient to prove the consistency of arithmetic).

The formally-undecidable proposition is constructed by arithmetization (or Gödel numbering); this has now become one of the principal methods of proof theory (meta-mathematics); it is described below.

One fixes a numbering (encoding) of the basic formal objects (formulas, finite sequences of formulas, etc.) by natural numbers so that the principal properties of these objects (to be an axiom or a logical derivation (cf. Derivation, logical) in accordance with the rules of the system, etc.) can be expressed by simple numbers. The calculation of the codes of results of combinatory transformations (e.g. substitution of a term for a variable in a formula) from the codes of the initial data are just as simple. It is possible, in this way, to write down an arithmetical formula $B(a,b)$ of the form $f(a,b)=0$, where $f$ is a primitive recursive function, in order to express the following condition: $b$ is the code of the formula which is obtained from the formula with the code $a$ by substitution of the natural number $a$ for the variable $x$. If $p$ is the code of the formula $\forall b\,\lnot B(x,b)$, the formula $\forall b\,\lnot B(p,b)$ denotes its own non-deducibility. It is thus formally undecidable. It follows that any consistent system with minimal arithmetical possibilities contains a true, but non-deducible statement of this type.

Gödel's second incompleteness theorem is obtained by formalizing the proof of Gödel's first incompleteness theorem. This proof involves a substantial use of the properties of the arithmetization of the syntax of the system under consideration, in that formulas expressing the following statements must be deducible: 1) the system is closed with respect to the rule of contraction of the argument (modus ponens); 2) the system is closed under substitution of terms for individual variables; and 3) the truth of a formula of a form $f(N)=0$, where $N$ is a natural number and $f$ is a primitive recursive function, implies its deducibility. These conditions are met for natural arithmetization, but it is possible, without altering the algorithmic features of the arithmetization (all functions and predicates remain primitive recursive), to alter it so that the formula expressing the consistency of the system (with respect to the new arithmetization) becomes deducible. In the new arithmetization, condition 1) is violated.

Gödel's second incompleteness theorem gives a criterion for the comparison of formal systems: If it is possible to prove the consistency of a system $T$ in a system $S$, then the latter system cannot be interpreted in the former. It can thus be proved that formal mathematical analysis is not interpretable in arithmetic, the theory of types is not interpretable in analysis (cf. Types, theory of), and set theory $Z$ is not interpretable in the theory of types.

References

[1] K. Gödel, "Ueber formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" Monatsh. Math. Physik , 38 (1931) pp. 178–198
[2] D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1–2 , Springer (1968–1970)
[3] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
How to Cite This Entry:
Gödel incompleteness theorem. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=G%C3%B6del_incompleteness_theorem&oldid=43438
This article was adapted from an original article by G.E. Mints (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article