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?
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$– AlweCommented 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$– Fedor PakhomovCommented 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$– AlweCommented Feb 3, 2022 at 14:27
Add a comment
|