Misplaced Pages

Revision as of 18:37, 18 October 2009

In mathematical logic, Gödel's incompleteness theorems, proved by Kurt Gödel in 1931, are two theorems stating inherent limitations of all but the most trivial formal systems for arithmetic of mathematical interest. The theorems are of considerable importance to the philosophy of mathematics. They are widely regarded as showing that Hilbert's program to find a complete and consistent set of axioms for all of mathematics is impossible, thus giving a negative answer to Hilbert's second problem.

Background

In mathematical logic, a theory is a set of sentences expressed in a formal language. Some statements in a theory are included without proof (these are the axioms of the theory), and others (the theorems) are included because they are implied by the axioms.

Because statements of a formal theory are written in symbolic form, it is possible to mechanically verify that a formal proof from a finite set of axioms is valid. This task, known as automatic proof verification, is closely related to automated theorem proving; the difference is that instead of constructing a new proof, the proof verifier simply checks that a provided formal proof (or, in some cases, instructions that can be followed to create a formal proof) is correct. This is not merely hypothetical; systems such as Isabelle are used today to formalize proofs and then check their validity.

Many theories of interest include an infinite set of axioms, however. To verify a formal proof when the set of axioms is infinite, it must be possible to determine whether a statement that is claimed to be an axiom is actually an axiom. This issue arises in first order theories of arithmetic, such as Peano arithmetic, because the principle of mathematical induction is expressed as an infinite set of axioms (an axiom schema).

A formal theory is said to be effectively generated if its set of axioms is a recursively enumerable set. This means that there is a computer program that, in principle, could enumerate all the axioms of the theory without listing any statements that are not axioms. This is equivalent to the ability to enumerate all the theorems of the theory without enumerating any statements that are not theorems. For example, each of the theories of Peano arithmetic and Zermelo–Fraenkel set theory has an infinite number of axioms and each is effectively generated.

In choosing a set of axioms, one goal is to be able to prove as many correct results as possible, without proving any incorrect results. A set of axioms is complete if, for any statement in the axioms' language, either that statement or its negation is provable from the axioms. A set of axioms is (simply) consistent if there is no statement so that both the statement and its negation are provable from the axioms. In the standard system of 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.

First incompleteness theorem

Gödel's first incompleteness theorem states that:

Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory (Kleene 1967, p. 250).

The true but unprovable statement referred to by the theorem is often referred to as “the Gödel sentence” for the theory. It is not unique; there are infinitely many statements in the language of the theory that share the property of being true but unprovable.

For each consistent formal theory T having the required small amount of number theory, the corresponding Gödel sentence G asserts: “G cannot be proved to be true within the theory T”. If G were provable under the axioms and rules of inference of T, then T would have a theorem, G, which effectively contradicts itself, and thus the theory T would be inconsistent. This means that if the theory T is consistent then G cannot be proved within it. This means that G's claim about its own unprovability is correct; in this sense G is not only unprovable but true. Thus provability-within-the-theory-T is not the same as truth; the theory T is incomplete.

If G is true: G cannot be proved within the theory, and the theory is incomplete. If G is false: then G can be proved within the theory and then the theory is inconsistent, since G is both provable and refutable from T.

Each theory has its own Gödel statement. It is possible to define a larger theory T’ that contains the whole of T, plus G as an additional axiom. This will not result in a complete theory, because Gödel's theorem will also apply to T’, and thus T’ cannot be complete. In this case, G is indeed a theorem in T’, because it is an axiom. Since G states only that it is not provable in T, no contradiction is presented by its provability in T’. However, because the incompleteness theorem applies to T’: there will be a new Gödel statement G’ for T’, showing that T’ is also incomplete. G’ will differ from G in that G’ will refer to T’, rather than T.

To prove the first incompleteness theorem, Gödel represented statements by numbers. Then the theory at hand, which is assumed to prove certain facts about numbers, also proves facts about its own statements. Questions about the provability of statements are represented as questions about the properties of numbers, which would be decidable by the theory if it were complete. In these terms, the Gödel sentence states that no natural number exists with a certain, strange property. A number with this property would encode a proof of the inconsistency of the theory. If there were such a number then the theory would be inconsistent, contrary to the consistency hypothesis. So, under the assumption that the theory is consistent, there is no such number.

Meaning of the first incompleteness theorem

Gödel's first incompleteness theorem shows that any consistent formal system that includes enough of the theory of the natural numbers is incomplete; there are true statements expressible in its language that are unprovable. Thus no formal system (satisfying the hypotheses of the theorem) that aims to characterize the natural numbers can actually do so, as there will be true number-theoretical statements which that system cannot prove. This fact has 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).

The existence of an incomplete formal system is in itself not particularly surprising. A system may be incomplete simply because not all the necessary axioms have been discovered. For example, Euclidean geometry without the parallel postulate is incomplete; it is not possible to prove or disprove the parallel postulate from the remaining axioms.

Gödel's theorem shows that, in theories that include a small portion of number theory, a complete and consistent finite list of axioms can never be created, nor even an infinite list that can be enumerated by a computer program. Each time a new statement is added as an axiom, there are other true statements that still cannot be proved, even with the new axiom. If an axiom is ever added that makes the system complete, it does so at the cost of making the system inconsistent.

It is possible to have a complete and consistent list of axioms that cannot be enumerated by a computer program. For example, one might take all true statements about the natural numbers to be axioms (and no false statements). But then there is no mechanical way to decide, given a statement about the natural numbers, whether it is an axiom or not, and thus no effective way to verify a formal proof in this theory.

