natural deduction vs sequent calculus
What, exactly, is the difference between natural deduction systems and sequent calculi?
A commonly-given answer: “Sequent calculi allow many formulae on the right-hand side of the turnstile , while natural deduction allows only one.” But this is not universally true; e.g., some formulations of LJ allow only one formula on the right-hand side.
It seems to be better to answer in terms of the nature of the rules. In a natural deduction system, each connective is defined by introduction and elimination rules. In contrast, connectives in a sequent calculus are defined by left and right rules. Additionally, sequent calculi invariably have a cut rule, which natural deduction systems invariably lack.