en.wikipedia.org, 2023-01-01 | Main page
Saved from web.archive.org, with Lynx.
   #alternate Edit this page Wikipedia (en)

Goedel's incompleteness theorems

   From Wikipedia, the free encyclopedia
   This is the latest accepted revision, reviewed on 23 December 2022.
   Jump to navigation Jump to search
   Limitative results in mathematical logic
   "Bew" redirects here. For other uses, see Bew (disambiguation).

   Goedel's incompleteness theorems are two theorems of mathematical logic
   that are concerned with the limits of provability in formal axiomatic
   theories. These results, published by Kurt Goedel 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 (i.e., an
   algorithm) is capable of proving all truths about the arithmetic of
   natural numbers. For any such consistent formal system, there will
   always be statements about 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, Goedel'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.
   [ ]


     * 1 Formal systems: completeness, consistency, and effective
          + 1.1 Effective axiomatization
          + 1.2 Completeness
          + 1.3 Consistency
          + 1.4 Systems which contain arithmetic
          + 1.5 Conflicting goals
     * 2 First incompleteness theorem
          + 2.1 Syntactic form of the Goedel sentence
          + 2.2 Truth of the Goedel sentence
          + 2.3 Relationship with the liar paradox
          + 2.4 Extensions of Goedel's original result
     * 3 Second incompleteness theorem
          + 3.1 Expressing consistency
          + 3.2 The Hilbert-Bernays conditions
          + 3.3 Implications for consistency proofs
     * 4 Examples of undecidable statements
          + 4.1 Undecidable statements provable in larger systems
     * 5 Relationship with computability
     * 6 Proof sketch for the first theorem
          + 6.1 Arithmetization of syntax
          + 6.2 Construction of a statement about "provability"
          + 6.3 Diagonalization
          + 6.4 Proof via Berry's paradox
          + 6.5 Computer verified proofs
     * 7 Proof sketch for the second theorem
     * 8 Discussion and implications
          + 8.1 Consequences for logicism and Hilbert's second problem
          + 8.2 Minds and machines
          + 8.3 Paraconsistent logic
          + 8.4 Appeals to the incompleteness theorems in other fields
     * 9 History
          + 9.1 Announcement
          + 9.2 Generalization and acceptance
          + 9.3 Criticisms
               o 9.3.1 Finsler
               o 9.3.2 Zermelo
               o 9.3.3 Wittgenstein
     * 10 See also
     * 11 References
          + 11.1 Citations
          + 11.2 Articles by Goedel
          + 11.3 Translations, during his lifetime, of Goedel's paper into
          + 11.4 Articles by others
          + 11.5 Books about the theorems
          + 11.6 Miscellaneous references
     * 12 External links

