一句话：为存在二阶逻辑与团队语义逻辑的并封闭片段给出句法刻画，并引入包含-排斥博弈及新原子。
并封闭性（团队对并封闭）是团队语义中不可判定的语义性质，直接处理相应片段困难。本文为存在二阶逻辑（ESO）和带团队语义的逻辑的并封闭片段给出句法刻画，通过引入一种范式使这些片段可被句法识别与操作。方法上，作者引入包含-排斥博弈，并证明它们恰好是对应的模型检测博弈，从而在语义片段与句法片段之间架起桥梁。在团队语义逻辑层面，作者进一步给出包含-排斥逻辑的限制以精确捕获并封闭片段；定义一个基于团队的原子，将其加入一阶逻辑后可精确捕获 ESO 的并封闭片段，回答了 Galliani 与 Hella 的公开问题。
We present syntactic characterisations for the union closed fragments of existential second-order logic and of logics with team semantics. Since union closure is a semantical and undecidable property, the normal form we introduce enables the handling and provides a better understanding of this fragment. We also introduce inclusion-exclusion games that turn out to be precisely the corresponding model-checking games. These games are not only interesting in their own right, but they also are a key factor towards building a bridge between the semantic and syntactic fragments. On the level of logics with team semantics we additionally present restrictions of inclusion-exclusion logic to capture the union closed fragment. Moreover, we define a team based atom that when adding it to first-order logic also precisely captures the union closed fragment of existential second-order logic which answers an open question by Galliani and Hella.
@article{paperbot1290,
title = {On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics},
author = {Matthias Hoelzel and Richard Wilke},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:14)2021}
}