Kreisel’s conjecture
For every formula in the language of Peano arithmetic formalized as in Kleene, if there exists a bound such that, for every , the numeral instance has a proof in this theory of length at most , then the universal closure is provable: . Equivalently, is a proof of .
References
Primary source
Additional references
- A finite algebraic target theorem for Kreisel’s conjecture — Archive for Mathematical Logic — Mario Piazza
Progress summary
A new paper gives a finite algebraic test relevant to the conjecture, but does not prove or disprove it.
Kreisel’s conjecture concerns the passage from bounded numeral-instance proofs to a universal closure. Historical literature records a proof by Tait with a gap later identified by Gandy, who supplied a corrected proof in a letter to Kreisel.
September 2026 algebraic criterion
Mario Piazza’s paper gives an exact finite criterion for factoring an idempotent-power map through a finite semilattice, bounded witnesses for one obstruction, and an effectively ultimately periodic realization framework. It clarifies why Parikh’s formulation needs arithmetic realization profiles, not continuation behavior alone. This is claimed progress, not a complete proof or disproof.
Current status (as of September 2026): A recent paper claims a finite algebraic and proof-analytic advance, but the supplied evidence does not establish a complete proof or disproof of Kreisel’s conjecture.
Solutions 0
No solutions have been posted yet.