Skip to main content
correct typo
Link
Alwe
  • 178
  • 6

Is there a simple proof of a consistency of EA?

Source Link
Alwe
  • 178
  • 6

Is there a simple proof of a consistency of EA?

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?