Gödel's Incompleteness Theorems
   HOME

TheInfoList



OR:

Gödel's incompleteness theorems are two
theorem In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of t ...
s of
mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
that are concerned with the limits of in formal axiomatic theories. These results, published by
Kurt Gödel Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imme ...
in 1931, are important both in mathematical logic and in the
philosophy of mathematics The philosophy of mathematics is the branch of philosophy that studies the assumptions, foundations, and implications of mathematics. It aims to understand the nature and methods of mathematics, and find out the place of mathematics in people's ...
. The theorems are widely, but not universally, interpreted as showing that
Hilbert's program In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early part of the 20th century, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathema ...
to find a complete and consistent set of
axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
s for all
mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
is impossible. The first incompleteness theorem states that no consistent system of
axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
s whose theorems can be listed by an
effective procedure In logic, mathematics and computer science, especially metalogic and computability theory, an effective methodGeoffrey Hunter (logician), Hunter, Geoffrey, ''Metalogic: An Introduction to the Metatheory of Standard First-Order Logic'', University o ...
(i.e., an
algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
) is capable of proving all truths about the arithmetic of
natural number In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called ''Cardinal n ...
s. 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 A diagonal argument, in mathematics, is a technique employed in the proofs of the following theorems: *Cantor's diagonal argument (the earliest) *Cantor's theorem * Russell's paradox *Diagonal lemma ** Gödel's first incompleteness theorem **Tarski ...
, Gödel's incompleteness theorems were the first of several closely related theorems on the limitations of formal systems. They were followed by
Tarski's undefinability theorem Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1933, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics. Informally, the theorem states that ''arithmetical truth ...
on the formal undefinability of truth,
Church Church may refer to: Religion * Church (building), a building for Christian religious activities * Church (congregation), a local congregation of a Christian denomination * Church service, a formalized period of Christian communal worship * C ...
's proof that Hilbert's ''
Entscheidungsproblem In mathematics and computer science, the ' (, ) is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the state ...
'' is unsolvable, and
Turing Alan Mathison Turing (; 23 June 1912 – 7 June 1954) was an English mathematician, computer scientist, logician, cryptanalyst, philosopher, and theoretical biologist. Turing was highly influential in the development of theoretical co ...
's theorem that there is no algorithm to solve the
halting problem In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a g ...
.


Formal systems: completeness, consistency, and effective axiomatization

The incompleteness theorems apply to
formal system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A form ...
s 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 First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
, 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 In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
, a system in which all variables are intended to denote natural numbers. In other systems, such as
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
, only some sentences of the formal system express statements about the natural numbers. The incompleteness theorems are about formal provability ''within'' these systems, rather than about "provability" in an informal sense. There are several properties that a formal system may have, including completeness, consistency, and the existence of an effective axiomatization. The incompleteness theorems show that systems which contain a sufficient amount of arithmetic cannot possess all three of these properties.


Effective axiomatization

A formal system is said to be ''effectively axiomatized'' (also called ''effectively generated'') if its set of theorems is a
recursively enumerable set In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if: *There is an algorithm such that the ...
. 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 In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as ...
(ZFC). The theory known as
true arithmetic In mathematical logic, true arithmetic is the set of all true first-order statements about the arithmetic of natural numbers. This is the theory associated with the standard model of the Peano axioms in the language of the first-order Peano axio ...
consists of all true statements about the standard integers in the language of Peano arithmetic. This theory is consistent and complete, and contains a sufficient amount of arithmetic. However it does not have a recursively enumerable set of axioms, and thus does not satisfy the hypotheses of the incompleteness theorems.


Completeness

A set of axioms is (''syntactically'', or ''negation''-)
complete Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies t ...
if, for any statement in the axioms' language, that statement or its negation is provable from the axioms . This is the notion relevant for Gödel's first Incompleteness theorem. It is not to be confused with ''semantic'' completeness, which means that the set of axioms proves all the semantic tautologies of the given language. In his
completeness theorem Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies ...
(not to be confused with the incompleteness theorems described here), Gödel proved that first order logic is ''semantically'' complete. But it is not syntactically complete, since there are sentences expressible in the language of first order logic that can be neither proved nor disproved from the axioms of logic alone. 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 Euclidean geometry is a mathematical system attributed to ancient Greek mathematics, Greek mathematician Euclid, which he described in his textbook on geometry: the ''Euclid's Elements, Elements''. Euclid's approach consists in assuming a small ...
without the
parallel postulate In geometry, the parallel postulate, also called Euclid's fifth postulate because it is the fifth postulate in Euclid's ''Elements'', is a distinctive axiom in Euclidean geometry. It states that, in two-dimensional geometry: ''If a line segment ...
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 order In mathematics, a partial order or total order < on a X is said to be dense if, for all x
s is not complete, but becomes complete with an extra axiom stating that there are no endpoints in the order. The
continuum hypothesis In mathematics, the continuum hypothesis (abbreviated CH) is a hypothesis about the possible sizes of infinite sets. It states that or equivalently, that In Zermelo–Fraenkel set theory with the axiom of choice (ZFC), this is equivalent to ...
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 In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
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 A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin ''modulus'', a measure. Models c ...
. In addition, no effectively axiomatized, consistent extension of Peano arithmetic can be complete.


Consistency

