Gödel's incompleteness theorems
gödel's incompleteness theorems, gödel's incompleteness theorems simplifiedGödel's incompleteness theorems are two theorems of mathematical logic that demonstrate the inherent limitations of every formal axiomatic system containing basic arithmetic These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible
The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure ie, an algorithm is capable of proving all truths about the arithmetic of the natural numbers For any such formal system, there will always be statements about the natural numbers that are true, but that are unprovable within the system The second incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency
Employing a diagonal argument, Gödel's incompleteness theorems were the first of several closely related theorems on the limitations of formal systems They were followed by Tarski's undefinability theorem on the formal undefinability of truth, Church's proof that Hilbert's Entscheidungsproblem is unsolvable, and Turing's theorem that there is no algorithm to solve the halting problem
Contents
 1 Formal systems: completeness, consistency, and effective axiomatization
 11 Effective axiomatization
 12 Completeness
 13 Consistency
 14 Systems which contain arithmetic
 15 Conflicting goals
 2 First incompleteness theorem
 21 Syntactic form of the Gödel sentence
 22 Truth of the Gödel sentence
 23 Relationship with the liar paradox
 24 Extensions of Gödel's original result
 3 Second incompleteness theorem
 31 Expressing consistency
 32 The Hilbert–Bernays conditions
 33 Implications for consistency proofs
 4 Examples of undecidable statements
 41 Undecidable statements provable in larger systems
 5 Relationship with computability
 6 Proof sketch for the first theorem
 61 Arithmetization of syntax
 62 Construction of a statement about "provability"
 63 Diagonalization
 64 Proof via Berry's paradox
 65 Computer verified proofs
 7 Proof sketch for the second theorem
 8 Discussion and implications
 81 Consequences for logicism and Hilbert's second problem
 82 Minds and machines
 83 Paraconsistent logic
 84 Appeals to the incompleteness theorems in other fields
 9 History
 91 Announcement
 92 Generalization and acceptance
 93 Criticisms
 931 Finsler
 932 Zermelo
 933 Wittgenstein
 10 See also
 11 Notes
 12 References
 121 Articles by Gödel
 122 Translations, during his lifetime, of Gödel's paper into English
 123 Articles by others
 124 Books about the theorems
 125 Miscellaneous references
 13 External links
