We present a categorical theory of the composition methods in finite model theory -- a key technique enabling modular reasoning about complex structures by building them out of simpler components. The crucial results required by the composition methods are Feferman-Vaught-Mostowski (FVM) type theorems, which characterize how logical equivalence behaves under composition and transformation of models. Our results are developed by extending the recently introduced game comonad semantics for model comparison games. This level of abstraction allow us to give conditions yielding FVM type results in a uniform way. Our theorems are parametric in the classes of models, logics and operations involved. Furthermore, they naturally account for the positive existential fragment, and extensions with counting quantifiers of these logics. We also reveal surprising connections between FVM type theorems, and classical concepts in the theory of monads. We illustrate our methods by recovering many classical theorems of practical interest, including a refinement of a previous result by Dawar, Severini, and Zapata concerning the 3-variable counting logic and cospectrality. To highlight the importance of our techniques being parametric in the logic of interest, we prove a family of FVM theorems for products of structures, uniformly in the logic in question, which cannot be done using specific game arguments.
翻译:我们提出了有限模型论中组合方法的范畴化理论——一种通过将较简单的组件组合起来构建较复杂的结构,并进行模块化推理的关键技术。组合方法所需的关键结果是Feferman-Vaught-Mostowski (FVM)型定理,其刻画了在模型合成和转换下逻辑等价性的行为。我们的结果通过扩展最近引入的模型比较博函语义进行开发。这种抽象层次允许我们以统一的方式给出产生FVM型结果的条件。我们的定理是以有限模型、逻辑和操作类参数化的。此外,它们自然地考虑了正存在分段和这些逻辑的计数量子化扩展。我们还揭示了FVM型定理与博函理论中的经典概念之间的令人惊讶的联系。我们通过恢复许多实际感兴趣的经典定理来说明我们的方法,其中包括Dawar、Severini和Zapata之前关于3变量计数逻辑和余谱的结果的改进。为了强调我们的技术在所涉及的逻辑中是参数化的重要性,我们证明了一类FVM定理,涉及结构的乘积,并统一应用于所考虑的逻辑,这是不能使用特定博弈论证明的。