Interpolation and the Exchange Rule
Wesley Fussner, George Metcalfe, Simon Santschi
TL;DR
The paper analyzes when deductive interpolation holds for axiomatic extensions of substructural logics, by translating interpolation into the amalgamation property of the corresponding algebraic varieties of residuated lattices. It shows a dichotomy driven by exchange: continuum-many non-commutative idempotent semilinear residuated lattices yield continuum-many extensions with interpolation when exchange is not derivable, while the commutative case collapses to exactly sixty AM varieties and hence sixty DI extensions (with model completions for their first-order theories). Central to the results are the nested-sum decompositions, Sugihara skeletons, and Galatos’ $A_S$-based atom construction, which enable a precise AM/DI classification in the commutative setting and the construction of continuum families in the non-commutative setting. The work also discusses the impact of dropping semilinearity or the $e=f$ constraint, showing a dramatic growth (over 12 million) in possible varieties with AM in the pointed, non-semilinear scenario, and leaving several open questions for broader generalizations. Overall, it advances a detailed algebraic map describing how exchange controls the prevalence of interpolation across a spectrum of substructural logics.
Abstract
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.