Gaps between intutionistic and classical arithmetic

58 Views Asked by At

Let $\mathrm{I}\Sigma_n$ stand for the classical theory of Robinson arithmetic + bounded induction + induction on $\Sigma_n$ formulas. Let $\mathrm{CI}\Sigma_n$ stand for the intuitionistic theory of the same axioms and finally also assume that all axioms of Robinson arithmetic are given in a constructively viable form.

Then, is there any $n$ and any formula $\varphi$ such that $$ \mathrm{I}\Sigma_{n-1} \not\vdash \varphi, \\ \mathrm{I}\Sigma_n \vdash \varphi, \\ \mathrm{CI}\Sigma_n \not\vdash \varphi, \\ \mathrm{CI}\Sigma_{n+1} \vdash \varphi? $$ The first condition is required to make the question nontrivial, otherwise, $\varphi \vee \neg \varphi$ for $\varphi$ provable in $\mathrm{CI}\Sigma_{n+1}$ but not in $\mathrm{CI}\Sigma_{n}$ would be an example.