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

2011-05-18T00:53:45Z

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.

Answer by Richard Borcherds for Are any natural examples of Gödel speed-up known?

2011-05-18T04:16:23Z

Friedman has given many examples of such speedups. One well known one is his finite version of Kruskal's tree theorem. In particular he gave examples of reasonably natural statements that have very short proofs in 2nd order arithmetic, and can be proved in Peano arithmetic, but the shortest proof in Peano arithmetic is ridiculously long.

Answer by Lucas K. for Are any natural examples of Gödel speed-up known?

2011-05-18T11:11:45Z

Take Goodstein's theorem for a particular n. The general case is not provable in PA. So, in higher order logic, the proof is of same length for every n. In PA the proof length grows when n becomes larger.

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

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

Answer by Richard Borcherds for Are any natural examples of Gödel speed-up known?

Answer by Lucas K. for Are any natural examples of Gödel speed-up known?