Gentzen's classical sequent calculus LK has explicit structural rules for contraction and weakening. They can be absorbed (in a right-sided formulation) by replacing the axiom P, ¬P by Γ,P,¬P for any context Γ, and replacing the original disjuction rule with Γ,A,B implies Γ,A∨B.
This paper presents a classical sequent calculus which is also free of contraction and weakening, but more symmetrically: both contraction and weakening are absorbed into conjunction, leaving the axiom rule intact. It uses a blended conjunction rule, combining the standard context-sharing and context-splitting rules: Γ,Δ,A and Γ,Σ,B implies Γ,Δ,Σ,A∧B. We refer to this system M as minimal sequent calculus.
We prove a minimality theorem for the propositional fragment Mp: any sequent calculus S
(within a standard class of right-sided calculi) is complete if and only if S
contains Mp (that is, each rule of Mp is derivable in S).
Thus one can view Mp as a minimal complete core of Gentzen's LK.
Keywords: Proof theory; Sequent calculus; Gentzen; Structural rules
Mathematical subject codes: 03B05; 03B20; 03B47