 These modal systems are easy to use, and they have been included in some logic textbooks for philosophy undergraduates. They are, however, often less elegant than natural deduction systems for first order logic. The natural deduction rules for classical logic support the interdefinability of the two quantifiers: \(\forall xA(x)\) and \(\exists xA(x)\) are provably equivalent to \(\neg\exists x\neg A(x)\) and \(\neg\forall x\neg A(x)\) by use of the quantifier and negation rules; and the rules for either quantifier are derivable, when it is defined in terms of the other, by use of the negation rules and the rules for the other quantifier. For most modal natural deduction systems, the analogous results do not hold, and the equivalences have to be postulated specially. Again, \(\exists xA(x)\lor\exists xB(x)\) is derivable from \(\exists x(A(x)\lor B(x))\) by use of the rules for the existential quantifier and disjunction, but the restrictions on \(\diamondsuit\)-E usually block the analogous derivation in modal natural deduction. Normalization theorems are known for some systems of modal natural deduction, but often they are not as strong as the analogous results for first order logic: sometimes the subformula property of normal derivations requires that the result of prefixing a limited number of modal operators to a formula count as one of its “honorary” subformulas.