Gödel's speed-up theorem

In mathematics, Gödel's speed-up theorem, proved by Gödel (1936), 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 unimaginably long. For example, the statement:

"This statement cannot be proved in Peano arithmetic in fewer than a googolplex 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 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 (Smoryński 1982). For example, the statement

"there is an integern such that if there is a sequence of rooted treesT₁, T₂, ..., T_n such that T_k has at most k +10 vertices, then some tree can be homeomorphicallyembedded 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 of the statement above, one obtains an inconsistent theory whose shortest known contradiction is equivalently long.

Gödel's speed-up theorem defines the shortest proof length of a proposition ${\displaystyle \varphi }$ in a formal system ${\displaystyle T}$ as follows. Let ${\displaystyle L_{T}(\varphi )}$ denote the shortest proof length of the proposition ${\displaystyle \varphi }$ in the system ${\displaystyle T}$, and let ${\displaystyle L_{S}(\varphi )}$ denote the shortest proof length of the proposition ${\displaystyle \varphi }$ in the system ${\displaystyle S}$.

${\displaystyle L_{T}(\varphi )=\min\{\|\pi \|_{T}\}}$

Here, ${\displaystyle \pi }$ is a proof of ${\displaystyle \varphi }$ in ${\displaystyle T}$, and ${\displaystyle \|\pi \|_{T}}$ represents its length.

Furthermore, let ${\displaystyle S\subseteq T}$ be a consistent and recursively axiomatizable formal system, and assume that ${\displaystyle S}$ is a stronger system than ${\displaystyle T}$. Then, for any computable function ${\displaystyle f\colon \mathbb {N} \to \mathbb {N} }$,

${\displaystyle L_{T}(\varphi )>f(L_{S}(\varphi ))}$

holds.^[1]

• Blum's speedup theorem
• List of long proofs

• Buss, Samuel R. (1994), "On Gödel's theorems on lengths of proofs. I. Number of lines and speedup for arithmetics", The Journal of Symbolic Logic, 59 (3): 737–756, doi:10.2307/2275906, ISSN 0022-4812, JSTOR 2275906, MR 1295967, S2CID 914043
• Buss, Samuel R. (1995), "On Gödel's theorems on lengths of proofs. II. Lower bounds for recognizing k symbol provability", in Clote, Peter; Remmel, Jeffrey (eds.), Feasible mathematics, II (Ithaca, NY, 1992), Progr. Comput. Sci. Appl. Logic, vol. 13, Boston, MA: Birkhäuser Boston, pp. 57–90, ISBN 978-0-8176-3675-3, MR 1322274
• Gödel, Kurt (1936), "Über die Länge von Beweisen", Ergebnisse Eines Mathematischen Kolloquiums (in German), vol. 7, pp. 23–24, ISBN 9780195039641, Reprinted with English translation in volume 1 of his collected works.{{citation}}: ISBN / Date incompatibility (help)
• Smoryński, C. (1982), "The varieties of arboreal experience", Math. Intelligencer, 4 (4): 182–189, doi:10.1007/bf03023553, MR 0685558