Algebraic proof theory for substructural logics: cut-elimination and completions

DOI10.1016/j.apal.2011.09.003zbMath1245.03026OpenAlexW2169981414MaRDI QIDQ409322

Agata Ciabattoni, Kazushige Terui, Nikolaos Galatos

Publication date: 13 April 2012

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

Full work available at URL: https://doi.org/10.1016/j.apal.2011.09.003

zbMATH Keywords

cut eliminationMacNeille completionsubstructural logicresiduated latticeGentzen systemalgebraic proof theorystrucural rulesubstructural hierarchy

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Other algebras related to logic (03G25) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Related Items (44)

Canonical formulas for \(k\)-potent commutative, integral, residuated lattices ⋮ Power and Limits of Structural Display Rules ⋮ Densification of FL chains via residuated frames ⋮ Jankov Formulas and Axiomatization Techniques for Intermediate Logics ⋮ Integrally closed residuated lattices ⋮ Proof theory for lattice-ordered groups ⋮ The distributivity on bi-approximation semantics ⋮ Syntactic Completeness of Proper Display Calculi ⋮ FULL LAMBEK CALCULUS WITH CONTRACTION IS UNDECIDABLE ⋮ Hypersequent rules with restricted contexts for propositional modal logics ⋮ Tools for the Investigation of Substructural and Paraconsistent Logics ⋮ THE LOGIC OF RESOURCES AND CAPABILITIES ⋮ Taming Paraconsistent (and Other) Logics ⋮ Judgement aggregation in non-classical logics ⋮ Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory ⋮ MOST SIMPLE EXTENSIONS OF ARE UNDECIDABLE ⋮ Distributive residuated frames and generalized bunched implication algebras ⋮ Intermediate logics admitting a structural hypersequent calculus ⋮ Topological duality and algebraic completions ⋮ Density revisited ⋮ Finite embeddability property for residuated lattices via regular languages ⋮ MacNeille completions of FL-algebras ⋮ Skolemization and Herbrand theorems for lattice-valued logics ⋮ Focused proof-search in the logic of bunched implications ⋮ Join-completions of partially ordered algebras ⋮ Disjunction property and complexity of substructural logics ⋮ Specifying Proof Systems in Linear Logic with Subexponentials ⋮ A note on the substructural hierarchy ⋮ Algebraic proof theory: hypersequents and hypercompletions ⋮ Unnamed Item ⋮ The bounded proof property via step algebras and step frames ⋮ Semantical Approach to Cut Elimination and Subformula Property in Modal Logic ⋮ MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics ⋮ Uniform proofs of standard completeness for extensions of first-order MTL ⋮ Conuclear images of substructural logics ⋮ Modal translation of substructural logics ⋮ Residuated structures and orthomodular lattices ⋮ Hyper-MacNeille completions of Heyting algebras ⋮ Expanding the Realm of Systematic Proof Theory ⋮ The logic of pseudo-uninorms and their residua ⋮ Extensions of Lambek Calculi ⋮ FIBRED ALGEBRAIC SEMANTICS FOR A VARIETY OF NON-CLASSICAL FIRST-ORDER LOGICS AND TOPOLOGICAL LOGICAL TRANSLATION ⋮ Finite-valued semantics for canonical labelled calculi ⋮ Poset products as relational models

Uses Software

• SQEMA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algorithmic correspondence and canonicity for distributive modal logic
• Cut elimination and strong separation for substructural logics: an algebraic approach
• MacNeille completions of FL-algebras
• Zur Kennzeichnung der Dedekind-MacNeilleschen Hülle einer geordneten Menge
• Towards a semantic characterization of cut-elimination
• Residuated lattices. An algebraic glimpse at substructural logics
• Extending intuitionistic linear logic with knotted structural rules
• Hypersequents, logical consequence and intermediate logics for concurrency
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Adding involution to residuated structures
• Algebraic aspects of cut elimination
• Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
• MacNeille completions of lattice expansions
• Minimal varieties of residuated lattices
• CANONICITY RESULTS OF SUBSTRUCTURAL AND LATTICE-BASED LOGICS
• Kripke Semantics for Basic Sequent Systems
• Ein System des Verknüpfenden Schliessens
• Correspondences between gentzen and hilbert systems
• Expanding the Realm of Systematic Proof Theory
• Logic Programming with Focusing Proofs in Linear Logic
• The finite model property for various fragments of intuitionistic linear logic
• Specially ordered groups
• Residuated frames with applications to decidability
• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
• Which structural rules admit cut elimination? An algebraic criterion
• MacNeille completions and canonical extensions
• Partially Ordered Sets
• Boolean Algebras with Operators. Part I
• Boolean Algebras with Operators
• On the completion by cuts of distributive lattices

This page was built for publication: Algebraic proof theory for substructural logics: cut-elimination and completions