A minimal classical sequent calculus free of structural rules

DOI10.1016/J.APAL.2010.03.001MaRDI QIDQ636359zbMATH OpenOpenAlexFDO

Authors Dominic J. D. Hughes

Publication date 26 August 2011

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/math/0506463

zbMATH Keywords

proof theorysequent calculusstructural rulesGentzen

Mathematics Subject Classification ID

Classical propositional logic (03B05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20)

Abstract: 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.

Recommendations

• Multiplicative conjunction and an algebraic meaning of contraction and weakening
• Contraction contracted
• Sequent calculus in natural deduction style
• Absorbing the structural rules in the sequent calculus with additional atomic rules
• scientific article; zbMATH DE number 218501

Cites work

• scientific article; zbMATH DE number 1943957 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 3327279 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 3105203 (Why is no real title available?)
• Linear logic
• Schlussweisen-Kalküle der Prädikatenlogik
• Strong normalisation of cut-elimination in classical logic
• Untersuchungen über das logische Schliessen. I

Cited in

(11)

• Cut elimination by unthreading
• A framework for proof systems
• Complementary proof nets for classical logic
• Contraction contracted
• Proofs and surfaces
• Investigations into a left-structural right-substructural sequent calculus
• Fractional semantics for classical logic
• Structural interactions and absorption of structural rules in BI sequent calculus
• Subject-predicate calculus free from existential import
• Absorbing the structural rules in the sequent calculus with additional atomic rules
• Sequent calculus for the intersection of LK and the reversed

This page was built for publication: A minimal classical sequent calculus free of structural rules

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q636359)