Sequent Calculus

A sequent calculus is a particular presentation of a logic or type theory that replaces the Judgement $\Gamma\vdash x:A$ with a sort of multi-term judgement $\Gamma\vdash\sigma:\Delta$ where both $\Gamma$ and $\Delta$ are Contexts.

Typically, we want to view both sides of the sequent as corresponding to different logical connectives. For classical sequent calculus, the idea is that the left-hand side of the turnstile corresponds to a formal Conjunction of propositions, whereas the right-hand side corresponds to a formal Disjunction.

Moreover, we end up splitting our Inference Rules for $\Gamma\vdash\Delta$ into two classes: Left Rules and Right Rules, which correspond to Elimination and Introduction rules, resp.

Moreover, proofs in sequent calculus do not have the same structure as Natural Deduction proofs. Instead of the usual structure of a bunch of Introduction Rules followed by Elimination Rules, where proofs to proceed from the "bottom up" and "top down" to meet in the middle, sequent calculi only have "bottom up" rules. In the parlance of Bidirectional Type Theory, every rule is a check rule.