Cut elimination and strong separation for substructural logics: an algebraic approach

DOI10.1016/j.apal.2010.01.003zbMath1245.03027MaRDI QIDQ636346

Hiroakira Ono, Nikolaos Galatos

Publication date: 26 August 2011

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.2010.01.003

zbMATH Keywords

Hilbert system; cut elimination; MacNeille completion; substructural logic; residuated lattice; Gentzen system; strong separation

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03G25: Other algebras related to logic

03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)

Related Items

Residuated frames with applications to decidability, Unnamed Item, One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity, Extensions of Lambek Calculi, Weakening Relation Algebras and FL$$^2$$-algebras, Some Syntactic Interpretations in Different Systems of Full Lambek Calculus, NONASSOCIATIVE SUBSTRUCTURAL LOGICS AND THEIR SEMILINEAR EXTENSIONS: AXIOMATIZATION AND COMPLETENESS PROPERTIES, The Monotone Lambek Calculus Is NP-Complete, UNDECIDABILITY OF CONSEQUENCE RELATION IN FULL NON-ASSOCIATIVE LAMBEK CALCULUS, A SUBSTRUCTURAL GENTZEN CALCULUS FOR ORTHOMODULAR QUANTUM LOGIC, An algebraic glimpse at bunched implications and separation logic, The atomic theory of left division of two-sided ideals of semirings with unit, Algebraic proof theory for substructural logics: cut-elimination and completions, Basic substructural core fuzzy logics and their extensions: mianorm-based logics, Completion and finite embeddability property for residuated ordered algebras., Weakening-free, non-associative fuzzy logics: micanorm-based logics, Involutive basic substructural core fuzzy logics: involutive mianorm-based logics, The completions of multi-posets and quantum B-algebras, Residuated structures and orthomodular lattices, Hyper-MacNeille completions of Heyting algebras, Complexity of the universal theory of bounded residuated distributive lattice-ordered groupoids, Prelinear algebras in relatively regular quasivarieties, Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL, Residuated expansions of lattice-ordered structures

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Residuated lattices. An algebraic glimpse at substructural logics
• Sequent-systems and groupoid models. I
• Lattice-valued representation of the cut-elimination theorem
• Relative pseudo-complements, join-extensions, and meet-retractions
• Closure operators and complete embeddings of residuated lattices
• A survey of abstract algebraic logic
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Generalized MV-algebras
• Algebraic aspects of cut elimination
• The finite embeddability property for residuated lattices, pocrims and BCK-algebras.
• Rule separation and embedding theorems for logics without weakening
• Untersuchungen über das logische Schliessen. I
• Fuzzy logics from substructural perspective
• Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
• The finite model property for BCI and related systems
• Finite Models of Some Substructural Logics
• THE STRUCTURE OF RESIDUATED LATTICES
• Equivalence of consequence relations: an order-theoretic and categorical perspective
• Glivenko theorems for substructural logics over FL
• On Action Logic: Equational Theories of Action Algebras
• Logics without the contraction rule
• Algebraizable logics
• Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
• The finite model property for various fragments of intuitionistic linear logic
• Residuated frames with applications to decidability
• Which structural rules admit cut elimination? An algebraic criterion
• On the finite embeddability property for residuated ordered groupoids