Gödel's incompleteness theorems
Encyclopedia
Gödel's incompleteness theorems are two theorem
s of mathematical logic
that establish inherent limitations of all but the most trivial axiomatic system
s capable of doing arithmetic
. The theorems, proven by Kurt Gödel
in 1931, are important both in mathematical logic and in the philosophy of mathematics
. The two results are widely, but not universally, interpreted as showing that Hilbert's program
to find a complete and consistent set of axiom
s for all of mathematics
is impossible, giving a negative answer to Hilbert's second problem
.
The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "effective procedure" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the natural numbers (arithmetic
). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, a corollary
of the first, shows that such a system cannot demonstrate its own consistency.
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 process 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 existence of a program that enumerates all the theorems of the theory without enumerating any statements that are not theorems. Examples of effectively generated theories with infinite sets of axioms include Peano arithmetic and Zermelo–Fraenkel set theory
.
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 such that both the statement and its negation are provable from the axioms. In the standard system of first-order 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 non-contradictory
theorems. Gödel's incompleteness theorems show that in certain cases it is not possible to obtain an effectively generated, complete, consistent theory.
This is proved by constructing a true but unprovable sentence G for each theory T, called “the Gödel sentence” for the theory. If just one of those can be built, it follows that infinitely many true-but-unprovable sentences can be built too. For example, the conjunction of G and any logically valid sentence will have the same property.
The Gödel sentence G is an equation that, formally speaking, asserts some equality between some sums and products of natural numbers, but that can also be informally interpreted as "this G cannot be formally derived under the axioms and rules of inference of T ". This interpretation of G leads to the following informal analysis. If G were provable under the axioms and rules of inference of T, then G would be false but derivable, and thus the theory T would be inconsistent. So, if the axioms and rules of derivation have been chosen so that only truths can be derived, it follows that G is true but cannot be derived. Therefore, we have been able to prove the truth of G by reasoning outside the system, but there is no hope we can ever prove the truth of G using a formal derivation inside the system. It follows that there are an infinite number of sentences such as G that are actually true but cannot be formally derived - in other words, T is incomplete. The claim G makes about its own underivability is correct, so provability-within-the-theory-T is not the same as truth. This informal analysis can be formalized to make a rigorous proof of the incompleteness theorem, as described in the section "Proof sketch for the first theorem" below.
Each effectively generated 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, provided that it is effectively generated. 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.
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
) argue that it is not a problem for logicism because the incompleteness theorems apply equally to second order logic as they do to arithmetic. They argue that only those who believe that the natural numbers are to be defined in terms of first order logic 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.
There are complete and consistent list of axioms for arithmetic 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), which gives the theory known as "true arithmetic
". The difficulty is that there is no mechanical way to decide, given a statement about the natural numbers, whether it is an axiom of this theory, and thus there is 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").
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
.
, 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.
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, first-order 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 technically ambiguous, 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 first-order 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 ProvA(P) which expresses that P is provable from the set of axioms defined by A(x).
In addition, the standard proof of the second incompleteness theorem assumes that ProvA(P) satisfies that Hilbert–Bernays provability conditions
. Letting #(P) represent the Gödel number of a formula P, the derivability conditions say:
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. 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) in a different theory which includes an axiom asserting that the ordinal
called ε0 is wellfounded; see Gentzen's consistency proof
. Gentzen's theorem spurred the development of ordinal analysis
in proof theory.
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 problem
s, 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 well-defined, 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 so-called "absolutely undecidable" statements, whose truth value can never be known or is ill-specified, 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 Paris-Harrington principle, a version of the Ramsey theorem, is undecidable in the first-order axiomatization of arithmetic called Peano arithmetic, but can be proven in the larger system of second-order arithmetic
. Kirby and Paris later showed Goodstein's theorem
, a statement about sequences of natural numbers somewhat simpler than the Paris-Harrington 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.
, 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 (Willard 2001) has studied many weak systems of arithmetic which do not satisfy the hypotheses of the second incompleteness theorem, and which are consistent and capable of proving their own consistency (see self-verifying theories
).
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 (called true 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–Fraenkel set theory
(ZFC), or in theories of arithmetic augmented with transfinite induction
, as in Gentzen's consistency proof
.
.
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 some given 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(x1, x2,...,xk) 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).
Chaitin's incompleteness theorem gives a different method of producing independent sentences, based on Kolmogorov complexity
. Like the proof presented by Kleene that was mentioned above, Chaitin's theorem only applies to theories with the additional property that all their axioms are true in the standard model of the natural numbers. Gödel's incompleteness theorem is distinguished by its applicability to consistent theories that nonetheless include statements that are false in the standard model; these theories are known as ω-inconsistent.
) in such a way that "proving a statement" can be replaced with "testing whether a number has a given property". This allows a self-referential formula to be constructed in a way that avoids any infinite regress of definitions. The same technique was later used by Alan Turing
in his work on the Entscheidungsproblem
.
In simple terms, a method can be devised so that every formula or statement that can be formulated in the system gets a unique number, called its Gödel number
, in such a way that it is possible to mechanically convert back and forth between formulas and Gödel numbers. The numbers involved might be very long indeed (in terms of number of digits), but this is not a barrier; all that matters is that such numbers can be constructed. A simple example is the way in which English is stored as a sequence of numbers in computers using ASCII
or Unicode
:
In principle, proving a statement true or false can be shown to be equivalent to proving that the number matching the statement does or doesn't have a given property. Because the formal system is strong enough to support reasoning about numbers in general, it can support reasoning about numbers which represent formulae and statements as well. Crucially, because the system can support reasoning about properties of numbers, the results are equivalent to reasoning about provability of their equivalent statements.
A formula F(x) that contains exactly one free variable x is called a statement form or class-sign. 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 a Gödel number denoted 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, the Gödel number of a proof can be defined. Now, for every statement p, one 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 potential Gödel number of its proof, is an arithmetical relation between two numbers. Therefore there is a statement form Bew(y) that uses this arithmetical relation to state that a Gödel number of a proof of y exists:
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.
, which says that for any sufficiently strong formal system and any statement form F there is a statement p such that the system proves
By letting F be the negation of Bew(x), p is obtained: 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:
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.
If p were provable, then Bew(G(p)) would be provable, as argued above. But p asserts the negation of Bew(G(p)). Thus the 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 supports construction of 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, it can be proved that the number 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 chosen system. So the chosen system is either inconsistent or incomplete. This logic can be applied to any formal system meeting the criteria. The conclusion is that all formal systems meeting the criteria are either inconsistent or incomplete. 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. So:
Note that if one tries to fix this by "adding the missing axioms" to avoid the undecidability of the system, then one has to add either p or "not p" as axioms. But this then creates a new formal system2 (old system + p), to which exactly the same process can be applied, creating a new statement form Bew2(x) for this new system. When the diagonal lemma is applied to this new form Bew2, a new statement p2 is obtained; this statement will be different from the previous one, and this new statement will be undecidable in the new system if it is ω-consistent, thus showing that system2 is equally inconsistent. So adding extra axioms cannot fix the problem.
(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).
in 1986 using Nqthm
(Shankar 1994) and by R. O'Connor in 2003 using Coq
(O'Connor 2005).
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. The demonstration above shows 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.
, 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:
On the other hand, from a strict formalist perspective this paraphrase would be considered meaningless because it presupposes that mathematical "truth" and "falsehood" are well-defined 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
:
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.
Theories such as Peano arithmetic, for which any computably enumerable consistent extension is incomplete, are called essentially undecidable or essentially incomplete.
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. Assuming that it is consistent, either its consistency cannot be proved or it cannot be represented by a Turing machine.
Avi Wigderson
(2010) has proposed that the concept of mathematical "knowability" should be based on computational complexity
rather than logical decidability. He writes that "when knowability is interpreted by modern standards, namely via computational complexity, the Gödel phenomena are very much with us."
and of inherently contradictory statements (dialetheia). Graham Priest
(1984, 2006) argues that replacing the notion of formal proof in Gödel's theorem with the usual notion of informal proof can be used to show that naive mathematics is inconsistent, and uses this as evidence for dialetheism
. The cause of this inconsistency is the inclusion of a truth predicate for a theory within the language of the theory (Priest 2006:47). Stewart Shapiro
(2002) gives a more mixed appraisal of the applications of Gödel's theorems to dialetheism. Carl Hewitt
(2008) has proposed that (inconsistent) paraconsistent logics that prove their own Gödel sentences may have applications in software engineering
.
(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 anti-realist 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.).
(2005, p. 46) observes:
He then proposes the proofs based on Computability
, or on information theory
, as described earlier in this article, as examples of proofs that should "counteract such impressions".
. His original goal was to obtain a positive solution to Hilbert's second problem
(Dawson 1997, p. 63). At the time, theories of the natural numbers and real numbers similar to second-order arithmetic
were known as "analysis", while theories of the natural numbers alone were known as "arithmetic".
Gödel was not the only person working on the consistency problem. Ackermann had published a flawed consistency proof for analysis in 1925, in which he attempted to use the method of ε-substitution originally developed by Hilbert. Later that year, von Neumann was able to correct the proof for a theory of arithmetic without any axioms of induction. By 1928, Ackermann had communicated a modified proof to Bernays; this modified proof led Hilbert to announce his belief in 1929 that the consistency of arithmetic had been demonstrated and that a consistency proof of analysis would likely soon follow. After the publication of the incompleteness theorems showed that Ackermann's modified proof must be erroneous, von Neumann produced a concrete example showing that its main technique was unsound (Zach 2006, p. 418, Zach 2003, p. 33).
In the course of his research, Gödel discovered that although a sentence which asserts its own falsehood leads to paradox, a sentence that asserts its own non-provability does not. In particular, Gödel was aware of the result now called Tarski's indefinability theorem
, although he never published it. Gödel announced his first incompleteness theorem to Carnap, Feigel and Waismann on August 26, 1930; all four would attend a key conference in Königsberg the following week.
This speech quickly became known as a summary of Hilbert's beliefs on mathematics (its final six words, "Wir müssen wissen. Wir werden wissen!", were used as Hilbert's epitaph in 1943). Although Gödel was likely in attendance for Hilbert's address, the two never met face to face (Dawson 1996, p. 72).
Gödel announced his first incompleteness theorem at a roundtable discussion session on the third day of the conference. The announcement drew little attention apart from that of von Neumann, who pulled Gödel aside for conversation. Later that year, working independently with knowledge of the first incompleteness theorem, von Neumann obtained a proof of the second incompleteness theorem, which he announced to Gödel in a letter dated November 20, 1930 (Dawson 1996, p. 70). Gödel had independently obtained the second incompleteness theorem and included it in his submitted manuscript, which was received by Monatshefte für Mathematik on November 17, 1930.
Gödel's paper was published in the Monatshefte in 1931 under the title Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I (On Formally Undecidable Propositions in Principia Mathematica and Related Systems I). As the title implies, Gödel originally planned to publish a second part of the paper; it was never written.
Gentzen published his consistency proof
for first-order arithmetic in 1936. Hilbert accepted this proof as "finitary" although (as Gödel's theorem had already shown) it cannot be formalized within the system of arithmetic that is being proved consistent.
The impact of the incompleteness theorems on Hilbert's program was quickly realized. Bernays included a full proof of the incompleteness theorems in the second volume of Grundlagen der Mathematik (1939), along with additional results of Ackermann on the ε-substitution method and Gentzen's consistency proof of arithmetic. This was the first full published proof of the second incompleteness theorem.
wrote Gödel to announce what he described as an "essential gap" in Gödel’s argument (Dawson:76). In October, Gödel replied with a 10-page letter (Dawson:76, Grattan-Guinness:512-513). But Zermelo did not relent and published his criticisms in print with “a rather scathing paragraph on his young competitor” (Grattan-Guinness:513). Gödel decided that to pursue the matter further was pointless, and Carnap agreed (Dawson:77). Much of Zermelo's subsequent work was related to logics stronger than first-order logic, with which he hoped to show both the consistency and categoricity of mathematical theories.
Paul Finsler
(1926) used a version of Richard's paradox
to construct an expression that was false but unprovable in a particular, informal framework he had developed. Gödel was unaware of this paper when he proved the incompleteness theorems (Collected Works Vol. IV., p. 9). Finsler wrote Gödel in 1931 to inform him about this paper, which Finsler felt had priority for an incompleteness theorem. Finsler's methods did not rely on formalized provability, and had only a superficial resemblance to Gödel's work (van Heijenoort 1967:328). Gödel read the paper but found it deeply flawed, and his response to Finsler laid out concerns about the lack of formalization (Dawson:89). Finsler continued to argue for his philosophy of mathematics, which eschewed formalization, for the remainder of his career.
wrote several passages about the incompleteness theorems that were published posthumously in his 1953 Remarks on the Foundations of Mathematics
. Gödel was a member of the Vienna Circle
during the period in which Wittgenstein's early ideal language philosophy and Tractatus Logico-Philosophicus
dominated the circle's thinking; writings of Gödel in his Nachlass
express the belief that Wittgenstein willfully misread Gödel's theorems.
Multiple commentators have read Wittgenstein as misunderstanding Gödel
(Rodych 2003), although Juliet Floyd and Hilary Putnam
(2000) have suggested that the majority of commentary misunderstands Wittgenstein. On their release, Bernays, Dummett, and Kreisel wrote separate reviews on Wittgenstein's remarks, all of which were extremely negative (Berto 2009:208). The unanimity of this criticism caused Wittgenstein's remarks on the incompleteness theorems to have little impact on the logic community. In 1972, Gödel wrote to Karl Menger
that Wittgenstein's comments demonstrate a fundamental misunderstanding of the incompleteness theorems.
Since the publication of Wittgenstein's Nachlass in 2000,
a series of papers in philosophy have sought to evaluate whether the original criticism of Wittgenstein's remarks was justified. Floyd and Putnam (2000) argue that Wittgenstein had a more complete understanding of the incompleteness theorem than was previously assumed. They are particularly concerned with the interpretation of a Gödel sentence for an ω-inconsistent theory as actually saying "I am not provable", since the theory has no models in which the provability predicate corresponds to actual provability. Rodych (2003) argues that their interpretation of Wittgenstein is not historically justified, while Bays (2004) argues against Floyd and Putnam's philosophical analysis of the provability predicate. Berto (2009) explores the relationship between Wittgenstein's writing and theories of paraconsistent logic.
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
s of mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
that establish inherent limitations of all but the most trivial axiomatic system
Axiomatic system
In mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of an axiomatic system and all its derived theorems...
s capable of doing arithmetic
Arithmetic
Arithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple day-to-day counting to advanced science and business calculations. It involves the study of quantity, especially as the result of combining numbers...
. The theorems, proven by Kurt Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
in 1931, are important both in mathematical logic and in the philosophy of mathematics
Philosophy of mathematics
The philosophy of mathematics is the branch of philosophy that studies the philosophical assumptions, foundations, and implications of mathematics. The aim of the philosophy of mathematics is to provide an account of the nature and methodology of mathematics and to understand the place of...
. The two results are widely, but not universally, interpreted as showing that Hilbert's program
Hilbert's program
In mathematics, Hilbert's program, formulated by German mathematician David Hilbert, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies...
to find a complete and consistent set of axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s for all of mathematics
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
is impossible, giving a negative answer to Hilbert's second problem
Hilbert's second problem
In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that arithmetic is consistent – free of any internal contradictions....
.
The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "effective procedure" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the natural numbers (arithmetic
Arithmetic
Arithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple day-to-day counting to advanced science and business calculations. It involves the study of quantity, especially as the result of combining numbers...
). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, a corollary
Corollary
A corollary is a statement that follows readily from a previous statement.In mathematics a corollary typically follows a theorem. The use of the term corollary, rather than proposition or theorem, is intrinsically subjective...
of the first, shows that such a system cannot demonstrate its own consistency.
Background
Because statements of a formal theory are written in symbolic form, it is possible to mechanically verify that a formal proofFormal proof
A formal proof or derivation is a finite sequence of sentences each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system...
from a finite set of axioms is valid. This task, known as automatic proof verification, is closely related to automated theorem proving
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
. 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 process 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
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
theories of arithmetic, such as Peano arithmetic
Peano axioms
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano...
, because the principle of mathematical induction
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
is expressed as an infinite set of axioms (an axiom schema
Axiom schema
In mathematical logic, an axiom schema generalizes the notion of axiom.An axiom schema is a formula in the language of an axiomatic system, in which one or more schematic variables appear. These variables, which are metalinguistic constructs, stand for any term or subformula of the system, which...
).
A formal theory is said to be effectively generated if its set of axioms is a recursively enumerable set
Recursively enumerable set
In computability theory, traditionally called recursion theory, a set S of natural numbers is called recursively enumerable, computably enumerable, semidecidable, provable or Turing-recognizable if:...
. 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 existence of a program that enumerates all the theorems of the theory without enumerating any statements that are not theorems. Examples of effectively generated theories with infinite sets of axioms include Peano arithmetic and Zermelo–Fraenkel set theory
Zermelo–Fraenkel set theory
In mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...
.
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
Complete theory
In mathematical logic, a theory is complete if it is a maximal consistent set of sentences, i.e., if it is consistent, and none of its proper extensions is consistent...
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
Consistency
Consistency can refer to:* Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
if there is no statement such that both the statement and its negation are provable from the axioms. In the standard system of first-order logic, an inconsistent set of axioms will prove every statement in its language (this is sometimes called the principle of explosion
Principle of explosion
The principle of explosion, or the principle of Pseudo-Scotus, is the law of classical logic and intuitionistic and similar systems of logic, according to which any statement can be proven from a contradiction...
), and is thus automatically complete. A set of axioms that is both complete and consistent, however, proves a maximal set
Maximal set
In recursion theory, the mathematical theory of computability, a maximal set is a coinfinite recursively enumerable subset A of the natural numbers such that for every further recursively enumerable subset B of the natural numbers, either B is cofinite or B is a finite variant of A or B is not a...
of non-contradictory
Contradiction
In classical logic, a contradiction consists of a logical incompatibility between two or more propositions. It occurs when the propositions, taken together, yield two conclusions which form the logical, usually opposite inversions of each other...
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 consistentConsistencyConsistency can refer to:* Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
and completeComplete theoryIn mathematical logic, a theory is complete if it is a maximal consistent set of sentences, i.e., if it is consistent, and none of its proper extensions is consistent...
. In particular, for any consistent, effectively generated formal theoryTheory (mathematical logic)In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...
that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory (Kleene 1967, p. 250).
This is proved by constructing a true but unprovable sentence G for each theory T, called “the Gödel sentence” for the theory. If just one of those can be built, it follows that infinitely many true-but-unprovable sentences can be built too. For example, the conjunction of G and any logically valid sentence will have the same property.
The Gödel sentence G is an equation that, formally speaking, asserts some equality between some sums and products of natural numbers, but that can also be informally interpreted as "this G cannot be formally derived under the axioms and rules of inference of T ". This interpretation of G leads to the following informal analysis. If G were provable under the axioms and rules of inference of T, then G would be false but derivable, and thus the theory T would be inconsistent. So, if the axioms and rules of derivation have been chosen so that only truths can be derived, it follows that G is true but cannot be derived. Therefore, we have been able to prove the truth of G by reasoning outside the system, but there is no hope we can ever prove the truth of G using a formal derivation inside the system. It follows that there are an infinite number of sentences such as G that are actually true but cannot be formally derived - in other words, T is incomplete. The claim G makes about its own underivability is correct, so provability-within-the-theory-T is not the same as truth. This informal analysis can be formalized to make a rigorous proof of the incompleteness theorem, as described in the section "Proof sketch for the first theorem" below.
Each effectively generated 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, provided that it is effectively generated. 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
Consistency proof
In logic, a consistent theory is one that does not contain a contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if and only if it has a model, i.e. there exists an interpretation under which all...
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 number-theoretical statements which that system cannot prove. This fact is sometimes thought to have severe consequences for the program of logicismLogicism
Logicism is one of the schools of thought in the philosophy of mathematics, putting forth the theory that mathematics is an extension of logic and therefore some or all mathematics is reducible to logic. Bertrand Russell and Alfred North Whitehead championed this theory fathered by Richard Dedekind...
proposed by Gottlob Frege
Gottlob Frege
Friedrich Ludwig Gottlob Frege was a German mathematician, logician and philosopher. He is considered to be one of the founders of modern logic, and made major contributions to the foundations of mathematics. He is generally considered to be the father of analytic philosophy, for his writings on...
and Bertrand Russell
Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, OM, FRS was a British philosopher, logician, mathematician, historian, and social critic. At various points in his life he considered himself a liberal, a socialist, and a pacifist, but he also admitted that he had never been any of these things...
, which aimed to define the natural numbers in terms of logic (Hellman 1981, p. 451–468). Some (like Bob Hale
Bob Hale (philosopher)
Robert Hale FBA, FRSE is a British philosopher, who is well-known for his contributions to the development of the neo-Fregean philosophy of mathematics in collaboration with Crispin Wright, and for his works in modality and philosophy of language....
and Crispin Wright
Crispin Wright
Crispin Wright is a British philosopher, who has written on neo-Fregean philosophy of mathematics, Wittgenstein's later philosophy, and on issues related to truth, realism, cognitivism, skepticism, knowledge, and objectivity....
) argue that it is not a problem for logicism because the incompleteness theorems apply equally to second order logic as they do to arithmetic. They argue that only those who believe that the natural numbers are to be defined in terms of first order logic 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
Euclidean geometry
Euclidean geometry is a mathematical system attributed to the Alexandrian Greek mathematician Euclid, which he described in his textbook on geometry: the Elements. Euclid's method consists in assuming a small set of intuitively appealing axioms, and deducing many other propositions from these...
without the parallel postulate
Parallel postulate
In geometry, the parallel postulate, also called Euclid's fifth postulate because it is the fifth postulate in Euclid's Elements, is a distinctive axiom in Euclidean geometry...
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
Number theory
Number theory is a branch of pure mathematics devoted primarily to the study of the integers. Number theorists study prime numbers as well...
, 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.
There are complete and consistent list of axioms for arithmetic 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), which gives the theory known as "true arithmetic
True arithmetic
In mathematical logic, true arithmetic is the theory Th of the natural numbers in the language of first-order Peano arithmetic...
". The difficulty is that there is no mechanical way to decide, given a statement about the natural numbers, whether it is an axiom of this theory, and thus there is 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
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
's second problem
Hilbert's second problem
In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that arithmetic is consistent – free of any internal contradictions....
, 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 paradoxLiar paradox
In philosophy and logic, the liar paradox or liar's paradox , is the statement "this sentence is false"...
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
Gödel number
In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. The concept was famously used by Kurt Gödel for the proof of his incompleteness theorems...
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
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
.
Original statements
The first incompleteness theorem first appeared as "Theorem VI" in Gödel's 1931 paper On Formally Undecidable Propositions in Principia Mathematica and Related Systems I. The second incompleteness theorem appeared as "Theorem XI" in the same paper.Extensions of Gödel's original result
Gödel demonstrated the incompleteness of the theory of Principia MathematicaPrincipia Mathematica
The Principia Mathematica is a three-volume work on the foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913...
, 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
Rosser's trick
In mathematical logic, Rosser's trick is a method for proving Gödel's incompleteness theorems without the assumption that the theory being considered is ω-consistent . This method was introduced by J...
) 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, if T includes a statement of its own consistency then 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, first-order Peano arithmetic
Peano axioms
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano...
(PA) can prove that the largest consistent subset
Subset
In mathematics, especially in set theory, a set A is a subset of a set B if A is "contained" inside B. A and B may coincide. The relationship of one set being a subset of another is called inclusion or sometimes containment...
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 technically ambiguous, 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 first-order 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 ProvA(P) which expresses that P is provable from the set of axioms defined by A(x).
In addition, the standard proof of the second incompleteness theorem assumes that ProvA(P) satisfies that Hilbert–Bernays provability conditions
Hilbert–Bernays provability conditions
In mathematical logic, the Hilbert–Bernays provability conditions, named after David Hilbert and Paul Bernays, are a set of requirements for formalized provability predicates in formal theories of arithmetic ....
. Letting #(P) represent the Gödel number of a formula P, the derivability conditions say:
- If T proves P, then T proves ProvA(#(P)).
- T proves 1.; that is, T proves that if T proves P, then T proves ProvA(#(P)). In other words, T proves that ProvA(#(P)) implies ProvA(#(ProvA(#(P)))).
- T proves that if T proves that (P → Q) and T proves P then T proves Q. In other words, T proves that ProvA(#(P → Q)) and ProvA(#(P)) imply ProvA(#(Q)).
Implications for consistency proofs
Gödel's second incompleteness theorem also implies that a theory T1 satisfying the technical conditions outlined above cannot prove the consistency of any theory T2 which proves the consistency of T1. This is because such a theory T1 can prove that if T2 proves the consistency of T1, then T1 is in fact consistent. For the claim that T1 is consistent has form "for all numbers n, n has the decidable property of not being a code for a proof of contradiction in T1". If T1 were in fact inconsistent, then T2 would prove for some n that n is the code of a contradiction in T1. But if T2 also proved that T1 is consistent (that is, that there is no such n), then it would itself be inconsistent. This reasoning can be formalized in T1 to show that if T2 is consistent, then T1 is consistent. Since, by second incompleteness theorem, T1 does not prove its consistency, it cannot prove the consistency of T2 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
Primitive recursive arithmetic
Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist...
(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
Hilbert's program
In mathematics, Hilbert's program, formulated by German mathematician David Hilbert, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies...
, 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. 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
Zermelo–Fraenkel set theory
In mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...
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
Gerhard Gentzen
Gerhard Karl Erich Gentzen was a German mathematician and logician. He had his major contributions in the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus...
proved the consistency of Peano arithmetic (PA) in a different theory which includes an axiom asserting that the ordinal
Ordinal number
In set theory, an ordinal number, or just ordinal, is the order type of a well-ordered set. They are usually identified with hereditarily transitive sets. Ordinals are an extension of the natural numbers different from integers and from cardinals...
called ε0 is wellfounded; see Gentzen's consistency proof
Gentzen's consistency proof
Gentzen's consistency proof is a result of proof theory in mathematical logic. It "reduces" the consistency of a simplified part of mathematics, not to something that could be proved , but to clarified logical principles.-Gentzen's theorem:In 1936 Gerhard Gentzen proved the consistency of...
. Gentzen's theorem spurred the development of ordinal analysis
Ordinal analysis
In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. The field was formed when Gerhard Gentzen in 1934 used cut elimination to prove, in modern terms, that the proof theoretic ordinal of Peano arithmetic is ε0.-Definition:Ordinal...
in proof theory.
Examples of undecidable statements
There are two distinct senses of the word "undecidable" in mathematics and computer science. The first of these is the proof-theoreticProof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
sense used in relation to Gödel's theorems, that of a statement being neither provable nor refutable in a specified deductive system
Deductive system
A deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the system....
. The second sense, which will not be discussed here, is used in relation to computability theory
Computability theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
and applies not to statements but to decision problem
Decision problem
In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...
s, 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
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
that correctly answers every question in the problem set (see undecidable problem
Undecidable problem
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is impossible to construct a single algorithm that always leads to a correct yes-or-no answer....
).
Because of the two meanings of the word undecidable, the term independent
Independence (mathematical logic)
In mathematical logic, independence refers to the unprovability of a sentence from other sentences.A sentence σ is independent of a given first-order theory T if T neither proves nor refutes σ; that is, it is impossible to prove σ from T, and it is also impossible to prove from T that...
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 well-defined, 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 so-called "absolutely undecidable" statements, whose truth value can never be known or is ill-specified, is a controversial point in the philosophy of mathematics
Philosophy of mathematics
The philosophy of mathematics is the branch of philosophy that studies the philosophical assumptions, foundations, and implications of mathematics. The aim of the philosophy of mathematics is to provide an account of the nature and methodology of mathematics and to understand the place of...
.
The combined work of Gödel and Paul Cohen
Paul Cohen (mathematician)
Paul Joseph Cohen was an American mathematician best known for his proof of the independence of the continuum hypothesis and the axiom of choice from Zermelo–Fraenkel set theory, the most widely accepted axiomatization of set theory.-Early years:Cohen was born in Long Branch, New Jersey, into a...
has given two concrete examples of undecidable statements (in the first sense of the term): The continuum hypothesis
Continuum hypothesis
In mathematics, the continuum hypothesis is a hypothesis, advanced by Georg Cantor in 1874, about the possible sizes of infinite sets. It states:Establishing the truth or falsehood of the continuum hypothesis is the first of Hilbert's 23 problems presented in the year 1900...
can neither be proved nor refuted in ZFC (the standard axiomatization of set theory
Set theory
Set theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...
), 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
Whitehead problem
In group theory, a branch of abstract algebra, the Whitehead problem is the following question:Shelah proved that Whitehead's problem is undecidable within standard ZFC set theory.-Refinement:...
in group theory
Group theory
In mathematics and abstract algebra, group theory studies the algebraic structures known as groups.The concept of a group is central to abstract algebra: other well-known algebraic structures, such as rings, fields, and vector spaces can all be seen as groups endowed with additional operations and...
was shown to be undecidable, in the first sense of the term, in standard set theory.
In 1977, Paris and Harrington proved that the Paris-Harrington principle, a version of the Ramsey theorem, is undecidable in the first-order axiomatization of arithmetic called Peano arithmetic, but can be proven in the larger system of second-order arithmetic
Second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. It was introduced by David Hilbert and Paul Bernays in their...
. Kirby and Paris later showed Goodstein's theorem
Goodstein's theorem
In mathematical logic, Goodstein's theorem is a statement about the natural numbers, made by Reuben Goodstein, which states that every Goodstein sequence eventually terminates at 0. showed that it is unprovable in Peano arithmetic...
, a statement about sequences of natural numbers somewhat simpler than the Paris-Harrington principle, to be undecidable in Peano arithmetic.
Kruskal's tree theorem
Kruskal's tree theorem
In mathematics, Kruskal's tree theorem states that the set of finite trees over a well-quasi-ordered set of labels is itself well-quasi-ordered...
, 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
Computational complexity theory
Computational complexity theory is a branch of the theory of computation in theoretical computer science and mathematics that focuses on classifying computational problems according to their inherent difficulty, and relating those classes to each other...
.
Gregory Chaitin
Gregory Chaitin
Gregory John Chaitin is an Argentine-American mathematician and computer scientist.-Mathematics and computer science:Beginning in 2009 Chaitin has worked on metabiology, a field parallel to biology dealing with the random evolution of artificial software instead of natural software .Beginning in...
produced undecidable statements in algorithmic information theory
Algorithmic information theory
Algorithmic information theory is a subfield of information theory and computer science that concerns itself with the relationship between computation and information...
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
Kolmogorov complexity
In algorithmic information theory , the Kolmogorov complexity of an object, such as a piece of text, is a measure of the computational resources needed to specify the object...
greater than c. While Gödel's theorem is related to the liar paradox
Liar paradox
In philosophy and logic, the liar paradox or liar's paradox , is the statement "this sentence is false"...
, Chaitin's result is related to Berry's paradox.
Limitations of Gödel's theorems
The conclusions of Gödel's theorems are only proven 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 first-order axiomatizations of Euclidean geometryEuclidean geometry
Euclidean geometry is a mathematical system attributed to the Alexandrian Greek mathematician Euclid, which he described in his textbook on geometry: the Elements. Euclid's method consists in assuming a small set of intuitively appealing axioms, and deducing many other propositions from these...
, 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 (Willard 2001) has studied many weak systems of arithmetic which do not satisfy the hypotheses of the second incompleteness theorem, and which are consistent and capable of proving their own consistency (see self-verifying theories
Self-verifying theories
Self-verifying theories are consistent first-order systems of arithmetic much weaker than Peano arithmetic that are capable of proving their own consistency. Dan Willard was the first to investigate their properties, and he has described a family of such systems...
).
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 (called true arithmetic
True arithmetic
In mathematical logic, true arithmetic is the theory Th of the natural numbers in the language of first-order 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–Fraenkel set theory
Zermelo–Fraenkel set theory
In mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...
(ZFC), or in theories of arithmetic augmented with transfinite induction
Transfinite induction
Transfinite induction is an extension of mathematical induction to well-ordered sets, for instance to sets of ordinal numbers or cardinal numbers.- Transfinite induction :Let P be a property defined for all ordinals α...
, as in Gentzen's consistency proof
Gentzen's consistency proof
Gentzen's consistency proof is a result of proof theory in mathematical logic. It "reduces" the consistency of a simplified part of mathematics, not to something that could be proved , but to clarified logical principles.-Gentzen's theorem:In 1936 Gerhard Gentzen proved the consistency of...
.
Relationship with computability
The incompleteness theorem is closely related to several results about undecidable sets in recursion theoryRecursion theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
.
Stephen Cole Kleene
Stephen Cole Kleene
Stephen Cole Kleene was an American mathematician who helped lay the foundations for theoretical computer science...
(1943) presented a proof of Gödel's incompleteness theorem using basic results of computability theory. One such result shows that the halting problem
Halting problem
In computability theory, the halting problem can be stated as follows: Given a description of a computer program, decide whether the program finishes running or continues to run forever...
is unsolvable: there is no computer program that can correctly determine, given a program P as input, whether P eventually halts when run with some given 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(x1, x2,...,xk) 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
Recursively inseparable sets
In computability theory, recursively inseparable sets are pairs of sets of natural numbers that cannot be "separated" with a computable set . These sets arise in the study of computability theory itself, particularly in relation to Π01 classes...
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).
Chaitin's incompleteness theorem gives a different method of producing independent sentences, based on Kolmogorov complexity
Kolmogorov complexity
In algorithmic information theory , the Kolmogorov complexity of an object, such as a piece of text, is a measure of the computational resources needed to specify the object...
. Like the proof presented by Kleene that was mentioned above, Chaitin's theorem only applies to theories with the additional property that all their axioms are true in the standard model of the natural numbers. Gödel's incompleteness theorem is distinguished by its applicability to consistent theories that nonetheless include statements that are false in the standard model; these theories are known as ω-inconsistent.
Proof sketch for the first theorem
The proof by contradiction has three essential parts. To begin, choose a formal system that meets the proposed criteria:- Statements in the system can be represented by natural numbers (known as Gödel numbers). The significance of this is that properties of statements—such as their truth and falsehood—will be equivalent to determining whether their Gödel numbers have certain properties, and that properties of the statements can therefore be demonstrated by examining their Gödel numbers. This part culminates in the construction of a formula expressing the idea that "statement S is provable in the system" (which can be applied to any statement "S" in the system).
- In the formal system it is possible to construct a number whose matching statement, when interpreted, is self-referential and essentially says that it (i.e. the statement itself) is unprovable. This is done using a technique called "diagonalizationDiagonal lemmaIn mathematical logic, the diagonal lemma or fixed point theorem establishes the existence of self-referential sentences in certain formal theories of the natural numbers -- specifically those theories that are strong enough to represent all computable functions...
" (so-called because of its origins as Cantor's diagonal argumentCantor's diagonal argumentCantor's diagonal argument, also called the diagonalisation argument, the diagonal slash argument or the diagonal method, was published in 1891 by Georg Cantor as a mathematical proof that there are infinite sets which cannot be put into one-to-one correspondence with the infinite set of natural...
). - Within the formal system this statement permits a demonstration that it is neither provable nor disprovable in the system, and therefore the system cannot in fact be ω-consistent. Hence the original assumption that the proposed system met the criteria is false.
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 technique is to show that statements can be matched with numbers (often called the arithmetization of syntaxSyntax
In linguistics, syntax is the study of the principles and rules for constructing phrases and sentences in natural languages....
) in such a way that "proving a statement" can be replaced with "testing whether a number has a given property". This allows a self-referential formula to be constructed in a way that avoids any infinite regress of definitions. The same technique was later used by Alan Turing
Alan Turing
Alan Mathison Turing, OBE, FRS , was an English mathematician, logician, cryptanalyst, and computer scientist. He was highly influential in the development of computer science, providing a formalisation of the concepts of "algorithm" and "computation" with the Turing machine, which played a...
in his work on the Entscheidungsproblem
Entscheidungsproblem
In mathematics, the is a challenge posed by David Hilbert in 1928. The asks for an algorithm that will take as input a description of a formal language and a mathematical statement in the language and produce as output either "True" or "False" according to whether the statement is true or false...
.
In simple terms, a method can be devised so that every formula or statement that can be formulated in the system gets a unique number, called its Gödel number
Gödel number
In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. The concept was famously used by Kurt Gödel for the proof of his incompleteness theorems...
, in such a way that it is possible to mechanically convert back and forth between formulas and Gödel numbers. The numbers involved might be very long indeed (in terms of number of digits), but this is not a barrier; all that matters is that such numbers can be constructed. A simple example is the way in which English is stored as a sequence of numbers in computers using ASCII
ASCII
The American Standard Code for Information Interchange is a character-encoding scheme based on the ordering of the English alphabet. ASCII codes represent text in computers, communications equipment, and other devices that use text...
or Unicode
Unicode
Unicode is a computing industry standard for the consistent encoding, representation and handling of text expressed in most of the world's writing systems...
:
- The word HELLO is represented by 72-69-76-76-79 using decimal ASCIIASCIIThe American Standard Code for Information Interchange is a character-encoding scheme based on the ordering of the English alphabet. ASCII codes represent text in computers, communications equipment, and other devices that use text...
, ie the number 7269767679. - The logical statement x=y => y=x is represented by 120-061-121-032-061-062-032-121-061-120 using octal ASCIIASCIIThe American Standard Code for Information Interchange is a character-encoding scheme based on the ordering of the English alphabet. ASCII codes represent text in computers, communications equipment, and other devices that use text...
, ie the number 120061121032061062032121061120.
In principle, proving a statement true or false can be shown to be equivalent to proving that the number matching the statement does or doesn't have a given property. Because the formal system is strong enough to support reasoning about numbers in general, it can support reasoning about numbers which represent formulae and statements as well. Crucially, because the system can support reasoning about properties of numbers, the results are equivalent to reasoning about provability of their equivalent statements.
Construction of a statement about "provability"
Having shown that in principle the system can indirectly make statements about provability, by analyzing properties of those numbers representing statements it is now possible to show how to create a statement that actually does this.A formula F(x) that contains exactly one free variable x is called a statement form or class-sign. As soon as x is replaced by a specific number, the statement form turns into a bona fide
Bona Fide
Bona Fide is a studio album from rock band Wishbone Ash. It is the first studio album in six years and is the only studio album to feature guitarist Ben Granfelt...
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 a Gödel number denoted 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, the Gödel number of a proof can be defined. Now, for every statement p, one 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 potential Gödel number of its proof, is an arithmetical relation between two numbers. Therefore there is a statement form Bew(y) that uses this arithmetical relation to state that a Gödel number of a proof of y 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 lemmaDiagonal lemma
In mathematical logic, the diagonal lemma or fixed point theorem establishes the existence of self-referential sentences in certain formal theories of the natural numbers -- specifically those theories that are strong enough to represent all computable functions...
, 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)).
By letting F be the negation of Bew(x), p is obtained: 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
Now assume that the formal system is ω-consistent. 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 the 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 supports construction of 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, it can be proved that the number 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 chosen system. So the chosen system is either inconsistent or incomplete. This logic can be applied to any formal system meeting the criteria. The conclusion is that all formal systems meeting the criteria are either inconsistent or incomplete. 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. So:
- In an ω-consistent formal system, neither p nor its negation can be proved, and so p is undecidable.
- In a consistent formal systemFormal systemIn formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
either the same situation occurs, or the negation of p can be proved; In the later case, a statement ("not p") is false but provable.
Note that if one tries to fix this by "adding the missing axioms" to avoid the undecidability of the system, then one has to add either p or "not p" as axioms. But this then creates a new formal system2 (old system + p), to which exactly the same process can be applied, creating a new statement form Bew2(x) for this new system. When the diagonal lemma is applied to this new form Bew2, a new statement p2 is obtained; this statement will be different from the previous one, and this new statement will be undecidable in the new system if it is ω-consistent, thus showing that system2 is equally inconsistent. So adding extra axioms cannot fix the problem.
Proof via Berry's paradox
George BoolosGeorge Boolos
George Stephen Boolos was a philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.- Life :...
(1989) sketches an alternative proof of the first incompleteness theorem that uses Berry's paradox rather than the liar paradox
Liar paradox
In philosophy and logic, the liar paradox or liar's paradox , is the statement "this sentence is false"...
to construct a true but unprovable formula. A similar proof method was independently discovered by Saul Kripke
Saul Kripke
Saul Aaron Kripke is an American philosopher and logician. He is a professor emeritus at Princeton and teaches as a Distinguished Professor of Philosophy at the CUNY Graduate Center...
(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).
Formalized proofs
Formalized proofs of versions of the incompleteness theorem have been developed by Natarajan ShankarNatarajan Shankar
Natarajan Shankar is a computer scientist working at SRI International, California.His PhD thesis was published as the book " Metamathematics, Machines, and Goedel's Proof" by Cambridge University Press in 1994. He has used the Boyer–Moore theorem prover to prove metatheorems such as the tautology...
in 1986 using Nqthm
Nqthm
Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.- History :The system was developed by Robert S. Boyer and J Strother Moore, professors of computer science at the University of Texas, Austin. They began work on the system in 1971 in...
(Shankar 1994) and by R. O'Connor in 2003 using Coq
Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
(O'Connor 2005).
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. The demonstration above shows 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 mathematicsPhilosophy of mathematics
The philosophy of mathematics is the branch of philosophy that studies the philosophical assumptions, foundations, and implications of mathematics. The aim of the philosophy of mathematics is to provide an account of the nature and methodology of mathematics and to understand the place of...
, 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:
- An all-encompassing axiomatic system can never be found that 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 well-defined 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
Foundations of mathematics
Foundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...
:
- If an axiomatic system can be proven to be consistent 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.
Theories such as Peano arithmetic, for which any computably enumerable consistent extension is incomplete, are called essentially undecidable or essentially incomplete.
Minds and machines
Authors including J. R. LucasJohn Lucas (philosopher)
- Overview :John Lucas was educated at Winchester College and Balliol College, Oxford, where he studied first mathematics, then Greats , obtaining first class honors, and proceeding to an MA in Philosophy in 1954. He spent the 1957-58 academic year at Princeton University, deepening his...
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
Turing machine
A Turing machine is a theoretical device that manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can be adapted to simulate the logic of any computer algorithm, and is particularly useful in explaining the functions of a CPU inside a...
, or by the Church–Turing thesis
Church–Turing thesis
In computability theory, the Church–Turing thesis is a combined hypothesis about the nature of functions whose values are effectively calculable; in more modern terms, algorithmically computable...
, 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
Hilary Putnam
Hilary Whitehall Putnam is an American philosopher, mathematician and computer scientist, who has been a central figure in analytic philosophy since the 1960s, especially in philosophy of mind, philosophy of language, philosophy of mathematics, and philosophy of science...
(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. Assuming that it is consistent, either its consistency cannot be proved or it cannot be represented by a Turing machine.
Avi Wigderson
Avi Wigderson
Avi Wigderson is an Israeli mathematician and computer scientist, a professor of mathematics at the Institute for Advanced Study in Princeton. His research interests include complexity theory, parallel algorithms, graph theory, cryptography, distributed computing, and neural...
(2010) has proposed that the concept of mathematical "knowability" should be based on computational complexity
Computational Complexity
Computational Complexity may refer to:*Computational complexity theory*Computational Complexity...
rather than logical decidability. He writes that "when knowability is interpreted by modern standards, namely via computational complexity, the Gödel phenomena are very much with us."
Paraconsistent logic
Although Gödel's theorems are usually studied in the context of classical logic, they also have a role in the study of paraconsistent logicParaconsistent logic
A paraconsistent logic is a logical system that attempts to deal with contradictions in a discriminating way. Alternatively, paraconsistent logic is the subfield of logic that is concerned with studying and developing paraconsistent systems of logic.Inconsistency-tolerant logics have been...
and of inherently contradictory statements (dialetheia). Graham Priest
Graham Priest
Graham Priest is Boyce Gibson Professor of Philosophy at the University of Melbourne and Distinguished Professor of Philosophy at the CUNY Graduate Center, as well as a regular visitor at St. Andrews University. Priest is a fellow in residence at Ormond College. He was educated at the University...
(1984, 2006) argues that replacing the notion of formal proof in Gödel's theorem with the usual notion of informal proof can be used to show that naive mathematics is inconsistent, and uses this as evidence for dialetheism
Dialetheism
Dialetheism is the view that some statements can be both true and false simultaneously. More precisely, it is the belief that there can be a true statement whose negation is also true...
. The cause of this inconsistency is the inclusion of a truth predicate for a theory within the language of the theory (Priest 2006:47). Stewart Shapiro
Stewart Shapiro
Stewart Shapiro is O'Donnell Professor of Philosophy at the Ohio State University and a regular visiting professor at the University of St Andrews in Scotland. He is an important contemporary figure in the philosophy of mathematics where he defends a version of structuralism. He studied...
(2002) gives a more mixed appraisal of the applications of Gödel's theorems to dialetheism. Carl Hewitt
Carl Hewitt
Carl Hewitt is Board Chair of the International Society for Inconsistency Robustness. He has been a Visiting Professor at Stanford University and the University of Keio. In 2000, he became emeritus in the EECS department at MIT....
(2008) has proposed that (inconsistent) paraconsistent logics that prove their own Gödel sentences may have applications in software engineering
Software engineering
Software Engineering is the application of a systematic, disciplined, quantifiable approach to the development, operation, and maintenance of software, and the study of these approaches; that is, the application of engineering to software...
.
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énTorkel Franzén
Torkel Franzén was a Swedish academic. He worked at the Department of Computer Science and Electrical Engineering at Luleå University of Technology, Sweden, in the fields of mathematical logic and computer science. He was known for his work on Gödel's incompleteness theorems and for his...
(2005); Alan Sokal
Alan Sokal
Alan David Sokal is a professor of mathematics at University College London and professor of physics at New York University. He works in statistical mechanics and combinatorics. To the general public he is best known for his criticism of postmodernism, resulting in the Sokal affair in...
and Jean Bricmont
Jean Bricmont
Jean Bricmont is a Belgian theoretical physicist, philosopher of science and a professor at the Université catholique de Louvain. He works on renormalization group and nonlinear differential equations....
(1999); and Ophelia Benson
Ophelia Benson
Ophelia Benson is co-author of The Dictionary of Fashionable Nonsense: A Guide for Edgy People, Why Truth Matters , and Does God Hate Women?....
and Jeremy Stangroom
Jeremy Stangroom
Jeremy Stangroom is a British writer, editor, and website designer. He is an editor and co-founder, with Julian Baggini, of The Philosophers’ Magazine, and has written and edited several philosophy books. He is also co-founder, with Ophelia Benson of the website 'Butterflies and Wheels'.Stangroom...
(2006). Bricmont and Stangroom (2006, p. 10), for example, quote from Rebecca Goldstein
Rebecca Goldstein
Rebecca Goldstein is an American novelist and professor of philosophy. She has written five novels, a number of short stories and essays, and biographical studies of mathematician Kurt Gödel and philosopher Baruch Spinoza....
's comments on the disparity between Gödel's avowed Platonism and the anti-realist uses to which his ideas are sometimes put. Sokal and Bricmont (1999, p. 187) criticize Régis Debray
Régis Debray
Jules Régis Debray is a French intellectual, journalist, government official and professor. He is known for his theorization of mediology, a critical theory of the long-term transmission of cultural meaning in human society; and for having fought in 1967 with Marxist revolutionary Che Guevara in...
's invocation of the theorem in the context of sociology; Debray has defended this use as metaphorical (ibid.).
The role of self-reference
Torkel FranzénTorkel Franzén
Torkel Franzén was a Swedish academic. He worked at the Department of Computer Science and Electrical Engineering at Luleå University of Technology, Sweden, in the fields of mathematical logic and computer science. He was known for his work on Gödel's incompleteness theorems and for his...
(2005, p. 46) observes:
Gödel's proof of the first incompleteness theorem and Rosser's strengthened version have given many the impression that the theorem can only be proved by constructing self-referential statements [...] or even that only strange self-referential statements are known to be undecidable in elementary arithmetic.
To counteract such impressions, we need only introduce a different kind of proof of the first incompleteness theorem.
He then proposes the proofs based on Computability
Computability theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
, or on information theory
Algorithmic information theory
Algorithmic information theory is a subfield of information theory and computer science that concerns itself with the relationship between computation and information...
, as described earlier in this article, as examples of proofs that should "counteract such impressions".
History
After Gödel published his proof of the completeness theorem as his doctoral thesis in 1929, he turned to a second problem for his habilitationHabilitation
Habilitation is the highest academic qualification a scholar can achieve by his or her own pursuit in several European and Asian countries. Earned after obtaining a research doctorate, such as a PhD, habilitation requires the candidate to write a professorial thesis based on independent...
. His original goal was to obtain a positive solution to Hilbert's second problem
Hilbert's second problem
In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that arithmetic is consistent – free of any internal contradictions....
(Dawson 1997, p. 63). At the time, theories of the natural numbers and real numbers similar to second-order arithmetic
Second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. It was introduced by David Hilbert and Paul Bernays in their...
were known as "analysis", while theories of the natural numbers alone were known as "arithmetic".
Gödel was not the only person working on the consistency problem. Ackermann had published a flawed consistency proof for analysis in 1925, in which he attempted to use the method of ε-substitution originally developed by Hilbert. Later that year, von Neumann was able to correct the proof for a theory of arithmetic without any axioms of induction. By 1928, Ackermann had communicated a modified proof to Bernays; this modified proof led Hilbert to announce his belief in 1929 that the consistency of arithmetic had been demonstrated and that a consistency proof of analysis would likely soon follow. After the publication of the incompleteness theorems showed that Ackermann's modified proof must be erroneous, von Neumann produced a concrete example showing that its main technique was unsound (Zach 2006, p. 418, Zach 2003, p. 33).
In the course of his research, Gödel discovered that although a sentence which asserts its own falsehood leads to paradox, a sentence that asserts its own non-provability does not. In particular, Gödel was aware of the result now called Tarski's indefinability theorem
Tarski's indefinability theorem
Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1936, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics...
, although he never published it. Gödel announced his first incompleteness theorem to Carnap, Feigel and Waismann on August 26, 1930; all four would attend a key conference in Königsberg the following week.
Announcement
The 1930 Königsberg conference was a joint meeting of three academic societies, with many of the key logicians of the time in attendance. Carnap, Heyting, and von Neumann delivered one-hour addresses on the mathematical philosophies of logicism, intuitionism, and formalism, respectively (Dawson 1996, p. 69). The conference also included Hilbert's retirement address, as he was leaving his position at the University of Göttingen. Hilbert used the speech to argue his belief that all mathematical problems can be solved. He ended his address by saying,- "For the mathematician there is no Ignorabimus, and, in my opinion, not at all for natural science either. ... The true reason why [no one] has succeeded in finding an unsolvable problem is, in my opinion, that there is no unsolvable problem. In contrast to the foolish Ignoramibus, our credo avers: We must know. We shall know!"
This speech quickly became known as a summary of Hilbert's beliefs on mathematics (its final six words, "Wir müssen wissen. Wir werden wissen!", were used as Hilbert's epitaph in 1943). Although Gödel was likely in attendance for Hilbert's address, the two never met face to face (Dawson 1996, p. 72).
Gödel announced his first incompleteness theorem at a roundtable discussion session on the third day of the conference. The announcement drew little attention apart from that of von Neumann, who pulled Gödel aside for conversation. Later that year, working independently with knowledge of the first incompleteness theorem, von Neumann obtained a proof of the second incompleteness theorem, which he announced to Gödel in a letter dated November 20, 1930 (Dawson 1996, p. 70). Gödel had independently obtained the second incompleteness theorem and included it in his submitted manuscript, which was received by Monatshefte für Mathematik on November 17, 1930.
Gödel's paper was published in the Monatshefte in 1931 under the title Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I (On Formally Undecidable Propositions in Principia Mathematica and Related Systems I). As the title implies, Gödel originally planned to publish a second part of the paper; it was never written.
Generalization and acceptance
Gödel gave a series of lectures on his theorems at Princeton in 1933–1934 to an audience that included Church, Kleene, and Rosser. By this time, Gödel had grasped that the key property his theorems required is that the theory must be effective (at the time, the term "general recursive" was used). Rosser proved in 1936 that the hypothesis of ω-consistency, which was an integral part of Gödel's original proof, could be replaced by simple consistency, if the Gödel sentence was changed in an appropriate way. These developments left the incompleteness theorems in essentially their modern form.Gentzen published his consistency proof
Gentzen's consistency proof
Gentzen's consistency proof is a result of proof theory in mathematical logic. It "reduces" the consistency of a simplified part of mathematics, not to something that could be proved , but to clarified logical principles.-Gentzen's theorem:In 1936 Gerhard Gentzen proved the consistency of...
for first-order arithmetic in 1936. Hilbert accepted this proof as "finitary" although (as Gödel's theorem had already shown) it cannot be formalized within the system of arithmetic that is being proved consistent.
The impact of the incompleteness theorems on Hilbert's program was quickly realized. Bernays included a full proof of the incompleteness theorems in the second volume of Grundlagen der Mathematik (1939), along with additional results of Ackermann on the ε-substitution method and Gentzen's consistency proof of arithmetic. This was the first full published proof of the second incompleteness theorem.
Criticism
In September 1931, Ernst ZermeloErnst Zermelo
Ernst Friedrich Ferdinand Zermelo was a German mathematician, whose work has major implications for the foundations of mathematics and hence on philosophy. He is known for his role in developing Zermelo–Fraenkel axiomatic set theory and his proof of the well-ordering theorem.-Life:He graduated...
wrote Gödel to announce what he described as an "essential gap" in Gödel’s argument (Dawson:76). In October, Gödel replied with a 10-page letter (Dawson:76, Grattan-Guinness:512-513). But Zermelo did not relent and published his criticisms in print with “a rather scathing paragraph on his young competitor” (Grattan-Guinness:513). Gödel decided that to pursue the matter further was pointless, and Carnap agreed (Dawson:77). Much of Zermelo's subsequent work was related to logics stronger than first-order logic, with which he hoped to show both the consistency and categoricity of mathematical theories.
Paul Finsler
Paul Finsler
Paul Finsler was a German and Swiss mathematician.Finsler did his undergraduate studies at the Technische Hochschule Stuttgart, and his graduate studies at the University of Göttingen, where he received his Ph.D. in 1919 under the supervision of Constantin Carathéodory...
(1926) used a version of Richard's paradox
Richard's paradox
In logic, Richard's paradox is a semantical antinomy in set theory and natural language first described by the French mathematician Jules Richard in 1905. Today, the paradox is ordinarily used in order to motivate the importance of carefully distinguishing between mathematics and metamathematics...
to construct an expression that was false but unprovable in a particular, informal framework he had developed. Gödel was unaware of this paper when he proved the incompleteness theorems (Collected Works Vol. IV., p. 9). Finsler wrote Gödel in 1931 to inform him about this paper, which Finsler felt had priority for an incompleteness theorem. Finsler's methods did not rely on formalized provability, and had only a superficial resemblance to Gödel's work (van Heijenoort 1967:328). Gödel read the paper but found it deeply flawed, and his response to Finsler laid out concerns about the lack of formalization (Dawson:89). Finsler continued to argue for his philosophy of mathematics, which eschewed formalization, for the remainder of his career.
Wittgenstein and Gödel
Ludwig WittgensteinLudwig Wittgenstein
Ludwig Josef Johann Wittgenstein was an Austrian philosopher who worked primarily in logic, the philosophy of mathematics, the philosophy of mind, and the philosophy of language. He was professor in philosophy at the University of Cambridge from 1939 until 1947...
wrote several passages about the incompleteness theorems that were published posthumously in his 1953 Remarks on the Foundations of Mathematics
Remarks on the Foundations of Mathematics
Remarks on the Foundations of Mathematics is a 1953 book of Ludwig Wittgenstein's notes on the philosophy of mathematics, translated from German to English by G.E.M. Anscombe, edited by G.H. von Wright and Rush Rhees, and published first in 1956...
. Gödel was a member of the Vienna Circle
Vienna Circle
The Vienna Circle was an association of philosophers gathered around the University of Vienna in 1922, chaired by Moritz Schlick, also known as the Ernst Mach Society in honour of Ernst Mach...
during the period in which Wittgenstein's early ideal language philosophy and Tractatus Logico-Philosophicus
Tractatus Logico-Philosophicus
The Tractatus Logico-Philosophicus is the only book-length philosophical work published by the Austrian philosopher Ludwig Wittgenstein in his lifetime. It was an ambitious project: to identify the relationship between language and reality and to define the limits of science...
dominated the circle's thinking; writings of Gödel in his Nachlass
Nachlass
Nachlass is a German word, used in academia to describe the collection of manuscripts, notes, correspondence, and so on left behind when a scholar dies. The word is a compound in German: nach means 'after', and the verb lassen means 'leave'. The plural can be either Nachlasse or Nachlässe...
express the belief that Wittgenstein willfully misread Gödel's theorems.
Multiple commentators have read Wittgenstein as misunderstanding Gödel
Godel
Godel or similar can mean:*Kurt Gödel , an Austrian logician, mathematician and philosopher*Gödel...
(Rodych 2003), although Juliet Floyd and Hilary Putnam
Hilary Putnam
Hilary Whitehall Putnam is an American philosopher, mathematician and computer scientist, who has been a central figure in analytic philosophy since the 1960s, especially in philosophy of mind, philosophy of language, philosophy of mathematics, and philosophy of science...
(2000) have suggested that the majority of commentary misunderstands Wittgenstein. On their release, Bernays, Dummett, and Kreisel wrote separate reviews on Wittgenstein's remarks, all of which were extremely negative (Berto 2009:208). The unanimity of this criticism caused Wittgenstein's remarks on the incompleteness theorems to have little impact on the logic community. In 1972, Gödel wrote to Karl Menger
Karl Menger
Karl Menger was a mathematician. He was the son of the famous economist Carl Menger. He is credited with Menger's theorem. He worked on mathematics of algebras, algebra of geometries, curve and dimension theory, etc...
that Wittgenstein's comments demonstrate a fundamental misunderstanding of the incompleteness theorems.
- "It is clear from the passages you cite that Wittgenstein did "not" understand [the first incompleteness theorem] (or pretended not to understand it). He interpreted it as a kind of logical paradox, while in fact is just the opposite, namely a mathematical theorem within an absolutely uncontroversial part of mathematics (finitary number theory or combinatorics)." (Wang 1996:197)
Since the publication of Wittgenstein's Nachlass in 2000,
a series of papers in philosophy have sought to evaluate whether the original criticism of Wittgenstein's remarks was justified. Floyd and Putnam (2000) argue that Wittgenstein had a more complete understanding of the incompleteness theorem than was previously assumed. They are particularly concerned with the interpretation of a Gödel sentence for an ω-inconsistent theory as actually saying "I am not provable", since the theory has no models in which the provability predicate corresponds to actual provability. Rodych (2003) argues that their interpretation of Wittgenstein is not historically justified, while Bays (2004) argues against Floyd and Putnam's philosophical analysis of the provability predicate. Berto (2009) explores the relationship between Wittgenstein's writing and theories of paraconsistent logic.
See also
- Gödel's completeness theoremGödel's completeness theoremGödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
- Gödel's speed-up theoremGödel's speed-up theoremIn mathematics, Gödel's speed-up theorem, proved by , shows that there are theorems whose proofs can be drastically shortened by working in more powerful axiomatic systems....
- Löb's TheoremLöb's theoremIn mathematical logic, Löb's theorem states that in a theory with Peano arithmetic, for any formula P, if it is provable that "if P is provable then P", then P is provable...
- Provability logicProvability logicProvability logic is a modal logic, in which the box operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic....
- Münchhausen Trilemma
- Non-standard model of arithmetic
- Tarski's undefinability theorem
- Minds, Machines and GödelMinds, Machines and GödelMinds, Machines and Gödel is J. R. Lucas's 1959 philosophical paper in which he argues that a human mathematician cannot be accurately represented by an algorithmic automaton...
- Third Man ArgumentThird Man ArgumentThe third man argument , first offered by Plato in his dialogue Parmenides, is a philosophical criticism of Plato's own theory of Forms...
Articles by Gödel
- 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173-98.
- 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. and On formally undecidable propositions of Principia Mathematica and related systems I in Solomon FefermanSolomon FefermanSolomon Feferman is an American philosopher and mathematician with major works in mathematical logic.He was born in New York City, New York, and received his Ph.D. in 1957 from the University of California, Berkeley under Alfred Tarski...
, ed., 1986. Kurt Gödel Collected works, Vol. I. Oxford University Press: 144-195. The original German with a facing English translation, preceded by a very illuminating introductory note by Kleene.- Hirzel, Martin, 2000, On formally undecidable propositions of Principia Mathematica and related systems I.. A modern translation by Hirzel.
- 1951, Some basic theorems on the foundations of mathematics and their implications in Solomon FefermanSolomon FefermanSolomon Feferman is an American philosopher and mathematician with major works in mathematical logic.He was born in New York City, New York, and received his Ph.D. in 1957 from the University of California, Berkeley under Alfred Tarski...
, ed., 1995. Kurt Gödel Collected works, Vol. III. Oxford University Press: 304-23.
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. BraithwaiteR. B. BraithwaiteRichard Bevan Braithwaite was an English philosopher who specialized in the philosophy of science, ethics, and the philosophy of religion. He was a lecturer in moral science at the University of Cambridge from 1934 to 1953, then Knightbridge Professor of Moral Philosophy there from 1953 to 1967...
(Introduction), 1962. On Formally Undecidable Propositions of Principia Mathematica and Related Systems, Dover Publications, New York (Dover edition 1992), ISBN 0-486-66980-7 (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 HawkingStephen HawkingStephen William Hawking, CH, CBE, FRS, FRSA is an English theoretical physicist and cosmologist, whose scientific books and public appearances have made him an academic celebrity...
editor, 2005. God Created the Integers: The Mathematical Breakthroughs That Changed History, Running Press, Philadelphia, ISBN 0-7624-1922-9. Gödel’s paper appears starting on p. 1097, with Hawking’s commentary starting on p. 1089. - Martin DavisMartin DavisMartin David Davis, is an American mathematician, known for his work on Hilbert's tenth problem . He received his Ph.D. from Princeton University in 1950, where his adviser was Alonzo Church . He is Professor Emeritus at New York University. He is the co-inventor of the Davis-Putnam and the DPLL...
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 HeijenoortJean Van HeijenoortJean Louis Maxime van Heijenoort was a pioneer historian of mathematical logic. He was also a personal secretary to Leon Trotsky from 1932 to 1939, and from then until 1947, an American Trotskyist activist.-Life:Van Heijenoort was born in Creil, France...
editor, 1967, 3rd edition 1967. From Frege to Gödel: A Source Book in Mathematical Logic, 1979-1931, Harvard University Press, Cambridge Mass., ISBN 0-674-32449-8 (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 BoolosGeorge BoolosGeorge Stephen Boolos was a philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.- Life :...
, 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 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
- Martin DavisMartin DavisMartin David Davis, is an American mathematician, known for his work on Hilbert's tenth problem . He received his Ph.D. from Princeton University in 1950, where his adviser was Alonzo Church . He is Professor Emeritus at New York University. He is the co-inventor of the Davis-Putnam and the DPLL...
, "The Incompleteness Theorem", in Notices of the AMS vol. 53 no. 4 (April 2006), p. 414. - Jean van HeijenoortJean Van HeijenoortJean Louis Maxime van Heijenoort was a pioneer historian of mathematical logic. He was also a personal secretary to Leon Trotsky from 1932 to 1939, and from then until 1947, an American Trotskyist activist.-Life:Van Heijenoort was born in Creil, France...
, 1963. "Gödel's Theorem" in Edwards, Paul, ed., Encyclopedia of Philosophy, Vol. 3. Macmillan: 348-57. - Geoffrey HellmanGeoffrey HellmanGeoffrey Hellman is an American professor and philosopher. He is Chairman of the Department of Philosophy at the University of Minnesota in Minneapolis, Minnesota.-Education:He obtained his B.A. and Ph.D...
, How to Gödel a Frege-Russell: 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 HilbertDavid HilbertDavid Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
, 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. | year=1994 | journal=Notre Dame Journal of Formal Logic | issn=0029-4527 | volume=35 | issue=3 | pages=403–412 | doi=10.1305/ndjfl/1040511346}} - Stephen Cole KleeneStephen Cole KleeneStephen Cole Kleene was an American mathematician who helped lay the foundations for theoretical computer science...
, 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. - 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, North-Holland 1982 ISBN 978-0444863881, pp. 821–866.
- Dan E. Willard (2001), "Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles", Journal of Symbolic Logic, v. 66 n. 2, pp. 536–596.
- Richard Zach, 2005, "Paper on the incompleteness theorems" in Grattan-Guinness, I.Ivor Grattan-GuinnessIvor Grattan-Guinness, born 23 June 1941, in Bakewell, in England, is a historian of mathematics and logic.He gained his Bachelor degree as a Mathematics Scholar at Wadham College, Oxford, got an M.Sc in Mathematical Logic and the Philosophy of Science at the London School of Economics in 1966...
, ed., Landmark Writings in Western Mathematics. Elsevier: 917-25.
Books about the theorems
- Francesco Berto. There's Something about Gödel: The Complete Guide to the Incompleteness Theorem John Wiley and Sons. 2010.
- Domeisen, Norbert, 1990. Logik der Antinomien. Bern: Peter Lang. 142 S. 1990. ISBN 3-261-04214-1. Zentralblatt MATH
- Torkel FranzénTorkel FranzénTorkel Franzén was a Swedish academic. He worked at the Department of Computer Science and Electrical Engineering at Luleå University of Technology, Sweden, in the fields of mathematical logic and computer science. He was known for his work on Gödel's incompleteness theorems and for his...
, 2005. Gödel's Theorem: An Incomplete Guide to its Use and Abuse. A.K. Peters. ISBN 1568812388 - Douglas HofstadterDouglas HofstadterDouglas Richard Hofstadter is an American academic whose research focuses on consciousness, analogy-making, artistic creation, literary translation, and discovery in mathematics and physics...
, 1979. Gödel, Escher, Bach: An Eternal Golden BraidGödel, Escher, BachGödel, Escher, Bach: An Eternal Golden Braid is a book by Douglas Hofstadter, described by his publishing company as "a metaphorical fugue on minds and machines in the spirit of Lewis Carroll"....
. Vintage Books. ISBN 0465026850. 1999 reprint: ISBN 0465026567. - Douglas Hofstadter, 2007. I Am a Strange LoopI Am a Strange LoopI Am a Strange Loop is a 2007 book by Douglas Hofstadter, examining in depth the concept of a strange loop originally developed in his 1979 book Gödel, Escher, Bach....
. Basic Books. ISBN 9780465030781. ISBN 0465030785. - Stanley JakiStanley JakiStanley L. Jaki, OSB was a Benedictine priest and Distinguished Professor of Physics at Seton Hall University, New Jersey since 1975...
, OSB, 2005. The drama of the quantities. Real View Books. - Per Lindström, 1997, Aspects of Incompleteness, Lecture Notes in Logic v. 10.
- J.R. Lucas, FBA, 1970. The Freedom of the Will. Clarendon Press, Oxford, 1970.
- Ernest NagelErnest NagelErnest Nagel was a Czech-American philosopher of science. Along with Rudolf Carnap, Hans Reichenbach, and Carl Hempel, he is sometimes seen as one of the major figures of the logical positivist movement....
, James Roy Newman, Douglas Hofstadter, 2002 (1958). Gödel's Proof, revised ed. ISBN 0814758169. - Rudy RuckerRudy RuckerRudolf von Bitter Rucker is an American mathematician, computer scientist, science fiction author, and philosopher, and is one of the founders of the cyberpunk literary movement. The author of both fiction and non-fiction, he is best known for the novels in the Ware Tetralogy, the first two of...
, 1995 (1982). Infinity and the Mind: The Science and Philosophy of the Infinite. Princeton Univ. Press. - 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 SmullyanRaymond SmullyanRaymond Merrill Smullyan is an American mathematician, concert pianist, logician, Taoist philosopher, and magician.Born in Far Rockaway, New York, his first career was stage magic. He then earned a BSc from the University of Chicago in 1955 and his Ph.D. from Princeton University in 1959...
, 1991. Godel's Incompleteness Theorems. Oxford Univ. Press. - —, 1994. Diagonalization and Self-Reference. Oxford Univ. Press.
- Hao Wang, 1997. A Logical Journey: From Gödel to Philosophy. MIT Press. ISBN 0262231891
Miscellaneous references
- Francesco Berto. "The Gödel Paradox and Wittgenstein's Reasons" Philosophia Mathematica (III) 17. 2009.
- John W. Dawson, JrJohn W. Dawson, JrJohn W. Dawson, Jr. is Professor of Mathematics, Emeritus at Pennsylvania State University at York. Born in Wichita, Kansas, he attended M.I.T. as a National Merit Scholar before earning a doctorate in mathematical logic from the University of Michigan in 1972...
., 1997. Logical Dilemmas: The Life and Work of Kurt Gödel, A.K. Peters, Wellesley Mass, ISBN 1-56881-256-6. - Goldstein, RebeccaRebecca GoldsteinRebecca Goldstein is an American novelist and professor of philosophy. She has written five novels, a number of short stories and essays, and biographical studies of mathematician Kurt Gödel and philosopher Baruch Spinoza....
, 2005, Incompleteness: the Proof and Paradox of Kurt Gödel, W. W. Norton & Company. ISBN 0-393-05169-2 - Juliet Floyd and Hilary Putnam, 2000, "A Note on Wittgenstein's 'Notorious Paragraph' About the Gödel Theorem", Journal of Philosophy v. 97 n. 11, pp. 624–632.
- Carl HewittCarl HewittCarl Hewitt is Board Chair of the International Society for Inconsistency Robustness. He has been a Visiting Professor at Stanford University and the University of Keio. In 2000, he became emeritus in the EECS department at MIT....
, 2008, "Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency", Coordination, Organizations, Institutions, and Norms in Agent Systems III, Springer-Verlag. - David HilbertDavid HilbertDavid Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
and Paul BernaysPaul BernaysPaul Isaac Bernays was a Swiss mathematician, who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant to, and close collaborator of, David Hilbert.-Biography:Bernays spent his childhood in Berlin. Bernays attended the...
, Grundlagen der Mathematik, Springer-Verlag. - John Hopcroft and Jeffrey Ullman 1979, Introduction to Automata theory, Addison-Wesley, ISBN 0-201-02988-X
- Stephen Cole KleeneStephen Cole KleeneStephen Cole Kleene was an American mathematician who helped lay the foundations for theoretical computer science...
, 1967, Mathematical Logic. Reprinted by Dover, 2002. ISBN 0-486-42533-9 - Graham PriestGraham PriestGraham Priest is Boyce Gibson Professor of Philosophy at the University of Melbourne and Distinguished Professor of Philosophy at the CUNY Graduate Center, as well as a regular visitor at St. Andrews University. Priest is a fellow in residence at Ormond College. He was educated at the University...
, 2006, In Contradiction: A Study of the Transconsistent, Oxford University Press, ISBN 0-199-26329-9 - Graham Priest, 1984, "Logic of Paradox Revisited", Journal of Philosophical Logic, v. 13, n. 2, pp. 153–179
- Hilary PutnamHilary PutnamHilary Whitehall Putnam is an American philosopher, mathematician and computer scientist, who has been a central figure in analytic philosophy since the 1960s, especially in philosophy of mind, philosophy of language, philosophy of mathematics, and philosophy of science...
, 1960, Minds and Machines in Sidney HookSidney HookSidney Hook was an American pragmatic philosopher known for his contributions to public debates.A student of John Dewey, Hook continued to examine the philosophy of history, of education, politics, and of ethics. After embracing Marxism in his youth, Hook was known for his criticisms of...
, ed., Dimensions of Mind: A Symposium. New York University Press. Reprinted in Anderson, A. R., ed., 1964. Minds and Machines. Prentice-Hall: 77. - Russell O'Connor, 2005, "Essential Incompleteness of Arithmetic Verified by Coq", Lecture Notes in Computer Science v. 3603, pp. 245–260.
- Victor Rodych, 2003, "Misunderstanding Gödel: New Arguments about Wittgenstein and New Remarks by Wittgenstein", Dialectica v. 57 n. 3, pp. 279–313.
- Stewart ShapiroStewart ShapiroStewart Shapiro is O'Donnell Professor of Philosophy at the Ohio State University and a regular visiting professor at the University of St Andrews in Scotland. He is an important contemporary figure in the philosophy of mathematics where he defends a version of structuralism. He studied...
, 2002, "Incompleteness and Inconsistency", Mind, v. 111, pp 817–32. - Alan SokalAlan SokalAlan David Sokal is a professor of mathematics at University College London and professor of physics at New York University. He works in statistical mechanics and combinatorics. To the general public he is best known for his criticism of postmodernism, resulting in the Sokal affair in...
and Jean BricmontJean BricmontJean Bricmont is a Belgian theoretical physicist, philosopher of science and a professor at the Université catholique de Louvain. He works on renormalization group and nonlinear differential equations....
, 1999, Fashionable NonsenseFashionable NonsenseFashionable Nonsense: Postmodern Intellectuals' Abuse of Science is a book by professors Alan Sokal and Jean Bricmont...
: Postmodern Intellectuals' Abuse of Science, Picador. ISBN 0-31-220407-8 - Joseph R. Shoenfield (1967), Mathematical Logic. Reprinted by A.K. Peters for the Association of Symbolic Logic, 2001. ISBN 978-156881135-2
- Jeremy StangroomJeremy StangroomJeremy Stangroom is a British writer, editor, and website designer. He is an editor and co-founder, with Julian Baggini, of The Philosophers’ Magazine, and has written and edited several philosophy books. He is also co-founder, with Ophelia Benson of the website 'Butterflies and Wheels'.Stangroom...
and Ophelia BensonOphelia BensonOphelia Benson is co-author of The Dictionary of Fashionable Nonsense: A Guide for Edgy People, Why Truth Matters , and Does God Hate Women?....
, Why Truth Matters, Continuum. ISBN 0-82-649528-1 - George Tourlakis, Lectures in Logic and Set Theory, Volume 1, Mathematical Logic, Cambridge University Press, 2003. ISBN 978-0-52175373-9
- Hao Wang, 1996, A Logical Journey: From Gödel to Philosophy, The MIT Press, Cambridge MA, ISBN 0-262-23189-1.
- Richard Zach, 2006, "Hilbert's program then and now", in Philosophy of Logic, Dale Jacquette (ed.), Handbook of the Philosophy of Science, v. 5., Elsevier, pp. 411–447.
External links
- Stanford Encyclopedia of PhilosophyStanford Encyclopedia of PhilosophyThe Stanford Encyclopedia of Philosophy is a freely-accessible online encyclopedia of philosophy maintained by Stanford University. Each entry is written and maintained by an expert in the field, including professors from over 65 academic institutions worldwide...
: "Kurt Gödel" -- by Juliette Kennedy. - MacTutor biographies:
- Kurt Gödel.
- Gerhard Gentzen.
- What is Mathematics:Gödel's Theorem and Around by Karlis Podnieks. An online free book.
- World's shortest explanation of Gödel's theorem using a printing machine as an example.
- October 2011 RadioLab episode about/including Gödel's Incompleteness theorem