Forcing and satisfaction in Kripke models of intuitionistic arithmetic

Logic Journal of the IGPL 27 (5):659-670 (2019)
  Copy   BIBTEX


We define a class of first-order formulas $\mathsf{P}^{\ast }$ which exactly contains formulas $\varphi$ such that satisfaction of $\varphi$ in any classical structure attached to a node of a Kripke model of intuitionistic predicate logic deciding atomic formulas implies its forcing in that node. We also define a class of $\mathsf{E}$-formulas with the property that their forcing coincides with their classical satisfiability in Kripke models which decide atomic formulas. We also prove that any formula with this property is an $\mathsf{E}$-formula. Kripke models of intuitionistic arithmetical theories usually have this property. As a consequence, we prove a new conservativity result for Peano arithmetic over Heyting arithmetic.



    Upload a copy of this work     Papers currently archived: 76,363

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

Homomorphisms and chains of Kripke models.Morteza Moniri & Mostafa Zaare - 2011 - Archive for Mathematical Logic 50 (3-4):431-443.
Weak Arithmetics and Kripke Models.Morteza Moniri - 2002 - Mathematical Logic Quarterly 48 (1):157-160.
Submodels of Kripke models.Albert Visser - 2001 - Archive for Mathematical Logic 40 (4):277-295.
Classical and Intuitionistic Models of Arithmetic.Kai F. Wehmeier - 1996 - Notre Dame Journal of Formal Logic 37 (3):452-461.
Preservation theorems for Kripke models.Morteza Moniri & Mostafa Zaare - 2009 - Mathematical Logic Quarterly 55 (2):177-184.
On the structure of kripke models of heyting arithmetic.Zoran Marković - 1993 - Mathematical Logic Quarterly 39 (1):531-538.
Intuitionistic weak arithmetic.Morteza Moniri - 2003 - Archive for Mathematical Logic 42 (8):791-796.
Models of intuitionistic TT and N.Daniel Dzierzgowski - 1995 - Journal of Symbolic Logic 60 (2):640-653.
Preservation theorems for bounded formulas.Morteza Moniri - 2007 - Archive for Mathematical Logic 46 (1):9-14.
A Semantic Approach to Conservativity.Tomasz Połacik - 2016 - Studia Logica 104 (2):235-248.


Added to PP

5 (#1,170,023)

6 months
1 (#451,398)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

No citations found.

Add more citations

References found in this work

Logic and Structure.Melvin Fitting - 1986 - Journal of Symbolic Logic 51 (3):826-827.
Intuitionistic validity in T-normal Kripke structures.Samuel R. Buss - 1993 - Annals of Pure and Applied Logic 59 (3):159-173.

Add more references