Many logicians believe that Gödel's incompleteness theorems struck a fatal blow to David Hilbert's second problem, which asked for a finitary consistency proof for mathematics. The second incompleteness theorem, in particular, is often viewed as making the problem impossible. Not all mathematicians agree with this analysis, however, and the status of Hilbert's second problem is not yet decided (see "Modern viewpoints on the status of the problem").

Relation to the liar paradox

The liar paradox is the sentence "This sentence is false." An analysis of the liar sentence shows that it cannot be true (for then, as it asserts, it is false), nor can it be false (for then, it is true). A Gödel sentence G for a theory T makes a similar assertion to the liar sentence, but with truth replaced by provability: G says "G is not provable in the theory T." The analysis of the truth and provability of G is a formalized version of the analysis of the truth of the liar sentence.

It is not possible to replace "not provable" with "false" in a Gödel sentence because the predicate "Q is the Gödel number of a false formula" cannot be represented as a formula of arithmetic. This result, known as Tarski's undefinability theorem, was discovered independently by Gödel (when he was working on the proof of the incompleteness theorem) and by Alfred Tarski.

Original statement

The first incompleteness theorem first appeared as "Theorem VI" in his 1931 paper On Formally Undecidable Propositions in Principia Mathematica and Related Systems I. In Gödel's original notation, it states:

"The general result about the existence of undecidable propositions reads as follows:

"Theorem VI. For every ω-consistent recursive class κ of FORMULAS there are recursive CLASS SIGNS r, such that neither v Gen r nor Neg(v Gen r) belongs to Flg(κ) (where v is the FREE VARIABLE of r).(van Heijenoort 1967:607.)

Extensions of Gödel's original result

Gödel demonstrated the incompleteness of the theory of Principia Mathematica, a particular theory of arithmetic, but a parallel demonstration could be given for any effective theory of a certain expressiveness. Gödel commented on this fact in the introduction to his paper, but restricted the proof to one system for concreteness. In modern statements of the theorem, it is common to state the effectiveness and expressiveness conditions as hypotheses for the incompleteness theorem, so that it is not limited to any particular formal theory. The terminology used to state these conditions was not yet developed in 1931 when Gödel published his results.

Gödel's original statement and proof of the incompleteness theorem requires the assumption that the theory is not just consistent but ω-consistent. A theory is ω-consistent if it is not ω-inconsistent, and is ω-inconsistent if there is a predicate P such that for every specific natural number n the theory proves ~P(n), and yet the theory also proves that there exists a natural number n such that P(n). That is, the theory says that a number with property P exists while denying that it has any specific value. The ω-consistency of a theory implies its consistency, but consistency does not imply ω-consistency. J. Barkley Rosser (1936) strengthened the incompleteness theorem by finding a variation of the proof (Rosser's trick) that only requires the theory to be consistent, rather than ω-consistent. This is mostly of technical interest, since all true formal theories of arithmetic (theories whose axioms are all true statements about natural numbers) are ω-consistent, and thus Gödel's theorem as originally stated applies to them. The stronger version of the incompleteness theorem that only assumes consistency, rather than ω-consistency, is now commonly known as Gödel's incompleteness theorem and as the Gödel–Rosser theorem.

Second incompleteness theorem

Gödel's second incompleteness theorem can be stated as follows:

For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, T includes a statement of its own consistency if and only if T is inconsistent.

This strengthens the first incompleteness theorem, because the statement constructed in the first incompleteness theorem does not directly express the consistency of the theory. The proof of the second incompleteness theorem is obtained, essentially, by formalizing the proof of the first incompleteness theorem within the theory itself.

A technical subtlety in the second incompleteness theorem is how to express the consistency of T as a formula in the language of T. There are many ways to do this, and not all of them lead to the same result. In particular, different formalizations of the claim that T is consistent may be inequivalent in T, and some may even be provable. For example, 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 rather vague, but what is meant here is the largest consistent initial segment of the axioms of PA ordered according to some criteria; for example, by "Gödel numbers", the numbers encoding the axioms as per the scheme used by Gödel mentioned above).

In the case of Peano arithmetic, or any familiar explicitly axiomatized theory T, it is possible to canonically define a formula Con(T) expressing the consistency of T; this formula expresses the property that "there does not exist a natural number coding a sequence of formulas, such that each formula is either one of the axioms of T, a logical axiom, or an immediate consequence of preceding formulas according to the rules of inference of 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 Prov_A(P) which expresses that P is provable from the set of axioms defined by A(x). In addition, Prov_A(P) must satisfy the so-called Hilbert–Bernays provability conditions:

1. If T proves P, then T proves Prov_A(P).
2. T proves 1.; that is, T proves that if T proves P, then T proves Prov_A(P).
3. T proves that if T proves that (P → Q) then T proves that provability of P implies provability of Q.

Solomon Feferman showed that Gödel's second incompleteness theorem goes through when the formula A(x) is chosen so that it has the form "there exists a number n satisfying the decidable predicate P" for some P.

Implications for consistency proofs

