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
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 ...
showed how to find explicit examples of statements in formal systems that are provable in that system but whose shortest proof is unimaginably long. For example, the statement:
:"This statement cannot be proved in
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 ...
in fewer than a
googolplex
A googolplex is the number 10, or equivalently, 10 or 1010,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000 . Written out in ordinary decimal notation, it is 1 fol ...
symbols"
is provable in Peano arithmetic (PA) but the shortest proof has at least a googolplex symbols, by an argument similar to the proof of
Gödel's first incompleteness theorem: If PA is consistent, then it cannot prove the statement in fewer than a googolplex symbols, because the existence of such a proof would itself be a theorem of PA, a contradiction. But simply enumerating all strings of length up to a googolplex and checking that each such string is not a proof (in PA) of the statement, yields a proof of the statement (which is necessarily longer than a googolplex symbols).
The statement has a short proof in a more powerful system: in fact the proof given in the previous paragraph is a proof in the system of Peano arithmetic plus the statement "Peano arithmetic is consistent" (which, per the incompleteness theorem, cannot be proved in Peano arithmetic).
In this argument, Peano arithmetic can be replaced by any more powerful consistent system, and a googolplex can be replaced by any number that can be described concisely in the system.
Harvey Friedman
__NOTOC__
Harvey Friedman (born 23 September 1948)Handbook of Philosophical Logic, , p. 38 is an American mathematical logician at Ohio State University in Columbus, Ohio. He has worked on reverse mathematics, a project intended to derive the axi ...
found some explicit natural examples of this phenomenon, giving some explicit statements in Peano arithmetic and other formal systems whose shortest proofs are ridiculously long . For example, the statement
:"there is an integer ''n'' such that if there is a sequence of rooted trees ''T''
1, ''T''
2, ..., ''T''
''n'' such that ''T''
''k'' has at most ''k''+10 vertices, then some tree can be homeomorphically
embedded in a later one"
is provable in Peano arithmetic, but the shortest proof has length at least ''A''(1000), where ''A''(0)=1 and ''A''(''n''+1)=2
''A''(''n''). The statement is a special case of
Kruskal's 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 by ; ...
and has a short proof in
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 of mathematics, foundation for much, but not all, ...
.
If one takes Peano arithmetic together with the negation of the statement above, one obtains an inconsistent theory whose shortest known contradiction is equivalently long.
See also
*
Blum's speedup theorem
In computational complexity theory, Blum's speedup theorem, first stated by Manuel Blum in 1967, is a fundamental theorem about the complexity of computable functions.
Each computable function has an infinite number of different program representa ...
*
List of long proofs
This is a list of unusually long mathematical proofs. Such proofs often use computational proof methods and may be considered non-surveyable.
, the longest mathematical proof, measured by number of published journal pages, is the classification ...
References
*
*
*
*
{{DEFAULTSORT:Godel's Speed-Up Theorem
Proof theory
Theorems in the foundations of mathematics
Speed-up theorem