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 can get much shorter proofs in a formal system . 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 such that the formal system for Peano Arithmetic proves in steps for every , then proves . The idea behind the conjecture is that a short proof of an instance of for large cannot use the whole information about the numeral for 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 such that has an unbounded speed-up over but is still conservative extension of .
is a corollary of KC but we also give a proof not using any unproven