We define classes Φn of formulae of first-order arithmetic with the following properties:
(i) Every φ ϵ Φn is classically equivalent to a Πn-formula (n ≠ 1, Φ1 := Σ1).
(ii) ![](//static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20151027053009061-0882:S0022481200011890_inline1.gif?pub-status=live)
(iii) IΠn and iΦn (i.e., Heyting arithmetic with induction schema restricted to Φn-formulae) prove the same Π2-formulae.
We further generalize a result by Visser and Wehmeier. namely that prenex induction within intuitionistic arithmetic is rather weak: After closing Φn both under existential and universal quantification (we call these classes Θn) the corresponding theories iΘn still prove the same Π2-formulae. In a second part we consider iΔ0 plus collection-principles. We show that both the provably recursive functions and the provably total functions of
are polynomially bounded. Furthermore we show that the contrapositive of the collection-schema gives rise to instances of the law of excluded middle and hence
.