A minimal classical sequent calculus free of structural rules

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 disjunction rule with Γ , A , B implies Γ , A ∨ B . aper 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. ve a minimality theorem for the propositional fragment Mp : any propositional 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 M as a minimal complete core of Gentzen’s LK .