Fitch-style rules for many modal logics.
David F. Siemens · Notre Dame Journal of Formal Logic · 1977
Fitch's original natural deduction rules for modal logic [l] give a calculus similar to S4, provided one uses strong negation introduction (SNI) and strong negation elimination (SNE).If SNI and weak negation elimination (WNE) are used, an intuitionistic modal calculus results.And Fitch presents an even weaker calculus using weak negation introduction (WNI) and WNE.The combination of WNI and SNE merely allows alternation to the doubly negated proposition.To all these combinations of rules may be added the rules for quantification, giving a variety of modal functional calculi.Cf. [2].Fitch [3] has shown some of the flexibility inherent in his rules by presenting formulations for the calculi known as B, M, S4, and S5, with quantification added, also for deontic versions of each of these, and for combinations of the alethic and deontic logics.Thomason [4] presented a Fitch-style calculus for the special calculus developed by Stalnaker and him, cf.[5] and [6].However, the technique is even more flexible than has been indicated.Combining the following rules in various ways with one of the sets giving one of the propositional or lower functional calculi, watching for potential paradoxes with the latter, gives calculi equivalent to those known in the literature, and to some that do not match.The rules are: For necessity: 1.Strong necessity introduction (SLI) L P Lp 2. Weak necessity introduction (WLI) P Lp