Speed-up theorem and Kreisel's Conjecture

Stefano Cavagnetto

Czech Academy of Sciences, Prague
stefanoc@math.cas.cz

Gödel in 1936 announced a speed-up theorem (GST) that holds when one switches from a weaker formal system for arithmetic to a stronger one. Theorems with long proofs in a formal system $T$ can get much shorter proofs in a formal system $S$. Gödel did not give a proof of his result but subsequently proofs were given by Parikh, by Krajicek and in a general version by Buss. Kreisel's Conjecture (KC) is an open problem in the study of lengths of proofs. KC states in the following way: If there exists $k$ such that the formal system for Peano Arithmetic $PA$ proves $A(s^{(n)}(0))$ in $k$ steps for every $n$, then $PA$ proves $(\forall x) A(x)$. The idea behind the conjecture is that a short proof of an instance $A(s^{(n)}(0))$ of $A(x)$ for large $n$ cannot use the whole information about the numeral for $n$ and thus should generalize to other numbers too.

We briefly recapitulate some basic fact about KC, GST and we show that the following proposition

Proposition: There exists a formal system $T$ such that $T$ has an unbounded speed-up over $PA$ but is still conservative extension of $PA$.

is a corollary of KC but we also give a proof not using any unproven assumption.