Formal systems: completeness, consistency, and effective axiomatization
The incompleteness theorems apply to formal systems that are of sufficient complexity to express the basic arithmetic of the natural numbers and which are complete, consistent, and effectively axiomatized, these concepts being detailed below Particularly in the context of firstorder logic, formal systems are also called formal theories In general, a formal system is a deductive apparatus that consists of a particular set of axioms along with rules of symbolic manipulation or rules of inference that allow for the derivation of new theorems from the axioms One example of such a system is firstorder Peano arithmetic, a system in which all variables are intended to denote natural numbers In other systems, such as set theory, only some sentences of the formal system express statements about the natural numbers The incompleteness theorems are about formal provability within these systems, rather than about "provability" in an informal sense
There are several properties that a formal system may have, including completeness, consistency, and the existence of an effective axiomatization The incompleteness theorems show that systems which contain a sufficient amount of arithmetic cannot possess all three of these properties
Effective axiomatization
A formal system is said to be effectively axiomatized also called effectively generated if its set of theorems is a recursively enumerable set Franzén 2004, p 112
This means that there is a computer program that, in principle, could enumerate all the theorems of the system without listing any statements that are not theorems Examples of effectively generated theories include Peano arithmetic and Zermelo–Fraenkel set theory ZFC
The theory known as true arithmetic consists of all true statements about the standard integers in the language of Peano arithmetic This theory is consistent, and complete, and contains a sufficient amount of arithmetic However it does not have a recursively enumerable set of axioms, and thus does not satisfy the hypotheses of the incompleteness theorems
Completeness
A set of axioms is syntactically, or negation complete if, for any statement in the axioms' language, that statement or its negation is provable from the axioms Smith 2007, p 24 This is the notion relevant for Gödel's first Incompleteness theorem It is not to be confused with semantic completeness, which means that the set of axiom proves all the semantic tautologies of the given language In his completeness theorem, Gödel proved that first order logic is semantically complete But it is not syntactically complete, since there are sentences expressible in the language of first order logic that can be neither proved nor disproved from the axioms of logic alone: for example, "the flower is pretty"
In a mere system of logic it would be absurd to expect syntactic completeness But in a system of mathematics, thinkers such as Hilbert had believed that it is just a matter of time to find such an axiomatization that would allow to either prove or disprove by proving its negation each and every mathematical formula
A formal system might be syntactically incomplete by design: such as logics generally are Or it may be incomplete simply because not all the necessary axioms have been discovered or included For example, Euclidean geometry without the parallel postulate is incomplete, because it is not possible to prove or disprove the parallel postulate from the remaining axioms Similarly, the theory of dense linear orders is not complete, but becomes complete with an extra axiom stating that there are no endpoints in the order The continuum hypothesis is a statement in the language of ZFC that is not provable within ZFC, so ZFC is not complete In this case, there is no obvious candidate for a new axiom that resolves the issue
The theory of firstorder Peano arithmetic is consistent, has an infinite but recursively enumerable set of axioms, and can encode enough arithmetic for the hypotheses of the incompleteness theorem Thus, by the first incompleteness theorem, Peano Arithmetic is not complete The theorem gives an explicit example of a statement of arithmetic that is neither provable nor disprovable in Peano's arithmetics Moreover, this statement is true in the usual model Moreover, no effectively axiomatized, consistent extension of Peano arithmetic can be complete
Consistency
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, and inconsistent otherwise
Peano arithmetic is provably consistent from ZFC, but not from within itself Similarly, ZFC is not provably consistent from within itself, but ZFC + "there exists an inaccessible cardinal" proves ZFC is consistent because if κ is the least such cardinal, then Vκ sitting inside the von Neumann universe is a model of ZFC, and a theory is consistent if and only if it has a model
If one takes all statements in the language of Peano arithmetic as axioms, then this theory is complete, has a recursively enumerable set of axioms, and can describe addition and multiplication However, it is not consistent
Additional examples of inconsistent theories arise from the paradoxes that result when the axiom schema of unrestricted comprehension is assumed in set theory
Systems which contain arithmetic
The incompleteness theorems apply only to formal systems which are able to prove a sufficient collection of facts about the natural numbers One sufficient collection is the set of theorems of Robinson arithmetic Q Some systems, such as Peano arithmetic, can directly express statements about natural numbers Others, such as ZFC set theory, are able to interpret statements about natural numbers into their language Either of these options is appropriate for the incompleteness theorems
The theory of algebraically closed fields of a given characteristic is complete, consistent, and has an infinite but recursively enumerable set of axioms However it is not possible to encode the integers into this theory, and the theory cannot describe arithmetic of integers A similar example is the theory of real closed fields, which is essentially equivalent to Tarski's axioms for Euclidean geometry So Euclidean geometry itself in Tarski's formulation is an example of a complete, consistent, effectively axiomatized theory
The system of Presburger arithmetic consists of a set of axioms for the natural numbers with just the addition operation multiplication is omitted Presburger arithmetic is complete, consistent, and recursively enumerable and can encode addition but not multiplication of natural numbers, showing that for Gödel's theorems one needs the theory to encode not just addition but also multiplication
Dan Willard 2001 has studied some weak families of arithmetic systems which allow enough arithmetic as relations to formalise Gödel numbering, but which are not strong enough to have multiplication as a function, and so fail to prove the second incompleteness theorem; these systems are consistent and capable of proving their own consistency see selfverifying theories
Conflicting goals
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 For example, we could imagine a set of true axioms which allow us to prove every true arithmetical claim about the natural numbers Smith 2007, p 2 In the standard system of firstorder logic, an inconsistent set of axioms will prove every statement in its language this is sometimes called the principle of explosion, and is thus automatically complete A set of axioms that is both complete and consistent, however, proves a maximal set of noncontradictory theorems Hinman 2005, p 143
The pattern illustrated in the previous sections with Peano arithmetic, ZFC, and ZFC + "there exists an inaccessible cardinal" cannot generally be broken Here ZFC + "there exists an inaccessible cardinal" cannot from itself, be proved consistent It is also not complete, as illustrated by the in ZFC + "there exists an inaccessible cardinal" theory unresolved continuum hypothesis
The first incompleteness theorem shows that, in formal systems that can express basic arithmetic, a complete and consistent finite list of axioms can never be created: each time an additional, consistent statement is added as an axiom, there are other true statements that still cannot be proved, even with the new axiom If an axiom is ever added that makes the system complete, it does so at the cost of making the system inconsistent It is not even possible for an infinite list of axioms to be complete, consistent, and effectively axiomatized
First incompleteness theorem
Gödel's first incompleteness theorem first appeared as "Theorem VI" in Gödel's 1931 paper On Formally Undecidable Propositions of Principia Mathematica and Related Systems I The hypotheses of the theorem were improved shortly thereafter by J Barkley Rosser 1936 using Rosser's trick
The resulting theorem incorporating Rosser's improvement may be paraphrased in English as follows, where "formal system" includes the assumption that the system is effectively generated
First Incompleteness Theorem: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; ie, there are statements of the language of F which can neither be proved nor disproved in F" Raatikainen 2015
The unprovable statement GF referred to by the theorem is often referred to as "the Gödel sentence" for the system F The proof constructs a particular Gödel sentence for the system F, but there are infinitely many statements in the language of the system that share the same properties, such as the conjunction of the Gödel sentence and any logically valid sentence
Each effectively generated system has its own Gödel sentence It is possible to define a larger system F’ that contains the whole of F plus GF as an additional axiom This will not result in a complete system, because Gödel's theorem will also apply to F’, and thus F’ also cannot be complete In this case, GF is indeed a theorem in F’, because it is an axiom Because GF states only that it is not provable in F, no contradiction is presented by its provability within F’ However, because the incompleteness theorem applies to F’, there will be a new Gödel statement GF′ for F’, showing that F’ is also incomplete GF′ will differ from GF in that GF′ will refer to F’, rather than F
Syntactic form of the Gödel sentence
The Gödel sentence is designed to refer, indirectly, to itself The sentence states that, when a particular sequence of steps is used to construct another sentence, that constructed sentence will not be provable in F However, the sequence of steps is such that the constructed sentence turns out to be GF itself In this way, the Gödel sentence GF indirectly states its own unprovability within F Smith 2007, p 135
To prove the first incompleteness theorem, Gödel demonstrated that the notion of provability within a system could be expressed purely in terms of arithmetical functions that operate on Gödel numbers of sentences of the system Therefore, the system, which can prove certain facts about numbers, can also indirectly prove facts about its own statements, provided that it is effectively generated Questions about the provability of statements within the system are represented as questions about the arithmetical properties of numbers themselves, which would be decidable by the system if it were complete
Thus, although the Gödel sentence refers indirectly to sentences of the system F, the Gödel sentence is actually written as a statement about natural numbers solely It asserts that no natural number has a particular property, where that property is given by a primitive recursive relation Smith 2007, p 141 As such, the Gödel sentence can be written in the language of arithmetic with a simple syntactic form In particular, it can be expressed as formula consisting of a number of leading universal quantifiers followed by a quantifierfree body these formulas are at level Π 1 0 ^ of the arithmetical hierarchy Via the MRDP theorem, the Gödel sentence can be rewritten as a statement that a particular polynomial in many variables with integer coefficients never takes the value zero when integers are substituted for its variables Franzén 2005, p 71
Truth of the Gödel sentence
The first incompleteness theorem shows that the Gödel sentence GF of an appropriate formal theory F is unprovable in F Because this unprovability is exactly what the sentence indirectly asserts, the Gödel sentence is, in fact, true Smoryński 1977 p 825; also see Franzén 2004 pp 28–33 For this reason, the sentence GF is often said to be "true but unprovable" Raatikainen 2015 The truth of the sentence GF may only be arrived at via a metaanalysis from outside the system In general, this metaanalysis can be carried out within the weak formal system known as primitive recursive arithmetic, which proves the implication ConF→GF, where ConF is a canonical sentence asserting the consistency of F Smoryński 1977 p 840, Kikuchi and Tanaka 1994 p 403
Although the Gödel sentence of a consistent theory is true as a statement about the intended interpretation of arithmetic, the Gödel sentence will be false in some nonstandard models of arithmetic, as a consequence of Gödel's completeness theorem Franzén 2005, p 135 That theorem shows that, when a sentence is independent of a theory, the theory will have models in which the sentence is true and models in which the sentence is false As described earlier, the Gödel sentence of a system F is an arithmetical statement which claims that no number exists with a particular property The incompleteness theorem shows that this claim will be independent of the system F, and the truth of the Gödel sentence follows from the fact that no standard natural number has the property in question Any model of in which the Gödel sentence is false must contain some element which satisfies the property within that model Such a model must be "nonstandard" – it must contain elements that do not correspond to any standard natural number Raatikainen 2015, Franzén 2005, p 135
Relationship with the liar paradox
Gödel specifically cites Richard's paradox and the liar paradox as semantical analogues to his syntactical incompleteness result in the introductory section of On Formally Undecidable Propositions in Principia Mathematica and Related Systems I The liar paradox is the sentence "This sentence is false" An analysis of the liar sentence shows that it cannot be true for then, as it asserts, it is false, nor can it be false for then, it is true A Gödel sentence G for a system F makes a similar assertion to the liar sentence, but with truth replaced by provability: G says "G is not provable in the system F" 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 both by Gödel, when he was working on the proof of the incompleteness theorem, and by the theorem's namesake, Alfred Tarski
Extensions of Gödel's original result
Compared to the theorems stated in Gödel's 1931 paper, many contemporary statements of the incompleteness theorems are more general in two ways These generalized statements are phrased to apply to a broader class of systems, and they are phrased to incorporate weaker consistency assumptions
Gödel demonstrated the incompleteness of the system of Principia Mathematica, a particular system of arithmetic, but a parallel demonstration could be given for any effective system 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 system 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 system is not just consistent but ωconsistent A system is ωconsistent if it is not ωinconsistent, and is ωinconsistent if there is a predicate P such that for every specific natural number m the system proves ~Pm, and yet the system also proves that there exists a natural number n such that Pn That is, the system says that a number with property P exists while denying that it has any specific value The ωconsistency of a system 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 system to be consistent, rather than ωconsistent This is mostly of technical interest, because 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
For each formal system F containing basic arithmetic, it is possible to canonically define a formula ConsF expressing the consistency of F This formula expresses the property that "there does not exist a natural number coding a formal derivation within the system F whose conclusion is a syntactic contradiction" The syntactic contradiction is often taken to be "0=1", in which case ConsF states "there is no natural number that codes a derivation of '0=1' from the axioms of F"
Gödel's second incompleteness theorem shows that, under general assumptions, this canonical consistency statement ConsF will not be provable in F The theorem first appeared as "Theorem XI" in Gödel's 1931 paper On Formally Undecidable Propositions in Principia Mathematica and Related Systems I In the following statement, the term "formalized system" also includes an assumption that F is effectively axiomatized
Second Incompleteness Theorem: "Assume F is a consistent formalized system which contains elementary arithmetic Then F ⊬ Cons F F " Raatikainen 2015
This theorem is stronger than the first incompleteness theorem because the statement constructed in the first incompleteness theorem does not directly express the consistency of the system The proof of the second incompleteness theorem is obtained by formalizing the proof of the first incompleteness theorem within the system F itself
Expressing consistency
There is a technical subtlety in the second incompleteness theorem regarding the method of expressing the consistency of F as a formula in the language of F There are many ways to express the consistency of a system, and not all of them lead to the same result The formula ConsF from the second incompleteness theorem is a particular expression of consistency
Other formalizations of the claim that F is consistent may be inequivalent in F, and some may even be provable For example, firstorder Peano arithmetic PA can prove that "the largest consistent subset of PA" is consistent But, because 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 meant here to be the largest consistent initial segment of the axioms of PA under some particular effective enumeration
The Hilbert–Bernays conditions
The standard proof of the second incompleteness theorem assumes that the provability predicate ProvAP satisfies the Hilbert–Bernays provability conditions Letting #P represent the Gödel number of a formula P, the derivability conditions say:
 If F proves P, then F proves ProvA#P
 F proves 1; that is, F proves that if F proves P, then F proves ProvA#P In other words, F proves that ProvA#P implies ProvA#ProvA#P
 F proves that if F proves that P → Q and F proves P then F proves Q In other words, F proves that ProvA#P → Q and ProvA#P imply ProvA#Q