A set of axioms is (simply)
consistent In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent i ...
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 In set theory, an uncountable cardinal is inaccessible if it cannot be obtained from smaller cardinals by the usual operations of cardinal arithmetic. More precisely, a cardinal is strongly inaccessible if it is uncountable, it is not a sum of ...
" proves ZFC is consistent because if is the least such cardinal, then sitting inside the
von Neumann universe In set theory and related branches of mathematics, the von Neumann universe, or von Neumann hierarchy of sets, denoted by ''V'', is the class of hereditary well-founded sets. This collection, which is formalized by Zermelo–Fraenkel set theory (Z ...
is a
model A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin ''modulus'', a measure. Models c ...
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 In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
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 A paradox is a logically self-contradictory statement or a statement that runs contrary to one's expectation. It is a statement that, despite apparently valid reasoning from true premises, leads to a seemingly self-contradictory or a logically u ...
that result when the axiom schema of unrestricted comprehension is assumed in set theory.


Systems which contain arithmetic

The incompleteness theorems apply only to formal systems which are able to prove a sufficient collection of facts about the natural numbers. One sufficient collection is the set of theorems of
Robinson arithmetic In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by R. M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is ...
. 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 field In mathematics, a field is algebraically closed if every non-constant polynomial in (the univariate polynomial ring with coefficients in ) has a root in . Examples As an example, the field of real numbers is not algebraically closed, because ...
s 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 field In mathematics, a real closed field is a field ''F'' that has the same first-order properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers. D ...
s, which is essentially equivalent to
Tarski's axioms Tarski's axioms, due to Alfred Tarski, are an axiom set for the substantial fragment of Euclidean geometry that is formulable in first-order logic with identity, and requiring no set theory (i.e., that part of Euclidean geometry that is formulabl ...
for
Euclidean geometry Euclidean geometry is a mathematical system attributed to ancient Greek mathematics, Greek mathematician Euclid, which he described in his textbook on geometry: the ''Euclid's Elements, Elements''. Euclid's approach consists in assuming a small ...
. So Euclidean geometry itself (in Tarski's formulation) is an example of a complete, consistent, effectively axiomatized theory. The system of
Presburger arithmetic Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitti ...
consists of a set of axioms for the natural numbers with just the addition operation (multiplication is omitted). Presburger arithmetic is complete, consistent, and recursively enumerable and can encode addition but not multiplication of natural numbers, showing that for Gödel's theorems one needs the theory to encode not just addition but also multiplication. has studied some weak families of arithmetic systems which allow enough arithmetic as relations to formalise Gödel numbering, but which are not strong enough to have multiplication as a function, and so fail to prove the second incompleteness theorem; that is to say, these systems are consistent and capable of proving their own consistency (see
self-verifying theories Self-verifying theories are consistent first-order systems of arithmetic, much weaker than Peano arithmetic, that are capable of proving their own consistency. Dan Willard was the first to investigate their properties, and he has described a family ...
).


Conflicting goals

In choosing a set of axioms, one goal is to be able to prove as many correct results as possible, without proving any incorrect results. For example, we could imagine a set of true axioms which allow us to prove every true arithmetical claim about the natural numbers . 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 In classical logic, intuitionistic logic and similar logical systems, the principle of explosion (, 'from falsehood, anything ollows; or ), or the principle of Pseudo-Scotus, is the law according to which any statement can be proven from a ...
), and is thus automatically complete. A set of axioms that is both complete and consistent, however, proves a
maximal set In recursion theory, the mathematical theory of computability, a maximal set is a coinfinite recursively enumerable subset ''A'' of the natural numbers such that for every further recursively enumerable subset ''B'' of the natural numbers, either ' ...
of non-
contradictory In traditional logic, a contradiction occurs when a proposition conflicts either with itself or established fact. It is often used as a tool to detect disingenuous beliefs and bias. Illustrating a general tendency in applied logic, Aristotle ...
theorems . 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 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

Gödel's first incompleteness theorem first appeared as "Theorem VI" in Gödel's 1931 paper "
On Formally Undecidable Propositions of Principia Mathematica and Related Systems "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" ("On Formally Undecidable Propositions of Principia Mathematica and Related Systems I") is a paper in mathematical logic by Kurt Gödel. Submitted November ...
I". The hypotheses of the theorem were improved shortly thereafter by using
Rosser's trick In mathematical logic, Rosser's trick is a method for proving Gödel's incompleteness theorems without the assumption that the theory being considered is ω-consistent (Smorynski 1977, p. 840; Mendelson 1977, p. 160). This method ...
. 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 within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of which can neither be proved nor disproved in ." (Raatikainen 2020)
The unprovable statement referred to by the theorem is often referred to as "the Gödel sentence" for the system . The proof constructs a particular Gödel sentence for the system , but there are infinitely many statements in the language of the system that share the same properties, such as the conjunction of the Gödel sentence and any logically valid sentence. Each effectively generated system has its own Gödel sentence. It is possible to define a larger system  that contains the whole of plus as an additional axiom. This will not result in a complete system, because Gödel's theorem will also apply to , and thus also cannot be complete. In this case, is indeed a theorem in , because it is an axiom. Because states only that it is not provable in , no contradiction is presented by its provability within . However, because the incompleteness theorem applies to , there will be a new Gödel statement for , showing that is also incomplete. will differ from in that will refer to , rather than .


Syntactic form of the Gödel sentence

The Gödel sentence is designed to refer, indirectly, to itself. The sentence states that, when a particular sequence of steps is used to construct another sentence, that constructed sentence will not be provable in . However, the sequence of steps is such that the constructed sentence turns out to be itself. In this way, the Gödel sentence indirectly states its own unprovability within . To prove the first incompleteness theorem, Gödel demonstrated that the notion of provability within a system could be expressed purely in terms of arithmetical functions that operate on Gödel numbers of sentences of the system. Therefore, the system, which can prove certain facts about numbers, can also indirectly prove facts about its own statements, provided that it is effectively generated. Questions about the provability of statements within the system are represented as questions about the arithmetical properties of numbers themselves, which would be decidable by the system if it were complete. Thus, although the Gödel sentence refers indirectly to sentences of the system , when read as an arithmetical statement the Gödel 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 In computability theory, a primitive recursive function is roughly speaking a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop can be determined ...
relation . As such, the Gödel sentence can be written in the language of arithmetic with a simple syntactic form. In particular, it can be expressed as 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 \Pi^0_1 of the
arithmetical hierarchy In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
). Via the
MRDP theorem In mathematics, a Diophantine equation is an equation of the form ''P''(''x''1, ..., ''x'j'', ''y''1, ..., ''y'k'') = 0 (usually abbreviated ''P''(', ') = 0) where ''P''(', ') is a polynomial with integer coefficients, where ''x''1, ..., '' ...
, the Gödel 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 .


Truth of the Gödel sentence

The first incompleteness theorem shows that the Gödel sentence of an appropriate formal theory is unprovable in . Because, when interpreted as a statement about arithmetic, this unprovability is exactly what the sentence (indirectly) asserts, the Gödel sentence is, in fact, true (; also see ). For this reason, the sentence is often said to be "true but unprovable." . However, since the Gödel sentence cannot itself formally specify its intended interpretation, the truth of the sentence 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 Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician , reprinted in translation in as a formalization of his finitist conception of the foundations of ...
, which proves the implication , where is a canonical sentence asserting the consistency of (, ). Although the Gödel sentence of a consistent theory is true as a statement about the
intended interpretation An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until ...
of arithmetic, the Gödel sentence will be false in some nonstandard models of arithmetic, as a consequence of Gödel's
completeness theorem Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies ...
. That theorem shows that, when a sentence is independent of a theory, the theory will have models in which the sentence is true and models in which the sentence is false. As described earlier, the Gödel sentence of a system 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 , and the truth of the Gödel sentence follows from the fact that no standard natural number has the property in question. Any model in which the Gödel sentence is false must contain some element which satisfies the property within that model. Such a model must be "nonstandard" – it must contain elements that do not correspond to any standard natural number (, ).


Relationship with the liar paradox

Gödel specifically cites
Richard's paradox In logic, Richard's paradox is a semantical antinomy of set theory and natural language first described by the French mathematician Jules Richard in 1905. The paradox is ordinarily used to motivate the importance of distinguishing carefully betwee ...
and the
liar paradox In philosophy and logic, the classical liar paradox or liar's paradox or antinomy of the liar is the statement of a liar that they are lying: for instance, declaring that "I am lying". If the liar is indeed lying, then the liar is telling the truth ...
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 In philosophy and logic, the classical liar paradox or liar's paradox or antinomy of the liar is the statement of a liar that they are lying: for instance, declaring that "I am lying". If the liar is indeed lying, then the liar is telling the truth ...
is the sentence "This sentence is false." An analysis of the liar sentence shows that it cannot be true (for then, as it asserts, it is false), nor can it be false (for then, it is true). A Gödel sentence for a system makes a similar assertion to the liar sentence, but with truth replaced by provability: says " is not provable in the system ." The analysis of the truth and provability of is a formalized version of the analysis of the truth of the liar sentence. It is not possible to replace "not provable" with "false" in a Gödel sentence because the predicate " is the Gödel number of a false formula" cannot be represented as a formula of arithmetic. This result, known as
Tarski's undefinability theorem Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1933, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics. Informally, the theorem states that ''arithmetical truth ...
, was discovered independently both by Gödel, when he was working on the proof of the incompleteness theorem, and by the theorem's namesake,
Alfred Tarski Alfred Tarski (, born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician a ...
.


Extensions of Gödel's original result

Compared to the theorems stated in Gödel's 1931 paper, many contemporary statements of the incompleteness theorems are more general in two ways. These generalized statements are phrased to apply to a broader class of systems, and they are phrased to incorporate weaker consistency assumptions. Gödel demonstrated the incompleteness of the system of ''
Principia Mathematica The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the foundations of mathematics written by mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. ...
'', a particular system of arithmetic, but a parallel demonstration could be given for any effective system of a certain expressiveness. Gödel commented on this fact in the introduction to his paper, but restricted the proof to one system for concreteness. In modern statements of the theorem, it is common to state the effectiveness and expressiveness conditions as hypotheses for the incompleteness theorem, so that it is not limited to any particular formal system. The terminology used to state these conditions was not yet developed in 1931 when Gödel published his results. Gödel's original statement and proof of the incompleteness theorem requires the assumption that the system is not just consistent but '' ω-consistent''. A system is ω-consistent if it is not ω-inconsistent, and is ω-inconsistent if there is a predicate such that for every specific natural number the system proves , and yet the system also proves that there exists a natural number such that (). That is, the system says that a number with property exists while denying that it has any specific value. The ω-consistency of a system implies its consistency, but consistency does not imply ω-consistency. strengthened the incompleteness theorem by finding a variation of the proof (
Rosser's trick In mathematical logic, Rosser's trick is a method for proving Gödel's incompleteness theorems without the assumption that the theory being considered is ω-consistent (Smorynski 1977, p. 840; Mendelson 1977, p. 160). This method ...
) that only requires the system to be consistent, rather than ω-consistent. This is mostly of technical interest, because all true formal theories of arithmetic (theories whose axioms are all true statements about natural numbers) are ω-consistent, and thus Gödel's theorem as originally stated applies to them. The stronger version of the incompleteness theorem that only assumes consistency, rather than ω-consistency, is now commonly known as Gödel's incompleteness theorem and as the Gödel–Rosser theorem.


Second incompleteness theorem

For each formal system containing basic arithmetic, it is possible to canonically define a formula Cons() expressing the consistency of . This formula expresses the property that "there does not exist a natural number coding a formal derivation within the system whose conclusion is a syntactic contradiction." The syntactic contradiction is often taken to be "0=1", in which case Cons() states "there is no natural number that codes a derivation of '0=1' from the axioms of ." Gödel's second incompleteness theorem shows that, under general assumptions, this canonical consistency statement Cons() will not be provable in . The theorem first appeared as "Theorem XI" in Gödel's 1931 paper " On Formally Undecidable Propositions in Principia Mathematica and Related Systems I". In the following statement, the term "formalized system" also includes an assumption that 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." can also be written as "Assume is a consistent formalized system which contains elementary arithmetic. Then F \not \vdash \text(F)." (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 itself.


Expressing consistency

There is a technical subtlety in the second incompleteness theorem regarding the method of expressing the consistency of as a formula in the language of . There are many ways to express the consistency of a system, and not all of them lead to the same result. The formula Cons() from the second incompleteness theorem is a particular expression of consistency. Other formalizations of the claim that is consistent may be inequivalent in , and some may even be provable. For example, first-order Peano arithmetic (PA) can prove that "the largest consistent
subset In mathematics, Set (mathematics), set ''A'' is a subset of a set ''B'' if all Element (mathematics), elements of ''A'' are also elements of ''B''; ''B'' is then a superset of ''A''. It is possible for ''A'' and ''B'' to be equal; if they are ...
of PA" is consistent. But, because PA is consistent, the largest consistent subset of PA is just PA, so in this sense PA "proves that it is consistent". What PA does not prove is that the largest consistent subset of PA is, in fact, the whole of PA. (The term "largest consistent subset of PA" is meant here to be the largest consistent initial segment of the axioms of PA under some particular effective enumeration.)


The Hilbert–Bernays conditions

The standard proof of the second incompleteness theorem assumes that the provability predicate satisfies the
Hilbert–Bernays provability conditions In mathematical logic, the Hilbert–Bernays provability conditions, named after David Hilbert and Paul Bernays, are a set of requirements for formalized provability predicates in formal theories of arithmetic (Smith 2007:224). These conditions are ...
. Letting represent the Gödel number of a formula , the provability conditions say: # If proves , then proves . # proves 1.; that is, proves . # proves   (analogue of
modus ponens In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. ...
). There are systems, such as Robinson arithmetic, which are strong enough to meet the assumptions of the first incompleteness theorem, but which do not prove the Hilbert–Bernays conditions. Peano arithmetic, however, is strong enough to verify these conditions, as are all theories stronger than Peano arithmetic.


Implications for consistency proofs

