HIGHER-LEVEL SEQUENT-SYSTEMS FOR INTUITIONISTIC MODAL LOGIC

Kosta Dosen

Abstract: This paper presents higher-level sequent-systems for intuitionistic analogues of $S5$ and $S4$. As in [3] rules for modal constants involve sequents of level 2, i.e., sequents having collections of ordinary sequents of level 1 on the left and right of the turnstile. Starting from a canonical higher-level sequent formulation of $S5$, the restriction of sequents of level 2 to those with the single-conclusion property produces $S4$, without changing anything else. A similar restriction on sequents of level 1 produces Heyting $S5$, and if this restriction is made on sequents of both level 1 and 2, we obtain Heyting $S4$. The paper contains a brief discussion of Kripke-style models for the intuitionistic propositional modal logics in question.

Classification (MSC2000): 03B45

Full text of the article:

• Compressed PostScript file (66 kilobytes)
• PDF file (177 kilobytes)