A minimal classical sequent calculus free of structural rules

DOI10.1016/J.APAL.2010.03.001zbMATH Open1225.03073arXivmath/0506463OpenAlexW2594450757MaRDI QIDQ636359FDOQ636359

Authors: Dominic J. D. Hughes 

Publication date: 26 August 2011

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

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.

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

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

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)

Cites Work

• Untersuchungen über das logische Schliessen. I
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Strong normalisation of cut-elimination in classical logic
• Schlussweisen-Kalküle der Prädikatenlogik
• Title not available (Why is that?)

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
• Sequent calculus for the intersection of LK and the reversed
• Absorbing the structural rules in the sequent calculus with additional atomic rules

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)