We present an extension and generalization of Sahlqvist--Van Benthem correspondence to the case of distribution-free modal logic, with, or without negation and/or implication connectives. We follow a reductionist strategy, reducing the correspondence problem at hand to the same problem, but for a suitable system of sorted modal logic (the modal companion of the distribution-free system). The reduction, via a fully abstract translation, builds on duality between normal lattice expansions and sorted residuated frames with relations (a generalization of classical Kripke frames with relations). The approach is scalable and it can be generalized to other systems, with or without distribution, such as distributive modal logic, or substructural logics with, or without additional modal operators.
翻译:本文提出萨奎斯特-范本特姆对应性在分布自由模态逻辑中的扩展与推广,该逻辑系统可包含或不包含否定及蕴涵联结词。我们采用还原主义策略,将当前对应性问题归约为排序模态逻辑系统(分布自由系统的模态伴随系统)中的同类问题。该归约过程通过完全抽象翻译实现,其理论基础是正规格扩张与带关系的排序剩余框架(经典带关系克里普克框架的推广)之间的对偶性。本方法具有可扩展性,可推广至其他含分布或不含分布的逻辑系统,例如分配模态逻辑,以及带或不带附加模态算子的子结构逻辑。