In proof theory and mathematical logic, sequent calculus is a widely known family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934, as a tool for studying (respectively, both classical and intuitionistic) natural deduction in first-order logic. Gentzen's so-called "Main Theorem" (Hauptsatz) about LK and LJ was the cut-elim...
more
In proof theory and mathematical logic, sequent calculus is a widely known family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934, as a tool for studying (respectively, both classical and intuitionistic) natural deduction in first-order logic. Gentzen's so-called "Main Theorem" (Hauptsatz) about LK and LJ was the cut-elimination theorem, a result with far-reaching meta-theoretic consequences, including consistency. Gentzen further demonstrated the power of the technique of cut-elimination a few years later, giving a (transfinite) proof of the consistency of Peano arithmetic, in surprising response to Gödel's incompleteness theorems. Since Gentzen, sequent calculi (also called Gentzen systems) and the general concepts relating to them have been widely applied in the fields of proof theory, mathematical logic, and automated deduction.
One way to classify...
less
