逻辑中组合方法的范畴论描述
计算机科学中的逻辑
2023-04-26 v2 范畴论
摘要
我们提出了有限模型论中组合方法的范畴论理论——这是一种通过将复杂结构由较简单组件构建来实现模块化推理的关键技术。组合方法所需的关键结果是 Feferman-Vaught-Mostowski（FVM）型定理，其刻画了逻辑等价在模型的组合与变换下的行为。我们的结果通过扩展最近引入的用于模型比较游戏的博弈余单子语义而得到发展。这种抽象层次使我们能够以统一的方式给出产生 FVM 型结果的条件。我们的定理在所涉及模型类、逻辑和运算中是参数化的。此外，它们自然地解释了正存在片段，以及这些逻辑带计数量词的扩展。我们还揭示了 FVM 型定理与单子理论中的经典概念之间令人惊讶的联系。我们通过恢复许多具有实际意义的经典定理来说明我们的方法，包括由 Dawar、Severini 和 Zapata 先前关于三变量计数逻辑与余谱性结果的一个改进。为了突出我们的技术在与所关注逻辑参数化方面的重要性，我们证明了一族关于结构积的 FVM 定理，在所讨论逻辑中是统一的，这是使用特定博弈论证无法做到的。
引用
@article{arxiv.2304.10196,
title = {A categorical account of composition methods in logic},
author = {Tomáš Jakl and Dan Marsden and Nihil Shah},
journal= {arXiv preprint arXiv:2304.10196},
year = {2023}
}