Partially-elementary extension Kripke models and Burr's hierarchy

Abstract

We investigate Kripke models of subtheories /'k,, of Heyting Arithmetic. The theories Al*,,, defined by W. Burr, can be regarded as the natural intuitionistic counterparts of subtheories Inn of Peano Arithmetic. In the paper we consider n-elementary extension Kripke models which are models whose worlds are ordered by the elementary extension relation with respect to A„ formulae instead of merely the (weak) submodel relation. We prove that every Inn-normal, n-elementary extension model is a model of /'k,,. This suggests a method of constructing non-trivial Kripke models of /'k„. We also show that every (n + 1)- elementary extension model of /'k„ is Inn-normal.