4
$\begingroup$

Let $\mathsf{EA}+\mathsf{CE}$ be elementary arithmetic with cut elimination theorem. Is there a simple (1-)consistency proof of $\mathsf{EA}$ over $\mathsf{EA}+\mathsf{CE}$? I think that a naïve consistency proof of $\mathsf{EA}$ fails because an evaluation function of terms of $\mathsf{EA}$ is not elementary recursive. Of course, $\mathsf{CE}$ implies totality of a superexponential function (by a theorem of Statman, Orevkov, and Pudlák). Hence, my question is: is there a (1-)consistency proof of $\mathsf{EA}$ over $\mathsf{EA}+\mathsf{CE}$ without proving totality of superexponential function?

$\endgroup$
3
  • $\begingroup$ An axiomatization of $I\Delta_0+\mathsf{exp}$ in the basic language of arithmetic includes a formula expressing totality of exponential which is $\Pi_2$-formula. I don't know how to prove a consistency of $\Pi_2$-formula with using cut elimination for usual sequent calculus. $\endgroup$
    – Alwe
    Jan 31, 2022 at 17:54
  • 1
    $\begingroup$ We could reason as follows. Paris-Wilkie theorem states that for any $\Delta_0$-formula $F(x,y)$ if $\mathsf{EA}\vdash \forall x\exists y F(x,y)$, then there is a $\mathsf{Q}$-cut $I$ s.t. $\mathsf{Q}\vdash \forall x\in I\exists y F(x,y)$. This could be proved using $\mathsf{CE}$ in $\mathsf{EA+CE}$. Thus provably in $\mathsf{EA+CE}$, for $\Sigma_1$-sentences $F$ we have $\mathsf{EA}\vdash F\Rightarrow \mathsf{Q}\vdash F$. By giving an exponential upper bound we prove in $\mathsf{EA}$ cut-free $\Sigma_1$-soundness of $\mathsf{Q}$. Combining all of this we get $1$-consistency of $\mathsf{EA}$. $\endgroup$ Feb 2, 2022 at 16:45
  • $\begingroup$ @FedorPakhomov It's nice proof. I would like to make your proof into an answer of my question. Please repost your comment as an answer, if you would like. $\endgroup$
    – Alwe
    Feb 3, 2022 at 14:27

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.