Editing Sequent calculus (section)

=== Relation to standard axiomatizations ===

Sequent calculus is related to other axiomatizations of classical propositional calculus, such as Frege's propositional calculus or [[Propositional_calculus#Łukasiewicz's_P2|Jan Łukasiewicz's axiomatization]] (itself a part of the standard [[Hilbert system]]): Every formula that can be proven in these has a reduction tree. This can be shown as follows: Every proof in propositional calculus uses only axioms and the inference rules. Each use of an axiom scheme yields a true logical formula, and can thus be proven in sequent calculus; examples for these are [[Sequent calculus#Example derivations|shown below]]. The only inference rule in the systems mentioned above is [[modus ponens]], which is implemented by the cut rule.