The Kreisel conjecture is a conjecture in proof theory that postulates that, if is a formula in the language of arithmetic for which
there exists a nonnegative integer such that, for every nonnegative integer , Peano arithmetic proves
in at most
steps, then Peano arithmetic proves its universal
closure, .
A special case of the conjecture was proven true by
M. Baaz in 1988 (Baaz and Pudlák 1993).
Baaz, M. and Pudlák P. "Kreisel's Conjecture for ."
In Arithmetic,
Proof Theory, and Computational Complexity, Papers from the Conference Held in Prague,
July 2-5, 1991 (Ed. P. Clote and J. Krajiček). New York: Oxford
University Press, pp. 30-60, 1993.Dawson, J. "The Gödel
Incompleteness Theorem from a Length of Proof Perspective." Amer. Math. Monthly86,
740-747, 1979.Kreisel, G. "On the Interpretation of Nonfinitistic
Proofs, II." J. Sym. Logic17, 43-58, 1952.Santos,
P. G. and Kahle, R. "Variants of Kreisel's Conjecture on a New Notion of
Provability." Bull. Sym. Logic24, 337-350, 2021.