From Wikipedia, the free encyclopedia
Gödel's incompleteness theorems are two theorems of mathematical
logic that state inherent limitations of all but the most
trivial axiomatic systems for mathematics.
They state that any consistent system of axioms whose theorems
can be listed by a computer program is incapable of proving certain
truths about arithmetic. This means that any consistent computable
formal theory which can prove some arithmetic truths
cannot prove all arithmetic truths.
The theorems were proven by Kurt Gödel in 1931, and are important in the
philosophy of mathematics.
The result is widely interpreted as showing that Hilbert's
program to find a complete and consistent set of axioms for all of mathematics is
impossible, thus giving a negative answer to Hilbert's second problem.
Background
In mathematical logic, a theory is a set of sentences expressed in a
formal
language. Some statements in a theory are included without proof
(these are the axioms of the
theory), and others (the theorems) are included because they are
implied by the axioms.
Because statements of a formal theory are written in symbolic
form, it is possible to mechanically verify that a formal proof from a
finite set of axioms is valid. This task, known as automatic proof
verification, is closely related to automated theorem proving;
the difference is that instead of constructing a new proof, the
proof verifier simply checks that a provided formal proof (or, in
some cases, instructions that can be followed to create a formal
proof) is correct. This is not merely hypothetical; systems such as
Isabelle are used today to
formalize proofs and then check their validity.
Many theories of interest include an infinite set of axioms,
however. To verify a formal proof when the set of axioms is
infinite, it must be possible to determine whether a statement that
is claimed to be an axiom is actually an axiom. This issue arises
in first
order theories of arithmetic, such as Peano arithmetic, because the principle of
mathematical induction is
expressed as an infinite set of axioms (an axiom schema).
A formal theory is said to be effectively generated if
its set of axioms is a recursively enumerable set.
This means that there is a computer program that, in principle,
could enumerate all the axioms of the theory without listing any
statements that are not axioms. This is equivalent to the ability
to enumerate all the theorems of the theory without enumerating any
statements that are not theorems. For example, each of the theories
of Peano arithmetic and Zermelo–Fraenkel set theory
has an infinite number of axioms and each is effectively
generated.
In choosing a set of axioms, one goal is to be able to prove as
many correct results as possible, without proving any incorrect
results. A set of axioms is complete if, for any statement in the
axioms' language, either that statement or its negation is provable
from the axioms. A set of axioms is (simply) consistent if there is no statement so that
both the statement and its negation are provable from the axioms.
In the standard system of firstorder logic, an inconsistent
set of axioms will prove every statement in its language (this is
sometimes called the principle of explosion), and is
thus automatically complete. A set of axioms that is both complete
and consistent, however, proves a maximal set of noncontradictory theorems. Gödel's
incompleteness theorems show that in certain cases it is not
possible to obtain an effectively generated, complete, consistent
theory.
First incompleteness
theorem
Gödel's first incompleteness theorem states
that:
 Any effectively generated theory capable of expressing
