Mathematics – Logic
Scientific paper
2005-06-22
Mathematics
Logic
To appear in Annals of Pure and Applied Logic. 15 pages
Scientific paper
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,(not P) by Gamma,P,(not P) for any context Gamma, and replacing the original disjunction rule with Gamma,A,B implies Gamma,(A 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: Gamma,Delta,A and Gamma,Sigma,B implies Gamma,Delta,Sigma,(A 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.
No associations
LandOfFree
A minimal classical sequent calculus free of structural rules does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A minimal classical sequent calculus free of structural rules, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A minimal classical sequent calculus free of structural rules will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-624434