Kripke submodels and universal sentences

We define two notions for intuitionistic predicate logic: that of a submodel of a Kripke model, and that of a universal sentence. We then prove a corresponding preservation theorem. If a Kripke model is viewed as a functor from a small category to the category of all classical models with (homo)morphisms between them, then we define a submodel of a Kripke model to be a restriction of the original Kripke model to a subcategory of its domain where every node in the subcategory is mapped to a classical submodel of the corresponding classical model in the range of the original Kripke model. We call a sentence universal if it is built inductively from atoms (including ⊤ and ⊥) using ∧, ∨, ∀, and →, with the restriction that antecedents of → must be atomic. We prove that an intuitionistic theory is axiomatized by universal sentences if and only if it is preserved under Kripke submodels. We also prove the following analogue of a classical model-consistency theorem: The univer...

• Type: Journal
• Year: 2007
• Where: MLQ
• Authors: Ben Ellison, Jonathan Fleischmann, Dan McGinn, Wim Ruitenburg
• Keywords: Kripke Model, MLQ 2007, Original Kripke Model, Universal Sentence