PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.)
Vol. 39(53), pp. 3--12 (1986)
HIGHER-LEVEL SEQUENT-SYSTEMS FOR INTUITIONISTIC MODAL LOGIC
Kosta DosenMatematicki institut SANU, Beograd, Yugoslavia
Abstract: This paper presents higher-level sequent-systems for intuitionistic analogues of $S5$ and $S4$. As in  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:
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