One-step Modal Logics, Intuitionistic and Classical, Part 1

Journal of Philosophical Logic 50 (5):837-872 (2021)
  Copy   BIBTEX


This paper and its sequel “look under the hood” of the usual sorts of proof-theoretic systems for certain well-known intuitionistic and classical propositional modal logics. Section 1 is preliminary. Of most importance: a marked formula will be the result of prefixing a formula in a propositional modal language with a step-marker, for this paper either 0 or 1. Think of 1 as indicating the taking of “one step away from 0.” Deductions will be constructed using marked formulas. Section 2 presents the model-theoretic concepts, based on those in [7], that guide the rest of this paper. Section 3 presents Natural Deduction systems IK and CK, formalizations of intuitionistic and classical one-step versions of K. In these systems, occurrences of step-markers allow deductions to display deductive structure that is covered over in familiar “no step” proof-theoretic systems for such logics. Box and Diamond are governed by Introduction and Elimination rules; the familiar K rule and Necessitation are derived (i.e. admissible) rules. CK will be the result of adding the 0-version of the Rule of Excluded Middle to the rules which generate IK. Note: IK is the result of merely dropping that rule from those generating CK, without addition of further rules or axioms (as was needed in [7]). These proof-theoretic systems yield intuitionistic and classical consequence relations by the obvious definition. Section 4 provides some examples of what can be deduced in IK. Section 5 defines some proof-theoretic concepts that are used in Section 6 to prove the soundness of the consequence relation for IK (relative to the class of models defined in Section 2.) Section 7 proves its completeness (relative to that class). Section 8 extends these results to the consequence relation for CK. (Looking ahead: Part 2 will investigate one-step proof-theoretic systems formalizing intuitionistic and classical one-step versions of some familiar logics stronger than K.)

Similar books and articles

One-Step Modal Logics, Intuitionistic and Classical, Part 2.Harold T. Hodes - 2021 - Journal of Philosophical Logic 50 (5):873-910.
On some intuitionistic modal logics.Hiroakira Ono - 1977 - Bulletin of the Section of Logic 6 (4):182-184.
Intuitionistic hybrid logic.Torben Braüner & Valeria de Paiva - 2006 - Journal of Applied Logic 4 (3):231-255.
Modal translations in substructural logics.Kosta Došen - 1992 - Journal of Philosophical Logic 21 (3):283 - 336.
Post Completeness in Congruential Modal Logics.Peter Fritz - 2016 - In Lev Beklemishev, Stéphane Demri & András Máté (eds.), Advances in Modal Logic, Volume 11. College Publications. pp. 288-301.
Fitch-style natural deduction for modal paralogics.Hans Lycke - 2009 - Logique Et Analyse 52 (207):193-218.
Modal sequents for normal modal logics.Claudio Cerrato - 1993 - Mathematical Logic Quarterly 39 (1):231-240.
Restricted Classical Modal Logics.Cezar Mortari - 2007 - Logic Journal of the IGPL 15 (5-6):741-757.
Abstract modal logics.Ramon Jansana - 1995 - Studia Logica 55 (2):273 - 299.


Added to PP

410 (#48,779)

6 months
133 (#27,967)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Harold Hodes
Cornell University

Citations of this work

One-Step Modal Logics, Intuitionistic and Classical, Part 2.Harold T. Hodes - 2021 - Journal of Philosophical Logic 50 (5):873-910.

Add more citations

References found in this work

A Study of Concepts.Christopher Peacocke - 1992 - Studia Logica 54 (1):132-133.
Ontological Pluralism.Jason Turner - 2010 - Journal of Philosophy 107 (1):5-34.
The logic of essence.Kit Fine - 1995 - Journal of Philosophical Logic 24 (3):241 - 273.
Proof Theory and Logical Complexity.Helmut Pfeifer & Jean-Yves Girard - 1989 - Journal of Symbolic Logic 54 (4):1493.
In the mood.Kai Frederick Wehmeier - 2004 - Journal of Philosophical Logic 33 (6):607-630.

View all 9 references / Add more references