mathematics Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...

, Gödel's speed-up theorem, proved by , shows that there are

theorem In mathematics and formal logic, a theorem is a statement (logic), statement that has been Mathematical proof, proven, or can be proven. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to esta ...

s 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 profoundly ...

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 nea ...

in fewer than a

googolplex A googolplex is the large number 10, or equivalently, 10 or . Written out in ordinary decimal notation, it is 1 followed by 10100 zeroes; that is, a 1 followed by a googol of zeroes. Its prime factorization is 2 ×5. History In 1920, ...

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 In deductive logic, a consistent theory is one that does not lead to a logical contradiction. A theory T is consistent if there is no formula \varphi such that both \varphi and its negation \lnot\varphi are elements of the set of consequences ...

, 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 In traditional logic, a contradiction involves a proposition conflicting 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's ...

. 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 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 An integer is the number zero (0), a positive natural number (1, 2, 3, ...), or the negation of a positive natural number (−1, −2, −3, ...). The negations or additive inverses of the positive natural numbers are referred to as negative in ...

''n'' such that if there is a sequence of rooted trees ''T''₁, ''T''₂, ..., ''T''_''n'' such that ''T_k'' has at most ''k'' + 10 vertices, then some tree can be

homeomorphic In mathematics and more specifically in topology, a homeomorphism ( from Greek roots meaning "similar shape", named by Henri Poincaré), also called topological isomorphism, or bicontinuous function, is a bijective and continuous function betw ...

ally 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 and has a short proof in second order arithmetic. If one takes Peano arithmetic together with the

negation In logic, negation, also called the logical not or logical complement, is an operation (mathematics), operation that takes a Proposition (mathematics), proposition P to another proposition "not P", written \neg P, \mathord P, P^\prime or \over ...

of the statement above, one obtains an inconsistent theory whose shortest known contradiction is equivalently long.

References

* * * * {{DEFAULTSORT:Godel's Speed-Up Theorem Proof theory Theorems in the foundations of mathematics Speed-up theorem

See also

References