 or sacrifice purity and have a zero-premiss rule ≻ φ ∨ (φ → ψ), or again just leave the implicational rules as they are and rely on further rules (not given here) governing negation to make up the shortfall and render such classically but not intuitionistically acceptable →-sequents—such as Peirce’s Law above—provable with their aid. (The same tensions would then arise for the ¬ rules, if one regards obliqueness as undesirable, with “double negation elimination” principles abandoning simplicity, or “excluded middle” principles, abandoning purity. Note that by a ‘classically acceptable sequent’ here is meant a sequent holding on all Boolean valuations.) An alternative for capturing the classical logic of → is to change from the logical framework Set-Fmla to Set-Set, in which finite (possibly empty) sets of formulas appear on the right of the ≻, just as on the left. Then the above →-Introduction rule can be remain intact, but with a set variable to collect side-formulas on the right: from Γ, φ≻ψ, Δ to Γ≻φ→ψ, Δ. (Suitable modifications should also be made to the remaining rules in this case.) These ‘multiple-succedent’ sequents are more popularly associated with a different approach to logic from the natural deduction approach (though they have often appeared in this setting), namely the sequent calculus approach, in which instead of being inserted or removed from the right of the ≻, by suitable introduction or elimination rules, together with the possible discharge of assumptions, the rules—again, ideally, pure and simple—always insert a connective, either to the left or the right, of the “≻”. The left insertion rules do the work of the elimination rules of the natural deduction approach, while the right insertion rules do the work of—indeed, are just—the natural deduction introduction rules. The left insertion rules, (# Left) for # ∈ {∧,∨,→} are then as follows for the classical case, with the right insertion rules (# Right) being the natural deduction introduction rules as above, with a set-variable on the right of the ≻ for the classical Set-Set case: