Given a classical theory T, a Kripke model K for the language L of T is called T-normal or locally PA just in case the classical L-structure attached to each node of K is a classical model of T. Van Dalen, Mulder, Krabbe, and Visser showed that Kripke models of Heyting Arithmetic (HA) over finite frames are locally PA, and that Kripke models of HA over frames ordered like the natural numbers contain infinitely many PA-nodes. We show that Kripke models (...) of the latter sort are in fact PA-normal. This result is extended to a somewhat larger class of frames. (shrink)

We consider Kripke semantics for intuitionistic arithmetic and ask ourselves whether an induction schema which is true in a world of a given model $\K$ is also forced at the corresponding node of $\K$.Mathematics Subject Classification: 03F50, 03F30, 03C90.

We define classes Φnof formulae of first-order arithmetic with the following properties:(i) Everyφϵ Φnis classically equivalent to a Πn-formula (n≠ 1, Φ1:= Σ1).(ii)(iii)IΠnandiΦ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 Φnboth under existential and universal quantification (we call these classes Θn) the corresponding theoriesiΘnstill prove the same Π2-formulae. In a second part we consideriΔ0plus collection-principles. We (...) show that both the provably recursive functions and the provably total functions ofare polynomially bounded. Furthermore we show that the contrapositive of the collection-schema gives rise to instances of the law of excluded middle and hence. (shrink)