Gödel's second incompleteness theorem also implies that a theory T₁ satisfying the technical conditions outlined above cannot prove the consistency of any theory T₂ which proves the consistency of T₁. This is because such a theory T₁ can prove that if T₂ proves the consistency of T₁, then T₁ is in fact consistent. For the claim that T₁ is consistent has form "for all numbers n, n has the decidable property of not being a code for a proof of contradiction in T₁". If T₁ were in fact inconsistent, then T₂ would prove for some n that n is the code of a contradiction in T₁. But if T₂ also proved that T₁ is consistent (that is, that there is no such n), then it would itself be inconsistent. This reasoning can be formalized in T₁ to show that if T₂ is consistent, then T₁ is consistent. Since, by second incompleteness theorem, T₁ does not prove its consistency, it cannot prove the consistency of T₂ either.

This corollary of the second incompleteness theorem shows that there is no hope of proving, for example, the consistency of Peano arithmetic using any finitistic means that can be formalized in a theory the consistency of which is provable in Peano arithmetic. For example, the theory of primitive recursive arithmetic (PRA), which is widely accepted as an accurate formalization of finitistic mathematics, is provably consistent in PA. Thus PRA cannot prove the consistency of PA. This fact is generally seen to imply that Hilbert's program, which aimed to justify the use of "ideal" (infinitistic) mathematical principles in the proofs of "real" (finitistic) mathematical statements by giving a finitistic proof that the ideal principles are consistent, cannot be carried out.

The corollary also indicates the epistemological relevance of the second incompleteness theorem. As Georg Kreisel remarked, it would actually provide no interesting information if a theory T proved its consistency. This is because inconsistent theories prove everything, including their consistency. Thus a consistency proof of T in T would give us no clue as to whether T really is consistent; no doubts about the consistency of T would be resolved by such a consistency proof. The interest in consistency proofs lies in the possibility of proving the consistency of a theory T in some theory T’ which is in some sense less doubtful than T itself, for example weaker than T. For many naturally occurring theories T and T’, such as T = Zermelo–Fraenkel set theory and T’ = primitive recursive arithmetic, the consistency of T’ is provable in T, and thus T’ can't prove the consistency of T by the above corollary of the second incompleteness theorem.

The second incompleteness theorem does not rule out consistency proofs altogether, only consistency proofs that could be formalized in the theory that is proved consistent. For example, Gerhard Gentzen proved the consistency of Peano arithmetic (PA) using the assumption that a certain ordinal called ε₀ is actually wellfounded; see Gentzen's consistency proof. Gentzen's theorem spurred the development of ordinal analysis in proof theory.

Original statement of Gödel’s Theorem XI

While contemporary usage calls it the “Second incompleteness Theorem”, in the original Gödel presented it as his “Theorem XI”. It is stated thus (in the following, “Section 2” is where his Theorem VI appears, and P is Gödel’s abbreviation for the system obtained by adding the Peano axioms to the logical system of Principia Mathematica.

”The results of Section 2 have a surprising consequence concerning a consistency proof for the system P (and its extensions), which can be stated as follows:

”Theorem XI. Let κ be any recursive consistent class of FORMULAS; then the SENTENTIAL FORMULA stating that κ is consistent is not κ-PROVABLE; in particular, the consistency of P is not provable in P, provided P is consistent (in the opposite case, of course, every proposition is provable )". (Brackets in original added by Gödel “to help the reader”, translation and typography in van Heijenoort 1967:614)

” “κ is consistent” (abbreviated by “Wid(κ)”) is defined as thus: Wid(κ)≡ (Ex)(Form(x) & ~Bew_κ(x))."

(Note: In the original "Bew" has a negation-“bar” written over it, indicated here by ~. “Wid” abbreviates “Widerspruchfreiheit = consistency”, “Form” abbreviates “Formel = formula”, “Bew” abbreviates “Beweisbar = provable” (translations from Meltzer and Braithwaite 1962, 1996 edition:33-34) )

” This follows if we substitute the empty class of FORMULAS for κ.”

Examples of undecidable statements

See also: List of statements undecidable in ZFC

There are two distinct senses of the word "undecidable" in mathematics and computer science. The first of these is the proof-theoretic sense used in relation to Gödel's theorems, that of a statement being neither provable nor refutable in a specified deductive system. The second sense, which will not be discussed here, is used in relation to computability theory and applies not to statements but to decision problems, which are countably infinite sets of questions each requiring a yes or no answer. Such a problem is said to be undecidable if there is no computable function that correctly answers every question in the problem set (see undecidable problem).

Because of the two meanings of the word undecidable, the term independent is sometimes used instead of undecidable for the "neither provable nor refutable" sense. The usage of "independent" is also ambiguous, however. Some use it to mean just "not provable", leaving open whether an independent statement might be refuted.

Undecidability of a statement in a particular deductive system does not, in and of itself, address the question of whether the truth value of the statement is 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 to be true 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.

Limitations of Gödel's theorems

The conclusions of Gödel's theorems only hold for the formal theories that satisfy the necessary hypotheses. Not all axiom systems satisfy these hypotheses, even when these systems have models that include the natural numbers as a subset. For example, there are first-order axiomatizations of Euclidean geometry and real closed fields that do not 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.

Gödel's theorems only apply to consistent theories. In first-order logic, because of the principle of explosion, an inconsistent theory T proves every formula in its language, including formulas that claim T is consistent.

Gödel's theorems only apply to effectively generated (that is, recursively enumerable) theories. If all true statements about natural numbers are taken as axioms for a theory, then this theory is a consistent, complete extension of Peano arithmetic for which none of Gödel's theorems hold, because this theory is not recursively enumerable.

The second incompleteness theorem only shows that the consistency of certain theories cannot be proved from the axioms of those theories themselves. It does not show that the consistency cannot be proved from other (consistent) axioms. For example, the consistency of the Peano arithmetic can be proved in Zermelo–Frankel set theory (ZFC), or in theories of arithmetic augmented with transfinite induction, as in Gentzen's consistency proof.

Relationship with computability

The incompleteness theorem is closely related to several results about undecidable sets in recursion theory.

Stephen Cole Kleene (1943) presented a proof of Gödel's incompleteness theorem using basic results of computability theory. One such result shows that the halting problem is unsolvable: there is no computer program that can correctly determine, given a program P as input, whether P eventually halts when run with no input. Kleene showed that the existence of a complete effective theory of arithmetic with certain consistency properties would force the halting problem to be decidable, a contradiction. Expositions of this proof at the undergraduate level are given by Charlesworth (1980) and Hopcroft and Ullman (1979).

Franzén (2005, p. 73) explains how Matiyasevich's solution to Hilbert's 10th problem can be used to obtain a proof to Gödel's first incompleteness theorem. Matiyasevich proved that there is no algorithm that, given a multivariate polynomial p(x₁, x₂,...,x_k) with integer coefficients, determines whether there is an integer solution to the equation p = 0. Because polynomials with integer coefficients, and integers themselves, are directly expressible in the language of arithmetic, if a multivariate integer polynomial equation p = 0 does have a solution in the integers then any sufficiently strong theory of arithmetic T will prove this. Moreover, if the theory T is ω-consistent, then it will never prove that some polynomial equation has a solution when in fact there is no solution in the integers. Thus, if T were complete and ω-consistent, it would be possible to algorithmically determine whether a polynomial equation has a solution by merely enumerating proofs of T until either "p has a solution" or "p has no solution" is found, in contradiction to Matiyasevich's theorem.

Smorynski (1977, p. 842) shows how the existence of recursively inseparable sets can be used to prove the first incompleteness theorem. This proof is often extended to show that systems such as Peano arithmetic are essentially undecidable (see Kleene 1967, p. 274).

Modern version of Gödel's proof

Gödel's original proof of the incompleteness theorems has been considered difficult to read. The notion of a computer and a computer program were not yet defined in 1931, and the ideas of the proof involve computation in an essential way.

Given the basic ideas of modern computer science, the original presentation of Gödel simplifies enormously. The notion of "arithmetization of syntax" in modern terms is just the idea that any statement in a formal language can be written up in ASCII or Unicode, and in this representation becomes a sequence of bytes, or equivalently, a large integer. Any deduction algorithm can be written as a computer program, and is therefore a manipulation of integers. The program itself can be stored in memory, and its code is also a big integer. The first sections of Gödel's paper only show that the algorithm of logical deduction can be encoded within arithmetic, which is obvious today, since the algorithm of logical deduction can be programmed on a computer.

The memory contents of a computer is a large integer M, which is a long sequence of bytes, and for the purposes of the incompleteness theorem, M can become arbitrarily large during the course of the computation. So unlike a real computer, the idealized computer in the proof has an unlimited memory. Each processor step of the computer is a simple function which takes M to f(M), where the function f describes the instruction set of the computer. M includes the registers and the instruction pointer, which also must be allowed to be arbitarily large, and whatever special memory adresses you would like, corresponding to input and output devices. The function f in any computer will be primitive recursive.

The incompleteness theorem talks about an axiom system which is sufficiently strong, which Gödel takes to be the theory of Arithmetic in Principia Mathematica. The details of PM are not essential, the only property which is required of the theory is that it can describe an idealized computer. It is assumed that the axioms will prove every calculational theorem, it will eventually prove that the result of every finite computation is whatever it is. So that if f applied N times to M results in M', which can be verified by computing it, there is a theorem in the axiom system that

f(M) = f(f(f ...N-times...f(M))..) = M'

This theorem does not involve any quantifiers, and does not require any induction or infinite set theory. In the statement, N M, and M' are finite explicit integers, and f is an explicit computable function.

This means that if a computer program P working on input I produces an answer A in a finite time, the axioms are sufficient to follow the computation and prove this result. It is further assumed that the axioms are consistent, which means that they will never prove a statement and its negation. The last assumption is that the axioms can be listed by a computer program, so that there exists a computer program DEDUCE which will list out the axioms, and find all deductions in the theory by formal logic. A system whose axioms and deductions can be made by a computer program is called computable. Standard logic includes the quantifier "forall", so that a statement of the form "forall N f(M) does not produce 0 in memory location 0xFFEE" is a statement of the theory. This means that any statement about the eventual behavior of a computer program is easy to write down.

Under these assumptions, Gödel's first incompleteness theorem is:

Any consistent computable axiom system S that describes a computer has a Gödel sentence G. G is true as a statement about computations on integers, but G cannot be proved by S.

To construct the Gödel sentence G, consider the computer program SPITE:

1. SPITE prints its own code into a variable R

2. SPITE deduces all theorems of S, looking for the theorem "R does not halt".

3. If it finds this theorem, it halts.

Step 1 is not completely obvious--- a program which prints its own code sometimes requires effort to write. If the program does not have read access to its own code in memory, it must include its own code in a suitable way in the subroutine that prints out the code. The subroutine must then use a trick to avoid infinite self-reference, by copying the code variable and printing it twice. A program which prints its own code in this way is called a Quine.

Step 2 makes sense, because the statement "R does not halt" is a statement about computer programs, about integers, so it can be encoded in the language of S by assumption. It is a statement with one forall quantifier in front: forall N, "f(R) is not a halting state"

Step 3 is the interesting part: the program is looking for a theorem about itself. Step 3 guarantees that if it finds this theorem, it will do the opposite.

The Gödel sentence G for the theory S is "SPITE does not halt". If the theory proves this, then SPITE will halt in finite time, S will prove that SPITE halts, and this means that S has proved both a statement and its negation. So a consistent theory S will not prove "SPITE does not halt", and this means that SPITE will not halt. G is true, but unprovable.

Gödel's 1931 paper does not explicitly write a Quine. Instead, Gödel uses a peculiar property of sentences in first order logic with variables, which allows self-reference by a different looking trick. This trick was isolated by Kleene, and was later shown to be equivalent to writing a Quine within computer science. Von Neumann made the analogy between the self-reference involved in Gödel's proof and the replication of biological systems, since printing out your own code into a variable is the same as making a copy of yourself. He explored this type of computational self-replication further in his book The Theory of Self-reproducing Automata, a classic of cybernetics. The connection between the self-reference in Gödel's theorem, in biology, and in the process of artistic creativity was also explored in the popular book Gödel, Escher, Bach: An Eternal Golden Braid.

If written out in full, the sentence "SPITE does not halt" is complicated, involving many ideas that are not directly related to logic. After presenting his theorem, Von Neumann asked Gödel for a more elegant statement of the theorem, so that the basic limitation could be more clearly understood. After thinking it over, Gödel came up with the second incompleteness theorem:

Any consistent computable axiom system S describing a computer cannot prove its own consistency.

The previous argument shows that if SPITE halts if and only if S is inconsistent. So if the argument for the first incompleteness theorem can be formalized in S, then if S were to prove its own consistency, it would prove that SPITE does not halt.

The modern statement of Gödel's incompleteness theorem was not proved by Gödel in 1931, but by Rosser in 1936.

Any consistent computable axiom system S describing a computer is incomplete

This theorem is not proved by Gödel's method, because of a subtlety, first noticed by Gödel. Although S cannot consistently prove "SPITE does not halt", S could still prove "SPITE halts" without an explicit contradiction. If S is consistent, then "SPITE halts" is a lie, SPITE doesn't actually halt. But it's not an inconsistency unless S proves that "SPITE doesn't halt" too. There's no reason that S has to do this.

An S which proves "SPITE halts" is in the strange position of asserting that SPITE halts, while it in fact does not. Under the assumptions of the second incompleteness theorem, such an S asserts that it is inconsistent, when it is in fact consistent. Gödel called this type of theory omega inconsistent. The notion has been refined since then, so that the particular type of omega inconsistency involved here has a more specialized name, it is called sigma-one inconsistency.

Gödel's method proves that any omega-consistent (or even just sigma-one consistent) effective system S describing a computer is incomplete. Gödel's incompleteness theorem is also true for omega-inconsistent systems, but the argument is slightly more complicated. To prove incompleteness, construct the computer program ROSSER:

1. ROSSER prints its code into variable R

2. ROSSER deduces all the theorems of S, looking for either a) "R does not print to the screen" or the negation b) "R does print to the screen"