elementary arithmetic cannot be both consistent and complete. In
particular, for any consistent,
effectively generated formal theory that proves certain
basic arithmetic truths, there is an arithmetical statement that is
true,^{[1]} but not
provable in the theory (Kleene 1967, p. 250).
The true but unprovable statement referred to by the theorem is
often referred to as “the Gödel sentence” for the theory. It is not
unique; there are infinitely many statements in the language of the
theory that share the property of being true but unprovable.^{[2]}
For each consistent formal theory T having the required
small amount of number theory, the corresponding Gödel sentence
G asserts: “G cannot be proved to be true within
the theory T”. If G were provable under the
axioms and rules of inference of T, then T would
have a theorem, G, which effectively contradicts itself,
and thus the theory T would be inconsistent. This means
that if the theory T is consistent then G cannot
be proved within it. This means that G's claim about its
own unprovability is correct; in this sense G is not only
unprovable but true. Thus provabilitywithinthetheoryT
is not the same as truth; the theory T is incomplete.
If G is true: G cannot be proved within the
theory, and the theory is incomplete. If G is false: then
G can be proved within the theory and then the theory is
inconsistent, since G is both provable and refutable from
T.
Each theory has its own Gödel statement. It is possible to
define a larger theory T’ that contains the whole of
T, plus G as an additional axiom. This will not
result in a complete theory, because Gödel's theorem will also
apply to T’, and thus T’ cannot be complete. In
this case, G is indeed a theorem in T’, because
it is an axiom. Since G states only that it is not
provable in T, no contradiction is presented by its
provability in T’. However, because the incompleteness
theorem applies to T’: there will be a new Gödel statement
G’ for T’, showing that T’ is also
incomplete. G’ will differ from G in that
G’ will refer to T’, rather than T.
To prove the first incompleteness theorem, Gödel represented
statements by numbers. Then the theory at hand, which is assumed to
prove certain facts about numbers, also proves facts about its own
statements. Questions about the provability of statements are
represented as questions about the properties of numbers, which
would be decidable by the theory if it were complete. In these
terms, the Gödel sentence states that no natural number exists with
a certain, strange property. A number with this property would
encode a proof of the inconsistency of
the theory. If there were such a number then the theory would be
inconsistent, contrary to the consistency hypothesis. So, under the
assumption that the theory is consistent, there is no such
number.
Meaning of the
first incompleteness theorem
Gödel's first incompleteness theorem shows that any consistent
formal system that includes enough of the theory of the natural
numbers is incomplete; there are true statements expressible in its
language that are unprovable. Thus no formal system (satisfying the
hypotheses of the theorem) that aims to characterize the natural
numbers can actually do so, as there will be true
numbertheoretical statements which that system cannot prove. This
fact is sometimes thought to have severe consequences for the
program of logicism
proposed by Gottlob
Frege and Bertrand Russell, which aimed to
define the natural numbers in terms of logic (Hellman 1981,
p. 451–468). Some (like Bob Hale and Crispin Wright)
believe that it is not a problem for logicism because the
incompleteness theorems apply equally to second order logic as they
do to arithmetic. It is only those who believe that the natural
numbers are to be defined in terms of first order logic  which is
consistent and complete  who have this problem.
The existence of an incomplete formal system is in itself not
particularly surprising. A system may be incomplete simply because
not all the necessary axioms have been discovered. For example, Euclidean
geometry without the parallel postulate is incomplete; it
is not possible to prove or disprove the parallel postulate from
the remaining axioms.
Gödel's theorem shows that, in theories that include a small
portion of number
theory, a complete and consistent finite list of axioms can
never be created, nor even an infinite list that can be
enumerated by a computer program. Each time a new statement is
added as an axiom, there are other true statements that still
cannot be proved, even with the new axiom. If an axiom is ever
added that makes the system complete, it does so at the cost of
making the system inconsistent.
It is possible to have a complete and consistent list
of axioms that cannot be enumerated by a computer program.
For example, one might take all true statements about the natural
numbers to be axioms (and no false statements). But then there is
no mechanical way to decide, given a statement about the natural
numbers, whether it is an axiom or not, and thus no effective way
to verify a formal proof in this theory.
Many logicians believe that Gödel's incompleteness theorems
struck a fatal blow to David Hilbert's second problem, which asked
for a finitary consistency proof for mathematics. The second
incompleteness theorem, in particular, is often viewed as making
the problem impossible. Not all mathematicians agree with this
analysis, however, and the status of Hilbert's second problem is
not yet decided (see "Modern viewpoints on the status of
the problem").
Relation to the liar
paradox
The liar
paradox is the sentence "This sentence is false." An analysis
of the liar sentence shows that it cannot be true (for then, as it
asserts, it is false), nor can it be false (for then, it is true).
A Gödel sentence G for a theory T makes a similar
assertion to the liar sentence, but with truth replaced by
provability: G says "G is not provable in the
theory T." The analysis of the truth and provability of
G is a formalized version of the analysis of the truth of
the liar sentence.
It is not possible to replace "not provable" with "false" in a
Gödel sentence because the predicate "Q is the Gödel number of a false formula" cannot be
represented as a formula of arithmetic. This result, known as Tarski's undefinability
theorem, was discovered independently by Gödel (when he was
working on the proof of the incompleteness theorem) and by Alfred Tarski.
Original
statement
The first incompleteness theorem first appeared as "Theorem VI"
in his 1931 paper On Formally Undecidable Propositions in
Principia Mathematica and Related Systems I. In Gödel's
original notation, it states:
 "The general result about the existence of undecidable
propositions reads as follows:
 "Theorem VI. For every ωconsistent recursive class κ
of FORMULAS there are recursive CLASS SIGNS r,
such that neither v Gen r nor Neg(v Gen
r) belongs to Flg(κ) (where v is the
FREE VARIABLE of r).^{[3]}(van
Heijenoort 1967:607.)
Extensions of
Gödel's original result
Gödel demonstrated the incompleteness of the theory of Principia Mathematica, a
particular theory of arithmetic, but a parallel demonstration could
be given for any effective theory of a certain expressiveness.
Gödel commented on this fact in the introduction to his paper, but
restricted the proof to one system for concreteness. In modern
statements of the theorem, it is common to state the effectiveness
and expressiveness conditions as hypotheses for the incompleteness
theorem, so that it is not limited to any particular formal theory.
The terminology used to state these conditions was not yet
developed in 1931 when Gödel published his results.
Gödel's original statement and proof of the incompleteness
theorem requires the assumption that the theory is not just
consistent but ωconsistent.
A theory is ωconsistent if it is not
ωinconsistent, and is ωinconsistent if there is a predicate
P such that for every specific natural number n
the theory proves ~P(n), and yet the theory also
proves that there exists a natural number n such that
P(n). That is, the theory says that a number with
property P exists while denying that it has any specific
value. The ωconsistency of a theory implies its consistency, but
consistency does not imply ωconsistency. J. Barkley
Rosser (1936) strengthened the incompleteness theorem by
finding a variation of the proof (Rosser's trick) that only requires the
theory to be consistent, rather than ωconsistent. This is mostly
of technical interest, since all true formal theories of arithmetic
(theories whose axioms are all true statements about natural
numbers) are ωconsistent, and thus Gödel's theorem as originally
stated applies to them. The stronger version of the incompleteness
theorem that only assumes consistency, rather than ωconsistency,
is now commonly known as Gödel's incompleteness theorem and as the
Gödel–Rosser theorem.
Second incompleteness
theorem
Gödel's second incompleteness theorem can be stated as
follows:
 For any formal effectively generated theory T
including basic arithmetical truths and also certain truths
about formal provability, T includes a statement of its
own consistency if and only if T is
inconsistent.
This strengthens the first incompleteness theorem, because the
statement constructed in the first incompleteness theorem does not
directly express the consistency of the theory. The proof of the
second incompleteness theorem is obtained, essentially, by
formalizing the proof of the first incompleteness theorem within
the theory itself.
A technical subtlety in the second incompleteness theorem is how
to express the consistency of T as a formula in the
language of T. There are many ways to do this, and not all
of them lead to the same result. In particular, different
formalizations of the claim that T is consistent may be
inequivalent in T, and some may even be provable. For
example, firstorder Peano arithmetic (PA) can prove that the
largest consistent subset of
PA is consistent. But since PA is consistent, the largest
consistent subset of PA is just PA, so in this sense PA "proves
that it is consistent". What PA does not prove is that the largest
consistent subset of PA is, in fact, the whole of PA. (The term
"largest consistent subset of PA" is rather vague, but what is
meant here is the largest consistent initial segment of the axioms
of PA ordered according to some criteria; for example, by "Gödel
numbers", the numbers encoding the axioms as per the scheme used by
Gödel mentioned above).
In the case of Peano arithmetic, or any familiar explicitly
axiomatized theory T, it is possible to canonically define
a formula Con(T) expressing the consistency of T;
this formula expresses the property that "there does not exist a
natural number coding a sequence of formulas, such that each
formula is either one of the axioms of T, a logical axiom,
or an immediate consequence of preceding formulas according to the
rules of inference of firstorder logic, and such that the last
formula is a contradiction".
The formalization of Con(T) depends on two factors:
formalizing the notion of a sentence being derivable from a set of
sentences and formalizing the notion of being an axiom of
T. Formalizing derivability can be done in canonical
fashion: given an arithmetical formula A(x) defining a set
of axioms, one can canonically form a predicate
Prov_{A}(P) which expresses that P is
provable from the set of axioms defined by A(x). In
addition, Prov_{A}(P) must satisfy the socalled
Hilbert–Bernays provability
conditions:
 If T proves P, then T proves
Prov_{A}(P).
 T proves 1.; that is, T proves that if
T proves P, then T proves
Prov_{A}(P).
 T proves that if T proves that (P →
Q) then T proves that provability of P
implies provability of Q.
Solomon
Feferman showed that Gödel's second incompleteness theorem goes
through when the formula A(x) is chosen so that it has the
form "there exists a number n satisfying the decidable
predicate P" for some P.
Implications for
consistency proofs
Gödel's second incompleteness theorem also implies that a theory
T_{1} satisfying the technical conditions outlined
above cannot prove the consistency of any theory
T_{2} which proves the consistency of
T_{1}. This is because such a theory
T_{1} can prove that if T_{2}
proves the consistency of T_{1}, then
T_{1} is in fact consistent. For the claim that
T_{1} is consistent has form "for all numbers
n, n has the decidable property of not being a
code for a proof of contradiction in T_{1}". If
T_{1} were in fact inconsistent, then
T_{2} would prove for some n that
n is the code of a contradiction in
T_{1}. But if T_{2} also proved
that T_{1} is consistent (that is, that there is
no such n), then it would itself be inconsistent. This reasoning
can be formalized in T_{1} to show that if
T_{2} is consistent, then T_{1}
is consistent. Since, by second incompleteness theorem,
T_{1} does not prove its consistency, it cannot
prove the consistency of T_{2} either.
This corollary of the second incompleteness theorem shows that
there is no hope of proving, for example, the consistency of Peano
arithmetic using any finitistic means that can be formalized in a
theory the consistency of which is provable in Peano arithmetic.
For example, the theory of primitive recursive
arithmetic (PRA), which is widely accepted as an accurate
formalization of finitistic mathematics, is provably consistent in
PA. Thus PRA cannot prove the consistency of PA. This fact is
generally seen to imply that Hilbert's program, which aimed to
justify the use of "ideal" (infinitistic) mathematical principles
in the proofs of "real" (finitistic) mathematical statements by
giving a finitistic proof that the ideal principles are consistent,
cannot be carried out.
The corollary also indicates the epistemological relevance of
the second incompleteness theorem. As Georg Kreisel remarked, it
would actually provide no interesting information if a theory
T proved its consistency. This is because inconsistent
theories prove everything, including their consistency. Thus a
consistency proof of T in T would give us no clue
as to whether T really is consistent; no doubts about the
consistency of T would be resolved by such a consistency
proof. The interest in consistency proofs lies in the possibility
of proving the consistency of a theory T in some theory
T’ which is in some sense less doubtful than T
itself, for example weaker than T. For many naturally
occurring theories T and T’, such as T =
Zermelo–Fraenkel set theory
and T’ = primitive recursive arithmetic, the consistency
of T’ is provable in T, and thus T’
can't prove the consistency of T by the above corollary of
the second incompleteness theorem.
The second incompleteness theorem does not rule out consistency
proofs altogether, only consistency proofs that could be formalized
in the theory that is proved consistent. For example, Gerhard Gentzen
proved the consistency of Peano arithmetic (PA) using the
assumption that a certain ordinal called ε_{0} is actually wellfounded; see Gentzen's consistency
proof. Gentzen's theorem spurred the development of ordinal
analysis in proof theory.
Original
statement of Gödel’s Theorem XI
While contemporary usage calls it the “Second incompleteness
Theorem”, in the original Gödel presented it as his “Theorem XI”.
It is stated thus (in the following, “Section 2” is where his
Theorem VI appears, and P is Gödel’s abbreviation for the
system obtained by adding the Peano axioms to the logical system of
Principia Mathematica.
 ”The results of Section 2 have a surprising consequence
concerning a consistency proof for the system P (and its
extensions), which can be stated as follows:
 ”Theorem XI. Let κ be any recursive consistent^{63}
class of FORMULAS; then the SENTENTIAL FORMULA
stating that κ is consistent is not κPROVABLE; in
particular, the consistency of P is not provable in
P,^{64} provided P is consistent (in the
opposite case, of course, every proposition is provable [in P])".
(Brackets in original added by Gödel “to help the reader”,
translation and typography in van Heijenoort 1967:614)
 ”^{63} “κ is consistent” (abbreviated by “Wid(κ)”) is
defined as thus: Wid(κ)≡ (Ex)(Form(x) &
~Bew_{κ}(x))."

 (Note: In the original "Bew" has a negation“bar” written over
it, indicated here by ~. “Wid” abbreviates “Widerspruchfreiheit =
consistency”, “Form” abbreviates “Formel = formula”, “Bew”
abbreviates “Beweisbar = provable” (translations from Meltzer and
Braithwaite 1962, 1996 edition:3334) )
 ”^{64} This follows if we substitute the empty class of
FORMULAS for κ.”
Examples of undecidable
statements
 See also: List of statements
undecidable in ZFC
There are two distinct senses of the word "undecidable" in
mathematics and computer science. The first of these is the prooftheoretic sense
used in relation to Gödel's theorems, that of a statement being
neither provable nor refutable in a specified deductive
system. The second sense, which will not be discussed here, is
used in relation to computability theory and applies
not to statements but to decision problems, which are countably
infinite sets of questions each requiring a yes or no answer. Such
a problem is said to be undecidable if there is no computable
function that correctly answers every question in the problem
set (see undecidable problem).
Because of the two meanings of the word undecidable, the term independent is
sometimes used instead of undecidable for the "neither provable nor
refutable" sense. The usage of "independent" is also ambiguous,
however. Some use it to mean just "not provable", leaving open
whether an independent statement might be refuted.
Undecidability of a statement in a particular deductive system
does not, in and of itself, address the question of whether the truth value of the
statement is welldefined, or whether it can be determined by other
means. Undecidability only implies that the particular deductive
system being considered does not prove the truth or falsity of the
statement. Whether there exist socalled "absolutely undecidable"
statements, whose truth value can never be known or is
illspecified, is a controversial point in the philosophy of
mathematics.
The combined work of Gödel and Paul Cohen has given two
concrete examples of undecidable statements (in the first sense of
the term): The continuum hypothesis can neither
be proved nor refuted in ZFC (the standard axiomatization of set theory), and the axiom of choice
can neither be proved nor refuted in ZF
(which is all the ZFC axioms except the axiom of choice).
These results do not require the incompleteness theorem. Gödel
proved in 1940 that neither of these statements could be disproved
in ZF or ZFC set theory. In the 1960s, Cohen proved that neither is
provable from ZF, and the continuum hypothesis cannot be proven
from ZFC.
In 1973, the Whitehead problem in group theory was
shown to be undecidable, in the first sense of the term, in
standard set theory.
In 1977, Paris and Harrington proved that the ParisHarrington principle, a version of
the Ramsey theorem, is undecidable in the
firstorder axiomatization of arithmetic called Peano arithmetic, but can be proven to be
true in the larger system of secondorder arithmetic. Kirby
and Paris later showed Goodstein's theorem, a statement
about sequences of natural numbers somewhat simpler than the
ParisHarrington principle, to be undecidable in Peano
arithmetic.
Kruskal's tree theorem, which
has applications in computer science, is also undecidable from
Peano arithmetic but provable in set theory. In fact Kruskal's tree
theorem (or its finite form) is undecidable in a much stronger
system codifying the principles acceptable on the basis of a
philosophy of mathematics called predicativism. The related but more
general graph minor theorem (2003) has consequences
for computational complexity
theory.
Gregory
Chaitin produced undecidable statements in algorithmic information
theory and proved another incompleteness theorem in that
setting. Chaitin's theorem states that for any theory that can
represent enough arithmetic, there is an upper bound c
such that no specific number can be proven in that theory to have
Kolmogorov complexity greater
than c. While Gödel's theorem is related to the liar paradox,
Chaitin's result is related to Berry's
paradox.
Limitations of Gödel's
theorems
Gödel's theorems only apply to consistent theories. In
firstorder logic, because of the principle of explosion, an
inconsistent theory T proves every formula in its
language, including formulas that claim T is
consistent.
The conclusions of Gödel's theorems only hold for the formal
theories that satisfy the necessary hypotheses. Not all axiom
systems satisfy these hypotheses, even when these systems have
models that include the natural numbers as a subset. For example,
there are firstorder axiomatizations of Euclidean
geometry, of real closed
fields, and of arithmetic in which multiplication is not
provably total; none of these meet the hypotheses of
Gödel's theorems. The key fact is that these axiomatizations are
not expressive enough to define the set of natural numbers or
develop basic properties of the natural numbers. Regarding the
third example, Dan E. Willard has studied many weak systems of
arithmetic which do not satisfy the hypotheses of the second
incompleteness theorem (e.g. Willard 2001).
Gödel's theorems only apply to effectively generated (that is,
recursively enumerable) theories. If all true statements about
natural numbers are taken as axioms for a theory, then this theory
is a consistent, complete extension of Peano arithmetic for which
none of Gödel's theorems hold, because this theory is not
recursively enumerable.
The second incompleteness theorem only shows that the
consistency of certain theories cannot be proved from the axioms of
those theories themselves. It does not show that the consistency
cannot be proved from other (consistent) axioms. For example, the
consistency of the Peano arithmetic
can be proved in Zermelo–Frankel set theory (ZFC), or in
theories of arithmetic augmented with transfinite induction, as in Gentzen's consistency
proof.
Relationship with
computability
The incompleteness theorem is closely related to several results
about undecidable sets in recursion theory.
Stephen Cole Kleene (1943)
presented a proof of Gödel's incompleteness theorem using basic
results of computability theory. One such result shows that the halting problem
is unsolvable: there is no computer program that can correctly
determine, given a program P as input, whether P
eventually halts when run with no input. Kleene showed that the
existence of a complete effective theory of arithmetic with certain
consistency properties would force the halting problem to be
decidable, a contradiction. This method of proof has also been
presented by Shoenfield (1967, p. 132); Charlesworth (1980); and
Hopcroft and Ullman (1979).
Franzén (2005, p. 73) explains how Matiyasevich's solution to Hilbert's 10th problem can be used to
obtain a proof to Gödel's first incompleteness theorem.
Matiyasevich proved that there is no algorithm that, given a
multivariate polynomial p(x_{1},
x_{2},...,x_{k}) with integer coefficients,
determines whether there is an integer solution to the equation
p = 0. Because polynomials with integer coefficients, and
integers themselves, are directly expressible in the language of
arithmetic, if a multivariate integer polynomial equation
p = 0 does have a solution in the integers then any
sufficiently strong theory of arithmetic T will prove
this. Moreover, if the theory T is ωconsistent, then it
will never prove that some polynomial equation has a solution when
in fact there is no solution in the integers. Thus, if T
were complete and ωconsistent, it would be possible to
algorithmically determine whether a polynomial equation has a
solution by merely enumerating proofs of T until either
"p has a solution" or "p has no solution" is
found, in contradiction to Matiyasevich's theorem.
Smorynski (1977, p. 842) shows how the existence of
recursively inseparable sets can be used to prove the first
incompleteness theorem. This proof is often extended to show that
systems such as Peano arithmetic are essentially undecidable (see Kleene 1967,
p. 274).
Formalized
proofs
Formalized proofs of versions of the incompleteness theorem have
been developed by N. Shankar in 1986 using Nqthm (Shankar 1994) and by R. O'Connor in 2003
using Coq (O'Connor 2005).
Proof sketch for the first
theorem
Throughout the proof we assume a formal system is fixed and
satisfies the necessary hypotheses. The proof has three essential
parts. The first part is to show that statements can be represented
by natural numbers, known as Gödel numbers, and that properties of
the statements can be detected by examining their Gödel numbers.
This part culminates in the construction of a formula expressing
the idea that a statement is provable in the system. The second
part of the proof is to construct a particular statement that,
essentially, says that it is unprovable. The third part of the
proof is to analyze this statement to show that it is neither
provable nor disprovable in the system.
Arithmetization of
syntax
The main problem in fleshing out the proof described above is
that it seems at first that to construct a statement p
that is equivalent to "p cannot be proved", p
would have to somehow contain a reference to p, which
could easily give rise to an infinite regress. Gödel's ingenious
trick, which was later used by Alan Turing in his work on the Entscheidungsproblem, is to
represent statements as numbers, which is often called the
arithmetization of syntax. This allows a selfreferential formula
to be constructed in a way that avoids any infinite regress of
definitions.
To begin with, every formula or statement that can be formulated
in our system gets a unique number, called its Gödel number. This is done in such
a way that it is easy to mechanically convert back and forth
between formulas and Gödel numbers. It is similar, for example, to
the way English sentences are encoded as sequences (or "strings")
of numbers using ASCII: such a
sequence is considered as a single (if potentially very large)
number. Because our system is strong enough to reason about
numbers, it is now also possible to reason about
formulas within the system.
A formula F(x) that contains exactly one free
variable x is called a statement form or
classsign. As soon as x is replaced by a
specific number, the statement form turns into a bona
fide statement, and it is then either provable in the
system, or not. For certain formulas one can show that for every
natural number n, F(n) is true if and only if it can be proven (the
precise requirement in the original proof is weaker, but for the
proof sketch this will suffice). In particular, this is true for
every specific arithmetic operation between a finite number of
natural numbers, such as "2*3=6".
Statement forms themselves are not statements and therefore
cannot be proved or disproved. But every statement form
F(x) can be assigned with a Gödel number which we
will denote by G(F). The choice of the
free variable used in the form F(x) is not
relevant to the assignment of the Gödel number
G(F).
Now comes the trick: The notion of provability itself can also
be encoded by Gödel numbers, in the following way. Since a proof is
a list of statements which obey certain rules, we can define the
Gödel number of a proof. Now, for every statement p, we
may ask whether a number x is the Gödel number of its
proof. The relation between the Gödel number of p and
x, the Gödel number of its proof, is an arithmetical
relation between two numbers. Therefore there is a statement form
Bew(x) that uses this arithmetical relation to state that
a Gödel number of a proof of x exists:
 Bew(y) = ∃ x ( y is the Gödel number
of a formula and x is the Gödel number of a proof of the
formula encoded by y).
The name Bew is short for beweisbar,
the German word for "provable"; this name was originally used by
Gödel to denote the provability formula just described. Note that
"Bew(y)" is merely an abbreviation that represents a
particular, very long, formula in the original language of
T; the string "Bew" itself is not claimed to be part of
this language.
An important feature of the formula Bew(y) is that if a
statement p is provable in the system then
Bew(G(p)) is also provable. This is
because any proof of p would have a corresponding Gödel
number, the existence of which causes
Bew(G(p)) to be satisfied.
Diagonalization
The next step in the proof is to obtain a statement that says it
is unprovable. Although Gödel constructed this statement directly,
the existence of at least one such statement follows from the diagonal lemma,
which says that for any sufficiently strong formal system and any
statement form F there is a statement p such that
the system proves
 p ↔ F(G(p)).
We obtain p by letting F be the negation of
Bew(x); thus p roughly states that its own Gödel
number is the Gödel number of an unprovable formula.
The statement p is not literally equal to
~Bew(G(p)); rather, p states
that if a certain calculation is performed, the resulting Gödel
number will be that of an unprovable statement. But when this
calculation is performed, the resulting Gödel number turns out to
be the Gödel number of p itself. This is similar to the
following sentence in English:
 ", when preceded by itself in quotes, is unprovable.", when
preceded by itself in quotes, is unprovable.
This sentence does not directly refer to itself, but when the
stated transformation is made the original sentence is obtained as
a result, and thus this sentence asserts its own unprovability. The
proof of the diagonal lemma employs a similar method.
Proof of
independence
We will now assume that our axiomatic system is ωconsistent. We let p be the
statement obtained in the previous section.
If p were provable, then
Bew(G(p)) would be provable, as argued
above. But p asserts the negation of
Bew(G(p)). Thus our system would be
inconsistent, proving both a statement and its negation. This
contradiction shows that p cannot be provable.
If the negation of p were provable, then
Bew(G(p)) would be provable (because
p was constructed to be equivalent to the negation of
Bew(G(p))). However, for each specific
number x, x cannot be the Gödel number of the
proof of p, because p is not provable (from the
previous paragraph). Thus on one hand the system proves there is a
number with a certain property (that it is the Gödel number of the
proof of p), but on the other hand, for every specific
number x, we can prove that it does not have this
property. This is impossible in an ωconsistent system. Thus the
negation of p is not provable.
Thus the statement p is undecidable: it can neither be
proved nor disproved within the system.
It should be noted that p is not provable (and thus
true) in every consistent system. The assumption of ωconsistency
is only required for the negation of p to be not provable.
Thus:
 In an ωconsistent formal system, we may prove neither
p nor its negation, and so p is undecidable.
 In a consistent formal system we may either have the same
situation, or we may prove the negation of p; In the later
case, we have a statement ("not p") which is false but
provable.
Note that if one tries to "add the missing axioms" to avoid the
undecidability of the system, then one has to add either p
or "not p" as axioms. But then the definition of "being a
Gödel number of a proof" of a statement changes. which means that
the statement form Bew(x) is now different. Thus when we
apply the diagonal lemma to this new form Bew, we obtain a new
statement p, different from the previous one, which will
be undecidable in the new system if it is ωconsistent.
Proof via Berry's
paradox
George Boolos
(1989) sketches an alternative proof of the first incompleteness
theorem that uses Berry's paradox
rather than the liar
paradox to construct a true but unprovable formula. A similar
proof method was independently discovered by Saul Kripke (Boolos 1998, p. 383).
Boolos's proof proceeds by constructing, for any computably enumerable set S of
true sentences of arithmetic, another sentence which is true but
not contained in S. This gives the first incompleteness
theorem as a corollary. According to Boolos, this proof is
interesting because it provides a "different sort of reason" for
the incompleteness of effective, consistent theories of arithmetic
(Boolos 1998, p. 388).
Proof sketch for the
second theorem
The main difficulty in proving the second incompleteness theorem
is to show that various facts about provability used in the proof
of the first incompleteness theorem can be formalized within the
system using a formal predicate for provability. Once this is done,
the second incompleteness theorem essentially follows by
formalizing the entire proof of the first incompleteness theorem
within the system itself.
Let p stand for the undecidable sentence constructed
above, and assume that the consistency of the system can be proven
from within the system itself. We have seen above that if the
system is consistent, then p is not provable. The proof of
this implication can be formalized within the system, and therefore
the statement "p is not provable", or "not
P(p)" can be proven in the system.
But this last statement is equivalent to p itself (and
this equivalence can be proven in the system), so p can be
proven in the system. This contradiction shows that the system must
be inconsistent.
Discussion and
implications
The incompleteness results affect the philosophy of mathematics,
particularly versions of formalism, which use
a single system formal logic to define their principles. One can
paraphrase the first theorem as saying the following:
 We can never find an allencompassing axiomatic system
which is able to prove all mathematical truths, but no
falsehoods.
On the other hand, from a strict formalist perspective this
paraphrase would be considered meaningless because it presupposes
that mathematical "truth" and "falsehood" are welldefined in an
absolute sense, rather than relative to each formal system.
The following rephrasing of the second theorem is even more
unsettling to the foundations of
mathematics:
 If an axiomatic system can be proven to be consistent
and complete from within itself, then it is
inconsistent.
Therefore, to establish the consistency of a system S, one needs
to use some other more powerful system T, but a proof in T
is not completely convincing unless T's consistency has already
been established without using S.
At first, Gödel's theorems seemed to leave some hope—it was
thought that it might be possible to produce a general algorithm that indicates
whether a given statement is undecidable or not, thus allowing
mathematicians to bypass the undecidable statements altogether.
However, the negative answer to the Entscheidungsproblem, obtained in
1936, showed that no such algorithm exists.
There are some who hold that a statement that is unprovable
within a deductive system may be quite provable in a metalanguage.
And what cannot be proven in that metalanguage can likely
be proven in a metametalanguage, recursively, ad infinitum, in
principle. By invoking such a system of typed metalanguages, along
with an axiom of Reducibility — which by an inductive assumption
applies to the entire stack of languages — one may, for all
practical purposes, overcome the obstacle of incompleteness.
Note that Gödel's theorems only apply to sufficiently
strong axiomatic systems. "Sufficiently strong" means that the
theory contains enough arithmetic to carry out the coding
constructions needed for the proof of the first incompleteness
theorem. Essentially, all that is required are some basic facts
about addition and multiplication as formalized, for example, in Robinson arithmetic Q. There are even
weaker axiomatic systems that are consistent and complete, for
instance Presburger arithmetic which
proves every true firstorder statement involving only
addition.
The axiomatic system may consist of infinitely many axioms (as
firstorder Peano arithmetic does), but for Gödel's theorem to
apply, there has to be an effective algorithm which is able to
check proofs for correctness. For instance, one might take the set
of all firstorder sentences which are true in the standard model
of the natural numbers. This system is complete;
Gödel's theorem does not apply because there is no effective
procedure that decides if a given sentence is an axiom. In fact,
that this is so is a consequence of Gödel's first incompleteness
theorem.
Another example of a specification of a theory to which Gödel's
first theorem does not apply can be constructed as follows: order
all possible statements about natural numbers first by length and
then lexicographically, start with an axiomatic
system initially equal to the Peano axioms, go through your list of
statements one by one, and, if the current statement cannot be
proven nor disproven from the current axiom system, add it to that
system. This creates a system which is complete, consistent, and
sufficiently powerful, but not computably
enumerable.
Gödel himself only proved a technically slightly weaker version
of the above theorems; the first proof for the versions stated
above was given by J. Barkley Rosser in 1936.
In essence, the proof of the first theorem consists of
constructing a statement p within a formal axiomatic
system that can be given a metamathematical interpretation of:
 p = "This statement cannot be proven in the given
formal theory"
As such, it can be seen as a modern variant of the Liar paradox,
although unlike the classical paradoxes it's not really
paradoxical.
If the axiomatic system is consistent, Gödel's proof shows that
p (and its negation) cannot be proven in the system.
Therefore p is true (p claims to be not provable,
and it is not provable) yet it cannot be formally proved in the
system. If the axiomatic system is ωconsistent, then the negation
of p cannot be proven either, and so p is
undecidable. In a system which is not ωconsistent (but
consistent), either we have the same situation, or we have a false
statement which can be proven (namely, the negation of
p).
Adding p to the axioms of the system would not solve
the problem: there would be another Gödel sentence for the enlarged
theory. Theories such as Peano arithmetic, for which any computably
enumerable consistent extension is incomplete, are called
essentially incomplete.
Minds and
machines
Authors including J. R. Lucas have debated what,
if anything, Gödel's incompleteness theorems imply about human
intelligence. Much of the debate centers on whether the human mind
is equivalent to a Turing machine, or by the Church–Turing thesis, any finite
machine at all. If it is, and if the machine is consistent, then
Gödel's incompleteness theorems would apply to it.
Hilary Putnam
(1960) suggested that while Gödel's theorems cannot be applied to
humans, since they make mistakes and are therefore inconsistent, it
may be applied to the human faculty of science or mathematics in
general. If we are to assume that it is consistent, then either we
cannot prove its consistency, or it cannot be represented by a
Turing machine.
Appeals
to the incompleteness theorems in other fields
Appeals and analogies are sometimes made to the incompleteness
theorems in support of arguments that go beyond mathematics and
logic. A number of authors have commented negatively on such
extensions and interpretations, including Torkel
Franzén (2005); Alan
Sokal and Jean
Bricmont (1999); and Ophelia Benson and Jeremy
Stangroom (2006). Bricmont and Stangroom (2006, p. 10), for
example, quote from Rebecca Goldstein's comments on the
disparity between Gödel's avowed Platonism and the antirealist uses to
which his ideas are sometimes put. Sokal and Bricmont (1999, p.
187) criticize Régis Debray's invocation of the theorem
in the context of sociology; Debray has defended this use as
metaphorical (ibid.).
See also
Notes
 ^
The word "true" is used disquotationally
here: the Gödel sentence is true in this sense because it "asserts
its own unprovability and it is indeed unprovable" (Smoryński 1977
p. 825; also see Franzén 2005 pp. 28–33). It is also possible to
read "G_{T} is true" in the formal sense
that primitive recursive
arithmetic proves the implication
Con(T)→G_{T}, where
Con(T) is a canonical sentence asserting the consistency
of T (Smoryński 1977 p. 840, Kikuchi and Tanaka 1994 p.
403)
 ^
For example, the conjunction of the Gödel sentence and any logically valid sentence will have this
property.
 ^
Here Flg(κ) represents the theory generated by κ and
"v Gen r" is a particular formula in
the language of arithmetic. "Flg" is from "Folgerungsmenge = set of
consequences" and "Gen" is from "Generalisation = generalization"
(cf Meltzer and Braithwaite 1962, 1992 edition:3334).
References
Articles
by Gödel
 1931, Über formal unentscheidbare Sätze der Principia
Mathematica und verwandter Systeme, I. Monatshefte für
Mathematik und Physik 38: 17398.
 1951, Some basic theorems on the foundations of mathematics
and their implications in Solomon Feferman, ed., 1995.
Collected works / Kurt Gödel, Vol. III. Oxford University
Press: 30423.
Translations, during his lifetime, of Gödel’s paper into
English
None of the following agree in all translated words and in
typography. The typography is a serious matter, because Gödel
expressly wished to emphasize “those metamathematical notions that
had been defined in their usual sense before . . ."(van Heijenoort
1967:595). Three translations exist. Of the first John Dawson
states that: “The Meltzer translation was seriously deficient and
received a devastating review in the Journal of Symbolic
Logic; ”Gödel also complained about Braithwaite’s commentary
(Dawson 1997:216). “Fortunately, the Meltzer translation was soon
supplanted by a better one prepared by Elliott Mendelson for Martin
Davis’s anthology The Undecidable . . . he found the
translation “not quite so good” as he had expected . . . [but
because of time constraints he] agreed to its publication” (ibid).
(In a footnote Dawson states that “he would regret his compliance,
for the published volume was marred throughout by sloppy typography
and numerous misprints” (ibid)). Dawson states that “The
translation that Gödel favored was that by Jean van
Heijenoort”(ibid). For the serious student another version exists
as a set of lecture notes recorded by Stephen Kleene and J. B.
Rosser "during lectures given by Gödel at to the Institute for
Advanced Study during the spring of 1934" (cf commentary by Davis
1965:39 and beginning on p. 41); this version is titled "On
Undecidable Propositions of Formal Mathematical Systems". In their
order of publication:
 B. Meltzer (translation) and R. B. Braithwaite (Introduction),
