Editing Sequent calculus (section)

===Distinction between natural deduction and sequent calculus===

Gentzen asserted a sharp distinction between his single-output natural deduction systems (NK and NJ) and his multiple-output sequent calculus systems (LK and LJ). He wrote that the intuitionistic natural deduction system NJ was somewhat ugly.<ref>{{harvnb|Gentzen|1934|p=188}}. "Der Kalkül ''NJ'' hat manche formale Unschönheiten."</ref> He said that the special role of the [[law of excluded middle|excluded middle]] in the classical natural deduction system NK is removed in the classical sequent calculus system LK.<ref>{{harvnb|Gentzen|1934|p=191}}. "In dem klassischen Kalkül ''NK'' nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül ''LK'' wird diese Sonderstellung aufgehoben."</ref> He said that the sequent calculus LJ gave more symmetry than natural deduction NJ in the case of intuitionistic logic, as also in the case of classical logic (LK versus NK).<ref>{{harvnb|Gentzen|1934|p=191}}. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener."</ref> Then he said that in addition to these reasons, the sequent calculus with multiple succedent formulas is intended particularly for his principal theorem ("Hauptsatz").<ref>{{harvnb|Gentzen|1934|p=191}}. "Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorläufig nicht näher begründet werden."</ref>