arXiv · math/0409070
First-Order Intuitionistic Logic with Decidable Propositional Atoms
Abstract
Intuitionistic logic extended with decidable propositional atoms combines classical properties in its propositional part and intuitionistic properties for derivable formulas not containing propositional symbols. Sequent calculus is used as a framework for investigating this extension. Admissibility of cut is retained. Constrained Kripke structures are introduced for modeling intuitionistic logic with decidable propositional atoms. The extent of the disjunction and existence properties is investigated. The latest information about this research can be found at http://sakharov.net/median.html
Explore related subjects
Keep this discovery
Alexander Sakharov. 2005-05-08. First-Order Intuitionistic Logic with Decidable Propositional Atoms. https://arxiv.org/abs/math/0409070
Cite the original work for its findings. Save a collection to share your selection of sources.