1962. On Formally Undecidable Propositions of Principia
Mathematica and Related Systems, Dover Publications, New York
(Dover edition 1992), ISBN 0486669807 (pbk.) This contains a
useful translation of Gödel's German abbreviations on
pp. 33–34. As noted above, typography, translation and
commentary is suspect. Unfortunately, this translation was
reprinted with all its suspect content by

 Stephen
Hawking editor, 2005. God Created the Integers: The
Mathematical Breakthroughs That Changed History, Running
Press, Philadelphia, ISBN 0762419229. Gödel’s paper appears
starting on p. 1097, with Hawking’s commentary starting on p.
1089.
 Martin Davis
editor, 1965. The Undecidable: Basic Papers on Undecidable
Propositions, Unsolvable problems and Computable Functions,
Raven Press, New York, no ISBN. Gödel’s paper begins on page 5,
preceded by one page of commentary.
 Jean van Heijenoort editor, 1967, 3rd
edition 1967. From Frege to Gödel: A Source Book in
Mathematical Logic, 19791931, Harvard University Press,
Cambridge Mass., ISBN 0674324498 (pbk). van Heijenoort did the
translation. He states that “Professor Gödel approved the
translation, which in many places was accommodated to his
wishes.”(p. 595). Gödel’s paper begins on p. 595; van
Heijenoort’s commentary begins on p. 592.
 Martin Davis
editor, 1965, ibid. "On Undecidable Propositions of Formal
Mathematical Systems." A copy with Gödel's corrections of errata
and Gödel's added notes begins on page 41, preceded by two pages of
Davis's commentary. Until Davis included this in his volume this
lecture existed only as mimeographed notes.
Articles by
others
 George
Boolos, 1989, "A New Proof of the Gödel Incompleteness
Theorem", Notices of the American Mathematical Society v.
36, pp. 388–390 and p. 676, reprinted in in Boolos, 1998,
Logic, Logic, and Logic, Harvard Univ. Press. ISBN 0 674
53766 1
 Arthur Charlesworth, 1980, "A Proof of Godel's Theorem in Terms
of Computer Programs," Mathematics Magazine, v. 54 n. 3,
pp. 109–121. JStor
 Solomon
Feferman, 1984, Toward Useful TypeFree
Theories, I, Journal of Symbolic Logic,
v. 49 n. 1, pp. 75–111.
 Jean van Heijenoort, 1963. "Gödel's
Theorem" in Edwards, Paul, ed., Encyclopedia of Philosophy,
Vol. 3. Macmillan: 34857.
 Geoffrey
Hellman, How to Gödel a FregeRussell: Gödel's
Incompleteness Theorems and Logicism. Noûs, Vol. 15, No. 4,
Special Issue on Philosophy of Mathematics. (Nov., 1981),
pp. 451–468.
 David