Formal systems: completeness, consistency, and effective axiomatization[edit]

   The incompleteness theorems apply to formal systems that are of
   sufficient complexity to express the basic arithmetic of the natural
   numbers and which are consistent and effectively axiomatized.
   Particularly in the context of first-order 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 first-order 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[edit]

   A formal system is said to be effectively axiomatized (also called
   effectively generated) if its set of theorems is a recursively
   enumerable set (Franzen 2005, 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


   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 Goedel's first Incompleteness theorem. It is not to be
   confused with semantic completeness, which means that the set of axioms
   proves all the semantic tautologies of the given language. In his
   completeness theorem (not to be confused with the incompleteness
   theorems described here), Goedel 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

   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 one to either prove or disprove (by proving its negation) each
   and every mathematical formula.

   A formal system might be syntactically incomplete by design, 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 some statements in the language (such as the parallel postulate
   itself) can not be proved 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 first order Peano arithmetic seems to be consistent.
   Assuming this is indeed the case, note that it 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 arithmetic. Moreover, this
   statement is true in the usual model. In addition, no effectively
   axiomatized, consistent extension of Peano arithmetic can be complete.


   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. That is to say, a consistent axiomatic
   system is one that is free from contradiction.

   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 k is the least such cardinal, then V[k] 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[edit]

   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 Goedel'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 Goedel
   numbering, but which are not strong enough to have multiplication as a
   function, and so fail to prove the second incompleteness theorem; that
   is to say, these systems are consistent and capable of proving their
   own consistency (see self-verifying theories).

Conflicting goals[edit]

   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 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 (Hinman 2005, p. 143) harv
   error: no target: CITEREFHinman2005 (help).

   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 continuum hypothesis, which is unresolvable^[1] in
   ZFC + "there exists an inaccessible cardinal".

   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[edit]

   See also: Proof sketch for Goedel's first incompleteness theorem

   Goedel's first incompleteness theorem first appeared as "Theorem VI" in
   Goedel'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; i.e., there are statements of the language of F which
     can neither be proved nor disproved in F." (Raatikainen 2020)

   The unprovable statement G[F] referred to by the theorem is often
   referred to as "the Goedel sentence" for the system F. The proof
   constructs a particular Goedel 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 Goedel sentence and any
   logically valid sentence.

   Each effectively generated system has its own Goedel sentence. It is
   possible to define a larger system F' that contains the whole of F plus
   G[F] as an additional axiom. This will not result in a complete system,
   because Goedel's theorem will also apply to F', and thus F' also cannot
   be complete. In this case, G[F] is indeed a theorem in F', because it
   is an axiom. Because G[F] 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
   Goedel statement G[F'] for F', showing that F' is also incomplete.
   G[F']will differ from G[F] in that G[F'] will refer to F', rather
   than F.

Syntactic form of the Goedel sentence[edit]

   The Goedel 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 G[F] itself. In this way, the
   Goedel sentence G[F] indirectly states its own unprovability within F
   (Smith 2007, p. 135).

   To prove the first incompleteness theorem, Goedel demonstrated that the
   notion of provability within a system could be expressed purely in
   terms of arithmetical functions that operate on Goedel 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 Goedel sentence refers indirectly to sentences of
   the system F, when read as an arithmetical statement the Goedel
   sentence directly refers only to natural numbers. 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
   Goedel sentence can be written in the language of arithmetic with a
   simple syntactic form. In particular, it can be expressed as a formula
   in the language of arithmetic consisting of a number of leading
   universal quantifiers followed by a quantifier-free body (these
   formulas are at level
   [MATH: <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle
   displaystyle="true" scriptlevel="0"> <msubsup> <mi
   mathvariant="normal">P</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn>
   </mrow> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msubsup>
   </mstyle> </mrow> <annotation
   encoding="application/x-tex">{\displaystyle \Pi _{1}^{0}}</annotation>
   </semantics> :MATH]
   \Pi _{1}^{0} of the arithmetical hierarchy). Via the MRDP theorem, the
   Goedel sentence can be re-written 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 (Franzen
   2005, p. 71).

Truth of the Goedel sentence[edit]

   The first incompleteness theorem shows that the Goedel sentence G[F] of
   an appropriate formal theory F is unprovable in F. Because, when
   interpreted as a statement about arithmetic, this unprovability is
   exactly what the sentence (indirectly) asserts, the Goedel sentence is,
   in fact, true (Smorynski 1977, p. 825; also see Franzen 2005,
   pp. 28-33). For this reason, the sentence G[F] is often said to be
   "true but unprovable." (Raatikainen 2015) harv error: no target:
   CITEREFRaatikainen2015 (help). However, since the Goedel sentence
   cannot itself formally specify its intended interpretation, the truth
   of the sentence G[F] may only be arrived at via a meta-analysis from
   outside the system. In general, this meta-analysis can be carried out
   within the weak formal system known as primitive recursive arithmetic,
   which proves the implication Con(F)->G[F], where Con(F) is a canonical
   sentence asserting the consistency of F (Smorynski 1977, p. 840,
   Kikuchi & Tanaka 1994, p. 403).

   Although the Goedel sentence of a consistent theory is true as a
   statement about the intended interpretation of arithmetic, the Goedel
   sentence will be false in some nonstandard models of arithmetic, as a
   consequence of Goedel's completeness theorem (Franzen 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 Goedel 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 Goedel sentence follows from the fact that no standard natural
   number has the property in question. Any model in which the Goedel
   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 harvnb error: no target:
   CITEREFRaatikainen2015 (help), Franzen 2005, p. 135).

Relationship with the liar paradox[edit]

   Goedel 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 Goedel 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 Goedel
   sentence because the predicate "Q is the Goedel 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 Goedel, when he was working on the proof of the incompleteness
   theorem, and by the theorem's namesake, Alfred Tarski.

Extensions of Goedel's original result[edit]

   Compared to the theorems stated in Goedel'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.

   Goedel 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. Goedel 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 Goedel published his results.

   Goedel's original statement and proof of the incompleteness theorem
   requires the assumption that the system is not just consistent but
   w-consistent. A system is w-consistent if it is not w-inconsistent, and
   is w-inconsistent if there is a predicate P such that for every
   specific natural number m the system proves ~P(m), and yet the system
   also proves that there exists a natural number n such that P(n). That
   is, the system says that a number with property P exists while denying
   that it has any specific value. The w-consistency of a system implies
   its consistency, but consistency does not imply w-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 w-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 w-consistent, and thus Goedel's theorem as originally stated
   applies to them. The stronger version of the incompleteness theorem
   that only assumes consistency, rather than w-consistency, is now
   commonly known as Goedel's incompleteness theorem and as the
   Goedel-Rosser theorem.

Second incompleteness theorem[edit]

   For each formal system F containing basic arithmetic, it is possible to
   canonically define a formula Cons(F) 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 Cons(F) states "there is no
   natural number that codes a derivation of '0=1' from the axioms of F."

   Goedel's second incompleteness theorem shows that, under general
   assumptions, this canonical consistency statement Cons(F) will not be
   provable in F. The theorem first appeared as "Theorem XI" in Goedel'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: "For any consistent system F within
     which a certain amount of elementary arithmetic can be carried out,
     the consistency of F cannot be proved in F itself." (Raatikainen

     can also be written as

     "Assume F is a consistent formalized system which contains
     elementary arithmetic. Then
     [MATH: <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle
     displaystyle="true" scriptlevel="0"> <mi>F</mi> <mo> !PROVES </mo>
     <mrow class="MJX-TeXAtom-ORD"> <mtext>Cons</mtext> </mrow> <mo
     stretchy="false">(</mo> <mi>F</mi> <mo stretchy="false">)</mo>
     </mstyle> </mrow> <annotation
     encoding="application/x-tex">{\displaystyle F\not \vdash
     {\text{Cons}}(F)}</annotation> </semantics> :MATH]
     {\displaystyle F\not \vdash {\text{Cons}}(F)} ." (Raatikainen 2020)
     (Then F does not prove consistency of F)

   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[edit]

   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
   Cons(F) 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,
   first-order 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[edit]

   The standard proof of the second incompleteness theorem assumes that
   the provability predicate Prov[A](P) satisfies the Hilbert-Bernays
   provability conditions. Letting #(P) represent the Goedel number of a
   formula P, the provability conditions say:
    1. If F proves P, then F proves Prov[A](#(P)).
    2. F proves 1.; that is, F proves Prov[A](#(P)) ->
    3. F proves Prov[A](#(P -> Q)) AND Prov[A](#(P)) -> Prov[A](#(Q))
       (analogue of modus ponens).

   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[edit]

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

   This corollary of the second incompleteness theorem shows that there is
   no hope of proving, for example, the consistency of Peano arithmetic
   using any finitistic means that can be formalized in a 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 (Franzen 2005, 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 altogether the
   possibility of proving the consistency of some theory T, only doing so
   in a theory that T itself can prove to be consistent. For example,
   Gerhard Gentzen proved the consistency of Peano arithmetic in a
   different system that includes an axiom asserting that the ordinal
   called e[0] is wellfounded; see Gentzen's consistency proof. Gentzen's
   theorem spurred the development of ordinal analysis in proof theory.

Examples of undecidable statements[edit]

   See also: List of statements independent of 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 Goedel'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 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 Goedel 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. Goedel 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

   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 Goedel's theorem is related to the
   liar paradox, Chaitin's result is related to Berry's paradox.

Undecidable statements provable in larger systems[edit]

   These are natural mathematical equivalents of the Goedel "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
   (first-order) Peano arithmetic, but can be proved in the stronger
   system of second-order 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[edit]

   See also: Halting problem S: Goedel's incompleteness theorems

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

   Stephen Cole Kleene (1943) presented a proof of Goedel'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) harvtxt error: no target:
   CITEREFShoenfield1967 (help); Charlesworth (1980) harvtxt error: no
   target: CITEREFCharlesworth1980 (help); and Hopcroft & Ullman (1979)
   harvtxt error: no target: CITEREFHopcroftUllman1979 (help).

   Franzen (2005, p. 73) explains how Matiyasevich's solution to Hilbert's
   10th problem can be used to obtain a proof to Goedel's first
   incompleteness theorem. Matiyasevich proved that there is no algorithm
   that, given a multivariate polynomial p(x[1], x[2],...,x[k]) with
   integer coefficients, determines whether there is an integer solution
   to the equation p = 0. Because polynomials with integer coefficients,
   and integers themselves, are directly expressible in the language of
   arithmetic, if a multivariate integer polynomial equation p = 0 does
   have a solution in the integers then any sufficiently strong system of
   arithmetic T will prove this. Moreover, if the system T is
   w-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 w-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. Hence it follows that T cannot be w-consistent
   and complete. 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, p. 416; Jones 1980 harvnb error: no target:
   CITEREFJones1980 (help)).

   Smorynski (1977, p. 842) harvtxt error: no target: CITEREFSmorynski1977
   (help) 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 harvnb error: no target:
   CITEREFKleene1967 (help)).

   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. Goedel'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 w-inconsistent.

Proof sketch for the first theorem[edit]

   Main article: Proof sketch for Goedel's first incompleteness theorem

   The proof by contradiction has three essential parts. To begin, choose
   a formal system that meets the proposed criteria:
    1. Statements in the system can be represented by natural numbers
       (known as Goedel numbers). The significance of this is that
       properties of statements--such as their truth and falsehood--will
       be equivalent to determining whether their Goedel numbers have
       certain properties, and that properties of the statements can
       therefore be demonstrated by examining their Goedel 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).
    2. In the formal system it is possible to construct a number whose
       matching statement, when interpreted, is self-referential and
       essentially says that it (i.e. the statement itself) is unprovable.
       This is done using a technique called "diagonalization" (so-called
       because of its origins as Cantor's diagonal argument).
    3. 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 w-consistent. Hence the
       original assumption that the proposed system met the criteria is

  Arithmetization of syntax[edit]

   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. Goedel's 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 self-referential formula to be constructed in a way that
   avoids any infinite regress of definitions. The same technique was
   later used by Alan Turing in his work on the Entscheidungsproblem.

   In simple terms, a method can be devised so that every formula or
   statement that can be formulated in the system gets a unique number,
   called its Goedel number, in such a way that it is possible to
   mechanically convert back and forth between formulas and Goedel
   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 how English can be
   stored as a sequence of numbers for each letter and then combined into
   a single larger number:

          + The word hello is encoded as 104-101-108-108-111 in ASCII,
            which can be converted into the number 104101108108111.
          + The logical statement x=y => y=x is encoded as
            120-061-121-032-061-062-032-121-061-120 in ASCII, which can be
            converted into 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"[edit]

   Having shown that in principle the system can indirectly make
   statements about provability, by analyzing properties of those numbers
   representing statements it is now possible to show how to create a
   statement that actually does this.

   A formula F(x) that contains exactly one free variable x is called a
   statement form or class-sign. As soon as x is replaced by a specific
   number, the statement form turns into a bona fide statement, and it is
   then either provable in the system, or not. For certain formulas one
   can show that for every natural number n,
   [MATH: <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle
   displaystyle="true" scriptlevel="0"> <mi>F</mi> <mo
   stretchy="false">(</mo> <mi>n</mi> <mo stretchy="false">)</mo>
   </mstyle> </mrow> <annotation
   encoding="application/x-tex">{\displaystyle F(n)}</annotation>
   </semantics> :MATH]
   F(n) 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 =

   Statement forms themselves are not statements and therefore cannot be
   proved or disproved. But every statement form F(x) can be assigned a
   Goedel number denoted by G(F). The choice of the free variable used in
   the form F(x) is not relevant to the assignment of the Goedel number

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

          Bew(y) = TE x (y is the Goedel number of a formula and x is the
          Goedel 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 Goedel 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 Goedel number, the existence
   of which causes Bew(G(p)) to be satisfied.


   The next step in the proof is to obtain a statement which, indirectly,
   asserts its own unprovability. Although Goedel 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)).

   By letting F be the negation of Bew(x), we obtain the theorem

          p <-> ~Bew(G(p))

   and the p defined by this roughly states that its own Goedel number is
   the Goedel 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 Goedel number
   will be that of an unprovable statement. But when this calculation is
   performed, the resulting Goedel number turns out to be the Goedel
   number of p itself. This is similar to the following sentence in

          ", 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 indirectly asserts its own unprovability. The
   proof of the diagonal lemma employs a similar method.

   Now, assume that the axiomatic system is w-consistent, and let p be the
   statement obtained in the previous section.

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

   If the negation of p were provable, then Bew(G(p)) would be provable
   (because p was constructed to be equivalent to the negation of
   Bew(G(p))). However, for each specific number x, x cannot be the Goedel
   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 Goedel 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 w-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 w-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 w-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

   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 Goedel number of a proof" of a statement
   changes. which means that the formula Bew(x) 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 w-consistent.

  Proof via Berry's paradox[edit]

   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) harv error: no target: CITEREFBoolos1998 (help). 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) harv
   error: no target: CITEREFBoolos1998 (help).

  Computer verified proofs[edit]

   See also: Automated theorem proving

   The 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. Goedel's
   original proofs of the incompleteness theorems, like most mathematical
   proofs, were written in natural language intended for human readers.

   Computer-verified proofs of versions of the first incompleteness
   theorem were announced by Natarajan Shankar in 1986 using Nqthm
   (Shankar 1994) harv error: no target: CITEREFShankar1994 (help), by
   Russell O'Connor in 2003 using Coq (O'Connor 2005) harv error: no
   target: CITEREFO'Connor2005 (help) and by John Harrison in 2009 using
   HOL Light (Harrison 2009) harv error: no target: CITEREFHarrison2009
   (help). A computer-verified proof of both incompleteness theorems was
   announced by Lawrence Paulson in 2013 using Isabelle (Paulson 2014)
   harv error: no target: CITEREFPaulson2014 (help).

