Abstract
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. \(\square \) and ♢ 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.)
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Fine, K. (1995). The Logic of Essence. Journal of Philosophical Logic, 24(3), 241–273.
Girard, J.-Y. (1987). Proof theory and logical complexity. Napoli: Bibliopolis.
Hodes, H.T. (2004). On the Sense and Reference of a Logical Constant. The Philosophical Quarterly, 54(214), 134–165.
Humberstone, L. (1982). Scope and Subjunctivity. Philosophia, 12(1-2), 99–126.
Parisi, A. (2017). Second-Order Modal logic. University of Connectituct doctoral dissertationss, 1480.
Peacocke, C. (1992). A study of concepts. Cambridge: MIT Press.
Plotkin, G., & Stirling, C. (1986). A framework for intuitionistic modal logics. In Halpern, J.Y. (Ed.) Theoretical aspects of reasoning about knowledge (pp. 399–406). Morgan Kaufmann Publishers.
Turner, J. (2010). Ontological Pluralism. Journal of Philosophy, 107(1), 5–34.
Wehmeier, K. (2004). In the Mood. Journal of Philosophical Logic, 33(6), 607–630.
Wehmeier, K., & Rückert, H. (2019). Still in the Mood. Topoi, 48(2), 361–377.
Wojcicki, R. (1988). Theory of logical calculi, Synthese Library. Berlin: Kluwer Academic Publishers.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Thanks to Philip Sink, and to the referee, for reading several drafts of this paper and catching many errors.
Rights and permissions
About this article
Cite this article
Hodes, H.T. One-Step Modal Logics, Intuitionistic and Classical, Part 1. J Philos Logic 50, 837–872 (2021). https://doi.org/10.1007/s10992-020-09574-5
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-020-09574-5