Hilbert, 1900, "Mathematical Problems."
English translation of a lecture delivered before the International
Congress of Mathematicians at Paris, containing Hilbert's statement
of his Second Problem.
 Kikuchi,
Makoto; Tanaka, Kazuyuki (1994), "On formalization of
modeltheoretic proofs of Gödel's theorems", Notre Dame Journal
of Formal Logic 35 (3): 403–412, doi:10.1305/ndjfl/1040511346, MR1326122, ISSN 00294527
 Stephen Cole Kleene, 1943,
"Recursive predicates and quantifiers," reprinted from
Transactions of the American Mathematical Society, v. 53
n. 1, pp. 41–73 in Martin Davis 1965, The
Undecidable (loc. cit.) pp. 255–287.
 Hilary
Putnam, 1960, Minds and Machines in Sidney Hook, ed.,
Dimensions of Mind: A Symposium. New York University
Press. Reprinted in Anderson, A. R., ed., 1964. Minds and
Machines. PrenticeHall: 77.
 Russell O'Connor (2005), "Essential Incompleteness of Arithmetic Verified by
Coq", Lecture Notes in Computer Science,
3603, pp. 245260, http://arxiv.org/abs/cs/0505034
 John Barkley Rosser, 1936, "Extensions of
some theorems of Gödel and Church," reprinted from the Journal
of Symbolic Logic vol. 1 (1936) pp. 87–91, in Martin Davis 1965,
The Undecidable (loc. cit.) pp. 230–235.
 John Barkley Rosser, 1939, "An Informal
Exposition of proofs of Gödel's Theorem and Church's Theorem",
Reprinted from the Journal of Symbolic Logic, vol. 4
(1939) pp. 53–60, in Martin Davis 1965, The
Undecidable (loc. cit.) pp. 223–230
 C. Smoryński, "The incompleteness theorems", in J. Barwise,
ed., Handbook of Mathematical Logic, NorthHolland 1982
ISBN 9780444863881, pp. 821–866.
 Dan E. Willard (2001), "SelfVerifying Axiom Systems,
the Incompleteness Theorem and Related Reflection Principles",
Journal of Symbolic Logic, v. 66 n. 2, pp. 536–596.
doi:10.2307/2695030
 Richard Zach, 2005, "Paper on the incompleteness theorems" in
GrattanGuinness, I., ed.,
Landmark Writings in Western Mathematics. Elsevier:
91725.
Books
about the theorems
 Domeisen, Norbert, 1990. Logik der Antinomien. Bern:
Peter Lang. 142 S. 1990. ISBN 3261042141. Zentralblatt MATH
 Torkel
Franzén, 2005. Gödel's Theorem: An Incomplete Guide to its
Use and Abuse. A.K. Peters. ISBN 1568812388 MR2007d:03001
 Douglas Hofstadter, 1979. Gödel,
Escher, Bach: An Eternal Golden Braid. Vintage Books. ISBN
0465026850. 1999 reprint: ISBN 0465026567. MR80j:03009
 Douglas Hofstadter, 2007. I Am a
Strange Loop. Basic Books. ISBN 9780465030781. ISBN
0465030785. MR2008g:00004
 Stanley Jaki,
OSB, 2005. The drama of the quantities. Real View Books.
 J.R. Lucas, FBA, 1970. The Freedom of
the Will. Clarendon Press, Oxford, 1970.
 Ernest Nagel,
James Roy Newman, Douglas Hofstadter, 2002 (1958).
Gödel's Proof, revised ed. ISBN 0814758169. MR2002i:03001
 Rudy Rucker,
1995 (1982). Infinity and the Mind: The Science and Philosophy
of the Infinite. Princeton Univ. Press. MR84d:03012
 Smith, Peter, 2007. An Introduction to Gödel's
Theorems. Cambridge University Press. MathSciNet
 N. Shankar, 1994. Metamathematics, Machines and Gödel's
Proof, Volume 38 of Cambridge tracts in theoretical computer
science. ISBN 0521585333
 Raymond
Smullyan, 1991. Godel's Incompleteness Theorems.
Oxford Univ. Press.
 —, 1994. Diagonalization and SelfReference. Oxford
