PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.) Vol. 39(53), pp. 312 (1986) 

HIGHERLEVEL SEQUENTSYSTEMS FOR INTUITIONISTIC MODAL LOGICKosta DosenMatematicki institut SANU, Beograd, YugoslaviaAbstract: This paper presents higherlevel sequentsystems 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 higherlevel sequent formulation of $S5$, the restriction of sequents of level 2 to those with the singleconclusion 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 Kripkestyle models for the intuitionistic propositional modal logics in question. Classification (MSC2000): 03B45 Full text of the article:
Electronic fulltext finalized on: 2 Nov 2001. This page was last modified: 16 Nov 2001.
© 2001 Mathematical Institute of the Serbian Academy of Science and Arts
