Skip to main content
added 180 characters in body
Source Link
Emil Jeřábek
  • 47.6k
  • 4
  • 150
  • 209

You didn’t specify what you mean by “complexity”. If one interprets it as the number of lines in the proof, this is a famous conjecture of Kreisel (usually stated contrapositively: if there is a constant $c$ such that $\phi(\overline n)$ has a PA proof with at most $c$ lines for all $n$, then PA proves $\forall x\,\phi(x)$).

Kreisel’s conjecture is still open for the most natural formulation of PA, however it is extremely sensitive to the choice of the language, and various variants of it have been proved and disproved. See Hrubeš for a recent paper in the positive direction, where you can also find pointers to other known results related to the conjecture.

You didn’t specify what you mean by “complexity”. If one interprets it as the number of lines in the proof, this is a famous conjecture of Kreisel (usually stated contrapositively: if there is a constant $c$ such that $\phi(\overline n)$ has a PA proof with at most $c$ lines for all $n$, then PA proves $\forall x\,\phi(x)$).

Kreisel’s conjecture is still open for the most natural formulation of PA, however it is extremely sensitive to the choice of the language, and various variants of it have been proved and disproved.

You didn’t specify what you mean by “complexity”. If one interprets it as the number of lines in the proof, this is a famous conjecture of Kreisel (usually stated contrapositively: if there is a constant $c$ such that $\phi(\overline n)$ has a PA proof with at most $c$ lines for all $n$, then PA proves $\forall x\,\phi(x)$).

Kreisel’s conjecture is still open for the most natural formulation of PA, however it is extremely sensitive to the choice of the language, and various variants of it have been proved and disproved. See Hrubeš for a recent paper in the positive direction, where you can also find pointers to other known results related to the conjecture.

Source Link
Emil Jeřábek
  • 47.6k
  • 4
  • 150
  • 209

You didn’t specify what you mean by “complexity”. If one interprets it as the number of lines in the proof, this is a famous conjecture of Kreisel (usually stated contrapositively: if there is a constant $c$ such that $\phi(\overline n)$ has a PA proof with at most $c$ lines for all $n$, then PA proves $\forall x\,\phi(x)$).

Kreisel’s conjecture is still open for the most natural formulation of PA, however it is extremely sensitive to the choice of the language, and various variants of it have been proved and disproved.