Intuitionistic axiomatizations for bounded extension Kripke models. (Q1412839)

In this paper some particular sets of formulas, or axiom systems, are introduced by means of syntactical closure conditions, and any extension of intuitionistic logic by such an axiom system is proved to be strongly complete with respect to a class of Kripke models defined suitably according to the axiom system. The classes of Kripke models thus characterized cover several interesting special cases such as cofinal extension models, G-expansion models, and end-extension models, where a G-expansion model with the falsehood G, for example, means a constant domain model. As applications, therefore, the authors obtain strongly complete axiomatizations for the extensions of intuitionistic logic characterized by these classes of Kripke models respectively. Moreover, the authors discuss applications to Heyting arithmetic HA as well, among which it is proved, for instance, that HA is strongly complete for its class of end-extension Kripke models, and cofinal extension models of HA are models of Peano arithmetic.