View source for Gödel incompleteness theorem

{{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.

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 $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|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====
<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>