A classical sequent calculus free of structural rules
Dominic Hughes · 2005
Gentzen’s system LK, classical sequent calculus, 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 untouched. It uses a hybrid conjunction rule, combining the standard context-sharing and context-splitting rules: Γ,∆,A and Γ,Σ,B implies Γ,∆,Σ, A ∧ B. We call this system Hybrid Logic. Hybrid conjunction is critical for the liberation from structural rules: relaxing it to the pair of standard conjunction rules breaks completeness. We prove a minimality theorem for hybrid logic: any sequent calculus (within a standard class of right-sided calculi) is complete iff it contains hybrid logic. Thus one can view hybrid logic as a “complete core ” of Gentzen’s LK. 1