Are any natural examples of Gödel speed-up known? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-20T20:30:28Z http://mathoverflow.net/feeds/question/65282 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/65282/are-any-natural-examples-of-godel-speed-up-known Are any natural examples of Gödel speed-up known? John Stillwell 2011-05-18T00:53:45Z 2011-05-19T05:27:16Z <p>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)$.</p> <p>Various versions of this theorem have been proved, depending on the strengthening of PA chosen, and on the definition of length. See, in particular, <a href="http://math.ucsd.edu/~sbuss/ResearchWeb/godelone/index.html" rel="nofollow">this paper</a>. However, I have not found a version with a <em>natural</em> sequence of theorems $T_k$. For example, it seems plausible that one could use <a href="http://en.wikipedia.org/wiki/Goodstein%27s_theorem" rel="nofollow">Goodstein's theorem</a>, by taking</p> <p>$T_k$ = The Goodstein process, starting with input $k$, eventually halts.</p> <p>Are any such "natural'' examples of Gödel speed-up known?</p> <p><strong>Update and clarification.</strong> 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$.</p> <p>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</p> <p>$g(k)$ = length of the shortest proof of $T_k$ in PA</p> <p>is computable, so we cannot ask $f$ to grow faster then $g$.</p> <p>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 <em>Harvey Friedman's Research on the Foundations of Mathematics</em> (North-Holland 1985),<br> and some other works, without finding a clear statement of speed-up in the above sense.</p> http://mathoverflow.net/questions/65282/are-any-natural-examples-of-godel-speed-up-known/65291#65291 Answer by Richard Borcherds for Are any natural examples of Gödel speed-up known? Richard Borcherds 2011-05-18T04:16:23Z 2011-05-18T04:16:23Z <p>Friedman has given many examples of such speedups. One well known one is his finite version of <a href="http://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem" rel="nofollow">Kruskal's tree theorem</a>. 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. </p> http://mathoverflow.net/questions/65282/are-any-natural-examples-of-godel-speed-up-known/65316#65316 Answer by Lucas K. for Are any natural examples of Gödel speed-up known? Lucas K. 2011-05-18T11:11:45Z 2011-05-18T11:11:45Z <p>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.</p>