There are systems, such as Robinson arithmetic, which are strong enough to meet the assumptions of the first incompleteness theorem, but which do not prove the Hilbert—Bernays conditions Peano arithmetic, however, is strong enough to verify these conditions, as are all theories stronger than Peano arithmetic
Implications for consistency proofs
Gödel's second incompleteness theorem also implies that a system F1 satisfying the technical conditions outlined above cannot prove the consistency of any system F2 that proves the consistency of F1 This is because such a system T1 can prove that if F2 proves the consistency of F1, then F1 is in fact consistent For the claim that F1 is consistent has form "for all numbers n, n has the decidable property of not being a code for a proof of contradiction in F1" If F1 were in fact inconsistent, then F2 would prove for some n that n is the code of a contradiction in F1 But if F2 also proved that F1 is consistent that is, that there is no such n, then it would itself be inconsistent This reasoning can be formalized in F1 to show that if F2 is consistent, then F1 is consistent Since, by second incompleteness theorem, F1 does not prove its consistency, it cannot prove the consistency of F2 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 system the consistency of which is provable in Peano arithmetic PA For example, the system 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 Franzén 2004, p 106
The corollary also indicates the epistemological relevance of the second incompleteness theorem It would actually provide no interesting information if a system F proved its consistency This is because inconsistent theories prove everything, including their consistency Thus a consistency proof of F in F would give us no clue as to whether F really is consistent; no doubts about the consistency of F would be resolved by such a consistency proof The interest in consistency proofs lies in the possibility of proving the consistency of a system F in some system F’ that is in some sense less doubtful than F itself, for example weaker than F For many naturally occurring theories F and F’, such as F = Zermelo–Fraenkel set theory and F’ = primitive recursive arithmetic, the consistency of F’ is provable in F, and thus F’ cannot prove the consistency of F by the above corollary of the second incompleteness theorem
The second incompleteness theorem does not rule out consistency proofs altogether, only consistency proofs that can be formalized in the system that is proved consistent For example, Gerhard Gentzen proved the consistency of Peano arithmetic in a different system that 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
Examples of undecidable statements
See also: List of statements independent of ZFCThere are two distinct senses of the word "undecidable" in mathematics and computer science The first of these is the prooftheoretic sense used in relation to Gödel's theorems, that of a statement being neither provable nor refutable in a specified deductive system The second sense, which will not be discussed here, is used in relation to computability theory and applies not to statements but to decision problems, which are countably infinite sets of questions each requiring a yes or no answer Such a problem is said to be undecidable if there is no computable function that correctly answers every question in the problem set see undecidable problem
Because of the two meanings of the word undecidable, the term independent is sometimes used instead of undecidable for the "neither provable nor refutable" sense
Undecidability of a statement in a particular deductive system does not, in and of itself, address the question of whether the truth value of the statement is welldefined, or whether it can be determined by other means Undecidability only implies that the particular deductive system being considered does not prove the truth or falsity of the statement Whether there exist socalled "absolutely undecidable" statements, whose truth value can never be known or is illspecified, is a controversial point in the philosophy of mathematics
The combined work of Gödel and Paul Cohen has given two concrete examples of undecidable statements in the first sense of the term: The continuum hypothesis can neither be proved nor refuted in ZFC the standard axiomatization of set theory, and the axiom of choice can neither be proved nor refuted in ZF which is all the ZFC axioms except the axiom of choice These results do not require the incompleteness theorem Gödel proved in 1940 that neither of these statements could be disproved in ZF or ZFC set theory In the 1960s, Cohen proved that neither is provable from ZF, and the continuum hypothesis cannot be proved from ZFC
In 1973, Saharon Shelah showed that the Whitehead problem in group theory is undecidable, in the first sense of the term, in standard set theory
Gregory Chaitin produced undecidable statements in algorithmic information theory and proved another incompleteness theorem in that setting Chaitin's incompleteness theorem states that for any system that can represent enough arithmetic, there is an upper bound c such that no specific number can be proved in that system 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
Undecidable statements provable in larger systems
These are natural mathematical equivalents of the Gödel "true but undecidable" sentence They can be proved in a larger system which is generally accepted as a valid form of reasoning, but are undecidable in a more limited system such as Peano Arithmetic
In 1977, Paris and Harrington proved that the Paris–Harrington principle, a version of the infinite Ramsey theorem, is undecidable in firstorder Peano arithmetic, but can be proved in the stronger system of secondorder arithmetic Kirby and Paris later showed that Goodstein's theorem, a statement about sequences of natural numbers somewhat simpler than the Paris–Harrington principle, is also 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 based on a philosophy of mathematics called predicativism The related but more general graph minor theorem 2003 has consequences for computational complexity theory
Relationship with computability
See also: Halting problem § Relationship with Gödel's incompleteness theoremsThe incompleteness theorem is closely related to several results about undecidable sets in recursion theory
Stephen Cole Kleene 1943 presented a proof of Gödel's incompleteness theorem using basic results of computability theory One such result shows that the halting problem is undecidable: there is no computer program that can correctly determine, given any program P as input, whether P eventually halts when run with a particular given input Kleene showed that the existence of a complete effective system 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 2004, 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 px1, 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 system of arithmetic T will prove this Moreover, if the system T is ωconsistent, then it will never prove that a particular 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 determine algorithmically 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 Moreover, for each consistent effectively generated system T, it is possible to effectively generate a multivariate polynomial p over the integers such that the equation p = 0 has no solutions over the integers, but the lack of solutions cannot be proved in T Davis 2006:416, Jones 1980
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
Proof sketch for the first theorem
Main article: Proof sketch for Gödel's first incompleteness theoremThis section may require cleanup to meet Wikipedia's quality standards The specific problem is: copyedit heavily and use standard terminology August 2016 Learn how and when to remove this template message 
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 selfreferential and essentially says that it ie the statement itself is unprovable This is done using a technique called "diagonalization" socalled because of its origins as Cantor's diagonal argument
 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 somehow have to 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 syntax in such a way that "proving a statement" can be replaced with "testing whether a number has a given property" This allows a selfreferential 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:
 The word HELLO is represented by 7269767679 using decimal ASCII, ie the number 7269767679
 The logical statement x=y => y=x is represented by 120061121032061062032121061120 using octal ASCII, 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 that 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 Fx that contains exactly one free variable x is called a statement form or classsign As soon as x is replaced by a specific number, the statement form turns into a bona fide statement, and it is then either provable in the system, or not For certain formulas one can show that for every natural number n, Fn is true if and only if it can be proved 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 Fx can be assigned a Gödel number denoted by GF The choice of the free variable used in the form Fx is not relevant to the assignment of the Gödel number GF
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 Bewy that uses this arithmetical relation to state that a Gödel number of a proof of y exists:
Bewy = ∃ 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 yThe 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 "Bewy" 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 Bewy is that if a statement p is provable in the system then BewGp is also provable This is because any proof of p would have a corresponding Gödel number, the existence of which causes BewGp to be satisfied
Diagonalization
The next step in the proof is to obtain a statement which, indirectly, asserts its own unprovability Although Gödel constructed this statement directly, the existence of at least one such statement follows from the diagonal lemma, which says that for any sufficiently strong formal system and any statement form F there is a statement p such that the system proves
p ↔ FGpBy letting F be the negation of Bewx, we obtain the theorem
p ↔ ~BewGpand the p defined by this 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 ~BewGp; 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 unprovableThis 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 indirectly asserts its own unprovability The proof of the diagonal lemma employs a similar method
Now, assume that the axiomatic system is ωconsistent, and let p be the statement obtained in the previous section
If p were provable, then BewGp would be provable, as argued above But p asserts the negation of BewGp 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 BewGp would be provable because p was constructed to be equivalent to the negation of BewGp However, for each specific number x, x cannot be the Gödel number of the proof of p, because p is not provable from the previous paragraph Thus on one hand the system proves there is a number with a certain property that it is the Gödel number of the proof of p, but on the other hand, for every specific number x, we can prove that it does not have this property This is impossible in an ωconsistent system Thus the negation of p is not provable
Thus the statement p is undecidable in our axiomatic system: it can neither be proved nor disproved within the system
In fact, to show that p is not provable only requires the assumption that the system is consistent The stronger assumption of ωconsistency is required to show that the negation of p is not provable Thus, if p is constructed for a particular system:
 If the system is ωconsistent, it can prove neither p nor its negation, and so p is undecidable
 If the system is consistent, it may have the same situation, or it may prove the negation of p In the later case, we have a statement "not p" which is false but provable, and the system is not ωconsistent