Proof sketch for the second theorem[edit]

   See also: Hilbert-Bernays provability conditions

   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 a system S using
   a formal predicate P for provability. Once this is done, the second
   incompleteness theorem follows by formalizing the entire proof of the
   first incompleteness theorem within the system S itself.

   Let p stand for the undecidable sentence constructed above, and assume
   for purposes of obtaining a contradiction that the consistency of the
   system S can be proved from within the system S itself. This is
   equivalent to proving the statement "System S is consistent". Now
   consider the statement c, where c = "If the system S is consistent,
   then p is not provable". The proof of sentence c can be formalized
   within the system S, and therefore the statement c, "p is not
   provable", (or identically, "not P(p)") can be proved in the system S.

   Observe then, that if we can prove that the system S is consistent (ie.
   the statement in the hypothesis of c), then we have proved that p is
   not provable. But this is a contradiction since by the 1st
   Incompleteness Theorem, this sentence (ie. what is implied in the
   sentence c, ""p" is not provable") is what we construct to be
   unprovable. Notice that this is why we require formalizing the first
   Incompleteness Theorem in S: to prove the 2nd Incompleteness Theorem,
   we obtain a contradiction with the 1st Incompleteness Theorem which can
   do only by showing that the theorem holds in S. So we cannot prove that
   the system S is consistent. And the 2nd Incompleteness Theorem
   statement follows.

