Skip to main content
added 105 characters in body
Source Link
Noah Schweber
  • 20.5k
  • 10
  • 110
  • 331

Yes, Gentzen found a single "induction instance" which is PA-unprovable: more-or-less $\varphi(\alpha)$ = "Every sentence with a proof of cut-rank $\alpha$ has a cut-free proof."

Now, this $\varphi$ is a $\Pi^0_2$ formula. If memory serves, this is suboptimal: with some coding work this can be improved from a $\Pi^0_2$ formula to a $\Sigma^0_1$ formula. The basic idea is to assign in a primitive recursive way to each ordinal $\alpha<\epsilon_0$ a sentence $p_\alpha$ and a candidate proof $s_\alpha$ of cut rank $<\alpha$ such that each pair occurs cofinally often, and then look at the formula $\psi(\alpha)$ = "Either $s_\alpha$ is not a proof of $p_\alpha$ or there is a cut free proof of $p_\alpha$."

And I think even that's suboptimal - that we can get to the level of $\Delta_0$ - but I'm not sure.

Yes, Gentzen found a single "induction instance" which is PA-unprovable: more-or-less $\varphi(\alpha)$ = "Every sentence with a proof of cut-rank $\alpha$ has a cut-free proof."

Now, this $\varphi$ is a $\Pi^0_2$ formula. If memory serves, this is suboptimal: with some coding work this can be improved from a $\Pi^0_2$ formula to a $\Sigma^0_1$ formula. The basic idea is to assign in a primitive recursive way to each ordinal $\alpha<\epsilon_0$ a sentence $p_\alpha$ and a candidate proof $s_\alpha$ of cut rank $<\alpha$ such that each pair occurs cofinally often, and then look at the formula $\psi(\alpha)$ = "Either $s_\alpha$ is not a proof of $p_\alpha$ or there is a cut free proof of $p_\alpha$."

Yes, Gentzen found a single "induction instance" which is PA-unprovable: more-or-less $\varphi(\alpha)$ = "Every sentence with a proof of cut-rank $\alpha$ has a cut-free proof."

Now, this $\varphi$ is a $\Pi^0_2$ formula. If memory serves, this is suboptimal: with some coding work this can be improved from a $\Pi^0_2$ formula to a $\Sigma^0_1$ formula. The basic idea is to assign in a primitive recursive way to each ordinal $\alpha<\epsilon_0$ a sentence $p_\alpha$ and a candidate proof $s_\alpha$ of cut rank $<\alpha$ such that each pair occurs cofinally often, and then look at the formula $\psi(\alpha)$ = "Either $s_\alpha$ is not a proof of $p_\alpha$ or there is a cut free proof of $p_\alpha$."

And I think even that's suboptimal - that we can get to the level of $\Delta_0$ - but I'm not sure.

Source Link
Noah Schweber
  • 20.5k
  • 10
  • 110
  • 331

Yes, Gentzen found a single "induction instance" which is PA-unprovable: more-or-less $\varphi(\alpha)$ = "Every sentence with a proof of cut-rank $\alpha$ has a cut-free proof."

Now, this $\varphi$ is a $\Pi^0_2$ formula. If memory serves, this is suboptimal: with some coding work this can be improved from a $\Pi^0_2$ formula to a $\Sigma^0_1$ formula. The basic idea is to assign in a primitive recursive way to each ordinal $\alpha<\epsilon_0$ a sentence $p_\alpha$ and a candidate proof $s_\alpha$ of cut rank $<\alpha$ such that each pair occurs cofinally often, and then look at the formula $\psi(\alpha)$ = "Either $s_\alpha$ is not a proof of $p_\alpha$ or there is a cut free proof of $p_\alpha$."