Kripke submodels and universal sentences

Mathematical Logic Quarterly 53 (3):311-320 (2007)
  Copy   BIBTEX


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 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 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 universal fragment of a theory Γ is contained in the universal fragment of a theory Δ if and only if every rooted Kripke model of Δ is strongly equivalent to a submodel of a rooted Kripke model of Γ. Our notions of Kripke submodel and universal sentence are natural in the sense that in the presence of the rule of excluded middle, they collapse to the classical notions of submodel and universal sentence



    Upload a copy of this work     Papers currently archived: 93,031

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Preservation theorems for Kripke models.Morteza Moniri & Mostafa Zaare - 2009 - Mathematical Logic Quarterly 55 (2):177-184.
Homomorphisms and chains of Kripke models.Morteza Moniri & Mostafa Zaare - 2011 - Archive for Mathematical Logic 50 (3-4):431-443.
Syntactic Preservation Theorems for Intuitionistic Predicate Logic.Jonathan Fleischmann - 2010 - Notre Dame Journal of Formal Logic 51 (2):225-245.
Submodels of Kripke models.Albert Visser - 2001 - Archive for Mathematical Logic 40 (4):277-295.
On the structure of kripke models of heyting arithmetic.Zoran Marković - 1993 - Mathematical Logic Quarterly 39 (1):531-538.
Diagram Construction in Intuitionistic Logic.Seyed Bagheri & Massoud Pourmahdian - 2006 - Logic Journal of the IGPL 14 (6):889-901.
Decidable Kripke models of intuitionistic theories.Hajime Ishihara, Bakhadyr Khoussainov & Anil Nerode - 1998 - Annals of Pure and Applied Logic 93 (1-3):115-123.


Added to PP

25 (#653,738)

6 months
10 (#309,337)

Historical graph of downloads
How can I increase my downloads?

References found in this work

No references found.

Add more references