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 , 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 ). 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.)