If one tries to "add the missing axioms" to avoid the incompleteness of the system, then one has to add either p or "not p" as axioms But then the definition of "being a Gödel number of a proof" of a statement changes which means that the formula Bewx is now different Thus when we apply the diagonal lemma to this new Bew, we obtain a new statement p, different from the previous one, which will be undecidable in the new system if it is ωconsistent
Proof via Berry's paradox
George Boolos 1989 sketches an alternative proof of the first incompleteness theorem that uses Berry's paradox rather than the liar paradox to construct a true but unprovable formula A similar proof method was independently discovered by Saul Kripke Boolos 1998, p 383 Boolos's proof proceeds by constructing, for any computably enumerable set S of true sentences of arithmetic, another sentence which is true but not contained in S This gives the first incompleteness theorem as a corollary According to Boolos, this proof is interesting because it provides a "different sort of reason" for the incompleteness of effective, consistent theories of arithmetic Boolos 1998, p 388
Computer verified proofs
See also: Automated theorem provingThe incompleteness theorems are among a relatively small number of nontrivial theorems that have been transformed into formalized theorems that can be completely verified by proof assistant software Gödel's original proofs of the incompleteness theorems, like most mathematical proofs, were written in natural language intended for human readers
Computerverified proofs of versions of the first incompleteness theorem were announced by Natarajan Shankar in 1986 using Nqthm Shankar 1994, by Russell O'Connor in 2003 using Coq O'Connor 2005 and by John Harrison in 2009 using HOL Light Harrison 2009 A computerverified proof of both incompleteness theorems was announced by Lawrence Paulson in 2013 using Isabelle Paulson 2014
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 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 proved 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 Pp" can be proved in the system
But this last statement is equivalent to p itself and this equivalence can be proved in the system, so p can be proved in the system This contradiction shows that the system must be inconsistent
Discussion and implications
The incompleteness results affect the philosophy of mathematics, particularly versions of formalism, which use a single system of formal logic to define their principles
Consequences for logicism and Hilbert's second problem
The incompleteness theorem is sometimes thought to have severe consequences for the program of logicism proposed by Gottlob Frege and Bertrand Russell, which aimed to define the natural numbers in terms of logic Hellman 1981, p 451–468 Bob Hale and Crispin Wright argue that it is not a problem for logicism because the incompleteness theorems apply equally to first 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
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"
Minds and machines
Main article: Mechanism philosophy § Gödelian argumentsAuthors including the philosopher J R Lucas and physicist Roger Penrose 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"
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 logic 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 system within the language of the system Priest 2006:47 Stewart Shapiro 2002 gives a more mixed appraisal of the applications of Gödel's theorems to dialetheism
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 Several authors have commented negatively on such extensions and interpretations, including Torkel Franzén 2004; Alan Sokal and Jean Bricmont 1999; and Ophelia Benson and Jeremy Stangroom 2006 Bricmont and Stangroom 2006, p 10, for example, quote from Rebecca Goldstein's comments on the disparity between Gödel's avowed Platonism and the antirealist uses to which his ideas are sometimes put Sokal and Bricmont 1999, p 187 criticize Régis Debray's invocation of the theorem in the context of sociology; Debray has defended this use as metaphorical ibid
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 habilitation 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 secondorder 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 system 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 nonprovability 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
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 onehour 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 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 system 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 for firstorder 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
Criticisms
Finsler
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 to 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
Zermelo
In September 1931, Ernst Zermelo 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 10page letter Dawson:76, GrattanGuinness:512513, where he pointed out that Zermelo mistakenly assumed that the notion of truth in a system is definable in that system which is not true in general by Tarski's undefinability theorem But Zermelo did not relent and published his criticisms in print with "a rather scathing paragraph on his young competitor" GrattanGuinness: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 firstorder logic, with which he hoped to show both the consistency and categoricity of mathematical theories
Wittgenstein
Ludwig Wittgenstein wrote several passages about the incompleteness theorems that were published posthumously in his 1953 Remarks on the Foundations of Mathematics, in particular one section sometimes called the "notorious paragraph" where he seems to confuse the notions of "true" and "provable" in Russell's system Gödel was a member of the Vienna Circle during the period in which Wittgenstein's early ideal language philosophy and Tractatus LogicoPhilosophicus dominated the circle's thinking There has been some controversy about whether Wittgenstein misunderstood the incompleteness theorem or just expressed himself unclearly Writings in Gödel's Nachlass express the belief that Wittgenstein misread his ideas
Multiple commentators have read Wittgenstein as misunderstanding Gödel Rodych 2003, although Juliet Floyd and Hilary Putnam 2000, as well as Graham Priest 2004 have provided textual readings arguing that most 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 stated: "Has Wittgenstein lost his mind Does he mean it seriously He intentionally utters trivially nonsensical statements" Wang 1996:179, and wrote to Karl Menger that Wittgenstein's comments demonstrate a misunderstanding of the incompleteness theorems writing:
"It is clear from the passages you cite that Wittgenstein did not understand 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:179Since 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 system as actually saying "I am not provable", since the system 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
 Logic portal
 Mathematics portal
 Gödel's completeness theorem
 Gödel's speedup theorem
 Gödel, Escher, Bach
 Löb's Theorem
 Minds, Machines and Gödel
 Münchhausen trilemma
 Nonstandard model of arithmetic
 Proof theory
 Provability logic
 Quining
 Tarski's undefinability theorem
 Theory of everything#Gödel's incompleteness theorem
 Third Man Argument