Gödel's second incompleteness theorem also implies that a system satisfying the technical conditions outlined above cannot prove the consistency of any system that proves the consistency of . This is because such a system can prove that if proves the consistency of , then is in fact consistent. For the claim that is consistent has form "for all numbers , has the decidable property of not being a code for a proof of contradiction in ". If were in fact inconsistent, then would prove for some that is the code of a contradiction in . But if also proved that is consistent (that is, that there is no such ), then it would itself be inconsistent. This reasoning can be formalized in to show that if is consistent, then is consistent. Since, by second incompleteness theorem, does not prove its consistency, it cannot prove the consistency of 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 Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician , reprinted in translation in as a formalization of his finitist conception of the foundations of ...
(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 In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early part of the 20th century, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathema ...
, which aimed to justify the use of "ideal" (infinitistic) mathematical principles in the proofs of "real" (finitistic) mathematical statements by giving a finitistic proof that the ideal principles are consistent, cannot be carried out . The corollary also indicates the epistemological relevance of the second incompleteness theorem. It would actually provide no interesting information if a system proved its consistency. This is because inconsistent theories prove everything, including their consistency. Thus a consistency proof of in would give us no clue as to whether really is consistent; no doubts about the consistency of would be resolved by such a consistency proof. The interest in consistency proofs lies in the possibility of proving the consistency of a system in some system that is in some sense less doubtful than itself, for example weaker than . For many naturally occurring theories and , such as = Zermelo–Fraenkel set theory and = primitive recursive arithmetic, the consistency of is provable in , and thus cannot prove the consistency of 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 , only doing so in a theory that itself can prove to be consistent. For example,
Gerhard Gentzen Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died ...
proved the consistency of Peano arithmetic in a different system that includes an axiom asserting that the ordinal called is
wellfounded In mathematics, a binary relation ''R'' is called well-founded (or wellfounded) on a class ''X'' if every non-empty subset ''S'' ⊆ ''X'' has a minimal element with respect to ''R'', that is, an element ''m'' not related by ''s& ...
; see
Gentzen's consistency proof Gentzen's consistency proof is a result of proof theory in mathematical logic, published by Gerhard Gentzen in 1936. It shows that the Peano axioms of first-order arithmetic do not contain a contradiction (i.e. are "consistent"), as long as a cer ...
. Gentzen's theorem spurred the development of
ordinal analysis In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory h ...
in proof theory.


Examples of undecidable statements

There are two distinct senses of the word "undecidable" in mathematics and computer science. The first of these is the
proof-theoretic Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding parts, ...
sense used in relation to Gödel's theorems, that of a statement being neither provable nor refutable in a specified
deductive system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A for ...
. The second sense, which will not be discussed here, is used in relation to
computability theory Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since e ...
and applies not to statements but to
decision problem In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm wheth ...
s, which are countably infinite sets of questions each requiring a yes or no answer. Such a problem is said to be undecidable if there is no
computable function Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do ...
that correctly answers every question in the problem set (see
undecidable problem In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer. The halting problem is an ...
). Because of the two meanings of the word undecidable, the term
independent Independent or Independents may refer to: Arts, entertainment, and media Artist groups * Independents (artist group), a group of modernist painters based in the New Hope, Pennsylvania, area of the United States during the early 1930s * Independ ...
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 In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values (''true'' or '' false''). Computing In some progr ...
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 philosophy of mathematics is the branch of philosophy that studies the assumptions, foundations, and implications of mathematics. It aims to understand the nature and methods of mathematics, and find out the place of mathematics in people's ...
. The combined work of Gödel and
Paul Cohen Paul Joseph Cohen (April 2, 1934 – March 23, 2007) was an American mathematician. He is best known for his proofs that the continuum hypothesis and the axiom of choice are independent from Zermelo–Fraenkel set theory, for which he was award ...
has given two concrete examples of undecidable statements (in the first sense of the term): The
continuum hypothesis In mathematics, the continuum hypothesis (abbreviated CH) is a hypothesis about the possible sizes of infinite sets. It states that or equivalently, that In Zermelo–Fraenkel set theory with the axiom of choice (ZFC), this is equivalent to ...
can neither be proved nor refuted in ZFC (the standard axiomatization of
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
), and the
axiom of choice In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...
can neither be proved nor refuted in ZF (which is all the ZFC axioms ''except'' the axiom of choice). These results do not require the incompleteness theorem. Gödel proved in 1940 that neither of these statements could be disproved in ZF or ZFC set theory. In the 1960s, Cohen proved that neither is provable from ZF, and the continuum hypothesis cannot be proved from ZFC. In 1973,
Saharon Shelah Saharon Shelah ( he, שהרן שלח; born July 3, 1945) is an Israeli mathematician. He is a professor of mathematics at the Hebrew University of Jerusalem and Rutgers University in New Jersey. Biography Shelah was born in Jerusalem on July 3, ...
showed that the
Whitehead problem In group theory, a branch of abstract algebra, the Whitehead problem is the following question: Saharon Shelah proved that Whitehead's problem is independent of ZFC, the standard axioms of set theory. Refinement Assume that ''A'' is an abel ...
in
group theory In abstract algebra, group theory studies the algebraic structures known as group (mathematics), groups. The concept of a group is central to abstract algebra: other well-known algebraic structures, such as ring (mathematics), rings, field ...
is undecidable, in the first sense of the term, in standard set theory.
Gregory Chaitin Gregory John Chaitin ( ; born 25 June 1947) is an Argentine-American mathematician and computer scientist. Beginning in the late 1960s, Chaitin made contributions to algorithmic information theory and metamathematics, in particular a computer-t ...
produced undecidable statements in
algorithmic information theory Algorithmic information theory (AIT) is a branch of theoretical computer science that concerns itself with the relationship between computation and information of computably generated objects (as opposed to stochastically generated), such as str ...
and proved another incompleteness theorem in that setting.
Chaitin's incompleteness theorem In algorithmic information theory (a subfield of computer science and mathematics), the Kolmogorov complexity of an object, such as a piece of text, is the length of a shortest computer program (in a predetermined programming language) that produ ...
states that for any system that can represent enough arithmetic, there is an upper bound such that no specific number can be proved in that system to have
Kolmogorov complexity In algorithmic information theory (a subfield of computer science and mathematics), the Kolmogorov complexity of an object, such as a piece of text, is the length of a shortest computer program (in a predetermined programming language) that produ ...
greater than . While Gödel's theorem is related to the
liar paradox In philosophy and logic, the classical liar paradox or liar's paradox or antinomy of the liar is the statement of a liar that they are lying: for instance, declaring that "I am lying". If the liar is indeed lying, then the liar is telling the truth ...
, Chaitin's result is related to
Berry's paradox The Berry paradox is a self-referential paradox arising from an expression like "The smallest positive integer not definable in under sixty letters" (a phrase with fifty-seven letters). Bertrand Russell, the first to discuss the paradox in print, ...
.


Undecidable statements provable in larger systems

These are natural mathematical equivalents of the Gödel "true but undecidable" sentence. They can be proved in a larger system which is generally accepted as a valid form of reasoning, but are undecidable in a more limited system such as Peano Arithmetic. In 1977,
Paris Paris () is the capital and most populous city of France, with an estimated population of 2,165,423 residents in 2019 in an area of more than 105 km² (41 sq mi), making it the 30th most densely populated city in the world in 2020. S ...
and Harrington proved that the Paris–Harrington principle, a version of the infinite Ramsey theorem, is undecidable in (first-order)
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
, but can be proved in the stronger system of
second-order arithmetic In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. A precurs ...
. Kirby and Paris later showed that
Goodstein's theorem In mathematical logic, Goodstein's theorem is a statement about the natural numbers, proved by Reuben Goodstein in 1944, which states that every ''Goodstein sequence'' eventually terminates at 0. Kirby and Paris showed that it is unprovable in Pe ...
, a statement about sequences of natural numbers somewhat simpler than the Paris–Harrington principle, is also undecidable in Peano arithmetic.
Kruskal's tree theorem In mathematics, Kruskal's tree theorem states that the set of finite trees over a well-quasi-ordered set of labels is itself well-quasi-ordered under homeomorphic embedding. History The theorem was conjectured by Andrew Vázsonyi and proved b ...
, 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 In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
. The related but more general
graph minor theorem Graph may refer to: Mathematics *Graph (discrete mathematics), a structure made of vertices and edges **Graph theory, the study of such graphs and their properties * Graph (topology), a topological space resembling a graph in the sense of discr ...
(2003) has consequences for
computational complexity theory In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each other. A computational problem is a task solved by ...
.


Relationship with computability

The incompleteness theorem is closely related to several results about undecidable sets in
recursion theory Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since e ...
. presented a proof of Gödel's incompleteness theorem using basic results of computability theory. One such result shows that the
halting problem In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a g ...
is undecidable: there is no computer program that can correctly determine, given any program as input, whether 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 ; ; and . explains how Matiyasevich's solution to Hilbert's 10th problem can be used to obtain a proof to Gödel's first incompleteness theorem. Matiyasevich proved that there is no algorithm that, given a multivariate polynomial with integer coefficients, determines whether there is an integer solution to the equation = 0. Because polynomials with integer coefficients, and integers themselves, are directly expressible in the language of arithmetic, if a multivariate integer polynomial equation = 0 does have a solution in the integers then any sufficiently strong system of arithmetic will prove this. Moreover, if the system is ω-consistent, then it will never prove that a particular polynomial equation has a solution when in fact there is no solution in the integers. Thus, if were complete and ω-consistent, it would be possible to determine algorithmically whether a polynomial equation has a solution by merely enumerating proofs of until either " has a solution" or " has no solution" is found, in contradiction to Matiyasevich's theorem. Hence it follows that cannot be -consistent and complete. Moreover, for each consistent effectively generated system , it is possible to effectively generate a multivariate polynomial over the integers such that the equation = 0 has no solutions over the integers, but the lack of solutions cannot be proved in (; ). shows how the existence of
recursively inseparable sets In computability theory, two disjoint sets of natural numbers are called computably inseparable or recursively inseparable if they cannot be "separated" with a computable set.Monk 1976, p. 100 These sets arise in the study of computability the ...
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 ).
Chaitin's incompleteness theorem In algorithmic information theory (a subfield of computer science and mathematics), the Kolmogorov complexity of an object, such as a piece of text, is the length of a shortest computer program (in a predetermined programming language) that produ ...
gives a different method of producing independent sentences, based on
Kolmogorov complexity In algorithmic information theory (a subfield of computer science and mathematics), the Kolmogorov complexity of an object, such as a piece of text, is the length of a shortest computer program (in a predetermined programming language) that produ ...
. Like the proof presented by Kleene that was mentioned above, Chaitin's theorem only applies to theories with the additional property that all their axioms are true in the standard model of the natural numbers. Gödel's incompleteness theorem is distinguished by its applicability to consistent theories that nonetheless include statements that are false in the standard model; these theories are known as ω-inconsistent.


