Problem #11

Kreisel's Conjecture

Open!

Let $\mathsf{PA}$ be Peano Arithmetic in the language with function symbols for successor, plus, and times, which is axiomatized with the successor induction schema and identity axioms. Suppose that $\varphi(x)$ is a formula such that, for some $k\in\mathbb{N}$ , $\varphi(\bar{n})$ has a Gentzen-style proof of length $\leq k$ for each $n\in\mathbb{N}$ . Does it follow that $\mathsf{PA}\vdash\forall x \varphi(x)$ ?

Proof Theory

Suggest an edit

Known Partial Results

The conjecture is true in the signature with function symbols for successor but ternary predicates for addition and multiplication (Parikh [Par73]).

The conjecture is true in the signature with function symbols for successor and addition but a ternary predicate for multiplication (Miyatake).

The conjecture is false if the signature is enriched with a function symbol for subtraction (Hrubeš).

The conjecture is true if $\mathsf{PA}$ is axiomatized with the least-number principle instead of successor induction (Hrubeš).

Reference for the problem statement

[AP24]Aguilera JP and Pakhomov F, Modern Perspectives in Proof Theory, Phil. Trans. R. Soc. A, 2024 [link] [doi]

Additional References

[Par73]Parikh, Rohit J., Some results on the length of proofs, Transactions of the American Mathematical Society, 1973

[BP93]Baaz, Matthias, and Pavel Pudlák, Kreisel's conjecture for L∃ 1, Arithmetic, proof theory and computational complexity, 1993

[Hru07]Hrubeš, Pavel, Theories very close to PA where Kreisel's Conjecture is false, The Journal of Symbolic Logic, 2007

[BW08]Baaz, Matthias, and Piotr Wojtylak, Generalizing proofs in monadic languages, Annals of Pure and Applied Logic, 2008

[Hru09]Hrubeš, Pavel, Kreisel's Conjecture with minimality principle, The Journal of Symbolic Logic, 2009

[SK21]Santos, Paulo Guilherme, and Reinhard Kahle, Variants of Kreisel's conjecture on a new notion of provability, Bulletin of Symbolic Logic, 2021

Comments

Loading comments…