Editing Gödel's incompleteness theorems (section)

== Examples of undecidable statements ==
{{See also|List of statements independent of ZFC}}

There are two distinct senses of the word "undecidable" in mathematics and computer science. The first of these is the [[proof theory|proof-theoretic]] sense used in relation to Gödel's theorems, that of a statement being neither provable nor refutable in a specified [[deductive system]].  The second sense, which will not be discussed here, is used in relation to [[computability theory]] and applies not to statements but to [[decision problem]]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]] that correctly answers every question in the problem set (see [[undecidable problem]]).

Because of the two meanings of the word undecidable, the term [[independence (mathematical logic)|independent]] is sometimes used instead of undecidable for the "neither provable nor refutable" sense.

Undecidability of a statement in a particular deductive system does not, in and of itself, address the question of whether the [[truth value]] of the statement is well-defined, or whether it can be determined by other means. Undecidability only implies that the particular deductive system being considered does not prove the truth or falsity of the statement. Whether there exist so-called "absolutely undecidable" statements, whose truth value can never be known or is ill-specified, is a controversial point in the [[philosophy of mathematics]].

The combined work of Gödel and [[Paul Cohen (mathematician)|Paul Cohen]] has given two concrete examples of undecidable statements (in the first sense of the term): The [[continuum hypothesis]] can neither be proved nor refuted in [[ZFC]] (the standard axiomatization of [[set theory]]), and the [[axiom of choice]] can neither be proved nor refuted in ZF (which is all the ZFC axioms ''except'' the axiom of choice).  These results do not require the incompleteness theorem.   Gödel proved in 1940 that neither of these statements could be disproved in ZF or ZFC set theory. In the 1960s, Cohen proved that neither is provable from ZF, and the continuum hypothesis cannot be proved from ZFC.

{{harvtxt|Shelah|1974}} showed that the [[Whitehead problem]] in [[group theory]] is undecidable, in the first sense of the term, in standard set theory.{{sfn|Shelah|1974}}

[[Gregory Chaitin]] produced undecidable statements in [[algorithmic information theory]] and proved another incompleteness theorem in that setting. [[Chaitin's incompleteness theorem]] states that for any system that can represent enough arithmetic, there is an upper bound {{mvar|c}} such that no specific number can be proved in that system to have [[Kolmogorov complexity]] greater than {{mvar|c}}. While Gödel's theorem is related to the [[liar paradox]], Chaitin's result is related to [[Berry's paradox]].

=== Undecidable statements provable in larger systems ===

These are natural mathematical equivalents of the Gödel "true but undecidable" sentence. They can be proved in a larger system which is generally accepted as a valid form of reasoning, but are undecidable in a more limited system such as Peano Arithmetic.

In 1977, [[Jeff Paris (mathematician)|Paris]] and [[Leo Harrington|Harrington]] proved that the [[Paris–Harrington theorem|Paris&ndash;Harrington principle]], a version of the infinite [[Ramsey theorem]], is undecidable in (first-order) [[Peano arithmetic]], but can be proved in the stronger system of [[second-order arithmetic]]. Kirby and Paris later showed that [[Goodstein's theorem]], a statement about sequences of natural numbers somewhat simpler than the Paris&ndash;Harrington principle, is also undecidable in Peano arithmetic.

[[Kruskal's tree theorem]], which has applications in computer science, is also undecidable from Peano arithmetic but provable in set theory. In fact Kruskal's tree theorem (or its finite form) is undecidable in a much stronger system ATR<sub>0</sub> codifying the principles acceptable based on a philosophy of mathematics called [[impredicativity|predicativism]].<ref name="Simpson2009">S. G. Simpson, ''Subsystems of Second-Order Arithmetic'' (2009). Perspectives in Logic, ISBN 9780521884396.</ref>  The related but more general [[graph minor theorem]] (2003) has consequences for [[computational complexity theory]].