Notes
 ^ Gödel's words are: " my proof is applicable to every formal system containing arithmetic", appearing in Letter 3 Gödel to Nagel dated March 14, 1957; page 147 in Kurt Gödel, 2003 and 2014, "Collected Works Volume V: Correspondence HV", Clarendon Press, Oxford UK, ISBN 9780191003776 Also cf introductory comments written by Charles Parsons and Wilfried Seig page 136
 ^ The Roman numeral "I" indicates that Gödel intended to publish a sequel but "The prompt acceptance of his results was one of the reasons that made him change his plan", cf the text and its footnote 68a in van Heijenoort 1967:616
References
Articles by Gödel
 Kurt Gödel, 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I", Monatshefte für Mathematik und Physik, v 38 n 1, pp 173–198
 —, 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I", in Solomon Feferman, ed, 1986 Kurt Gödel Collected works, Vol I Oxford University Press, pp 144–195 ISBN 9780195147209 The original German with a facing English translation, preceded by an introductory note by Stephen Cole Kleene
 —, 1951, "Some basic theorems on the foundations of mathematics and their implications", in Solomon Feferman, ed, 1995 Kurt Gödel Collected works, Vol III, Oxford University Press, pp 304–323 ISBN 9780195147223
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 agreed to its publication" ibid In a footnote Dawson states that "he would regret his compliance, for the published volume was marred throughout by sloppy typography and numerous misprints" ibid Dawson states that "The translation that Gödel favored was that by Jean van Heijenoort" ibid For the serious student another version exists as a set of lecture notes recorded by Stephen Kleene and J B Rosser "during lectures given by Gödel at to the Institute for Advanced Study during the spring of 1934" cf commentary by Davis 1965:39 and beginning on p 41; this version is titled "On Undecidable Propositions of Formal Mathematical Systems" In their order of publication:
 B Meltzer translation and R B Braithwaite Introduction, 1962 On Formally Undecidable Propositions of Principia Mathematica and Related Systems, Dover Publications, New York Dover edition 1992, ISBN 0486669807 pbk This contains a useful translation of Gödel's German abbreviations on pp 33–34 As noted above, typography, translation and commentary is suspect Unfortunately, this translation was reprinted with all its suspect content by
 Stephen Hawking editor, 2005 God Created the Integers: The Mathematical Breakthroughs That Changed History, Running Press, Philadelphia, ISBN 0762419229 Gödel's paper appears starting on p 1097, with Hawking's commentary starting on p 1089
 Martin Davis editor, 1965 The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable problems and Computable Functions, Raven Press, New York, no ISBN Gödel's paper begins on page 5, preceded by one page of commentary
 Jean van Heijenoort editor, 1967, 3rd edition 1967 From Frege to Gödel: A Source Book in Mathematical Logic, 18791931, Harvard University Press, Cambridge Mass, ISBN 0674324498 pbk van Heijenoort did the translation He states that "Professor Gödel approved the translation, which in many places was accommodated to his wishes" p 595 Gödel's paper begins on p 595; van Heijenoort's commentary begins on p 592
 Martin Davis editor, 1965, ibid "On Undecidable Propositions of Formal Mathematical Systems" A copy with Gödel's corrections of errata and Gödel's added notes begins on page 41, preceded by two pages of Davis's commentary Until Davis included this in his volume this lecture existed only as mimeographed notes