Proof sketch for the first theorem

The
proof by contradiction In logic and mathematics, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition, by showing that assuming the proposition to be false leads to a contradiction. Proof by contradiction is also known as ...
has three essential parts. To begin, choose a formal system that meets the proposed criteria: # Statements in the system can be represented by natural numbers (known as Gödel numbers). The significance of this is that properties of statements—such as their truth and falsehood—will be equivalent to determining whether their Gödel numbers have certain properties, and that properties of the statements can therefore be demonstrated by examining their Gödel numbers. This part culminates in the construction of a formula expressing the idea that ''"statement is provable in the system"'' (which can be applied to any statement "" in the system). # In the formal system it is possible to construct a number whose matching statement, when interpreted, is
self-referential Self-reference occurs in natural or formal languages when a sentence, idea or formula refers to itself. The reference may be expressed either directly—through some intermediate sentence or formula—or by means of some encoding. In philoso ...
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 In set theory, Cantor's diagonal argument, also called the diagonalisation argument, the diagonal slash argument, the anti-diagonal argument, the diagonal method, and Cantor's diagonalization proof, was published in 1891 by Georg Cantor as a m ...
). # Within the formal system this statement permits a demonstration that it is neither provable nor disprovable in the system, and therefore the system cannot in fact be ω-consistent. Hence the original assumption that the proposed system met the criteria is false.


Arithmetization of syntax

The main problem in fleshing out the proof described above is that it seems at first that to construct a statement that is equivalent to " cannot be proved", would somehow have to contain a reference to , which could easily give rise to an infinite regress. Gödel's technique is to show that statements can be matched with numbers (often called the arithmetization of
syntax In linguistics, syntax () is the study of how words and morphemes combine to form larger units such as phrases and sentences. Central concerns of syntax include word order, grammatical relations, hierarchical sentence structure ( constituency) ...
) in such a way that ''"proving a statement"'' can be replaced with ''"testing whether a number has a given property"''. This allows a self-referential formula to be constructed in a way that avoids any infinite regress of definitions. The same technique was later used by
Alan Turing Alan Mathison Turing (; 23 June 1912 – 7 June 1954) was an English mathematician, computer scientist, logician, cryptanalyst, philosopher, and theoretical biologist. Turing was highly influential in the development of theoretical com ...
in his work on the ''
Entscheidungsproblem In mathematics and computer science, the ' (, ) is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the state ...
''. In simple terms, a method can be devised so that every formula or statement that can be formulated in the system gets a unique number, called its Gödel number, in such a way that it is possible to mechanically convert back and forth between formulas and Gödel numbers. The numbers involved might be very long indeed (in terms of number of digits), but this is not a barrier; all that matters is that such numbers can be constructed. A simple example is 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 ASCII ( ), abbreviated from American Standard Code for Information Interchange, is a character encoding standard for electronic communication. ASCII codes represent text in computers, telecommunications equipment, and other devices. Because of ...
, 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 ASCII ( ), abbreviated from American Standard Code for Information Interchange, is a character encoding standard for electronic communication. ASCII codes represent text in computers, telecommunications equipment, and other devices. Because of ...
, 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"

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 that contains exactly one free variable is called a ''statement form'' or ''class-sign''. As soon as 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 , 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 "23 = 6". Statement forms themselves are not statements and therefore cannot be proved or disproved. But every statement form can be assigned a Gödel number denoted by . The choice of the free variable used in the form () is not relevant to the assignment of the Gödel number . The notion of provability itself can also be encoded by Gödel numbers, in the following way: since a proof is a list of statements which obey certain rules, the Gödel number of a proof can be defined. Now, for every statement , one may ask whether a number is the Gödel number of its proof. The relation between the Gödel number of and , the potential Gödel number of its proof, is an arithmetical relation between two numbers. Therefore, there is a statement form that uses this arithmetical relation to state that a Gödel number of a proof of exists: : ( is the Gödel number of a formula and is the Gödel number of a proof of the formula encoded by ). The name Bew is short for ''beweisbar'', the German word for "provable"; this name was originally used by Gödel to denote the provability formula just described. Note that "" is merely an abbreviation that represents a particular, very long, formula in the original language of ; the string "" itself is not claimed to be part of this language. An important feature of the formula is that if a statement is provable in the system then is also provable. This is because any proof of would have a corresponding Gödel number, the existence of which causes to be satisfied.


Diagonalization

The next step in the proof is to obtain a statement which, indirectly, asserts its own unprovability. Although Gödel constructed this statement directly, the existence of at least one such statement follows from the
diagonal lemma In mathematical logic, the diagonal lemma (also known as diagonalization lemma, self-reference lemma or fixed point theorem) establishes the existence of self-referential sentences in certain formal theories of the natural numbers—specificall ...
, which says that for any sufficiently strong formal system and any statement form there is a statement such that the system proves :. By letting be the negation of , we obtain the theorem : and the defined by this roughly states that its own Gödel number is the Gödel number of an unprovable formula. The statement is not literally equal to ; rather, states that if a certain calculation is performed, the resulting Gödel number will be that of an unprovable statement. But when this calculation is performed, the resulting Gödel number turns out to be the Gödel number of itself. This is similar to the following sentence in English: :", when preceded by itself in quotes, is unprovable.", when preceded by itself in quotes, is unprovable. This sentence does not directly refer to itself, but when the stated transformation is made the original sentence is obtained as a result, and thus this sentence indirectly asserts its own unprovability. The proof of the diagonal lemma employs a similar method. Now, assume that the axiomatic system is ω-consistent, and let be the statement obtained in the previous section. If were provable, then would be provable, as argued above. But asserts the negation of . Thus the system would be inconsistent, proving both a statement and its negation. This contradiction shows that cannot be provable. If the negation of were provable, then would be provable (because was constructed to be equivalent to the negation of ). However, for each specific number , cannot be the Gödel number of the proof of , because is not provable (from the previous paragraph). Thus on one hand the system proves there is a number with a certain property (that it is the Gödel number of the proof of ), but on the other hand, for every specific number , we can prove that it does not have this property. This is impossible in an ω-consistent system. Thus the negation of is not provable. Thus the statement is undecidable in our axiomatic system: it can neither be proved nor disproved within the system. In fact, to show that is not provable only requires the assumption that the system is consistent. The stronger assumption of ω-consistency is required to show that the negation of is not provable. Thus, if is constructed for a particular system: *If the system is ω-consistent, it can prove neither nor its negation, and so is undecidable. *If the system is consistent, it may have the same situation, or it may prove the negation of . In the later case, we have a statement ("not ") which is false but provable, and the system is not ω-consistent. If one tries to "add the missing axioms" to avoid the incompleteness of the system, then one has to add either or "not " as axioms. But then the definition of "being a Gödel number of a proof" of a statement changes. which means that the formula is now different. Thus when we apply the diagonal lemma to this new Bew, we obtain a new statement , different from the previous one, which will be undecidable in the new system if it is ω-consistent.


Proof via Berry's paradox

sketches an alternative proof of the first incompleteness theorem that uses
Berry's paradox The Berry paradox is a self-referential paradox arising from an expression like "The smallest positive integer not definable in under sixty letters" (a phrase with fifty-seven letters). Bertrand Russell, the first to discuss the paradox in print, ...
rather than the
liar paradox In philosophy and logic, the classical liar paradox or liar's paradox or antinomy of the liar is the statement of a liar that they are lying: for instance, declaring that "I am lying". If the liar is indeed lying, then the liar is telling the truth ...
to construct a true but unprovable formula. A similar proof method was independently discovered by
Saul Kripke Saul Aaron Kripke (; November 13, 1940 – September 15, 2022) was an American philosopher and logician in the analytic tradition. He was a Distinguished Professor of Philosophy at the Graduate Center of the City University of New York and em ...
. Boolos's proof proceeds by constructing, for any
computably enumerable In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if: *There is an algorithm such that the ...
set of true sentences of arithmetic, another sentence which is true but not contained in . 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 .


