A simplified natural deduction approach to certain modal systems (Q1097870)

Natural deduction rules - in the manner of, say, Copi - are here defined for the normal modal systems T, S.4, B and S.5, through the device of attaching chains of numerical subscripts to lines in a derivation and restricting the introduction and elimination rules for the modal operators to appropriate configurations of subscripts. These subscripts thus do the work of subordinate proofs and restricted reiteration rules withint the more convenient format of Fitch-style natural deduction versions of the these systems. With the controlled manipulation of subscripts decision procedures for the systems are easily forthcoming. Moreover, Kripkean model-structures may readily be determined from terminated proof-tries, which generates an easy completeness theorem. The systems are extended to quantified modal logics.