Title: Hypersequent calculi for intuitionistic logic with classical atoms
Abstract: We discuss a propositional logic which combines classical reasoning with constructive reasoning, i.e., intuitionistic logic augmented with a class of propositional variables for which we postulate the decidability property. We call it intuitionistic logic with classical atoms. We introduce two hypersequent calculi for this logic. Our main results presented here are cut-elimination with the subformula property for the calculi. As corollaries, we show decidability, an extended form of the disjunction property, the existence of embedding into an intuitionistic modal logic and a partial form of interpolation.
Publication Year: 2009
Publication Date: 2009-12-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 9
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot