无限树的函数（单子）二阶理论
摘要：无限树上单调二阶逻辑（MSO）的完全公理化。MSO在无限树上是一个丰富的系统，其可决定性（“Rabin的树定理”）是关于逻辑可决定性的已知结果中最强大的之一。通过完全公理化，我们指的是一个具有多项式时间可识别的公理集的完全演绎系统。通过对形式导出的朴素枚举，这实际上给出了Rabin的树定理的证明。演绎系统包括将二阶逻辑视为两排序为一阶逻辑的常规规则，以及自然的适应。此外，它还包含一个表达某些奇偶博弈（位置性）决定性的公理方案。主要困难在于MSO语言的有限表达能力。实际上，我们设计了MSO的扩展，称为功能（单调）二阶逻辑（FSO），它允许我们统一地操作（世代性）有限集合和相应的带标签树，其语言允许比MSO更高的抽象。
作者：Anupam Das and Colin Riba
论文ID：1903.05878
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22