Discussion and implications[edit]

   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[edit]

   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, pp. 451-468) harv error: no target:
   CITEREFHellman1981 (help). 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 Goedel'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[edit]

   Main article: Mechanism (philosophy) S: Goedelian arguments

   Authors including the philosopher J. R. Lucas and physicist Roger
   Penrose have debated what, if anything, Goedel'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 Goedel's incompleteness theorems would
   apply to it.

   Hilary Putnam (1960) suggested that while Goedel'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

   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 Goedel
   phenomena are very much with us."

   Douglas Hofstadter, in his books Goedel, Escher, Bach and I Am a
   Strange Loop, cites Goedel's theorems as an example of what he calls a
   strange loop, a hierarchical, self-referential structure existing
   within an axiomatic formal system. He argues that this is the same kind
   of structure which gives rise to consciousness, the sense of "I", in
   the human mind. While the self-reference in Goedel's theorem comes from
   the Goedel sentence asserting its own unprovability within the formal
   system of Principia Mathematica, the self-reference in the human mind
   comes from the way in which the brain abstracts and categorises stimuli
   into "symbols", or groups of neurons which respond to concepts, in what
   is effectively also a formal system, eventually giving rise to symbols
   modelling the concept of the very entity doing the perception.
   Hofstadter argues that a strange loop in a sufficiently complex formal
   system can give rise to a "downward" or "upside-down" causality, a
   situation in which the normal hierarchy of cause-and-effect is flipped
   upside-down. In the case of Goedel's theorem, this manifests, in short,
   as the following:

   "Merely from knowing the formula's meaning, one can infer its truth or
   falsity without any effort to derive it in the old-fashioned way, which
   requires one to trudge methodically "upwards" from the axioms. This is
   not just peculiar; it is astonishing. Normally, one cannot merely look
   at what a mathematical conjecture says and simply appeal to the content
   of that statement on its own to deduce whether the statement is true or
   false." (I Am a Strange Loop.)^[3]

   In the case of the mind, a far more complex formal system, this
   "downward causality" manifests, in Hofstadter's view, as the ineffable
   human instinct that the causality of our minds lies on the high level
   of desires, concepts, personalities, thoughts and ideas, rather than on
   the low level of interactions between neurons or even fundamental
   particles, even though according to physics the latter seems to possess
   the causal power.

   "There is thus a curious upside-downness to our normal human way of
   perceiving the world: we are built to perceive "big stuff" rather than
   "small stuff", even though the domain of the tiny seems to be where the
   actual motors driving reality reside." (I Am a Strange Loop.)^[3]

  Paraconsistent logic[edit]

   Although Goedel'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
   Goedel'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, p. 47) harv error: no target: CITEREFPriest2006 (help). Stewart
   Shapiro (2002) gives a more mixed appraisal of the applications of
   Goedel's theorems to dialetheism.

  Appeals to the incompleteness theorems in other fields[edit]

   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 Franzen (2005); Panu Raatikainen
   (2005); Alan Sokal and Jean Bricmont (1999); and Ophelia Benson and
   Jeremy Stangroom (2006). Bricmont & Stangroom (2006, p. 10) harvtxt
   error: no target: CITEREFBricmontStangroom2006 (help), for example,
   quote from Rebecca Goldstein's comments on the disparity between
   Goedel's avowed Platonism and the anti-realist uses to which his ideas
   are sometimes put. Sokal & Bricmont (1999, p. 187) harvtxt error: no
   target: CITEREFSokalBricmont1999 (help) criticize Regis Debray's
   invocation of the theorem in the context of sociology; Debray has
   defended this use as metaphorical (ibid.).


   After Goedel 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 second-order arithmetic
   were known as "analysis", while theories of the natural numbers alone
   were known as "arithmetic".

   Goedel 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 e-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 2007, p. 418;
   Zach 2003, p. 33).

   In the course of his research, Goedel discovered that although a
   sentence which asserts its own falsehood leads to paradox, a sentence
   that asserts its own non-provability does not. In particular, Goedel
   was aware of the result now called Tarski's indefinability theorem,
   although he never published it. Goedel announced his first
   incompleteness theorem to Carnap, Feigel and Waismann on August 26,
   1930; all four would attend the Second Conference on the Epistemology
   of the Exact Sciences, a key conference in Koenigsberg the following


   The 1930 Koenigsberg conference was a joint meeting of three academic
   societies, with many of the key logicians of the time in attendance.
   Carnap, Heyting, and von Neumann delivered one-hour addresses on the
   mathematical philosophies of logicism, intuitionism, and formalism,
   respectively (Dawson 1996, p. 69). The conference also included
   Hilbert's retirement address, as he was leaving his position at the
   University of Goettingen. Hilbert used the speech to argue his belief
   that all mathematical problems can be solved. He ended his address by

     For the mathematician there is no Ignorabimus, and, in my opinion,
     not at all for natural science either. ... The true reason why [no
     one] has succeeded in finding an unsolvable problem is, in my
     opinion, that there is no unsolvable problem. In contrast to the
     foolish Ignorabimus, 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 muessen wissen. Wir werden
   wissen!", were used as Hilbert's epitaph in 1943). Although Goedel was
   likely in attendance for Hilbert's address, the two never met face to
   face (Dawson 1996, p. 72).

   Goedel 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 Goedel
   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
   Goedel in a letter dated November 20, 1930 (Dawson 1996, p. 70). Goedel
   had independently obtained the second incompleteness theorem and
   included it in his submitted manuscript, which was received by
   Monatshefte fuer Mathematik on November 17, 1930.

   Goedel's paper was published in the Monatshefte in 1931 under the title
   "Ueber formal unentscheidbare Saetze der Principia Mathematica und
   verwandter Systeme I" ("On Formally Undecidable Propositions in
   Principia Mathematica and Related Systems I"). As the title implies,
   Goedel originally planned to publish a second part of the paper in the
   next volume of the Monatshefte; the prompt acceptance of the first
   paper was one reason he changed his plans (van Heijenoort 1967, page
   328, footnote 68a) harv error: no target: CITEREFvan_Heijenoort1967

  Generalization and acceptance[edit]

   Goedel 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, Goedel 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 w-consistency, which was an integral part of Goedel's
   original proof, could be replaced by simple consistency, if the Goedel
   sentence was changed in an appropriate way. These developments left the
   incompleteness theorems in essentially their modern form.

   Gentzen published his consistency proof for first-order arithmetic in
   1936. Hilbert accepted this proof as "finitary" although (as Goedel'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 e-substitution method
   and Gentzen's consistency proof of arithmetic. This was the first full
   published proof of the second incompleteness theorem.



   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. Goedel was unaware of this paper when he
   proved the incompleteness theorems (Collected Works Vol. IV., p. 9).
   Finsler wrote to Goedel 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 Goedel's work (van Heijenoort 1967, p. 328)
   harv error: no target: CITEREFvan_Heijenoort1967 (help). Goedel read
   the paper but found it deeply flawed, and his response to Finsler laid
   out concerns about the lack of formalization (Dawson, p. 89 harvnb
   error: no target: CITEREFDawson (help)^[full citation needed]). Finsler
   continued to argue for his philosophy of mathematics, which eschewed
   formalization, for the remainder of his career.


   In September 1931, Ernst Zermelo wrote to Goedel to announce what he
   described as an "essential gap" in Goedel's argument (Dawson, p. 76
   harvnb error: no target: CITEREFDawson (help)^[full citation needed]).
   In October, Goedel replied with a 10-page letter (Dawson, p. 76 harvnb
   error: no target: CITEREFDawson (help)^[full citation needed],
   Grattan-Guinness, pp. 512-513 harvnb error: no target:
   CITEREFGrattan-Guinness (help)^[full citation needed]), 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" (Grattan-Guinness, pp. 513 harvnb error: no
   target: CITEREFGrattan-Guinness (help)^[full citation needed]). Goedel
   decided that to pursue the matter further was pointless, and Carnap
   agreed (Dawson, p. 77 harvnb error: no target: CITEREFDawson
   (help)^[full citation needed]). Much of Zermelo's subsequent work was
   related to logics stronger than first-order logic, with which he hoped
   to show both the consistency and categoricity of mathematical theories.


   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. Goedel was a member of the
   Vienna Circle during the period in which Wittgenstein's early ideal
   language philosophy and Tractatus Logico-Philosophicus dominated the
   circle's thinking. There has been some controversy about whether
   Wittgenstein misunderstood the incompleteness theorem or just expressed
   himself unclearly. Writings in Goedel's Nachlass express the belief
   that Wittgenstein misread his ideas.

   Multiple commentators have read Wittgenstein as misunderstanding Goedel
   (Rodych 2003) harv error: no target: CITEREFRodych2003 (help), 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, p. 208) harv error: no target:
   CITEREFBerto2009 (help). The unanimity of this criticism caused
   Wittgenstein's remarks on the incompleteness theorems to have little
   impact on the logic community. In 1972, Goedel stated: "Has
   Wittgenstein lost his mind? Does he mean it seriously? He intentionally
   utters trivially nonsensical statements" (Wang 1996, p. 179) harv
   error: no target: CITEREFWang1996 (help), 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 [the first incompleteness theorem] (or pretended not to
     understand it). He interpreted it as a kind of logical paradox,
     while in fact is just the opposite, namely a mathematical theorem
     within an absolutely uncontroversial part of mathematics (finitary
     number theory or combinatorics). (Wang 1996, p. 179) harv error: no
     target: CITEREFWang1996 (help)

   Since the publication of Wittgenstein's Nachlass in 2000, a series of
   papers in philosophy have sought to evaluate whether the original
   criticism of Wittgenstein's remarks was justified. Floyd & 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 Goedel sentence for
   an w-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) harvtxt error: no target:
   CITEREFRodych2003 (help) argues that their interpretation of
   Wittgenstein is not historically justified, while Bays (2004) harvtxt
   error: no target: CITEREFBays2004 (help) argues against Floyd and
   Putnam's philosophical analysis of the provability predicate. Berto
   (2009) harvtxt error: no target: CITEREFBerto2009 (help) explores the
   relationship between Wittgenstein's writing and theories of
   paraconsistent logic.

