Editing Sequent calculus (section)

===Properties of the system LK===

This system of rules can be shown to be both [[soundness|sound]] and [[completeness (logic)|complete]] with respect to first-order logic, i.e. a statement <math>A</math> follows [[semantics|semantically]] from a set of premises <math>\Gamma</math> <math>(\Gamma \vDash A)</math> [[if and only if]] the sequent <math>\Gamma \vdash A</math> can be derived by the above rules.<ref>{{harvnb|Kleene|2002|p=336}}, wrote in 1967 that "it was a major logical discovery by Gentzen 1934–5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."</ref>

In the sequent calculus, the rule of [[cut-elimination|cut is admissible]]. This result is also referred to as Gentzen's ''Hauptsatz'' ("Main Theorem").<ref name=curry_cut_elimination /><ref name=kleene_cut_elimination />