Computer verified proofs

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 In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
software. Gödel's original proofs of the incompleteness theorems, like most mathematical proofs, were written in
natural language In neuropsychology, linguistics, and philosophy of language, a natural language or ordinary language is any language that has evolved naturally in humans through use and repetition without conscious planning or premeditation. Natural languages ...
intended for human readers. Computer-verified proofs of versions of the first incompleteness theorem were announced by
Natarajan Shankar Natarajan Shankar is a computer scientist working at SRI International in Menlo Park, California, where he leads the Symbolic Analysis Laboratory. Education Shankar received his Ph.D. degree in computer science, under advisors Robert S. Boyer an ...
in 1986 using
Nqthm Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2. History The system was developed by Robert S. Boyer and J Strother Moore, professors of computer science at the University of Texas ...
, by Russell O'Connor in 2003 using
Coq Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...
and by John Harrison in 2009 using
HOL Light HOL Light is a member of the HOL theorem prover family. Like the other members, it is a proof assistant for classical higher order logic. Compared with other HOL systems, HOL Light is intended to have relatively simple foundations. HOL Light is aut ...
. A computer-verified proof of both incompleteness theorems was announced by
Lawrence Paulson Lawrence Charles Paulson (born 1955) is an American computer scientist. He is a Professor of Computational Logic at the University of Cambridge Computer Laboratory and a Fellow of Clare College, Cambridge. Education Paulson graduated from the ...
in 2013 using Isabelle .


Proof sketch for the second theorem

