Distributive residuated frames and generalized bunched implication algebras
Distributive residuated frames and generalized bunched implication algebras
复制标题
分配剩余框架和广义群蕴涵代数
作者：
Nikolaos Galatos;P. Jipsen
我们证明了分配满Lambek微积分的（非结合的）Gentzen系统在简单结构规则下的所有扩展都具有切消性。此外，这些规则的扩展不增加复杂性，但具有有限模型性质，因此分布剩余格的许多子变种都具有可决的方程理论。对于其他一些扩展，我们证明了有限嵌入性，这暗示了全称论的可决性，并证明了我们的结果同样适用于广义束蕴涵代数。我们的分析是在剩余框架的一般设置下进行的。
We show that all extensions of the (non-associative) Gentzen system for distributive full Lambek calculus by simple structural rules have the cut elimination property. Also, extensions by such rules that do not increase complexity have the finite model property, hence many subvarieties of the variety of distributive residuated lattices have decidable equational theories. For some other extensions, we prove the finite embeddability property, which implies the decidability of the universal theory, and we show that our results also apply to generalized bunched implication algebras. Our analysis is conducted in the general setting of residuated frames.