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

DOI10.1016/j.apal.2010.01.003zbMath1245.03027OpenAlexW2073214104MaRDI 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 systemcut eliminationMacNeille completionsubstructural logicresiduated latticeGentzen systemstrong separation

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

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

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