A minimal classical sequent calculus free of structural rules

作者：Hughes Dominic^*

来源：Annals of Pure and Applied Logic, 2010, 161(10): 1244-1253.

DOI：10.1016/j.apal.2010.03.001

• Proof theory
• Sequent calculus
• Gentzen
• 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, (SIC) by (SIC). P, (SIC)P for any context (SIC), and replacing the original disjunction rule with (SIC), A, B implies (SIC), A boolean OR 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: (SIC), Delta, A and (SIC), Sigma, B implies (SIC), Delta, Sigma, A boolean AND B. We refer to this system M as minimal sequent calculus.
We prove 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.

• 出版日期2010-7