Title: Axiomatizations of intuitionistic double negation
Abstract: We investigate intuitionistic propositional modal logics in which a modal operator is equivalent to intuitionistic double negation. Whereas ¬¬ is divisible into two negations, is a single indivisible operator. We shall first consider an axiomatization of the Heyting propositional calculus H, with the connectives →,∧,∨ and ¬, extended with . This system will be called Hdn (“dn” stands for “double negation”). Next, we shall consider an axiomatization of the fragment of H without ¬ extended with . This system will be called Hdn. We shall show that these systems are sound and complete with respect to specific classes of Kripke-style models with two accessibility relations, one intuitionistic and the other modal. This type of models is investigated in [2] and [3], and here we try to apply the techniques of these papers to an intuitionistic modal operator with a natural interpretation. The full results of our investigation will be published in [4] and [1].
Publication Year: 1983
Publication Date: 1983-01-01
Language: en
Type: article
Access and Citation
Cited By Count: 4
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot