Intuitionistic axiomatizations for bounded extension Kripke models

We present axiom systems, and provide soundness and strong completeness theorems, for classes of Kripke models with restricted extension rules among the node structures of the model. As examples we present an axiom system for the class of cofinal extension Kripke models, and an axiom system for the class of end-extension Kripke models. We also show that Heyting arithmetic (HA) is strongly complete for its class of end-extension models. Cofinal extension models of HA are models of Peano arithmetic (PA). (C) 2003 Elsevier B.V. All rights reserved.