 Typically, natural deduction systems for classical logic are formulated by adding an extra, classicizing, rule to a natural deduction system for intuitionistic logic: any of a variety of possible rules can be  added.[23]  The immediate and permutative reductions are possible in derivations in classical natural deduction, but there is another case to consider: a logically complex formula might be concluded by the classicizing rule and then used as the major premiss of an elimination rule. This formula might be more complex than the final conclusion or any of the premises of the derivation, in which case its use would intuitively seem just as much a “detour” as those eliminated by the normalization of an intuitionistic derivation. Worse, if we allowed such detours, we would lose the “control” over the complexity of derivations necessary for technical applications of the normalization theorem. So a normal derivation, in natural deduction for classical logic, should be defined as one in which no conclusion of an introduction rule is used as the major premiss of an elimination rule (as before) and in which no formula obtained by the classicizing rule is used as the major premiss of an elimination rule. Gentzen appears to have thought that no reduction process was possible which would allow arbitrary derivations in the classical system to be transformed into this kind of normal derivation. (It is possible that the particular classicizing rule he envisaged (see  note 23)  makes this harder than other formulations would.)