Articles by others
 George Boolos, 1989, "A New Proof of the Gödel Incompleteness Theorem", Notices of the American Mathematical Society, v, 36, pp 388–390 and p 676, reprinted in Boolos, 1998, Logic, Logic, and Logic, Harvard Univ Press ISBN 0674537661
 Bernd Buldt, 2014, "The Scope of Gödel's First Incompleteness Theorem", Logica Universalis, v 8, pp 499–552 doi:101007/s1178701401073
 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 Davis, 2006, "The Incompleteness Theorem", Notices of the AMS, v 53 n 4, pp 414
 Jean van Heijenoort, 1963, "Gödel's Theorem" in Edwards, Paul, ed, Encyclopedia of Philosophy, v 3 Macmillan, pp 348–57
 Geoffrey Hellman, 1981, "How to Gödel a FregeRussell: Gödel's Incompleteness Theorems and Logicism", Noûs, v 15 n 4, Special Issue on Philosophy of Mathematics, pp 451–468
 David Hilbert, 1900, "Mathematical Problems" English translation of a lecture delivered before the International Congress of Mathematicians at Paris, containing Hilbert's statement of his Second Problem
 Martin Hirzel, 2000, On formally undecidable propositions of Principia Mathematica and related systems I An English translation of Gödel's paper
 Makoto Kikuchi and Kazayuki Tanaka, 1994, "On formalization of modeltheoretic proofs of Gödel's theorems",Notre Dame Journal of Formal Logic, v 5 n 3, pp 403–412 doi:101305/ndjfl/1040511346 MR 1326122
 Stephen Cole Kleene, 1943, "Recursive predicates and quantifiers", reprinted from Transactions of the American Mathematical Society, v 53 n 1, pp 41–73 in Martin Davis 1965, The Undecidable loc cit pp 255–287
 Panu Raatikainen, 2015, "Gödel's Incompleteness Theorems", Stanford Encyclopedia of Philosophy Accessed April 3, 2015
 John Barkley Rosser, 1936, "Extensions of some theorems of Gödel and Church", reprinted from the Journal of Symbolic Logic, v 1 1936 pp 87–91, in Martin Davis 1965, The Undecidable loc cit pp 230–235
 —, 1939, "An Informal Exposition of proofs of Gödel's Theorem and Church's Theorem", Reprinted from the Journal of Symbolic Logic, v 4 1939 pp 53–60, in Martin Davis 1965, The Undecidable loc cit pp 223–230
 C Smoryński, 1982, "The incompleteness theorems", in Jon Barwise, ed, Handbook of Mathematical Logic, NorthHolland, pp 821–866 ISBN 9780444863881
 Dan E Willard, 2001, "SelfVerifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles", Journal of Symbolic Logic, v 66 n 2, pp 536–596 doi:102307/2695030
 Richard Zach, 2003 "The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program" Synthese, v 137 n 1, pp 211–259 doi:101023/A:1026247421383
 —, 2005, "Kurt Gödel, Paper on the incompleteness theorems" in Ivor GrattanGuinness, ed Landmark Writings in Western Mathematics, Elsevier, pp 917–925 doi:101016/B9780444508713/501522
