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

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.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1093/jigpal/jzy075
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 53,688
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

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

Citations of this work BETA

No citations found.

Add more citations

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 index

Total views
4 ( #1,184,903 of 2,349,560 )

Recent downloads (6 months)
1 ( #510,673 of 2,349,560 )

How can I increase my downloads?


My notes