一句话:用 game comonad 语义统一刻画有限模型论组合方法中的 FVM 型定理,并给出参数化构造。
有限模型论中的组合方法通过将复杂结构拆成简单组件来支持模块化推理,其核心是 Feferman–Vaught–Mostowski(FVM)型定理,刻画逻辑等价在模型组合与变换下的行为。本文将近期用于模型比较博弈的 game comonad 语义推广为范畴论框架,给出统一条件以导出 FVM 型结果。该框架对模型类、逻辑和操作保持参数化,并自然涵盖正存在片段及带计数量词的扩展;还揭示了 FVM 定理与单子论经典概念的联系。作者用该框架重新得到若干经典定理,包括对 Dawar、Severini 和 Zapata 关于三变量计数逻辑与同谱性的结果的精细化,并证明结构乘积的一族对逻辑一致的 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 be-haves 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.