Constructing Kripke Models of Certain Fragments of Heyting's Arithmetic


Kai_F. Wehmeier


We present nontrivial methods of constructing Kripke models for the fragments of HA obtained by restricting the induction schema to instances with ${\varPi}_1$- and ${\varPi}_2$-induction formulae respectively. The model construction for ${\varPi}_1$-induction was applied in [W96a] and [W97] to investigate the provably recursive functions of this theory. The construction of ${\varPi}_2$-induction models is a modification of Smorynski's collection operation introduced in [S73].