Books about the theorems
 Francesco Berto There's Something about Gödel: The Complete Guide to the Incompleteness Theorem John Wiley and Sons 2010
 Norbert Domeisen, 1990 Logik der Antinomien Bern: Peter Lang 142 S 1990 ISBN 3261042141 Zentralblatt MATH
 Torkel Franzén, 2004 Gödel's Theorem: An Incomplete Guide to its Use and Abuse AK Peters ISBN 1568812388 MR 2007d:03001
 Douglas Hofstadter, 1979 Gödel, Escher, Bach: An Eternal Golden Braid Vintage Books ISBN 0465026850 1999 reprint: ISBN 0465026567 MR 80j:03009
 —, 2007 I Am a Strange Loop Basic Books ISBN 9780465030781 ISBN 0465030785 MR 2008g:00004
 Stanley Jaki, OSB, 2005 The drama of the quantities Real View Books
 Per Lindström, 1997 Aspects of Incompleteness, Lecture Notes in Logic v 10
 JR Lucas, FBA, 1970 The Freedom of the Will Clarendon Press, Oxford, 1970
 Ernest Nagel, James Roy Newman, Douglas Hofstadter, 2002 1958 Gödel's Proof, revised ed ISBN 0814758169 MR 2002i:03001
 Rudy Rucker, 1995 1982 Infinity and the Mind: The Science and Philosophy of the Infinite Princeton Univ Press MR 84d:03012
 Peter Smith, 2007 An Introduction to Gödel's Theorems Cambridge University Press MathSciNet
 N Shankar, 1994 Metamathematics, Machines and Gödel's Proof, Volume 38 of Cambridge tracts in theoretical computer science ISBN 0521585333
 Raymond Smullyan, 1987 Forever Undecided ISBN 0192801414  puzzles based on undecidability in formal systems
 —, 1991 Godel's Incompleteness Theorems Oxford Univ Press
 —, 1994 Diagonalization and SelfReference Oxford Univ Press MR 96c:03001
 —, 2013 The Godelian Puzzle Book: Puzzles, Paradoxes and Proofs Courier Corporation ISBN 9780486497051
 Hao Wang, 1997 A Logical Journey: From Gödel to Philosophy MIT Press ISBN 0262231891 MR 97m:01090
