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

Harold Hodes
Cornell University
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.)
Keywords Intiutionistic and classical modal logics  Introduction and elimination rules  Natural deduction  One-step  Plotikin-Sterling frames and models  Soundness and completeness theorems
Categories (categorize this paper)
DOI 10.1007/s10992-020-09574-5
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

 PhilArchive page | Other versions
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

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 10 references / Add more references

Citations of this work BETA

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

Add more citations

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 index

Total views
101 ( #118,762 of 2,533,691 )

Recent downloads (6 months)
24 ( #37,434 of 2,533,691 )

How can I increase my downloads?


My notes