 Before going on to difficult things like classical logic, it may be worth while to give an example of how these ideas can be generalized. In Nelson 1949, David Nelson presented a variant of intuitionistic logic, agreeing with Heyting’s on the positive connectives and quantifiers, but having a different negation operator. (Some subsequent logicians, considering systems with both operators, call Nelson’s negation ‘strong negation’.) It is easy to formulate natural deduction rules for Nelson’s logic if we allow negative introduction and elimination rules in the style of Fitch. Negative negation introduction and elimination allow \(\neg\neg A\) to be inferred from \(A\) and vice versa. Negative \(\rightarrow\) rules allow \(\neg(A\rightarrow B)\) to be treated as if it were \((A\land\neg B)\). Negative (conjunction, disjunction, universal quantifier, existential quantifier) rules parallel the usual (disjunction, conjunction, existential quantifier, universal quantifier) rules: for example, \(\neg(A\land B)\) can be inferred by \(\neg\land\)-I from either \(\neg A\) or \(\neg B\), and a conclusion, \(C\), follows from \(\neg(A\land B)\) by \(\neg\land\)-E from three items: \(\neg(A\land B)\), a subproof in which \(C\) is derived from the hypothesis \(\neg A\), and a subproof in which C is derived from the hypothesis \(\neg B\). Since the pair of negative Int-Elim rules for any operator are related in a way parallel to the relation between (ordinary) Int-Elim rules for some operator, detours in a formal proof can be reduced in ways analogous to Gentzen’s reductions for standard intuitionistic logic. A normalization theorem can therefore be proven in much the same way as that for the standard logic. A normal derivation won’t have quite the same subformula property as normal derivations in the standard logic (every formula of a normal Nelson derivation will be a weak subformula—that is, either a subformula or the negation of a subformula—of the final conclusion or of some premiss), but close enough for many technical applications.