3. If it finds a), it prints "hello" to the screen, and halts. If it finds b), it halts without printing anything.

Since ROSSER halts either if it finds a) or if it finds b), S cannot consistently prove either the statement "ROSSER does not print to the screen", nor the negation "ROSSER does print to the screen". Either way, it would follow ROSSER until it halts, and then it would also prove the opposite. This was the first significant extension of Gödel's method, and it was formulated by Rosser in 1936, using Gödel's original arithmetization of the deduction methods of logic. In the same year, Turing developed the modern notion of computer, making Gödel's methods obsolete. Extensions of Godel's method continued in the 1950's, with the development of the method of injury priority.

Proof sketch for the first theorem

Throughout the proof we assume a formal system is fixed and satisfies the necessary hypotheses. The proof has three essential parts. The first part is to show that statements can be represented by natural numbers, known as Gödel numbers, and that properties of the statements can be detected by examining their Gödel numbers. This part culminates in the construction of a formula expressing the idea that a statement is provable in the system. The second part of the proof is to construct a particular statement that, essentially, says that it is unprovable. The third part of the proof is to analyze this statement to show that it is neither provable nor disprovable in the system.

Arithmetization of syntax

The main problem in fleshing out the proof described above is that it seems at first that to construct a statement p that is equivalent to "p cannot be proved", p would have to somehow contain a reference to p, which could easily give rise to an infinite regress. Gödel's ingenious trick, which was later used by Alan Turing in his work on the Entscheidungsproblem, is to represent statements as numbers, which is often called the arithmetization of syntax. This allows a self-referential formula to be constructed in a way that avoids any infinite regress of definitions.

To begin with, every formula or statement that can be formulated in our system gets a unique number, called its Gödel number. This is done in such a way that it is easy to mechanically convert back and forth between formulas and Gödel numbers. It is similar, for example, to the way English sentences are encoded as sequences (or "strings") of numbers using ASCII: such a sequence is considered as a single (if potentially very large) number. Because our system is strong enough to reason about numbers, it is now also possible to reason about formulas within the system.

A formula F(x) that contains exactly one free variable x is called a statement form or 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 with a Gödel number which we will denote by G(F). The choice of the free variable used in the form F(x) is not relevant to the assignment of the Gödel number G(F).

