 The rules employed in this  proof[8]  illustrate an aspect of natural deduction that is thought (by some) to be very important in the metatheory of natural deduction: that each connective of the language should have an introduction rule and an elimination rule—or as this is sometimes put, the entire logic should be organized into pairs of Introduction and Elimination (Int-Elim for short) rules for each logical operator. We discuss this feature in  §5  on normalization. We note here that Fitch’s exact formulation does not meet this Int-Elim requirement because it has, in addition to the usual rules, Int-Elim rules for certain combinations of connectives, namely the negations of connectives. Thus there are Int-Elim rules for such formula types as \(\neg(\phi\land\psi)\), \(\neg(\phi\lor\psi)\) and \(\neg(\phi\rightarrow\psi)\):