NNIL, A study in intuitionistic propositional logic

In this paper we study NNIL, the class of formulas of the Intuitionistic Propositional Calculus. IPC with no nestings of implications to the left. We show that the formulas of this class are precisely the formulas of the language of IPC that are preserved under taking submodels of Kripke models for IPC (for various notions of submodel). This makes NNIL an analogue of the purely universal formulas in Predicate Logic. We prove a number of interpolation properties for NNIL, and explore the extent to which these properties can be generalized to more complicated classes of formulas