Let T be a first-order theory. A T-normal Kripke structure is one in which every world is a classical model of T. This paper gives a characterization of the intuitionistic theory T of sentences intuitionistically valid in all T-normal Kripke structures and proves the corresponding soundness and completeness theorems. For Peano arithmetic , the theory PA is a proper subtheory of Heyting arithmetic , so HA is complete but not sound for PA-normal Kripke structures.

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 (this is established by different means also in [D94]). 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 arithmetical 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 concerned: 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 ${\Bbb N}$ . 0 $iI\!\Pi_1$ is unusual also in that it lacks closure under Markov's Rule $\mbox{MR}_{PR}$. (shrink)

The author proved in his Ph.D. Thesis [W. Veldman, Investigations in intuitionistic hierarchy theory, Ph.D. Thesis, Katholieke Universiteit Nijmegen, 1981] that, in intuitionistic analysis, the positively Borel subsets of Baire space form a genuinely growing hierarchy: every level of the hierarchy contains sets that do not occur at any lower level. It follows from this result that there are natural examples of analytic and also of co-analytic sets that are not positively Borel. It turns out, however, that, in intuitionistic analysis, (...) one may give surprisingly different and, in some sense, much more simple examples of analytic and co-analytic sets that fail to be positively Borel. In the paper, two such examples are given. In proving them correct, one obtains new proofs of the Borel Hierarchy Theorem. Brouwer’s Continuity Principle plays a crucial role in arguments. (shrink)