Rule separation and embedding theorems for logics without weakening

DOI10.1023/B:STUD.0000032087.02579.E2MaRDI QIDQ1826930zbMATH OpenFDO

Authors C. J. van Alten, J. G. Raftery

Publication date 6 August 2004

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/B:STUD.0000032087.02579.E2

zbMATH Keywords

distributionless positive relevant logicfinite embeddability propertyintuitionistic linear logicLattice-Rlinear logicresiduated latticeseparation theorem

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Logical aspects of lattices and related structures (03G10)

Review text

For the intuitionistic propositional linear logic without bounds, 0, and exponentials axiomatized in a natural way, the authors prove a separation theorem in such a full and strong form that not only a provable formula but any derivable rule is derivable only by those ones concerning the logical constants occurring there in addition to the implication. Since the variety of residuated lattices provides a class of algebraic models for the logic, the result gives rise to several structural consequences for subreducts of residuated lattices. The separation theorem is also shown to hold similarly for the logic extended by the contraction axiom, which coincides on the distributionless positive relevant logic as a matter of fact. In this case, moreover, the proof permits the construction of finite models, that is, includes a direct proof of the finite model property for the derivable rules in the logic thus extended. Algebraically this means that the variety of sequare-increasing residuated lattices has the finite embeddability property, from which therefore follows that it has a decidable universal theory.

Recommendations

• Logics without the contraction rule and residuated lattices
• The finite model property for knotted extensions of propositional linear logic
• On a contraction-less intuitionistic propositional logic with conjunction and fusion
• The finite model property for various fragments of intuitionistic linear logic
• Residuated frames with applications to decidability

Cited in

(21)

• Constructive logic with strong negation is a substructural logic. II
• Varieties of De Morgan monoids: minimality and irreducible algebras
• Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
• Subdirectly irreducible residuated semilattices and positive universal classes
• On varieties of biresiduation algebras
• Semi-linear varieties of lattice-ordered algebras.
• The finite model property for knotted extensions of propositional linear logic
• Correspondences between gentzen and hilbert systems
• Representable idempotent commutative residuated lattices
• ASSERTIONALLY EQUIVALENT QUASIVARIETIES
• Residuated Structures, Concentric Sums and Finiteness Conditions
• Paraconsistent constructive logic with strong negation as a contraction-free relevant logic
• Residuated frames with applications to decidability
• Universal algebraic methods for non-classical logics
• An undecidability result for separation logic with theory reasoning
• Cut elimination and strong separation for substructural logics: an algebraic approach
• Contextual deduction theorems
• On pretabular extensions of relevance logic
• Modal expansions of ririgs
• Constructive logic with strong negation is a substructural logic. I
• Completion and finite embeddability property for residuated ordered algebras.

This page was built for publication: Rule separation and embedding theorems for logics without weakening

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