一句话:系统比较命题团队逻辑中各类依赖原子在存在片段与全片段下的简洁性,给出指数下界与多项式上界。
命题团队逻辑是命题层面的一阶团队逻辑,可表达 dependence、independence、inclusion、exclusion 和 anonymity 等非经典原子;但除 dependence 外,其余原子的翻译此前仅有指数规模构造。本文系统比较这些原子在存在片段(分离析取仅允许正出现)与带无限制否定的全命题团队逻辑中的简洁性。作者将 Ehrenfeucht–Fraïssé 博弈的变体 formula size game 引入团队逻辑,用于证明规模下界;在存在片段中对所有上述原子得到指数下界,而在全片段中对所有原子给出多项式上界。
Propositional team logic is the propositional analog to first-order team logic. Non-classical atoms of dependence, independence, inclusion, exclusion and anonymity can be expressed in it, but for all atoms except dependence only exponential translations are known. In this paper, we systematically compare their succinctness in the existential fragment, where the splitting disjunction only occurs positively, and in full propositional team logic with unrestricted negation. By introducing a variant of the Ehrenfeucht-Fra\"{i}ss\'{e} game called formula size game into team logic, we obtain exponential lower bounds in the existential fragment for all atoms. In the full fragment, we present polynomial upper bounds also for all atoms.