On Some Syntactic Properties of the Modalized Heyting Calculus

Other literature type, Preprint English OPEN
Muravitsky, Alexei;
  • Publisher: Cornell University
  • Identifiers: doi: 10.13140/rg.2.2.35315.53281
  • Subject: Mathematics - Logic | 03B45
    arxiv: Computer Science::Logic in Computer Science | Mathematics::Logic

We show that the modalized Heyting calculus introduced by Leo Esakia admits a normal axiomatization. Then, we prove that the inference rules $\square\alpha/\alpha$ and $\square\alpha\rightarrow\alpha/\alpha$ are admissible in this calculus. Finally, we show that this ca... View more
  • References (13)
    13 references, page 1 of 2

    [1] Alexander Chagrov and Michael Zakharyaschev. Modal logic, volume 35 of Oxford Logic Guides. The Clarendon Press, Oxford University Press, New York, 1997. Oxford Science Publications.

    [2] Leo Esakia. The modalized Heyting calculus: a conservative modal extension of the intuitionistic logic. J. Appl. Non-Classical Logics, 16(3-4):349-366, 2006.

    [3] Alfred Horn. The separation theorem of intuitionist propositional calculus. J. Symbolic Logic, 27:391-399, 1962.

    [4] Tsutomu Hosoi and Hiroakira Ono. Intermediate propositional logics (a survey). J. Tsuda College, (5):67-82, 1973.

    [5] Stephen Cole Kleene. Introduction to metamathematics. D. Van Nostrand Co., Inc., New York, N. Y., 1952.

    [6] A. V. Kuznetsov and A. Y. Muravitsky. Provability as modality. In Current problems in logic and methodology of sciences, pages 193-230. “Naukova Dumka, Kiev, 1980. Russian.

    [7] A. V. Kuznetsov and A. Yu. Muravitsky. On superintuitionistic logics as fragments of proof logic extensions. Studia Logica, 45(1):77-99, 1986.

    [8] Charles H. Lambros. A shortened proof of Sobocin´ski's theorem concerning a restricted rule of substitution in the field of propositional calculi. Notre Dame J. Formal Logic, 20(1):112-114, 1979.

    [9] A. Yu. Muravitski˘ı. Extensions of the logic of provability. Mat. Zametki, 33(6):915-927, 1983.

    [10] A. Yu. Muravitski˘ı. Correspondence of proof-intuitionistic logic extensions to proof-logic extensions. Dokl. Akad. Nauk SSSR, 281(4):789-793, 1985.

  • Metrics
Share - Bookmark