See also[edit]

     * Philosophy portal
     * icon Mathematics portal

     * Goedel machine
     * Goedel's completeness theorem
     * Goedel's speed-up theorem
     * Goedel, Escher, Bach
     * Loeb's Theorem
     * Minds, Machines and Goedel
     * Non-standard model of arithmetic
     * Proof theory
     * Provability logic
     * Quining
     * Tarski's undefinability theorem
     * Theory of everything#Goedel's incompleteness theorem
     * Typographical Number Theory



    1. ^ in technical terms: independent; see Continuum
       hypothesis#Independence from ZFC
    2. ^ Shelah, Saharon (1974). "Infinite Abelian groups, Whitehead
       problem and some constructions". Israel Journal of Mathematics. 18
       (3): 243-256. doi:10.1007/BF02757281. MR 0357114.
    3. ^ ^a ^b Hofstadter, Douglas R. (2007) [2003]. "Chapter 12. On
       Downward Causality". I Am a Strange Loop. ISBN 978-0-465-03078-1.

  Articles by Goedel[edit]

     * Kurt Goedel, 1931, "Ueber formal unentscheidbare Saetze der
       Principia Mathematica und verwandter Systeme, I", Monatshefte fuer
       Mathematik und Physik, v. 38 n. 1, pp. 173-198.


     --, 1931, "Ueber formal unentscheidbare Saetze der Principia
   Mathematica und verwandter Systeme, I", in Solomon Feferman, ed., 1986.
   Kurt Goedel Collected works, Vol. I. Oxford University Press,
   pp. 144-195. ISBN 978-0195147209. The original German with a facing
   English translation, preceded by an introductory note by Stephen Cole

     --, 1951, "Some basic theorems on the foundations of mathematics and
   their implications", in Solomon Feferman, ed., 1995. Kurt Goedel
   Collected works, Vol. III, Oxford University Press, pp. 304-323.
   ISBN 978-0195147223.

  Translations, during his lifetime, of Goedel's paper into English[edit]

   None of the following agree in all translated words and in typography.
   The typography is a serious matter, because Goedel expressly wished to
   emphasize "those metamathematical notions that had been defined in
   their usual sense before . . ." (van Heijenoort 1967, p. 595) harv
   error: no target: CITEREFvan_Heijenoort1967 (help). 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; "Goedel also complained about Braithwaite's
   commentary (Dawson 1997, p. 216). "Fortunately, the Meltzer translation
   was soon supplanted by a better one prepared by Elliott Mendelson for
   Martin Davis's anthology The Undecidable . . . he found the translation
   "not quite so good" as he had expected . . . [but because of time
   constraints he] agreed to its publication" (ibid). (In a footnote
   Dawson states that "he would regret his compliance, for the published
   volume was marred throughout by sloppy typography and numerous
   misprints" (ibid)). Dawson states that "The translation that Goedel
   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 Goedel at to
   the Institute for Advanced Study during the spring of 1934" (cf
   commentary by Davis 1965, p. 39 harvnb error: no target:
   CITEREFDavis1965 (help) 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

   ISBN 0-486-66980-7 (pbk.) This contains a useful translation of
   Goedel'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. Goedel'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. Goedel's paper begins on
       page 5, preceded by one page of commentary.
     * Jean van Heijenoort editor, 1967, 3rd edition 1967. From Frege to
       Goedel: A Source Book in Mathematical Logic, 1879-1931, Harvard
       University Press, Cambridge Mass.,

   ISBN 0-674-32449-8 (pbk). van Heijenoort did the translation. He states
   that "Professor Goedel approved the translation, which in many places
   was accommodated to his wishes." (p. 595). Goedel'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 Goedel's corrections of
   errata and Goedel'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[edit]

     * George Boolos, 1989, "A New Proof of the Goedel Incompleteness
       Theorem", Notices of the American Mathematical Society, v, 36,
       pp. 388-390 and p. 676, reprinted in Boolos, 1998, Logic, Logic,
       and Logic, Harvard Univ. Press.

   ISBN 0-674-53766-1

     Bernd Buldt, 2014, "The Scope of Goedel's First Incompleteness
   Theorem Archived 2016-03-06 at the Wayback Machine", Logica
   Universalis, v. 8, pp. 499-552. doi:10.1007/s11787-014-0107-3

     Charlesworth, Arthur (1981). "A Proof of Godel's Theorem in Terms of
   Computer Programs". Mathematics Magazine. 54 (3): 109-121.
   doi:10.2307/2689794. JSTOR 2689794.

     Davis, Martin (2006). "The Incompleteness Theorem" (PDF). Notices of
   the AMS. 53 (4): 414.

     Jean van Heijenoort, 1963, "Goedel's Theorem" in Edwards, Paul, ed.,
   Encyclopedia of Philosophy, v. 3. Macmillan, pp. 348-57.

     Geoffrey Hellman, 1981, "How to Goedel a Frege-Russell: Goedel's
   Incompleteness Theorems and Logicism", Nous, 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 Goedel's paper. Archived from the original. Sept. 16, 2004.

     Kikuchi, Makoto; Tanaka, Kazuyuki (July 1994). "On Formalization of
   Model-Theoretic Proofs of Goedel's Theorems". Notre Dame Journal of
   Formal Logic. 35 (3): 403-412. doi:10.1305/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.

     Raatikainen, Panu (2020). "Goedel's Incompleteness Theorems".
   Stanford Encyclopedia of Philosophy. Retrieved November 7, 2022.

     Raatikainen, Panu (2005). "On the philosophical relevance of Goedel's
   incompleteness theorems". Revue Internationale de Philosophie. 59 (4):
   513-534. doi:10.3917/rip.234.0513. S2CID 52083793.

     John Barkley Rosser, 1936, "Extensions of some theorems of Goedel 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 Goedel'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

     Smorynski, C. (1977). "The incompleteness theorems". In Jon Barwise
   (ed.). Handbook of mathematical logic. Amsterdam: North-Holland Pub.
   Co. pp. 821-866. ISBN 978-0-444-86388-1.

     Dan E. Willard, 2001, "Self-Verifying Axiom Systems, the
   Incompleteness Theorem and Related Reflection Principles", Journal of
   Symbolic Logic, v. 66 n. 2, pp. 536-596. doi:10.2307/2695030
   JSTOR 2695030

     Zach, Richard (2003). "The Practice of Finitism: Epsilon Calculus and
   Consistency Proofs in Hilbert's Program" (PDF). Synthese. Springer
   Science and Business Media LLC. 137 (1): 211-259. arXiv:math/0102189.
   doi:10.1023/a:1026247421383. ISSN 0039-7857. S2CID 16657040.

     Zach, Richard (2005). "Kurt Goedel, paper on the incompleteness
   theorems (1931)". In Grattan-Guinness, Ivor (ed.). Landmark Writings in
   Western Mathematics 1640-1940. Elsevier. pp. 917-925.
   doi:10.1016/b978-044450871-3/50152-2. ISBN 9780444508713.

  Books about the theorems[edit]

     * Francesco Berto. There's Something about Goedel: 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 3-261-04214-1. Zbl 0724.03003.

     Franzen, Torkel (2005). Goedel's theorem : an incomplete guide to its
   use and abuse. Wellesley, MA: A K Peters. ISBN 1-56881-238-8.
   MR 2146326.

     Douglas Hofstadter, 1979. Goedel, Escher, Bach: An Eternal Golden
   Braid. Vintage Books. ISBN 0-465-02685-0. 1999 reprint:
   ISBN 0-465-02656-7. MR530196

      --, 2007. I Am a Strange Loop. Basic Books. ISBN 978-0-465-03078-1.
   ISBN 0-465-03078-5. MR2360307

     Stanley Jaki, OSB, 2005. The drama of the quantities. Real View

     Per Lindstroem, 1997. Aspects of Incompleteness, Lecture Notes in
   Logic v. 10.

     J.R. Lucas, FBA, 1970. The Freedom of the Will. Clarendon Press,
   Oxford, 1970.

     Ernest Nagel, James Roy Newman, Douglas Hofstadter, 2002 (1958).
   Goedel's Proof, revised ed. ISBN 0-8147-5816-9. MR1871678

     Rudy Rucker, 1995 (1982). Infinity and the Mind: The Science and
   Philosophy of the Infinite. Princeton Univ. Press. MR658492

     Smith, Peter (2007). An introduction to Goedel's Theorems. Cambridge,
   U.K.: Cambridge University Press. ISBN 978-0-521-67453-9. MR 2384958.

     N. Shankar, 1994. Metamathematics, Machines and Goedel's Proof,
   Volume 38 of Cambridge tracts in theoretical computer science.
   ISBN 0-521-58533-3

     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 Self-Reference. Oxford Univ. Press.

     --, 2013. The Godelian Puzzle Book: Puzzles, Paradoxes and Proofs.
   Courier Corporation. ISBN 978-0-486-49705-1.

     Hao Wang, 1997. A Logical Journey: From Goedel to Philosophy. MIT
   Press. ISBN 0-262-23189-1 MR1433803

  Miscellaneous references[edit]

     * Francesco Berto, 2009, "The Goedel Paradox and Wittgenstein's
       Reasons" Philosophia Mathematica (III) 17.

   Dawson, John W. Jr. (1996). Logical dilemmas: The life and work of Kurt
   Goedel. Taylor & Francis. ISBN 978-1-56881-025-6.

     Dawson, John W. Jr. (1997). Logical dilemmas: The life and work of
   Kurt Goedel. Wellesley, Massachusetts: A. K. Peters.
   ISBN 978-1-56881-256-4. OCLC 36104240.

     Rebecca Goldstein, 2005, Incompleteness: the Proof and Paradox of
   Kurt Goedel, W. W. Norton & Company. ISBN 0-393-05169-2

     Floyd, Juliet; Putnam, Hilary (2000). "A Note on Wittgenstein's
   "Notorious Paragraph" about the Godel Theorem". The Journal of
   Philosophy. JSTOR. 97 (11): 624-632. doi:10.2307/2678455.
   ISSN 0022-362X. JSTOR 2678455.

     John Harrison, 2009, "Handbook of Practical Logic and Automated
   Reasoning", Cambridge University Press, ISBN 0521899575

     David Hilbert and Paul Bernays, Grundlagen der Mathematik,

     John Hopcroft and Jeffrey Ullman 1979, Introduction to Automata
   Theory, Languages, and Computation, Addison-Wesley, ISBN 0-201-02988-X

     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 0-486-42533-9

     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 machine-assisted proof of Goedel'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 Goedel's Theorem in Max Koelbel,
   ed., Wittgenstein's lasting significance, Psychology Press,
   pp. 207-227.

     --, 2006, In Contradiction: A Study of the Transconsistent, Oxford
   University Press, ISBN 0-19-926329-9

     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.

     Wolfgang Rautenberg, 2010, A Concise Introduction to Mathematical
   Logic, 3rd. ed., Springer, ISBN 978-1-4419-1220-6

     Victor Rodych, 2003, "Misunderstanding Goedel: New Arguments about
   Wittgenstein and New Remarks by Wittgenstein", Dialectica v. 57 n. 3,
   pp. 279-313. doi:10.1111/j.1746-8361.2003.tb00272.x

     Stewart Shapiro, 2002, "Incompleteness and Inconsistency", Mind, v.
   111, pp 817-32. doi:10.1093/mind/111.444.817

     Alan Sokal and Jean Bricmont, 1999, Fashionable Nonsense: Postmodern
   Intellectuals' Abuse of Science, Picador. ISBN 0-312-20407-8

     Joseph R. Shoenfield (1967), Mathematical Logic. Reprinted by A.K.
   Peters for the Association for Symbolic Logic, 2001.
   ISBN 978-1-56881-135-2

     Jeremy Stangroom and Ophelia Benson, Why Truth Matters, Continuum.
   ISBN 0-8264-9528-1

     George Tourlakis, Lectures in Logic and Set Theory, Volume 1,
   Mathematical Logic, Cambridge University Press, 2003.
   ISBN 978-0-521-75373-9

     Avi Wigderson, 2010, "The Goedel Phenomena in Mathematics: A Modern
   View", in Kurt Goedel and the Foundations of Mathematics: Horizons of
   Truth, Cambridge University Press.

     Hao Wang, 1996, A Logical Journey: From Goedel to Philosophy, The MIT
   Press, Cambridge MA, ISBN 0-262-23189-1.

     Zach, Richard (2007). "Hilbert's Program Then and Now". In Jacquette,
   Dale (ed.). Philosophy of logic. Handbook of the Philosophy of Science.
   Vol. 5. Amsterdam: Elsevier. pp. 411-447. arXiv:math/0508572.
   doi:10.1016/b978-044451541-4/50014-2. ISBN 978-0-444-51541-4.
   OCLC 162131413. S2CID 291599.