Miscellaneous references
 Francesco Berto, 2009, "The Gödel Paradox and Wittgenstein's Reasons" Philosophia Mathematica III 17
 John W Dawson, Jr, 1997 Logical Dilemmas: The Life and Work of Kurt Gödel, A K Peters, Wellesley Mass, ISBN 1568812566
 Rebecca Goldstein, 2005, Incompleteness: the Proof and Paradox of Kurt Gödel, W W Norton & Company ISBN 0393051692
 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
 John Harrison, 2009, "Handbook of Practical Logic and Automated Reasoning", Cambridge University Press, ISBN 0521899575
 David Hilbert and Paul Bernays, Grundlagen der Mathematik, SpringerVerlag
 John Hopcroft and Jeffrey Ullman 1979, Introduction to Automata Theory, Languages, and Computation, AddisonWesley, ISBN 020102988X
 James P Jones, Undecidable Diophantine Equations, Bulletin of the American Mathematical Society, v 3 n 2, 1980, pp 859–862
 Stephen Cole Kleene, 1967, Mathematical Logic Reprinted by Dover, 2002 ISBN 0486425339
 Russell O'Connor, 2005, "Essential Incompleteness of Arithmetic Verified by Coq", Lecture Notes in Computer Science v 3603, pp 245–260
 Lawrence Paulson, 2013, "A machineassisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets", Review of Symbolic Logic, v 7 n 3, 484–498
 Graham Priest, 1984, "Logic of Paradox Revisited", Journal of Philosophical Logic, v 13,` n 2, pp 153–179
 —, 2004, Wittgenstein's Remarks on Gödel's Theorem in Max Kölbel, ed, Wittgenstein's lasting significance, Psychology Press, pp 207–227
 —, 2006, In Contradiction: A Study of the Transconsistent, Oxford University Press, ISBN 0199263299
 Hilary Putnam, 1960, Minds and Machines in Sidney Hook, ed, Dimensions of Mind: A Symposium New York University Press Reprinted in Anderson, A R, ed, 1964 Minds and Machines PrenticeHall: 77
 Wolfgang Rautenberg, 2010, A Concise Introduction to Mathematical Logic, 3rd ed, Springer, ISBN 9781441912206
 Victor Rodych, 2003, "Misunderstanding Gödel: New Arguments about Wittgenstein and New Remarks by Wittgenstein", Dialectica v 57 n 3, pp 279–313 doi:101111/j174683612003tb00272x
 Stewart Shapiro, 2002, "Incompleteness and Inconsistency", Mind, v 111, pp 817–32 doi:101093/mind/111444817
 Alan Sokal and Jean Bricmont, 1999, Fashionable Nonsense: Postmodern Intellectuals' Abuse of Science, Picador ISBN 0312204078
 Joseph R Shoenfield 1967, Mathematical Logic Reprinted by AK Peters for the Association for Symbolic Logic, 2001 ISBN 9781568811352
 Jeremy Stangroom and Ophelia Benson, Why Truth Matters, Continuum ISBN 0826495281
 George Tourlakis, Lectures in Logic and Set Theory, Volume 1, Mathematical Logic, Cambridge University Press, 2003 ISBN 9780521753739
 Avi Wigderson, 2010, "The Gödel Phenomena in Mathematics: A Modern View", in Kurt Gödel and the Foundations of Mathematics: Horizons of Truth, Cambridge University Press
 Hao Wang, 1996, A Logical Journey: From Gödel to Philosophy, The MIT Press, Cambridge MA, ISBN 0262231891
 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
 Godel's Incompleteness Theorems on In Our Time at the BBC Incompleteness Theorems listen now
 Kurt Gödel entry by Juliette Kennedy in the Stanford Encyclopedia of Philosophy, July 5, 2011
 Gödel's Incompleteness Theorems entry by Panu Raatikainen in the Stanford Encyclopedia of Philosophy, November 11, 2013
 Paraconsistent Logic § Arithmetic and Gödel's Theorem entry in the Stanford Encyclopedia of Philosophy
 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
 Hazewinkel, Michiel, ed 2001, "Gödel incompleteness theorem", Encyclopedia of Mathematics, Springer, ISBN 9781556080104
gödel's incompleteness theorems, gödel's incompleteness theorems pdf, gödel's incompleteness theorems simplified
Gödel's incompleteness theorems Information about

Gödel's incompleteness theorems beatiful post thanks!
29.10.2014
Gödel's incompleteness theorems
Gödel's incompleteness theorems
Gödel's incompleteness theorems viewing the topic.
There are excerpts from wikipedia on this article and video
Random Posts
B♭ (musical note)
B♭ Bflat; also called si bémol is the eleventh step of the Western chromatic scale starting from C ...Fourth dimension in art
New possibilities opened up by the concept of fourdimensional space and difficulties involved in tr...Holt Renfrew
Holt, Renfrew & Co, Limited, commonly known as Holt Renfrew or Holt's,1 is a chain of highend C...Later Silla
Later Silla 668–935, Hangul: 후신라; Hanja: 後新羅; RR: Hushila, Korean pronunciation: ...Search Engine
Our site has a system which serves search engine function.
You can search all data in our system with above button which written "What did you look for? "
Welcome to our simple, stylish and fast search engine system.
We have prepared this method why you can reach most accurate and most up to date knowladge.
The search engine that developed for you transmits you to the latest and exact information with its basic and quick system.
You can find nearly everything data which found from internet with this system.
Random Posts
Body politic
The body politic is a metaphor that regards a nation as a corporate entity,2 likened to a human body...Kakamega
Kakamega is a town in western Kenya lying about 30 km north of the Equator It is the headquarte...Academic year
An academic year is a period of time which schools, colleges and universities use to measure a quant...Lucrezia Borgia
Lucrezia Borgia Italian pronunciation: luˈkrɛttsja ˈbɔrdʒa; Valencian: Lucrècia Borja luˈkrɛsia...© Copyright © 2014. Search Engine