Fragments of HA based on \(\Sigma_ 1\)-induction (Q1920237)

In the first part of this paper we investigate the intuitionistic version \(iI\Sigma_1\) of \(I\Sigma_1\) (in the language of PRA), using Kleene's recursive realizability techniques. Our treatment closely parallels the usual one for HA and establishes a number of nice properties for \(iI\Sigma_1\), e.g. existence of primitive recursive choice functions. We then sharpen an unpublished theorem of Visser's to the effect that quantifier alternation alone is much less powerful intuitionistically than classically: \(iI \Sigma_1\) together with induction over arbitrary prenex formulas is \(\Pi_2\)-conservative over \(iI \Pi_2\). In the second part of the article we study the relation of \(iI \Sigma_1\) to \(iI \Pi_1\) (in the usual arithmetic language). The situation here is markedly different from the classical case in that \(iI \Pi_1\) and \(iI \Sigma_1\) are mutually incomparable, while \(iI \Sigma_1\) is significantly stronger than \(iI \Pi_1\) as far as provably recursive functions are considered: All primitive recursive functions can be proved total in \(iI \Sigma_1\) whereas the provably recursive functions of \(iI \Pi_1\) are all majorized by polynomials over \(\mathbb{N}\). \(iI \Pi_1\) is unusual also in that it lacks closure under Markov's Rule \(\text{MR}_{PR}\).