The main difficulty in proving the second incompleteness theorem is to show that various facts about provability used in the proof of the first incompleteness theorem can be formalized within a system using a formal predicate for provability. Once this is done, the second incompleteness theorem follows by formalizing the entire proof of the first incompleteness theorem within the system itself. Let stand for the undecidable sentence constructed above, and assume for purposes of obtaining a contradiction that the consistency of the system can be proved from within the system itself. This is equivalent to proving the statement "System is consistent". Now consider the statement , where = "If the system is consistent, then is not provable". The proof of sentence can be formalized within the system , and therefore the statement , " is not provable", (or identically, "not ") can be proved in the system . Observe then, that if we can prove that the system is consistent (ie. the statement in the hypothesis of ), then we have proved that is not provable. But this is a contradiction since by the 1st Incompleteness Theorem, this sentence (ie. what is implied in the sentence , """ is not provable") is what we construct to be unprovable. Notice that this is why we require formalizing the first Incompleteness Theorem in : 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 . So we cannot prove that the system is consistent. And the 2nd Incompleteness Theorem statement follows.


Discussion and implications

The incompleteness results affect the
philosophy of mathematics The philosophy of mathematics is the branch of philosophy that studies the assumptions, foundations, and implications of mathematics. It aims to understand the nature and methods of mathematics, and find out the place of mathematics in people's ...
, particularly versions of
formalism Formalism may refer to: * Form (disambiguation) * Formal (disambiguation) * Legal formalism, legal positivist view that the substantive justice of a law is a question for the legislature rather than the judiciary * Formalism (linguistics) * Scie ...
, which use a single system of formal logic to define their principles.


Consequences for logicism and Hilbert's second problem

The incompleteness theorem is sometimes thought to have severe consequences for the program of
logicism In the philosophy of mathematics, logicism is a programme comprising one or more of the theses that — for some coherent meaning of 'logic' — mathematics is an extension of logic, some or all of mathematics is reducible to logic, or some or all ...
proposed by
Gottlob Frege Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic phil ...
and
Bertrand Russell Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British mathematician, philosopher, logician, and public intellectual. He had a considerable influence on mathematics, logic, set theory, linguistics, ...
, which aimed to define the natural numbers in terms of logic . Bob Hale and
Crispin Wright Crispin James Garth Wright (; born 21 December 1942) is a British philosopher, who has written on neo-Fregean (neo-logicist) philosophy of mathematics, Wittgenstein's later philosophy, and on issues related to truth, realism, cognitivism, skep ...
argue that it is not a problem for logicism because the incompleteness theorems apply equally to first order logic as they do to arithmetic. They argue that only those who believe that the natural numbers are to be defined in terms of first order logic have this problem. Many logicians believe that Gödel's incompleteness theorems struck a fatal blow to
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many a ...
'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

Authors including the philosopher J. R. Lucas and physicist
Roger Penrose Sir Roger Penrose (born 8 August 1931) is an English mathematician, mathematical physicist, philosopher of science and Nobel Laureate in Physics. He is Emeritus Rouse Ball Professor of Mathematics in the University of Oxford, an emeritus fello ...
have debated what, if anything, Gödel's incompleteness theorems imply about human intelligence. Much of the debate centers on whether the human mind is equivalent to a
Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
, or by the
Church–Turing thesis In computability theory, the Church–Turing thesis (also known as computability thesis, the Turing–Church thesis, the Church–Turing conjecture, Church's thesis, Church's conjecture, and Turing's thesis) is a thesis about the nature of comp ...
, any finite machine at all. If it is, and if the machine is consistent, then Gödel's incompleteness theorems would apply to it. suggested that while Gödel's theorems cannot be applied to humans, since they make mistakes and are therefore inconsistent, it may be applied to the human faculty of science or mathematics in general. Assuming that it is consistent, either its consistency cannot be proved or it cannot be represented by a Turing machine. has proposed that the concept of mathematical "knowability" should be based on
computational complexity In computer science, the computational complexity or simply complexity of an algorithm is the amount of resources required to run it. Particular focus is given to computation time (generally measured by the number of needed elementary operations) ...
rather than logical decidability. He writes that "when ''knowability'' is interpreted by modern standards, namely via computational complexity, the Gödel phenomena are very much with us." Douglas Hofstadter, in his books ''
Gödel, Escher, Bach ''Gödel, Escher, Bach: an Eternal Golden Braid'', also known as ''GEB'', is a 1979 book by Douglas Hofstadter. By exploring common themes in the lives and works of logician Kurt Gödel, artist M. C. Escher, and composer Johann Sebastian Bach, t ...
'' and ''
I Am a Strange Loop ''I Am a Strange Loop'' is a 2007 book by Douglas Hofstadter, examining in depth the concept of a '' strange loop'' to explain the sense of "I". The concept of a ''strange loop'' was originally developed in his 1979 book '' Gödel, Escher, Bach' ...
'', cites Gödel'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 Gödel's theorem comes from the Gödel 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 Gödel'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.'') 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.'')


Paraconsistent logic

Although Gödel's theorems are usually studied in the context of classical logic, they also have a role in the study of
paraconsistent logic A paraconsistent logic is an attempt at a logical system to deal with contradictions in a discriminating way. Alternatively, paraconsistent logic is the subfield of logic that is concerned with studying and developing "inconsistency-tolerant" syste ...
and of inherently contradictory statements (''
dialetheia Dialetheism (from Greek 'twice' and 'truth') is the view that there are statements that are both true and false. More precisely, it is the belief that there can be a true statement whose negation is also true. Such statements are called "true ...
''). argues that replacing the notion of formal proof in Gödel's theorem with the usual notion of informal proof can be used to show that naive mathematics is inconsistent, and uses this as evidence for
dialetheism Dialetheism (from Greek 'twice' and 'truth') is the view that there are statements that are both true and false. More precisely, it is the belief that there can be a true statement whose negation is also true. Such statements are called "true ...
. The cause of this inconsistency is the inclusion of a truth predicate for a system within the language of the system . gives a more mixed appraisal of the applications of Gödel's theorems to dialetheism.


Appeals to the incompleteness theorems in other fields

Appeals and analogies are sometimes made to the incompleteness theorems in support of arguments that go beyond mathematics and logic. Several authors have commented negatively on such extensions and interpretations, including
Torkel Franzén Torkel Franzén (1 April 1950, Norrbotten County – 19 April 2006, Stockholm) was a Swedish academic. Biography Franzén worked at the Department of Computer Science and Electrical Engineering at Luleå University of Technology, Sweden, in the f ...
(2005); Panu ; ; and . , for example, quote from
Rebecca Goldstein Rebecca Newberger Goldstein (born February 23, 1950) is an American philosopher, novelist, and public intellectual. She has written ten books, both fiction and non-fiction. She holds a Ph.D. in philosophy of science from Princeton University, and ...
's comments on the disparity between Gödel's avowed
Platonism Platonism is the philosophy of Plato and philosophical systems closely derived from it, though contemporary platonists do not necessarily accept all of the doctrines of Plato. Platonism had a profound effect on Western thought. Platonism at le ...
and the
anti-realist In analytic philosophy, anti-realism is a position which encompasses many varieties such as metaphysical, mathematical, semantic, scientific, moral and epistemic. The term was first articulated by British philosopher Michael Dummett in an argument ...
uses to which his ideas are sometimes put. criticize
Régis Debray Jules Régis Debray (; born 2 September 1940) is a French philosopher, journalist, former government official and academic. He is known for his theorization of mediology, a critical theory of the long-term transmission of cultural meaning in h ...
's invocation of the theorem in the context of sociology; Debray has defended this use as metaphorical (ibid.).


History

After Gödel published his proof of the
completeness theorem Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies ...
as his doctoral thesis in 1929, he turned to a second problem for his
habilitation Habilitation is the highest university degree, or the procedure by which it is achieved, in many European countries. The candidate fulfills a university's set criteria of excellence in research, teaching and further education, usually including a ...
. His original goal was to obtain a positive solution to
Hilbert's second problem In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his Hilbert's problems, 23 problems. It asks for a proof that the arithmetic is consistency proof, consistent – free of any internal contradictions. Hilber ...
. At the time, theories of the natural numbers and real numbers similar to
second-order arithmetic In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. A precurs ...
were known as "analysis", while theories of the natural numbers alone were known as "arithmetic". Gödel was not the only person working on the consistency problem. Ackermann had published a flawed consistency proof for analysis in 1925, in which he attempted to use the method of ε-substitution originally developed by Hilbert. Later that year,
von Neumann Von Neumann may refer to: * John von Neumann (1903–1957), a Hungarian American mathematician * Von Neumann family * Von Neumann (surname), a German surname * Von Neumann (crater), a lunar impact crater See also * Von Neumann algebra * Von Ne ...
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 (; ). In the course of his research, Gödel discovered that although a sentence which asserts its own falsehood leads to paradox, a sentence that asserts its own non-provability does not. In particular, Gödel was aware of the result now called
Tarski's indefinability theorem Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1933, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics. Informally, the theorem states that ''arithmetical truth ...
, although he never published it. Gödel announced his first incompleteness theorem to Carnap, Feigel and Waismann on August 26, 1930; all four would attend the
Second Conference on the Epistemology of the Exact Sciences The Second Conference on the Epistemology of the Exact Sciences (german: 2. Tagung für Erkenntnislehre der exakten Wissenschaften in Königsberg) was held on 5–7 September 1930 in Königsberg, then located in East Prussia. It was at this conferen ...
, a key conference in
Königsberg Königsberg (, ) was the historic Prussian city that is now Kaliningrad, Russia. Königsberg was founded in 1255 on the site of the ancient Old Prussian settlement ''Twangste'' by the Teutonic Knights during the Northern Crusades, and was named ...
the following week.


Announcement

The 1930 Königsberg conference was a joint meeting of three academic societies, with many of the key logicians of the time in attendance. Carnap, Heyting, and von Neumann delivered one-hour addresses on the mathematical philosophies of logicism, intuitionism, and formalism, respectively . The conference also included Hilbert's retirement address, as he was leaving his position at the University of Göttingen. Hilbert used the speech to argue his belief that all mathematical problems can be solved. He ended his address by saying, This speech quickly became known as a summary of Hilbert's beliefs on mathematics (its final six words, "''Wir müssen wissen. Wir werden wissen!''", were used as Hilbert's epitaph in 1943). Although Gödel was likely in attendance for Hilbert's address, the two never met face to face . Gödel announced his first incompleteness theorem at a roundtable discussion session on the third day of the conference. The announcement drew little attention apart from that of von Neumann, who pulled Gödel aside for conversation. Later that year, working independently with knowledge of the first incompleteness theorem, von Neumann obtained a proof of the second incompleteness theorem, which he announced to Gödel in a letter dated November 20, 1930 . Gödel had independently obtained the second incompleteness theorem and included it in his submitted manuscript, which was received by ''Monatshefte für Mathematik'' on November 17, 1930. Gödel's paper was published in the ''Monatshefte'' in 1931 under the title "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" (" On Formally Undecidable Propositions in Principia Mathematica and Related Systems I"). As the title implies, Gödel originally planned to publish a second part of the paper in the next volume of the ''Monatshefte''; the prompt acceptance of the first paper was one reason he changed his plans .


Generalization and acceptance

Gödel gave a series of lectures on his theorems at Princeton in 1933–1934 to an audience that included Church, Kleene, and Rosser. By this time, Gödel had grasped that the key property his theorems required is that the system must be effective (at the time, the term "general recursive" was used). Rosser proved in 1936 that the hypothesis of ω-consistency, which was an integral part of Gödel's original proof, could be replaced by simple consistency, if the Gödel sentence was changed in an appropriate way. These developments left the incompleteness theorems in essentially their modern form. Gentzen published his
consistency proof In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent i ...
for first-order arithmetic in 1936. Hilbert accepted this proof as "finitary" although (as Gödel's theorem had already shown) it cannot be formalized within the system of arithmetic that is being proved consistent. The impact of the incompleteness theorems on Hilbert's program was quickly realized. Bernays included a full proof of the incompleteness theorems in the second volume of ''Grundlagen der Mathematik'' (
1939 This year also marks the start of the Second World War, the largest and deadliest conflict in human history. Events Below, the events of World War II have the "WWII" prefix. January * January 1 ** Third Reich *** Jews are forbidden to ...
), along with additional results of Ackermann on the ε-substitution method and Gentzen's consistency proof of arithmetic. This was the first full published proof of the second incompleteness theorem.


Criticisms


Finsler

used a version of
Richard's paradox In logic, Richard's paradox is a semantical antinomy of set theory and natural language first described by the French mathematician Jules Richard in 1905. The paradox is ordinarily used to motivate the importance of distinguishing carefully betwee ...
to construct an expression that was false but unprovable in a particular, informal framework he had developed. Gödel was unaware of this paper when he proved the incompleteness theorems (Collected Works Vol. IV., p. 9). Finsler wrote to Gödel in 1931 to inform him about this paper, which Finsler felt had priority for an incompleteness theorem. Finsler's methods did not rely on formalized provability, and had only a superficial resemblance to Gödel's work . Gödel read the paper but found it deeply flawed, and his response to Finsler laid out concerns about the lack of formalization (). Finsler continued to argue for his philosophy of mathematics, which eschewed formalization, for the remainder of his career.


Zermelo

In September 1931,
Ernst Zermelo Ernst Friedrich Ferdinand Zermelo (, ; 27 July 187121 May 1953) was a German logician and mathematician, whose work has major implications for the foundations of mathematics. He is known for his role in developing Zermelo–Fraenkel axiomatic se ...
wrote to Gödel to announce what he described as an "essential gap" in Gödel's argument (). In October, Gödel replied with a 10-page letter (, ), 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 Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1933, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics. Informally, the theorem states that ''arithmetical truth ...
). But Zermelo did not relent and published his criticisms in print with "a rather scathing paragraph on his young competitor" (). Gödel decided that to pursue the matter further was pointless, and Carnap agreed (). 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.


Wittgenstein

Ludwig Wittgenstein Ludwig Josef Johann Wittgenstein ( ; ; 26 April 1889 – 29 April 1951) was an Austrian-British philosopher who worked primarily in logic, the philosophy of mathematics, the philosophy of mind, and the philosophy of language. He is considere ...
wrote several passages about the incompleteness theorems that were published posthumously in his 1953 '' Remarks on the Foundations of Mathematics'', in particular one section sometimes called the "notorious paragraph" where he seems to confuse the notions of "true" and "provable" in Russell's system. Gödel was a member of the
Vienna Circle The Vienna Circle (german: Wiener Kreis) of Logical Empiricism was a group of elite philosophers and scientists drawn from the natural and social sciences, logic and mathematics who met regularly from 1924 to 1936 at the University of Vienna, cha ...
during the period in which Wittgenstein's early
ideal language philosophy Ideal language philosophy is contrasted with ordinary language philosophy. From about 1910 to 1930, analytic philosophers like Bertrand Russell and Ludwig Wittgenstein emphasized creating an ideal language for philosophical analysis, which would b ...
and
Tractatus Logico-Philosophicus The ''Tractatus Logico-Philosophicus'' (widely abbreviated and cited as TLP) is a book-length philosophical work by the Austrian philosopher Ludwig Wittgenstein which deals with the relationship between language and reality and aims to define the ...
dominated the circle's thinking. There has been some controversy about whether Wittgenstein misunderstood the incompleteness theorem or just expressed himself unclearly. Writings in Gödel's
Nachlass ''Nachlass'' (, older spelling ''Nachlaß'') is a German word, used in academia to describe the collection of manuscripts, notes, correspondence, and so on left behind when a scholar dies. The word is a compound in German: ''nach'' means "after ...
express the belief that Wittgenstein misread his ideas. Multiple commentators have read Wittgenstein as misunderstanding Gödel , although
Juliet Floyd Juliet Floyd is professor of philosophy at Boston University. Her strongest research interests lie in early analytic philosophy (on which she has edited a volume) and she has used early analytic philosophy as a lens to examine a diverse array of ...
and , as well as 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 . The unanimity of this criticism caused Wittgenstein's remarks on the incompleteness theorems to have little impact on the logic community. In 1972, Gödel stated: "Has Wittgenstein lost his mind? Does he mean it seriously? He intentionally utters trivially nonsensical statements" , and wrote to
Karl Menger Karl Menger (January 13, 1902 – October 5, 1985) was an Austrian-American mathematician, the son of the economist Carl Menger. In mathematics, Menger studied the theory of algebras and the dimension theory of low- regularity ("rough") curves ...
that Wittgenstein's comments demonstrate a misunderstanding of the incompleteness theorems writing: 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. argue that Wittgenstein had a more complete understanding of the incompleteness theorem than was previously assumed. They are particularly concerned with the interpretation of a Gödel sentence for an ω-inconsistent system as actually saying "I am not provable", since the system has no models in which the provability predicate corresponds to actual provability. argues that their interpretation of Wittgenstein is not historically justified, while argues against Floyd and Putnam's philosophical analysis of the provability predicate. explores the relationship between Wittgenstein's writing and theories of paraconsistent logic.


See also

*
Gödel machine A Gödel machine is a hypothetical self-improving computer program that solves problems in an optimal way. It uses a recursive self-improvement protocol in which it rewrites its own code when it can prove the new code provides a better strategy. The ...
*
Gödel's completeness theorem Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. The completeness theorem applies to any first-order theory: I ...
*
Gödel's speed-up theorem In mathematics, Gödel's speed-up theorem, proved by , shows that there are theorems whose proofs can be drastically shortened by working in more powerful axiomatic systems. Kurt Gödel showed how to find explicit examples of statements in formal ...
* ''
Gödel, Escher, Bach ''Gödel, Escher, Bach: an Eternal Golden Braid'', also known as ''GEB'', is a 1979 book by Douglas Hofstadter. By exploring common themes in the lives and works of logician Kurt Gödel, artist M. C. Escher, and composer Johann Sebastian Bach, t ...
'' *
Löb's Theorem In mathematical logic, Löb's theorem states that in Peano arithmetic (PA) (or any formal system including PA), for any formula ''P'', if it is provable in PA that "if ''P'' is provable in PA then ''P'' is true", then ''P'' is provable in PA. If Pr ...
* ''
Minds, Machines and Gödel "Minds, Machines and Gödel" is J. R. Lucas's 1959 philosophical paper in which he argues that a human mathematician cannot be accurately represented by an algorithmic automaton. Appealing to Gödel's incompleteness theorem, he argues that for a ...
'' * Non-standard model of arithmetic *
Proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...
*
Provability logic Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic. Examples ...
*
Quining Indirect self-reference describes an object referring to itself ''indirectly''. For example, define the function f such that f(x) = x(x). Any function passed as an argument to f is invoked with itself as an argument, and thus in any use of that a ...
*
Tarski's undefinability theorem Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1933, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics. Informally, the theorem states that ''arithmetical truth ...
* Theory of everything#Gödel's incompleteness theorem * Typographical Number Theory


References


Citations


Articles by Gödel

* Kurt Gödel, 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I", Monatshefte für Mathematik und Physik, v. 38 n. 1, pp. 173–198. * —, 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I", in
Solomon Feferman Solomon Feferman (December 13, 1928 – July 26, 2016) was an American philosopher and mathematician who worked in mathematical logic. Life Solomon Feferman was born in The Bronx in New York City to working-class parents who had immigrated to th ...
, ed., 1986. ''Kurt Gödel Collected works, Vol. I''. Oxford University Press, pp. 144–195. . The original German with a facing English translation, preceded by an introductory note by
Stephen Cole Kleene Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
. * —, 1951, "Some basic theorems on the foundations of mathematics and their implications", in
Solomon Feferman Solomon Feferman (December 13, 1928 – July 26, 2016) was an American philosopher and mathematician who worked in mathematical logic. Life Solomon Feferman was born in The Bronx in New York City to working-class parents who had immigrated to th ...
, ed., 1995. ''Kurt Gödel Collected works, Vol. III'', Oxford University Press, pp. 304–323. .


Translations, during his lifetime, of Gödel's paper into English

None of the following agree in all translated words and in typography. The typography is a serious matter, because Gödel expressly wished to emphasize "those metamathematical notions that had been defined in their usual sense before . . ." . Three translations exist. Of the first John Dawson states that: "The Meltzer translation was seriously deficient and received a devastating review in the ''Journal of Symbolic Logic''; "Gödel also complained about Braithwaite's commentary . "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 . . . ut because of time constraints heagreed to its publication" (ibid). (In a footnote Dawson states that "he would regret his compliance, for the published volume was marred throughout by sloppy typography and numerous misprints" (ibid)). Dawson states that "The translation that Gödel favored was that by Jean van Heijenoort" (ibid). For the serious student another version exists as a set of lecture notes recorded by Stephen Kleene and J. B. Rosser "during lectures given by Gödel at to the Institute for Advanced Study during the spring of 1934" (cf commentary by 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 Richard Bevan Braithwaite (15 January 1900 – 21 April 1990) was an English philosopher who specialized in the philosophy of science, ethics, and the philosophy of religion. Life Braithwaite was born in Banbury, Oxfordshire, son of th ...
(Introduction), 1962. ''On Formally Undecidable Propositions of Principia Mathematica and Related Systems'', Dover Publications, New York (Dover edition 1992), (pbk.) This contains a useful translation of Gödel's German abbreviations on pp. 33–34. As noted above, typography, translation and commentary is suspect. Unfortunately, this translation was reprinted with all its suspect content by :* Stephen Hawking editor, 2005. ''God Created the Integers: The Mathematical Breakthroughs That Changed History'', Running Press, Philadelphia, . Gödel's paper appears starting on p. 1097, with Hawking's commentary starting on p. 1089. * Martin Davis editor, 1965. ''The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable problems and Computable Functions'', Raven Press, New York, no ISBN. Gödel's paper begins on page 5, preceded by one page of commentary. *
Jean van Heijenoort Jean Louis Maxime van Heijenoort (; July 23, 1912 – March 29, 1986) was a historian of mathematical logic. He was also a personal secretary to Leon Trotsky from 1932 to 1939, and an American Trotskyist until 1947. Life Van Heijenoort was born ...
editor, 1967, 3rd edition 1967. ''From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931'', Harvard University Press, Cambridge Mass., (pbk). van Heijenoort did the translation. He states that "Professor Gödel approved the translation, which in many places was accommodated to his wishes." (p. 595). Gödel's paper begins on p. 595; van Heijenoort's commentary begins on p. 592. * Martin Davis editor, 1965, ibid. "On Undecidable Propositions of Formal Mathematical Systems." A copy with Gödel's corrections of errata and Gödel's added notes begins on page 41, preceded by two pages of Davis's commentary. Until Davis included this in his volume this lecture existed only as mimeographed notes.


Articles by others

*
George Boolos George Stephen Boolos (; 4 September 1940 – 27 May 1996) was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology. Life Boolos is of Greek-Jewish descent. He graduated with an A.B. i ...
, 1989, "A New Proof of the Gödel Incompleteness Theorem", ''Notices of the American Mathematical Society'', v, 36, pp. 388–390 and p. 676, reprinted in Boolos, 1998, ''Logic, Logic, and Logic'', Harvard Univ. Press. * Bernd Buldt, 2014,
The Scope of Gödel's First Incompleteness Theorem
", ''
Logica Universalis ''Logica Universalis'' is a peer-reviewed academic journal which covers research related to universal logic Originally the expression ''Universal logic'' was coined by analogy with the expression ''Universal algebra''. The first idea was to dev ...
'', v. 8, pp. 499–552. * * *
Jean van Heijenoort Jean Louis Maxime van Heijenoort (; July 23, 1912 – March 29, 1986) was a historian of mathematical logic. He was also a personal secretary to Leon Trotsky from 1932 to 1939, and an American Trotskyist until 1947. Life Van Heijenoort was born ...
, 1963, "Gödel's Theorem" in Edwards, Paul, ed., ''Encyclopedia of Philosophy, v. 3''. Macmillan, pp. 348–57. *
Geoffrey Hellman Geoffrey Hellman (born August 16, 1943) is an American professor and philosopher. He is Professor of Philosophy at the University of Minnesota in Minneapolis, Minnesota. He obtained his B.A. (1965) and Ph.D. (1972) degrees in philosophy from Harv ...
, 1981, "How to Gödel a Frege-Russell: Gödel's Incompleteness Theorems and Logicism", ''Noûs'', v. 15 n. 4, Special Issue on Philosophy of Mathematics, pp. 451–468. *
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many a ...
, 1900,
Mathematical Problems.
English translation of a lecture delivered before the International Congress of Mathematicians at Paris, containing Hilbert's statement of his Second Problem. * Martin Hirzel, 2000,
On formally undecidable propositions of Principia Mathematica and related systems I.
" An English translation of Gödel's paper. Archived fro
the original
Sept. 16, 2004. * *
Stephen Cole Kleene Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
, 1943, "Recursive predicates and quantifiers", reprinted from ''Transactions of the American Mathematical Society'', v. 53 n. 1, pp. 41–73 in Martin Davis 1965, ''The Undecidable'' (loc. cit.) pp. 255–287. * * *
John Barkley Rosser John Barkley Rosser Sr. (December 6, 1907 – September 5, 1989) was an American logician, a student of Alonzo Church, and known for his part in the Church–Rosser theorem, in lambda calculus. He also developed what is now called the " Rosser si ...
, 1936, "Extensions of some theorems of Gödel and Church", reprinted from the ''Journal of Symbolic Logic'', v. 1 (1936) pp. 87–91, in Martin Davis 1965, ''The Undecidable'' (loc. cit.) pp. 230–235. * —, 1939, "An Informal Exposition of proofs of Gödel's Theorem and Church's Theorem", Reprinted from the ''Journal of Symbolic Logic'', v. 4 (1939) pp. 53–60, in Martin Davis 1965, ''The Undecidable'' (loc. cit.) pp. 223–230 * * 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. * *


Books about the theorems

* Francesco Berto. ''There's Something about Gödel: The Complete Guide to the Incompleteness Theorem'' John Wiley and Sons. 2010. * Norbert Domeisen, 1990
''Logik der Antinomien''
Bern: Peter Lang. 142 S. 1990. . . * * Douglas Hofstadter, 1979. '' Gödel, Escher, Bach: An Eternal Golden Braid''. Vintage Books. . 1999 reprint: . * —, 2007. ''
I Am a Strange Loop ''I Am a Strange Loop'' is a 2007 book by Douglas Hofstadter, examining in depth the concept of a '' strange loop'' to explain the sense of "I". The concept of a ''strange loop'' was originally developed in his 1979 book '' Gödel, Escher, Bach' ...
''. Basic Books. . . *
Stanley Jaki Stanley L. Jaki (Jáki Szaniszló László) (17 August 1924 in Győr, Hungary – 7 April 2009 in Madrid, Spain) was a Hungarian-born priest of the Benedictine order. From 1975 to his death, he was Distinguished University Professor at Seton H ...
, OSB, 2005. ''The drama of the quantities''
Real View Books.
*
Per Lindström Per "Pelle" Lindström (9 April 1936 – 21 August 2009, Gothenburg) ASLbr>Newsletter September 2009 was a Swedish logician, after whom Lindström's theorem and the Lindström quantifier are named. (He also independently discovered Ehrenfeucht– ...
, 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 Ernest Nagel (November 16, 1901 – September 20, 1985) was an American philosopher of science. Suppes, Patrick (1999)Biographical memoir of Ernest Nagel In '' American National Biograph''y (Vol. 16, pp. 216-218). New York: Oxford University Pr ...
, James Roy Newman, Douglas Hofstadter, 2002 (1958). ''Gödel's Proof'', revised ed. . *
Rudy Rucker Rudolf von Bitter Rucker (; born March 22, 1946) is an American mathematician, computer scientist, science fiction author, and one of the founders of the cyberpunk literary movement. The author of both fiction and non-fiction, he is best known f ...
, 1995 (1982). ''Infinity and the Mind: The Science and Philosophy of the Infinite''. Princeton Univ. Press. * * N. Shankar, 1994. ''Metamathematics, Machines and Gödel's Proof'', Volume 38 of Cambridge tracts in theoretical computer science. *
Raymond Smullyan Raymond Merrill Smullyan (; May 25, 1919 – February 6, 2017) was an American mathematician, magician, concert pianist, logician, Taoist, and philosopher. Born in Far Rockaway, New York, his first career was stage magic. He earned a BSc from th ...
, 1987. ''Forever Undecided'' - 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. . * Hao Wang, 1997. ''A Logical Journey: From Gödel to Philosophy''. MIT Press.


Miscellaneous references

* Francesco Berto, 2009, "The Gödel Paradox and Wittgenstein's Reasons" ''
Philosophia Mathematica ''Philosophia Mathematica'' is a philosophical journal devoted to the philosophy of mathematics, published by Oxford University Press Oxford University Press (OUP) is the university press of the University of Oxford. It is the largest univers ...
'' (III) 17. * * *
Rebecca Goldstein Rebecca Newberger Goldstein (born February 23, 1950) is an American philosopher, novelist, and public intellectual. She has written ten books, both fiction and non-fiction. She holds a Ph.D. in philosophy of science from Princeton University, and ...
, 2005, ''Incompleteness: the Proof and Paradox of Kurt Gödel'', W. W. Norton & Company. * * John Harrison, 2009, "Handbook of Practical Logic and Automated Reasoning", Cambridge University Press, *
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many a ...
and
Paul Bernays Paul Isaac Bernays (17 October 1888 – 18 September 1977) was a Swiss mathematician who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant and close collaborator of ...
, ''
Grundlagen der Mathematik ''Grundlagen der Mathematik'' (English: ''Foundations of Mathematics'') is a two-volume work by David Hilbert and Paul Bernays. Originally published in 1934 and 1939, it presents fundamental mathematical ideas and introduced second-order arithme ...
'', Springer-Verlag. *
John Hopcroft John Edward Hopcroft (born October 7, 1939) is an American theoretical computer scientist. His textbooks on theory of computation (also known as the Cinderella book) and data structures are regarded as standards in their fields. He is the IBM P ...
and
Jeffrey Ullman Jeffrey David Ullman (born November 22, 1942) is an American computer scientist and the Stanford W. Ascherman Professor of Engineering, Emeritus, at Stanford University. His textbooks on compilers (various editions are popularly known as the dr ...
1979, ''
Introduction to Automata Theory, Languages, and Computation ''Introduction to Automata Theory, Languages, and Computation'' is an influential computer science textbook by John Hopcroft and Jeffrey Ullman on formal languages and the theory of computation. Rajeev Motwani contributed to later editions beg ...
'', Addison-Wesley, * James P. Jones
"Undecidable Diophantine Equations"
''Bulletin of the American Mathematical Society'', v. 3 n. 2, 1980, pp. 859–862. *
Stephen Cole Kleene Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
, 1967, ''Mathematical Logic''. Reprinted by Dover, 2002. * Russell O'Connor, 2005,
Essential Incompleteness of Arithmetic Verified by Coq
, Lecture Notes in Computer Science v. 3603, pp. 245–260. *
Lawrence Paulson Lawrence Charles Paulson (born 1955) is an American computer scientist. He is a Professor of Computational Logic at the University of Cambridge Computer Laboratory and a Fellow of Clare College, Cambridge. Education Paulson graduated from the ...
, 2013, "A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets", ''Review of Symbolic Logic'', v. 7 n. 3, 484–498. *
Graham Priest Graham Priest (born 1948) is Distinguished Professor of Philosophy at the CUNY Graduate Center, as well as a regular visitor at the University of Melbourne, where he was Boyce Gibson Professor of Philosophy and also at the University of St Andr ...
, 1984, "Logic of Paradox Revisited", ''Journal of Philosophical Logic'', v. 13,` n. 2, pp. 153–179. * —, 2004, ''Wittgenstein's Remarks on Gödel's Theorem'' in Max Kölbel, ed., ''Wittgenstein's lasting significance'', Psychology Press, pp. 207–227. * —, 2006, ''In Contradiction: A Study of the Transconsistent'', Oxford University Press, *
Hilary Putnam Hilary Whitehall Putnam (; July 31, 1926 – March 13, 2016) was an American philosopher, mathematician, and computer scientist, and a major figure in analytic philosophy in the second half of the 20th century. He made significant contributions ...
, 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 Wolfgang Rautenberg (27 February 1936 − 4 September 2011) was a German mathematician and logician whose areas of research were model theory, non-classical logic, modal logic, temporal logic and self reference. Life Rautenberg was born in Pot ...
, 2010,
A Concise Introduction to Mathematical Logic
', 3rd. ed., Springer, * Victor Rodych, 2003, "Misunderstanding Gödel: New Arguments about Wittgenstein and New Remarks by Wittgenstein", ''Dialectica'' v. 57 n. 3, pp. 279–313. *
Stewart Shapiro Stewart Shapiro (; born 1951) is O'Donnell Professor of Philosophy at the Ohio State University and distinguished visiting professor at the University of Connecticut. He is a leading figure in the philosophy of mathematics where he defends the a ...
, 2002, "Incompleteness and Inconsistency", ''Mind'', v. 111, pp 817–32. *
Alan Sokal Alan David Sokal (; born January 24, 1955) is an American professor of mathematics at University College London and professor emeritus of physics at New York University. He works in statistical mechanics and combinatorics. He is a critic of postmo ...
and
Jean Bricmont Jean Bricmont (; born 12 April 1952) is a Belgian theoretical physicist and philosopher of science. Professor at the Catholic University of Louvain (UCLouvain), he works on renormalization group and nonlinear differential equations. Since 2004, ...
, 1999, ''
Fashionable Nonsense ''Fashionable Nonsense: Postmodern Intellectuals' Abuse of Science'' (1998; UK: ''Intellectual Impostures''), first published in French in 1997 as french: Impostures intellectuelles, label=none, is a book by physicists Alan Sokal and Jean Bricmont ...
: Postmodern Intellectuals' Abuse of Science'', Picador. *
Joseph R. Shoenfield Joseph Robert Shoenfield (1927, Detroit – November 15, 2000, Durham, North Carolina) was an American mathematical logician. Education Shoenfield obtained his PhD in 1953 with Raymond Louis Wilder at the University of Michigan (''Models of form ...
(1967), ''Mathematical Logic''. Reprinted by A.K. Peters for the
Association for Symbolic Logic The Association for Symbolic Logic (ASL) is an international organization of specialists in mathematical logic and philosophical logic. The ASL was founded in 1936, and its first president was Alonzo Church. The current president of the ASL is ...
, 2001. *
Jeremy Stangroom Jeremy Stangroom is a British writer, editor, and website designer. He is an editor and co-founder, with Julian Baggini, of ''The Philosophers’ Magazine'', and has written and edited several philosophy books. He is also co-founder, with Opheli ...
and
Ophelia Benson Ophelia Benson is an American author, editor, blogger, and feminist. Benson is the editor of the website ''Butterflies and Wheels'' and a columnist and former associate editor of ''The Philosophers' Magazine''. She is also a columnist for ''Free ...
, ''Why Truth Matters'', Continuum. * George Tourlakis, ''Lectures in Logic and Set Theory, Volume 1, Mathematical Logic'', Cambridge University Press, 2003. *
Avi Wigderson Avi Wigderson ( he, אבי ויגדרזון; born 9 September 1956) is an Israeli mathematician and computer scientist. He is the Herbert H. Maass Professor in the school of mathematics at the Institute for Advanced Study in Princeton, New Jerse ...
, 2010,
The Gödel Phenomena in Mathematics: A Modern View
, in ''Kurt Gödel and the Foundations of Mathematics: Horizons of Truth'', Cambridge University Press. * Hao Wang, 1996, ''A Logical Journey: From Gödel to Philosophy'', The MIT Press, Cambridge MA, . *


External links

* * . * .
''Paraconsistent Logic § Arithmetic and Gödel's Theorem''
entry in the
Stanford Encyclopedia of Philosophy The ''Stanford Encyclopedia of Philosophy'' (''SEP'') combines an online encyclopedia of philosophy with peer-reviewed publication of original papers in philosophy, freely accessible to Internet users. It is maintained by Stanford University. Eac ...
. * MacTutor biographies: *
Kurt Gödel.
*



by ''Karlis Podnieks''. An online free book.

using a printing machine as an example.
October 2011 RadioLab episode
about/including Gödel's Incompleteness theorem *
How Gödel's Proof Works
by
Natalie Wolchover Natalie Ann Wolchover (born October 16, 1986) is a science journalist. She is a senior writer and editor for ''Quanta Magazine'', and has been involved with ''Quanta''s development since its inception in 2013. In 2022 she won a Pulitzer Prize for ...
,
Quanta Magazine ''Quanta Magazine'' is an editorially independent online publication of the Simons Foundation covering developments in physics, mathematics, biology and computer science. ''Undark Magazine'' described ''Quanta Magazine'' as "highly regarded for ...
, July 14, 2020.

an

Gödel's incompleteness theorems formalised in Isabelle/HOL ` {{DEFAULTSORT:Goedels Incompleteness Theorems Theorems in the foundations of mathematics Mathematical logic Model theory Proof theory Epistemology Metatheorems
Incompleteness theorems Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies t ...