# Are any natural examples of Gödel speed-up known?

In 1936 Gödel announced a theorem to the effect that proofs of certain theorems $T_1,T_2,\ldots$ become dramatically shorter when one passes from a formal system, such as Peano arithmetic PA, to a stronger one, such as a system in which Con(PA) is provable. More precisely, given any computable function $f$, we can find a sequence $T_1,T_2,\ldots$ of theorems such that $T_k$ has a proof of length of order $k$ in the stronger system, whereas any proof of $T_k$ in PA has length at least $f(k)$.

Various versions of this theorem have been proved, depending on the strengthening of PA chosen, and on the definition of length. See, in particular, this paper. However, I have not found a version with a natural sequence of theorems $T_k$. For example, it seems plausible that one could use Goodstein's theorem, by taking

$T_k$ = The Goodstein process, starting with input $k$, eventually halts.

Are any such "natural'' examples of Gödel speed-up known?

Update and clarification. Gödel's speed-up theorem gives, for any computable function $f$, a sequence of theorems $T_1,T_2,\ldots$ of PA such that each $T_k$ has a proof of length $O(k)$ in some strengthening of PA, while the shortest proof of $T_k$ in PA has length $\ge f(k)$. In this theorem, the sequence $T_1, T_2,\ldots$ depends on $f$.

If we want a "natural" sequence $T_1,T_2,\ldots$ (in particular, if $T_k=\varphi(k)$ for some fixed formula $\varphi$) then we can no longer demand that $f$ be an arbitrary computable function, or even of arbitrary computable rate of growth. This is because (assuming the sequence $T_1,T_2,\ldots$ is c.e.) the function

$g(k)$ = length of the shortest proof of $T_k$ in PA

is computable, so we cannot ask $f$ to grow faster then $g$.

So, since I want the sequence $T_1,T_2,\ldots$ to be fixed, I have to be satisfied if $T_k$ has shortest proof in PA with length of $O(f(k))$ some reasonably fast-growing $f$. It seems that Harvey Friedman has examples that fit the bill, as Richard Borcherds has pointed out. However, before I accept Richard's answer, I would like to know a precise reference. I have pored over Harvey Friedman's Research on the Foundations of Mathematics (North-Holland 1985),
and some other works, without finding a clear statement of speed-up in the above sense.

• I doubt that the Goodstein statements of the form $T_{k}$ specified in Stillwell's Question satisfy Gödel-type speed-up. This is based on the observation that such statements are $\Sigma_1$, whereas the statements $T_{k}$ of Gödel's are $\Pi _{2}$ [also, in the paper cited by Stillwell, Buss's improved version of Gödel's theorem produces $\Pi _{1}$ statements]. – Ali Enayat May 18 '11 at 20:58
• There is always estatis.coders.fm/falso – Justin Hilburn May 19 '11 at 7:04

• The speed-up asked for in the question of Stillwell involves arbitrary recursive functions [i.e., superrecursive speed-up]. It also deals with the infinite sequence of theories $Z_n$ : = "n-th order arithmetic". Neither feature seems to be present in Friedman's treatment of the Kruskal theorem. – Ali Enayat May 18 '11 at 20:58
• You are saying that because ZFC or even PA+"$\epsilon_0$ is well-founded" proves the universal version, we can deduce any particular $T_k$ in one additional step by universal instantiation, so the $T_k$ have constant-length proofs in such a theory (measured by the number of assertions). And although each $T_k$ is provable in PA, could you explain how we know that these proof lengths must grow? Of course, we can find very long proofs for each $n$ by computing the Goodstein sequence for that $n$, and perhaps the idea is that any proof must essentially do this, but how do we know this? – Joel David Hamkins May 18 '11 at 12:30
• @JDH: The proofs have to grow by counting, since there are only finitely many short proofs. Of course, it's not obvious that the proofs grow faster than $\log n$, which is what one needs to make a sensible statement. – Daniel Litt May 19 '11 at 5:36
• @Daniel: It is an interesting question whether the length of the shortest proof of $T_k$ is strictly increasing with $k$, but I know of no current tools that would allow one to approach this problem. I strongly suspect (for technical reasons) that at the very least for every $n$, the value $g(2^n)=$ the length of the smallest proof of $T_{2^n}$ is strictly larger than all the previous $g(m)$, but do not think this question is tractable with current tools. – Andrés E. Caicedo May 19 '11 at 6:10
• Daniel, if you measure the proof length as I mentioned by the number of statements (not the Goedel code), then there are infinitely many proofs of any finite size. This is why the $T_k$ have constant length proofs in ZFC. So the counting argument doesn't work. If you want to measure proof size by Goedel code, then there are only finitely many proofs of a given size, but in this case, you don't have constant length proofs of the $T_k$ in ZFC. (In the linked Sam Buss article, proof length is measured by the number of applications of modus ponens.) – Joel David Hamkins May 19 '11 at 10:36