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

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.