Now comes the trick: The notion of provability itself can also be encoded by Gödel numbers, in the following way. Since a proof is a list of statements which obey certain rules, we can define the Gödel number of a proof. Now, for every statement p, we may ask whether a number x is the Gödel number of its proof. The relation between the Gödel number of p and x, the Gödel number of its proof, is an arithmetical relation between two numbers. Therefore there is a statement form Bew(x) that uses this arithmetical relation to state that a Gödel number of a proof of x exists:

Bew(y) = ∃ x ( y is the Gödel number of a formula and x is the Gödel number of a proof of the formula encoded by y).

The name Bew is short for beweisbar, the German word for "provable"; this name was originally used by Gödel to denote the provability formula just described. Note that "Bew(y)" is merely an abbreviation that represents a particular, very long, formula in the original language of T; the string "Bew" itself is not claimed to be part of this language.

An important feature of the formula Bew(y) is that if a statement p is provable in the system then Bew(G(p)) is also provable. This is because any proof of p would have a corresponding Gödel number, the existence of which causes Bew(G(p)) to be satisfied.

Diagonalization

The next step in the proof is to obtain a statement that says it is unprovable. Although Gödel constructed this statement directly, the existence of at least one such statement follows from the diagonal lemma, which says that for any sufficiently strong formal system and any statement form F there is a statement p such that the system proves

p ↔ F(G(p)).

We obtain p by letting F be the negation of Bew(x); thus p roughly states that its own Gödel number is the Gödel number of an unprovable formula.

The statement p is not literally equal to ~Bew(G(p)); rather, p states that if a certain calculation is performed, the resulting Gödel number will be that of an unprovable statement. But when this calculation is performed, the resulting Gödel number turns out to be the Gödel number of p itself. This is similar to the following sentence in English:

", when preceded by itself in quotes, is unprovable.", when preceded by itself in quotes, is unprovable.

This sentence does not directly refer to itself, but when the stated transformation is made the original sentence is obtained as a result, and thus this sentence asserts its own unprovability. The proof of the diagonal lemma employs a similar method.

Proof of independence

We will now assume that our axiomatic system is ω-consistent. We let p be the statement obtained in the previous section.

If p were provable, then Bew(G(p)) would be provable, as argued above. But p asserts the negation of Bew(G(p)). Thus our system would be inconsistent, proving both a statement and its negation. This contradiction shows that p cannot be provable.

If the negation of p were provable, then Bew(G(p)) would be provable (because p was constructed to be equivalent to the negation of Bew(G(p))). However, for each specific number x, x cannot be the Gödel number of the proof of p, because p is not provable (from the previous paragraph). Thus on one hand the system proves there is a number with a certain property (that it is the Gödel number of the proof of p), but on the other hand, for every specific number x, we can prove that it does not have this property. This is impossible in an ω-consistent system. Thus the negation of p is not provable.

Thus the statement p is undecidable: it can neither be proved nor disproved within the system.

It should be noted that p is not provable (and thus true) in every consistent system. The assumption of ω-consistency is only required for the negation of p to be not provable. Thus:

• In an ω-consistent formal system, we may prove neither p nor its negation, and so p is undecidable.
• In a consistent formal system we may either have the same situation, or we may prove the negation of p; In the later case, we have a statement ("not p") which is false but provable.

Note that if one tries to "add the missing axioms" to avoid the undecidability of the system, then one has to add either p or "not p" as axioms. But then the definition of "being a Gödel number of a proof" of a statement changes. which means that the statement form Bew(x) is now different. Thus when we apply the diagonal lemma to this new form Bew, we obtain a new statement p, different from the previous one, which will be undecidable in the new system if it is ω-consistent.

Proof via Berry's paradox

George Boolos (1989) sketches an alternative proof of the first incompleteness theorem that uses Berry's paradox rather than the liar paradox to construct a true but unprovable formula. A similar proof method was independently discovered by Saul Kripke (Boolos 1998, p. 383). Boolos's proof proceeds by constructing, for any computably enumerable set S of true sentences of arithmetic, another sentence which is true but not contained in S. This gives the first incompleteness theorem as a corollary. According to Boolos, this proof is interesting because it provides a "different sort of reason" for the incompleteness of effective, consistent theories of arithmetic (Boolos 1998, p. 388).

Proof sketch for the second theorem

The main difficulty in proving the second incompleteness theorem is to show that various facts about provability used in the proof of the first incompleteness theorem can be formalized within the system using a formal predicate for provability. Once this is done, the second incompleteness theorem essentially follows by formalizing the entire proof of the first incompleteness theorem within the system itself.

Let p stand for the undecidable sentence constructed above, and assume that the consistency of the system can be proven from within the system itself. We have seen above that if the system is consistent, then p is not provable. The proof of this implication can be formalized within the system, and therefore the statement "p is not provable", or "not P(p)" can be proven in the system.

But this last statement is equivalent to p itself (and this equivalence can be proven in the system), so p can be proven in the system. This contradiction shows that the system must be inconsistent.

Discussion and implications

The incompleteness results affect the philosophy of mathematics, particularly versions of formalism, which use a single system formal logic to define their principles. One can paraphrase the first theorem as saying the following:

We can never find an all-encompassing axiomatic system which is able to prove all mathematical truths, but no falsehoods.

On the other hand, from a strict formalist perspective this paraphrase would be considered meaningless because it presupposes that mathematical "truth" and "falsehood" are 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:

If an axiomatic system can be proven to be consistent and complete from within itself, then it is inconsistent.

Therefore, to establish the consistency of a system S, one needs to use some other more powerful system T, but a proof in T is not completely convincing unless T's consistency has already been established without using S.

