It was proved by Maksimova in 1977 that exactly eight varieties of Heyting algebras have the amalgamation property, and hence exactly eight axiomatic extensions of intuitionistic propositional logic have the deductive interpolation property. The prevalence of the deductive interpolation property for axiomatic extensions of substructural logics and the amalgamation property for varieties of pointed residuated lattices, their equivalent algebraic semantics, is far less well understood, however. Taking as our starting point a formulation of intuitionistic propositional logic as the full Lambek calculus with exchange, weakening, and contraction, we investigate the role of the exchange rule--algebraically, the commutativity law--in determining the scope of these properties. First, we show that there are continuum-many varieties of idempotent semilinear residuated lattices that have the amalgamation property and contain non-commutative members, and hence continuum-many axiomatic extensions of the corresponding logic that have the deductive interpolation property in which exchange is not derivable. We then show that, in contrast, exactly sixty varieties of commutative idempotent semilinear residuated lattices have the amalgamation property, and hence exactly sixty axiomatic extensions of the corresponding logic with exchange have the deductive interpolation property. From this latter result, it follows also that there are exactly sixty varieties of commutative idempotent semilinear residuated lattices whose first-order theories have a model completion.
翻译:摘要:1977年,马克西莫娃证明了恰有八个海廷代数簇具有并合性质,因此恰有八个直觉主义命题逻辑的公理化扩张具有演绎插值性质。然而,对于子结构逻辑公理化扩张的演绎插值性质以及其代数语义(带尖点的剩余格簇)的并合性质,人们的理解尚不充分。本文以直觉主义命题逻辑的表述为基础(即带有交换、弱化与收缩规则的完全兰贝克演算),探讨交换规则(即代数中的交换律)在决定这些性质适用范围中的作用。首先,我们证明存在连续无穷多个幂等半线性剩余格簇具有并合性质,且其成员包含非交换元,因此对应逻辑中恰有连续无穷多个无法推导出交换规则的公理化扩张具有演绎插值性质。随后,我们证明与之形成对比的是,恰有六十个交换幂等半线性剩余格簇具有并合性质,因此对应逻辑中恰有六十个带有交换规则的公理化扩张具有演绎插值性质。由后一结论还可推出:恰有六十个交换幂等半线性剩余格簇的一阶理论具有模型完备化。