 The historically first seem to be systems of natural deduction for modal logics. The logical behavior of necessity and possibility operators in familiar modal logics has deep analogies to the logical behavior of universal and existential quantifiers. (This, of course, is what makes the “possible worlds” semantics for modality—on which the necessity of a proposition is construed as its holding in every member of some range of “worlds”, and its possibility as its holding in at least one—so natural.) Introduction and elimination rules for the modal operators, then, can be formulated in ways analogous to those for the quantifiers. The elimination rule for necessity and the introduction rule for possibility (at least for alethic modal logics…) are easy: what is necessary is true, and what is true is possible. For Necessity Introduction, we can have the rule that \(\square A\) may be asserted after a subproof (of a special kind: in Fitch’s nomenclature, a strict subproof) in which \(A\) occurs: there will be some restriction, differing in formulations for different modal logics, on reiteration into these special subproofs. (Intuitively, in terms of the possible worlds semantic interpretation, the idea is that something asserted before the beginning of the subproof can be reiterated into it only if its truth does not depend on any special feature of the actual world.) Possibility Elimination will similarly ape the form of \(\exists\)-Elim: for at least some range of formulas \(B\), \(B\) may be inferred from \(\diamondsuit A\) in the presence of a strict subproof having \(A\) as a hypothesis and containing \(B\), with the complication that \(B\) must satisfy a condition analogous to the condition permitting formulas to be reiterated into strict subproofs. (For many modal logics, the easiest way of formulating the condition is to make \(B\) suitable, as it were, after the fact: if \(B\) is of the form \(\diamondsuit C\), it may be asserted after \(\diamondsuit A\) and a strict subproof with \(A\) as hypothesis in which \(C\) occurs.) Fitch (1952) defines systems like this for the modal logics S\(_4\) and T. (He doesn’t name T in the book, describing the system only as “resembling S\(_2\)”.) Curry (1950) and, in greater detail, Curry (1963) gives similar rules for S\(_4\), formulated in a Gentzen-style rather than Fitch-style presentation of Natural Deduction. Fitch (1966) gives formulations of a variety of alethic and deontic propositional modal logics; Fitting (1983) is a comprehensive study of a variety of modal natural deduction systems and their metatheoretic properties.