用 k 元包含-排除逻辑刻画 k 元存在二阶逻辑
逻辑
2018-06-19 v4 计算机科学中的逻辑
摘要
本文分析 k 元包含-排除逻辑 INEX[k]，它通过用 k 元包含和排除原子扩展一阶逻辑得到。我们展示 INEX[k] 的每个公式都可以用 k 元存在二阶逻辑 ESO[k] 的公式表达。反之，每个最多具有 k 元自由关系变量的 ESO[k] 公式可以用 INEX[k] 公式表达。由此得出，在句子层面上，INEX[k] 刻画了 ESO[k] 的表达能力。我们还引入了几个在 INEX[k] 中可表达的有用算子。特别地，我们定义了包含和排除量词以及所谓的项值保持析取，这对本文主要结果的证明至关重要。此外，我们提出了团队语义的一种新相对化方法并分析了包含和排除原子的对偶性。
引用
@article{arxiv.1502.05632,
title = {Capturing k-ary Existential Second Order Logic with k-ary Inclusion-Exclusion Logic},
author = {Raine Rönnholm},
journal= {arXiv preprint arXiv:1502.05632},
year = {2018}
}
备注
Extended version of a paper published in Annals of Pure and Applied Logic 169 (3), 177-215