一句话:用扩展的博弈余单子语义统一刻画 FVM 型定理,为有限模型论中的组合方法提供参数化范畴论基础。
本文建立有限模型论中组合方法的范畴论理论。组合方法通过由简单组件构造复杂结构来实现模块化推理,其核心是 Feferman–Vaught–Mostowski(FVM)型定理,用以刻画逻辑等价在组合与变换下的行为。作者扩展用于模型比较博弈的博弈余单子语义,在范畴抽象下给出统一条件,参数化地导出 FVM 型定理;参数涵盖模型类、逻辑与操作,并自然处理存在/正存在片段及计数量词扩展。文中还揭示 FVM 型定理与单子论经典概念的联系。方法可恢复多个经典定理,细化 Dawar 等人关于三变量计数逻辑与同谱性的结果,并证明乘积结构的一族 FVM 定理,而特定博弈论证无法做到。
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 existential and positive existential fragments, 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. This is an extended version of the LiCS 2023 conference paper of the same name.arXiv admin note: substantial text overlap with arXiv:2304.10196
@article{paperbot3360,
title = {A categorical account of composition methods in logic (extended version)},
author = {Tomáš Jakl and Dan Marsden and Nihil Shah},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:10)2025}
}