Sequentkalkyl

Sequentkalkyl, or sequent calculus, is a formal framework for proving logical formulas by manipulating sequents. A sequent has the form Γ ⊢ Δ, where Γ (the antecedent) and Δ (the succedent) are typically sequences or multisets of formulas. The idea is that the conjunction of the formulas on the left implies the disjunction of the formulas on the right. In classical sequent calculus, the right side may contain multiple formulas; in intuitionistic variants, the right side is restricted to at most one formula.

Proofs in sequent calculus are built from introduction rules that operate on the logical connectives, applied to either the left or right side of the sequent, together with structural rules that rearrange or modify the components. Structural rules include weakening, contraction, and exchange, or their admissibility, depending on the formulation. A basic axiom is A ⊢ A, expressing an identity principle. The cut rule allows deriving a result from intermediate lemmas, but the core result of the theory, cut elimination, shows that any proof can be transformed into a cut-free proof. This leads to the subformula property, where every formula occurring in a cut-free proof is a subformula of the original sequents.

There are two prominent versions: LK for classical logic and LJ for intuitionistic logic. Sequent calculus is central in proof theory, providing a clear syntactic account of logical consequence, aiding meta-logical results such as consistency proofs and normalization. It also informs automated theorem proving and type theory. In Swedish mathematical literature, sequentkalkyl is the term used for this formalism, directly corresponding to the English sequent calculus.