Examples of undecidable decision problems:
0. Halting problem: there does not exist a computer program which tells you whether another computer program eventually halts.
1. Kleene's separation lemma: there does not exists a program program which tells you whether another computer program R returns a yes or a no.
- Proof: construct SPITE to print its code, calculate the expected output, and do the opposite.
In recursion theory, Kleene's separation lemma is usually stated this way: "There is a subset S of a recursively enumerable set R which cannot be recursively separated from its complement R-S". R is the set of programs that return yes or no. S is the set of programs that return yes, and R-S is the set of programs that return no.
2. There does not exist a program which tells you whether any other computer program finishes in polynomial or exponential time.
- Proof: construct SPITE(N) to ignore the input N, print its code, calculate the expected running time, then run an algorithm of the opposite running time on N. The first part does not depend on the input, and runs in fixed time.
3. word problem for groups: There does not exist a program which determines whether two elements in a finitely presented groups are equivalent. The decision problem was first posed by Max Dehn in 1911. Alan Turing proved that the problem for finitely presented monoids (no inverses) was equivalent to the halting problem and therefore undecidable, and the problem for groups was shown to be equivalent to the halting problem in 1952.
4. Behavior of Cellular automata: There does not exist a program which can determine whether an arbitrary starting configuration of Conway's Game of Life will eventually reach the empty configuration.
All the practical decision problems which have been shown to be undecidable, including all the ones above, are equivalent to the halting problem, Turing showed that there are much stronger degrees of undecidablity, while Post showed that there are weaker ones. It remains an open question to find natural mathematical forms for these types of undecidable problems.
Because undecidable can either refer to decision problems or to theorems, the term "independent" is sometimes used instead to mean "neither provable nor refutable". The usage of "independent" is also ambiguous, though, because some people use it to mean just "not provable", without saying whether it can be refuted.
Undecidability of a statement in a particular deductive system does not all by itself address the question of whether the truth value of the statement is well-defined, or whether it can be determined by other means. Undecidability only means that the particular deductive system being considered does not prove the statement true or false. Whether there exist so-called "absolutely undecidable" statements, whose truth value can never be known or is ill-specified, is a controversial point among various philosophical schools.
Kurt Godel produced the first undecidable statement in set theory, as an immediate corollary of the incompleteness theorem:
0. Undecidable in ZFC: There exists an inaccessible cardinal: An inaccessible cardinal is a set which is larger than any of the sets ZFC. The set of sets which are smaller than the inaccessible cardinal form a model for ZFC.
The combined work of Gödel and Paul Cohen produced the first two examples of otherwise interesting statements which are independent of the standard Zermelo Fraenkel axioms for set theory.
1. Undecidable in ZFC: The continuum hypothesis: there is no set which is bigger than the set of all integers but smaller than the set of all real numbers.
2. Undecidable in ZF: The axiom of choice: Every set has a one to one map to an ordinal.
Robert Solovay in 1979 proved the following independence theorem:
3. Undecidable in ZF: All subsets of the interval have a well defined Lebesgue measure.
Using the axiom of choice, it is easy to construct non-measurable sets and paradoxical decompositions. This theorem established that it is impossible to reach these paradoxes without uncountable choice.
Many other problems were shown to be undecidable in ZFC by Saharon Shelah, including the following in 1973.
The first statement which was proven to be undecidable in Peano arithmetic was the well foundedness of . Gentzen in 1936 proved the consistency of PA followed from this, and it immediately follows from Godel's theorem that it is undecidable in PA.
0. Undecidable in PA: any decreasing sequence of ordinals which starts at ends at 0.
Goodstein's theorem is a restatement of the well foundedness of designed to show skeptics that this can in fact be a reasonable statement about integers. Kirby and Paris later explicitly showed that Goodstein's theorem implies the consistency of Peano arithmetic. Although it is clear that Goodstein already knew this, he did not prove it.
1. Undecidable in PA: Goodstein's sequence terminates at 0 for all starting integers N.
In 1977, Paris and Harrington proved that the Paris-Harrington principle, a version of the Ramsey theorem, is equivalent to the consistency of Peano arithmetic. It is unprovable in the Peano axioms but can be proven to be true in any system which is capable of proving the consistency of Peano arithmetic, in particular set theory or second-order arithmetic.
4. Undecidable in PA: For every k-coloring of unordered m-tuples of integers, there exists a subset S such that: 1. every m-tuple of integers in S has the same color, 2. the number of elements in S is bigger than the least member of S. 3. S has more than a prespecified number of elements.
5. Undecidable in PA: Kruskal's tree theorem, which has applications in computer science, is also undecidable from the Peano axioms but provable in set theory. In fact Kruskal's tree theorem (or its finite form) is undecidable in a much stronger system codifying the principles acceptable on basis of a philosophy of mathematics called predicativism.
Algorithmic Information Theory
Gregory Chaitin produced undecidable statements in algorithmic information theory and proved another incompleteness theorem in that setting. Chaitin's theorem states that for any theory that can represent enough arithmetic, there is an upper bound c such that no specific number can be proven in that theory to have Kolmogorov complexity greater than c. While Godel's theorem is related to the liar paradox, Chaitin's result is related to Berry's paradox.
Limitations of Gödel's theorems
The conclusions of Gödel's theorems only hold for the formal systems that can describe a computer. Not all axiom systems can describe the functioning of a general purpose computer, even when these systems have models that include the natural numbers as a subset. For example, there are first-order axiomatizations of Euclidean geometry and real closed fields that do not meet the hypotheses of Gödel's theorems. The key fact is that these axiomatizations are not expressive enough to define an arbitrary primitive recursive function on the set of natural numbers.
A second limitation is that Gödel's theorems only apply to systems that are used as their own proof systems. For example, the consistency of the Peano arithmetic can be proved in set theory, but this proof is meaningless in the case that set theory is inconsistent, which cannot be proven in set theory. In 1936, Gerhard Gentzen proved the consistency of Peano arithmetic using a principle which is more powerful than what is usually called arithmetic, although it still talks about finite objects. That principle is that counting down from eventually reaches zero.
Discussion and implications
The incompleteness results affect the philosophy of mathematics, particularly viewpoints like formalism, which uses formal logic to define its principles. One can paraphrase the first theorem as saying, "we can never find an all-encompassing axiomatic system which is able to prove all mathematical truths, but no falsehoods."
On the other hand, from a strict formalist perspective this paraphrase would be considered meaningless because it presupposes that mathematical "truth" and "falsehood" are well-defined in an absolute sense, rather than relative to each formal system. The absolute formalist statement is in terms of verifiable statements, which are statements about computer programs. "We can never find an all-encompassing axiomatic system which is able to decide which computer programs halt".
The following rephrasing of the second theorem is even more unsettling to the foundations of mathematics:
- If an axiomatic system can be proven to be consistent from within itself, then it is inconsistent.
Therefore, in order to establish the consistency of a system S, one needs to use some other more powerful system T, but a proof in T is not necessarily completely convincing unless T's consistency has already been established without using S.
At first, Gödel's theorems left a loophole—it might be possible to produce a general algorithm that indicates whether a given statement is undecidable or not, thus allowing mathematicians to bypass the undecidable statements altogether. However, the negative answer to the Entscheidungsproblem, obtained by Church and Turing in 1936, showed that no such algorithm exists, since the Halting problem is undecidable.
There are some who hold that a statement that is unprovable within a deductive system will be provable in a metalanguage. And what cannot be proven in that metalanguage will be proven in a meta-metalanguage, recursively, ad infinitum. By invoking such a system of typed metalanguages, along with an axiom of Reducibility — which by an inductive assumption applies to the entire stack of languages — one may, for all practical purposes, overcome the obstacle of incompleteness.
The first to take this point of view was Hilbert, who did not accept that Godel's theorem presents an impediment to his formalist program. Hilbert believed that the proof of the theorem itself constructs the more powerful system T, and shows that the system is obviously consistent. Hilbert suggested that any system of mathematical deduction should allow extensions of the following form
- PA or Finite set theory.
- Reflection Axioms, which assert the consistency of the system 1.
- New Reflection Axioms which assert the consistency of system 2.
and so on. While Godel's theorem establishes that this process never ends after a finite number of steps, or even when iterated in any way which can be formalized as a computer program, it does not prove that this process considered as a process will not eventually decide any theorem, when repeated far enough in a non-algorithmic way. Paul Cohen considered the principle that this reflection process decides all theorems about the integers as a founding article of faith in mathematics .
Note that Gödel's theorems only apply to sufficiently strong axiomatic systems. "Sufficiently strong" means that the theory contains enough arithmetic to carry out the coding constructions needed for the proof of the first incompleteness theorem. Essentially, all that is required are some basic facts about addition and multiplication as formalized, e.g., in Robinson arithmetic Q. There are even weaker axiomatic systems that are consistent and complete, for instance Presburger arithmetic which proves every true first-order statement involving only addition.
The axiomatic system may consist of infinitely many axioms (as first-order Peano arithmetic does), but for Gödel's theorem to apply, there has to be an effective algorithm which is able to check proofs for correctness. For instance, one might take the set of all first-order sentences which are true in the standard model of the natural numbers. This system is complete; Gödel's theorem does not apply because there is no effective procedure that decides if a given sentence is an axiom. In fact, that this is so is a consequence of Gödel's first incompleteness theorem.
Another example of a specification of a theory to which Gödel's first theorem does not apply can be constructed as follows: order all possible statements about natural numbers first by length and then lexicographically, start with an axiomatic system initially equal to the Peano axioms, go through your list of statements one by one, and, if the current statement cannot be proven nor disproven from the current axiom system, add it to that system. This creates a system which is complete, consistent, and sufficiently powerful, but not computably enumerable.
Gödel himself only proved a technically slightly weaker version of the above theorems; the first proof for the versions stated above was given by J. Barkley Rosser in 1936.
In essence, the proof of the first theorem consists of constructing a statement p within a formal axiomatic system that can be given a meta-mathematical interpretation of:
- p = "This statement cannot be proven in the given formal theory"
As such, it can be seen as a modern variant of the Liar paradox, although unlike the classical paradoxes it's not really paradoxical.
If the axiomatic system is consistent, Gödel's proof shows that p (and its negation) cannot be proven in the system. Therefore p is true (p claims to be not provable, and it is not provable) yet it cannot be formally proved in the system. If the axiomatic system is ω-consistent, then the negation of p cannot be proven either, and so p is undecidable. In a system which is not ω-consistent (but consistent), either we have the same situation, or we have a false statement which can be proven (namely, the negation of p).
Adding p to the axioms of the system would not solve the problem: there would be another Gödel sentence for the enlarged theory. Theories such as Peano arithmetic, for which any computably enumerable consistent extension is incomplete, are called essentially incomplete.
Minds and machines
Authors including J. R. Lucas have debated what, if anything, Gödel's incompleteness theorems imply about human intelligence. Much of the debate centers on whether the human mind is equivalent to a Turing machine, or by the Church-Turing thesis, any finite machine at all. If it is, and if the machine is consistent, then Gödel's incompleteness theorems would apply to it.
Hilary Putnam (1960) suggested that while Gödel's theorems cannot be applied to humans, since they make mistakes and are therefore inconsistent, it may be applied to the human faculty of science or mathematics in general. If we are to believe that it is consistent, then either we cannot prove its consistency, or it cannot be represented by a Turing machine.
Douglas Hofstadter, in Godel, Escher, Bach, made the case that the process of spiting predictions about your own behavior, so central to the proof of Godel's theorem, is the essence of self-awareness, conciousness and creativity.
Postmodernism and continental philosophy
Appeals are sometimes made to the incompleteness theorems to support by analogy ideas which go beyond mathematics and logic. For instance, Régis Debray applies it to politics. A number of authors have commented, mostly negatively, on such extensions and interpretations, including Torkel Franzen, Alan Sokal and Jean Bricmont, Ophelia Benson and Jeremy Stangroom. The last two quote biographer Rebecca Goldstein commenting on the disparity between Gödel's avowed Platonism and the anti-realist uses to which his ideas are put by humanist intellectuals.
Theories of everything and physics
Stephen Hawking and others argue that (an analogous argument to) Gödel's theorem implies that even the most sophisticated formulation of physics will be incomplete, and that therefore there can never be an ultimate theory that can be formulated as a finite number of principles. 
The proof of Godel's theorem makes it manifest to many people that it has nothing to say about a theory of everything. Godel's theorem is a statement about computers, whose rules are already known. Knowing the rules and knowing what will eventually come out of the rules are two different issues, and Godel's theorem only talks about the latter.
- Hilbert D. "Die Grundlagen Der Elementaren Zahlentheorie" p. 215
- Cohen P., "Set Theory and the Continuum Hypothesis"
- "The secret takes the form of a logical law, an extension of Gödel's theorem: There can be no organised system without closure and no system can be closed by elements internal to that system alone".Debray, R. Critique of Political Reason, quoted in Sokal and Bricmont's Fashionable Nonsense.
- In their Why Truth Matters
- The Proof and paradox of Kurt Gödel
- Stephen Hawking "Gödel and the end of physics"