TOPICS
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).
Portions of this entry contributed by Lorenzo Sauras-Altuzarra
."
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. Monthly 86,
740-747, 1979.Kreisel, G. "On the Interpretation of Nonfinitistic
Proofs, II." J. Sym. Logic 17, 43-58, 1952.Santos,
P. G. and Kahle, R. "Variants of Kreisel's Conjecture on a New Notion of
Provability." Bull. Sym. Logic 24, 337-350, 2021.Sauras-Altuzarra, Lorenzo and Weisstein, Eric W. "Kreisel Conjecture." From MathWorld--A Wolfram Web Resource. https://mathworld.wolfram.com/KreiselConjecture.html