At first, Gödel's theorems seemed to leave some hope—it was thought that it might be possible to produce a general algorithm that indicates whether a given statement is undecidable or not, thus allowing mathematicians to bypass the undecidable statements altogether. However, the negative answer to the Entscheidungsproblem, obtained in 1936, showed that no such algorithm exists.

There are some who hold that a statement that is unprovable within a deductive system may be quite provable in a metalanguage. And what cannot be proven in that metalanguage can likely be proven in a meta-metalanguage, recursively, ad infinitum, in principle. By invoking such a system of typed metalanguages, along with an axiom of Reducibility — which by an inductive assumption applies to the entire stack of languages — one may, for all practical purposes, overcome the obstacle of incompleteness.

Note that Gödel's theorems only apply to sufficiently strong axiomatic systems. "Sufficiently strong" means that the theory contains enough arithmetic to carry out the coding constructions needed for the proof of the first incompleteness theorem. Essentially, all that is required are some basic facts about addition and multiplication as formalized, for example, in Robinson arithmetic Q. There are even weaker axiomatic systems that are consistent and complete, for instance Presburger arithmetic which proves every true first-order statement involving only addition.

The axiomatic system may consist of infinitely many axioms (as first-order Peano arithmetic does), but for Gödel's theorem to apply, there has to be an effective algorithm which is able to check proofs for correctness. For instance, one might take the set of all first-order sentences which are true in the standard model of the natural numbers. This system is complete; Gödel's theorem does not apply because there is no effective procedure that decides if a given sentence is an axiom. In fact, that this is so is a consequence of Gödel's first incompleteness theorem.

Another example of a specification of a theory to which Gödel's first theorem does not apply can be constructed as follows: order all possible statements about natural numbers first by length and then lexicographically, start with an axiomatic system initially equal to the Peano axioms, go through your list of statements one by one, and, if the current statement cannot be proven nor disproven from the current axiom system, add it to that system. This creates a system which is complete, consistent, and sufficiently powerful, but not computably enumerable.

Gödel himself only proved a technically slightly weaker version of the above theorems; the first proof for the versions stated above was given by J. Barkley Rosser in 1936.

In essence, the proof of the first theorem consists of constructing a statement p within a formal axiomatic system that can be given a meta-mathematical interpretation of:

p = "This statement cannot be proven in the given formal theory"

As such, it can be seen as a modern variant of the Liar paradox, although unlike the classical paradoxes it's not really paradoxical.

If the axiomatic system is consistent, Gödel's proof shows that p (and its negation) cannot be proven in the system. Therefore p is true (p claims to be not provable, and it is not provable) yet it cannot be formally proved in the system. If the axiomatic system is ω-consistent, then the negation of p cannot be proven either, and so p is undecidable. In a system which is not ω-consistent (but consistent), either we have the same situation, or we have a false statement which can be proven (namely, the negation of p).

Adding p to the axioms of the system would not solve the problem: there would be another Gödel sentence for the enlarged theory. Theories such as Peano arithmetic, for which any computably enumerable consistent extension is incomplete, are called essentially incomplete.

Minds and machines

Authors including J. R. Lucas have debated what, if anything, Gödel's incompleteness theorems imply about human intelligence. Much of the debate centers on whether the human mind is equivalent to a Turing machine, or by the Church–Turing thesis, any finite machine at all. If it is, and if the machine is consistent, then Gödel's incompleteness theorems would apply to it.

Hilary Putnam (1960) suggested that while Gödel's theorems cannot be applied to humans, since they make mistakes and are therefore inconsistent, it may be applied to the human faculty of science or mathematics in general. If we are to believe that it is consistent, then either we cannot prove its consistency, or it cannot be represented by a Turing machine.

Appeals to the incompleteness theorems in other fields

Appeals and analogies are sometimes made to the incompleteness theorems in support of arguments that go beyond mathematics and logic. A number of authors have commented negatively on such extensions and interpretations, including Torkel Franzén (2005); Alan Sokal and Jean Bricmont (1999); and Ophelia Benson and Jeremy Stangroom (2006). Bricmont and Stangroom (2006, p. 10), for example, quote from Rebecca Goldstein's comments on the disparity between Gödel's avowed Platonism and the anti-realist uses to which his ideas sometimes put. Sokal and Bricmont (1999, p. 187) criticize Régis Debray's invocation of the theorem in the context of sociology; Debray has defended this use as metaphorical (ibid.).

See also

• Consistency proof
• Gödel's completeness theorem
• Löb's Theorem
• Provability logic
• Logicism
• Münchhausen Trilemma
• Non-standard arithmetic
• Self-verifying theories
• Tarski's indefinability theorem
• Minds, Machines and Gödel
• Third Man Argument

Notes

1. The word "true" is used disquotationally here: the Gödel sentence is true in this sense because it "asserts its own unprovability and it is indeed unprovable" (Smoryński 1977 p. 825; also see Franzén 2005 pp. 28–33). It is also possible to read "G_T is true" in the formal sense that primitive recursive arithmetic proves the implication Con(T)→G_T, where Con(T) is a canonical sentence asserting the consistency of T (Smoryński 1977 p. 840, Kikuchi and Tanaka 1994 p. 403)
2. For example, the conjunction of the Gödel sentence and any logically valid sentence will have this property.
3. Here Flg(κ) represents the theory generated by κ and "v Gen r" is a particular formula in the language of arithmetic. "Flg" is from "Folgerungsmenge = set of consequences" and "Gen" is from "Generalisation = generalization" (cf Meltzer and Braithwaite 1962, 1992 edition:33-34).

