Intuitionistic Open Induction and Least Number Principle and the Buss Operator
Mohammad Ardeshir, Mojtaba Moniri · Notre Dame Journal of Formal Logic · 1998
In "Intuitionistic validity in $T$-normal Kripke structures," Buss asked whether every intuitionistic theory is, for some classical theory $T$, that of all $T$-normal Kripke structures ${\cal H}(T)$ for which he gave an r.e. axiomatization. In the language of arithmetic $\mathit{Iop}$ and $\mathit{Lop}$ denote PA$^{-}$ plus Open Induction or Open LNP, $\mathit{iop}$ and $\mathit{lop}$ are their intuitionistic deductive closures. We show $\mathcal{H}\mathit{(Iop)}$ $=\mathit{lop}$ is recursively axiomatizable and $\mathit{lop}\vdash_{i\ c}\dashv \mathit{iop}$, while $i\forall_{1} ot\vdash \mathit{lop}$. If $iT$ proves PEM $_{\mathrm{atomic}}$ but not totality of a classically provably total Diophantine function of $T$, then $\mathcal{H}(T) ot\subseteq iT$ and so $iT ot\in \mathrm{range({\cal H})}$. A result due to Wehmeier then implies $i\Pi_{1} ot\in\mbox{range}({\cal H})$. We prove $\mathit{Iop}$ is not $\forall_{2}$-conservative over $i\forall_{1}$. If $\mathit{Iop}\subseteq T\subseteq I\forall_{1}$, then $iT$ is not closed under MR $_{\mathrm{open}}$ or Friedman's translation, so $iT ot\in$ range (${\cal H}$). Both $\mathit{Iop}$ and $I\forall_{1}$ are closed under the negative translation.