Rule separation and embedding theorems for logics without weakening (Q1826930)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Rule separation and embedding theorems for logics without weakening
scientific article

    Statements

    Rule separation and embedding theorems for logics without weakening (English)
    0 references
    0 references
    0 references
    6 August 2004
    0 references
    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.
    0 references
    0 references
    0 references
    linear logic
    0 references
    separation theorem
    0 references
    residuated lattice
    0 references
    finite embeddability property
    0 references
    Lattice-R
    0 references
    intuitionistic linear logic
    0 references
    distributionless positive relevant logic
    0 references