27
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • $\begingroup$ 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]. $\endgroup$
    – Ali Enayat
    May 18, 2011 at 20:58
  • $\begingroup$ There is always estatis.coders.fm/falso $\endgroup$
    – Justin Hilburn
    May 19, 2011 at 7:04

2 Answers 2

Reset to default
17
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 3
    $\begingroup$ 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. $\endgroup$
    – Ali Enayat
    May 18, 2011 at 20:58
4
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • 6
    $\begingroup$ 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? $\endgroup$
    – Joel David Hamkins
    May 18, 2011 at 12:30
  • $\begingroup$ @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. $\endgroup$
    – Daniel Litt
    May 19, 2011 at 5:36
  • 1
    $\begingroup$ @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. $\endgroup$
    – Andrés E. Caicedo
    May 19, 2011 at 6:10
  • $\begingroup$ If the length of the proof grows slower than n itself, I think this can be fixed, by first feeding the 'n' to a fast growing function. So, we get Goodstein(f(n)). For f(n), we can take Goodstein. $\endgroup$
    – Lucas K.
    May 19, 2011 at 7:52
  • 1
    $\begingroup$ 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.) $\endgroup$
    – Joel David Hamkins
    May 19, 2011 at 10:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.