External links[edit]

     * Godel's Incompleteness Theorems on In Our Time at the BBC
     * "Kurt Goedel" entry by Juliette Kennedy in the Stanford
       Encyclopedia of Philosophy, July 5, 2011.
     * "Goedel's Incompleteness Theorems" entry by Panu Raatikainen in the
       Stanford Encyclopedia of Philosophy, November 11, 2013.
     * Paraconsistent Logic S: Arithmetic and Goedel's Theorem entry in
       the Stanford Encyclopedia of Philosophy.
     * MacTutor biographies:
          + Kurt Goedel. Archived 2005-10-13 at the Wayback Machine
          + Gerhard Gentzen.
     * What is Mathematics:Goedel's Theorem and Around by Karlis Podnieks.
       An online free book.
     * World's shortest explanation of Goedel's theorem using a printing
       machine as an example.
     * October 2011 RadioLab episode about/including Goedel's
       Incompleteness theorem

   "Goedel incompleteness theorem", Encyclopedia of Mathematics, EMS
   Press, 2001 [1994]

     How Goedel's Proof Works by Natalie Wolchover, Quanta Magazine, July
   14, 2020.

     [1] and [2] Goedel's incompleteness theorems formalised in


     * v
     * t
     * e

   Metalogic and metamathematics

     * Cantor's theorem
     * Entscheidungsproblem
     * Church-Turing thesis
     * Consistency
     * Effective method
     * Foundations of mathematics
          + of geometry
     * Goedel's completeness theorem
     * Goedel's incompleteness theorems
     * Soundness
     * Completeness
     * Decidability
     * Interpretation
     * Loewenheim-Skolem theorem
     * Metatheorem
     * Satisfiability
     * Independence
     * Type-token distinction
     * Use-mention distinction

     * v
     * t
     * e

   Mathematical logic


     * Axiom
          + list
     * Cardinality
     * First-order logic
     * Formal proof
     * Formal semantics
     * Foundations of mathematics
     * Information theory
     * Logical consequence
     * Model
     * Set
     * Theorem
     * Theory
     * Type theory

   Theorems (list)
    & Paradoxes

     * Goedel's completeness and incompleteness theorems
     * Tarski's undefinability
     * Banach-Tarski paradox
     * Cantor's theorem, paradox and diagonal argument
     * Compactness
     * Halting problem
     * Lindstroem's
     * Loewenheim-Skolem
     * Russell's paradox


     * Classical logic
     * Logical truth
     * Tautology
     * Proposition
     * Inference
     * Logical equivalence
     * Consistency
          + Equiconsistency
     * Argument
     * Soundness
     * Validity
     * Syllogism
     * Square of opposition
     * Venn diagram

     * Boolean algebra
     * Boolean functions
     * Logical connectives
     * Propositional calculus
     * Propositional formula
     * Truth tables
     * Many-valued logic
          + 3
          + Finite
          + infty

     * First-order
     * Second-order
          + Monadic
     * Higher-order
     * Free
     * Quantifiers
     * Predicate
     * Monadic predicate calculus

   Set theory

     * Set
          + Hereditary
     * Class
     * (Ur-)Element
     * Ordered pair
     * Ordinal number
     * Subset
     * Equality
     * Extensionality
     * Forcing
     * Relation
          + Equivalence
          + Partition
     * Set operations:
          + Intersection
          + Union
          + Complement
          + Cartesian product
          + Power set
          + Identities

   Types of Sets
     * Countable
     * Uncountable
     * Empty
     * Inhabited
     * Singleton
     * Finite
     * Infinite
     * Transitive
     * Ultrafilter
     * Recursive
     * Fuzzy
     * Universal
     * Universe
          + Constructible
          + Grothendieck
          + Von Neumann

   Maps & Cardinality
     * Function/Map
          + Domain
          + Codomain
          + Image
     * In/Sur/Bi-jection
     * Schroeder-Bernstein theorem
     * Isomorphism
     * Goedel numbering
     * Enumeration
     * Large cardinal
          + Inaccessible
     * Aleph number
     * Operation
          + Binary

   Set theories
     * Zermelo-Fraenkel
          + Axiom of choice
          + Continuum hypothesis
     * General
     * Kripke-Platek
     * Morse-Kelley
     * Naive
     * New Foundations
     * Tarski-Grothendieck
     * Von Neumann-Bernays-Goedel
     * Constructive

   Syntax & Language

     * Alphabet
     * Arity
     * Automata
     * Axiom schema
     * Expression
          + Ground
     * Extension
          + by definition
          + Conservative
     * Relation
     * Formal
          + Grammar
          + Language
          + Proof
          + System
          + Theory
     * Formation rule
     * Formula
          + Atomic
          + Closed
          + Ground
          + Open
     * Free/bound variable
     * Metalanguage
     * Logical connective
          + NOT
          + OR
          + AND
          + ->
          + <->
          + =
     * Predicate
          + Functional
          + Variable
          + Propositional variable
     * Quantifier
          + TE
          + !
          + FA
          + rank
     * Sentence
          + Atomic
          + Spectrum
     * Signature
     * String
     * Substitution
     * Symbol
          + Function
          + Logical/Constant
          + Non-logical
          + Variable
     * Term

   Example axiomatic
   systems (list)
     * of arithmetic:
          + Peano
          + second-order
          + elementary function
          + primitive recursive
          + Robinson
          + Skolem
     * of the real numbers
          + Tarski's axiomatization
     * of Boolean algebras
          + canonical
          + minimal axioms
     * of geometry:
          + Euclidean
          + Elements
          + Hilbert's
          + non-Euclidean
          + Tarski's
     * Principia Mathematica

   Proof theory

     * Formal proof
     * Natural deduction
     * Logical consequence
     * Rule of inference
     * Sequent calculus
     * Theorem
     * Systems
          + Formal
          + Axiomatic
          + Deductive
          + Hilbert
               o list
     * Complete theory
     * Independence (from ZFC)
     * Proof of impossibility
     * Ordinal analysis
     * Reverse mathematics
     * Self-verifying theories

   Model theory

     * Interpretation
     * Model
          + Equivalence
          + Finite
          + Saturated
          + Spectrum
          + Substructure
     * Non-standard model
          + of arithmetic
     * Diagram
          + Elementary
     * Categorical theory
     * Model complete theory
     * Satisfiability
     * Semantics of logic
     * Strength
     * Theories of truth
          + Semantic
          + Tarski's
          + Kripke's
     * T-schema
     * Transfer principle
     * Truth predicate
     * Truth value
     * Type
     * Ultraproduct
     * Validity

   Computability theory

     * Church encoding
     * Church-Turing thesis
     * Computably enumerable
     * Computable function
     * Computable set
     * Decision problem
          + Decidable
          + Undecidable
          + P
          + NP
          + P versus NP problem
     * Kolmogorov complexity
     * Lambda calculus
     * Primitive recursive function
     * Recursion
     * Recursive set
     * Turing machine
     * Type theory


     * Abstract logic
     * Category theory
     * Concrete/Abstract Category
     * Category of sets
     * History of logic
     * History of mathematical logic
          + timeline
     * Logicism
     * Mathematical object
     * Philosophy of mathematics
     * Supertask

   icon  Mathematics portal

   Authority control: National libraries Edit this at Wikidata
     * France (data)
     * Germany
     * Israel
     * United States
     * Latvia
     * Czech Republic

   Retrieved from

     * Theorems in the foundations of mathematics
     * Mathematical logic
     * Model theory
     * Proof theory
     * Epistemology
     * Metatheorems
     * Works by Kurt Goedel

   Hidden categories:
     * Articles with short description
     * Short description is different from Wikidata
     * Harv and Sfn no-target errors
     * All articles with incomplete citations
     * Articles with incomplete citations from August 2021
     * Webarchive template wayback links
     * Articles with Stanford Encyclopedia of Philosophy links
     * Articles with BNF identifiers
     * Articles with GND identifiers
     * Articles with J9U identifiers
     * Articles with LCCN identifiers
     * Articles with LNB identifiers
     * Articles with NKC identifiers