References

Articles by Gödel

• 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173-98.
  • Hirzel, Martin, 2000, On formally undecidable propositions of Principia Mathematica and related systems I.. A modern translation by the author.
• 1951, Some basic theorems on the foundations of mathematics and their implications in Solomon Feferman, ed., 1995. Collected works / Kurt Gödel, Vol. III. Oxford University Press: 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 . . . 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 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 Hawking 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 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, 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 Boolos, 1989, "A New Proof of the Gödel Incompleteness Theorem", Notices of the American Mathematical Society v. 36, pp. 388–390 and p. 676, reprinted in in Boolos, 1998, Logic, Logic, and Logic, Harvard Univ. Press. ISBN 0 674 53766 1
• Arthur Charlesworth, 1980, "A Proof of Godel's Theorem in Terms of Computer Programs," Mathematics Magazine, v. 54 n. 3, pp. 109–121. JStor
• Solomon Feferman, 1984, Toward Useful Type-Free Theories, I, Journal of Symbolic Logic, v. 49 n. 1, pp. 75–111.
• Geoffrey Hellman, 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 Hilbert, 1900, "Mathematical Problems." English translation of a lecture delivered before the International Congress of Mathematicians at Paris, containing Hilbert's statement of his Second Problem.
• Kikuchi, Makoto; Tanaka, Kazuyuki (1994), "On formalization of model-theoretic proofs of Gödel's theorems", Notre Dame Journal of Formal Logic, 35 (3): 403–412, doi:10.1305/ndjfl/1040511346, ISSN 0029-4527, MR1326122
• Stephen Cole Kleene, 1943, "Recursive predicates and quantifiers," reprinted from Transactions of the American Mathematical Society, v. 53 n. 1, pp. 41–73 in Martin Davis 1965, The Undecidable (loc. cit.) pp. 255–287.
• Hilary Putnam, 1960, Minds and Machines in Sidney Hook, ed., Dimensions of Mind: A Symposium. New York University Press. Reprinted in Anderson, A. R., ed., 1964. Minds and Machines. Prentice-Hall: 77.
• 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.
• Jean van Heijenoort, 1963. "Gödel's Theorem" in Edwards, Paul, ed., Encyclopedia of Philosophy, Vol. 3. Macmillan: 348-57.
• Richard Zach, 2005, "Paper on the incompleteness theorems" in Grattan-Guiness, I., ed., Landmark Writings in Western Mathematics. Elsevier: 917-25.

Books about the theorems

• Domeisen, Norbert, 1990. Logik der Antinomien. Bern: Peter Lang. 142 S. 1990. ISBN 3-261-04214-1. Zentralblatt MATH
• Torkel Franzén, 2005. Gödel's Theorem: An Incomplete Guide to its Use and Abuse. A.K. Peters. ISBN 1568812388 MR2007d:03001
• Douglas Hofstadter, 1979. Gödel, Escher, Bach: An Eternal Golden Braid. Vintage Books. ISBN 0465026850. 1999 reprint: ISBN 0465026567. MR80j:03009
• Douglas Hofstadter, 2007. I Am a Strange Loop. Basic Books. ISBN 9780465030781. ISBN 0465030785. MR2008g:00004
• Stanley Jaki, OSB, 2005. The drama of the quantities. Real View Books.
• J.R. Lucas, FBA, 1970. The Freedom of the Will. Clarendon Press, Oxford, 1970.
• Ernest Nagel, James Roy Newman, Douglas R. Hofstadter, 2002 (1958). Gödel's Proof, revised ed. ISBN 0814758169. MR2002i:03001
• Rudy Rucker, 1995 (1982). Infinity and the Mind: The Science and Philosophy of the Infinite. Princeton Univ. Press. MR84d:03012
• Smith, Peter, 2007. An Introduction to Gödel's Theorems. Cambridge University Press. MathSciNet
• Raymond Smullyan, 1991. Godel's Incompleteness Theorems. Oxford Univ. Press.
• —, 1994. Diagonalization and Self-Reference. Oxford Univ. Press. MR96c:03001
• Hao Wang, 1997. A Logical Journey: From Gödel to Philosophy. MIT Press. ISBN 0262231891 MR97m:01090

Miscellaneous references

• John W. Dawson, Jr., 1997. Logical Dilemmas: The Life and Work of Kurt Gödel, A.K. Peters, Wellesley Mass, ISBN 1-56881-256-6.
• Goldstein, Rebecca, 2005, Incompleteness: the Proof and Paradox of Kurt Gödel, W. W. Norton & Company. ISBN 0-393-05169-2
• John Hopcroft and Jeffrey Ullman 1979, Introduction to Automata theory, Addison-Wesley, ISBN 0-201-02988-X
• Stephen Cole Kleene, 1967, Mathematical Logic. Reprinted by Dover, 2002. ISBN 0-486-42533-9
• Alan Sokal and Jean Bricmont, 1999, Fashionable Nonsense: Postmodern Intellectuals' Abuse of Science, Picador. ISBN 0-31-220407-8
• Jeremy Stangroom and Ophelia Benson, Why Truth Matters, Continuum. ISBN 0-82-649528-1

External links

• Stanford Encyclopedia of Philosophy: "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.

Template:Computable knowledge

• Mathematical theorems
• Mathematical logic
• Model theory
• Proof theory
• Epistemology