Stefano Cavagnetto
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
assumption.