Navigation menu

Personal tools

     * Not logged in
     * Talk
     * Contributions
     * Create account
     * Log in


     * Article
     * Talk

   [ ] English


     * Read
     * Edit
     * View history

   [ ] More

   ____________________ Search Go


     * Main page
     * Contents
     * Current events
     * Random article
     * About Wikipedia
     * Contact us
     * Donate


     * Help
     * Learn to edit
     * Community portal
     * Recent changes
     * Upload file


     * What links here
     * Related changes
     * Upload file
     * Special pages
     * Permanent link
     * Page information
     * Cite this page
     * Wikidata item


     * Download as PDF
     * Printable version


     * Alemannisch
     * a+l+e+r+b+y+tm
     * Asturianu
     * B"lgarski
     * Bosanski
     * Catal`a
     * CHvashla
     * Cestina
     * Dansk
     * Deutsch
     * Eesti
     * Ellynika'
     * Espanol
     * Esperanto
     * Euskara
     * f+a+r+s+
     * Franc,ais
     * Gaeilge
     * Galego
     * Hrvatski
     * Ido
     * Bahasa Indonesia
     * Italiano
     * E+B+R+J+T+
     * Latina
     * Magyar
     * Nederlands
     * Norsk bokmaal
     * Norsk nynorsk
     * Novial
     * Polski
     * Portugues
     * Russkij
     * Sicilianu
     * Simple English
     * Slovencina
     * Srpski / srpski
     * Suomi
     * Svenska
     * Tuerkc,e
     * Ukrayins'ka
     * a+r+d+w+
     * Tie>'ng Vie>-.t

   Edit links

     * This page was last edited on 23 December 2022, at 10:31 (UTC).
     * Text is available under the Creative Commons Attribution-ShareAlike
       License 3.0; additional terms may apply. By using this site, you
       agree to the Terms of Use and Privacy Policy. Wikipedia(R) is a
       registered trademark of the Wikimedia Foundation, Inc., a
       non-profit organization.

     * Privacy policy
     * About Wikipedia
     * Disclaimers
     * Contact Wikipedia
     * Mobile view
     * Developers
     * Statistics
     * Cookie statement

     * Wikimedia Foundation
     * Powered by MediaWiki
Saved from web.archive.org, with Lynx.
Main page
© 2022 Matei. No cookies®