  In allowing to discharge A →⊥ in order to infer A, this rule undermines the subformula principle. Furthermore, in containing both ⊥ and A →⊥, it refers to two different logical constants in a single rule, so there is no separation of logical constants any more. Finally, as an elimination rule for ⊥ it does not follow the general pattern of introductions and eliminations. As a consequence, it destroys the introduction form property that every closed derivation can be reduced to one which uses an introduction rule in the last step.