Univ. Press. MR96c:03001
 Hao
Wang, 1997. A Logical Journey: From Gödel to
Philosophy. MIT Press. ISBN 0262231891 MR97m:01090
Miscellaneous references
 John W.
Dawson, Jr., 1997. Logical Dilemmas: The Life and Work of
Kurt Gödel, A.K. Peters, Wellesley Mass, ISBN
1568812566.
 Goldstein, Rebecca, 2005,
Incompleteness: the Proof and Paradox of Kurt Gödel, W. W.
Norton & Company. ISBN 0393051692
 John Hopcroft and Jeffrey Ullman 1979, Introduction to
Automata theory, AddisonWesley, ISBN 020102988X
 Stephen Cole Kleene, 1967,
Mathematical Logic. Reprinted by Dover, 2002. ISBN
0486425339
 Alan Sokal and Jean Bricmont,
1999, Fashionable Nonsense: Postmodern Intellectuals' Abuse of
Science, Picador. ISBN 0312204078
 Joseph R. Shoenfield (1967), Mathematical Logic.
Reprinted by A.K. Peters for the Association of Symbolic Logic,
2001. ISBN 9781568811352
 Jeremy
Stangroom and Ophelia Benson, Why Truth
Matters, Continuum. ISBN 0826495281
External
links
Computable knowledge 

Topics and
Concepts 


Proposals and
Implementations 
Zairja • Ars Magna ( Ramon Llull, 1300) •
An Essay towards a Real Character and a Philosophical
Language ( John Wilkins, 1688) • Calculus ratiocinator & Characteristica universalis
( Gottfried
Leibniz, 1700) • Dewey Decimal
Classification ( Melvil Dewey, 1876) • Begriffsschrift
( Gottlob Frege,
1879) • Mundaneum ( Paul Otlet & Henri La
Fontaine, 1910) • Logical atomism ( Bertrand
Russell, 1918) • Tractatus
LogicoPhilosophicus ( Ludwig Wittgenstein, 1921) • Hilbert's
program ( David
Hilbert, 1920s) • Incompleteness
theorem ( Kurt Gödel, 1931) • Memex ( Vannevar Bush, 1945) • Cyc (1984) • True Knowledge (2007) • Wolfram Alpha ( Stephen
Wolfram, 2009)


In fiction 

