Gödel's speed-up theorem
Encyclopedia
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 systems that are provable in that system but whose shortest proof is absurdly long. For example, the statement:
is provable in Peano arithmetic but the shortest proof has at least a googolplex symbols. It has a short proof in a more powerful system: in fact it is easily provable in Peano arithmetic together with the statement that Peano arithmetic is consistent (which cannot be proved in Peano arithmetic by Gödel's incompleteness theorem).
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
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.
Kurt Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
showed how to find explicit examples of statements in formal systems that are provable in that system but whose shortest proof is absurdly long. For example, the statement:
- "This statement cannot be proved in Peano arithmetic in less than a googolplex symbols"
is provable in Peano arithmetic but the shortest proof has at least a googolplex symbols. It has a short proof in a more powerful system: in fact it is easily provable in Peano arithmetic together with the statement that Peano arithmetic is consistent (which cannot be proved in Peano arithmetic by Gödel's incompleteness theorem).
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
Harvey Friedman
Harvey Friedman is a mathematical logician at Ohio State University in Columbus, Ohio. He is noted especially for his work on reverse mathematics, a project intended to derive the axioms of mathematics from the theorems considered to be necessary...
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.