一句话：为无限树上的 MSO 给出完备公理化，并引入表达能力更强的 FSO 以证明 Rabin 树定理。
本文研究无限树上的一元二阶逻辑（MSO）的完备公理化。MSO 在无限树上的可判定性即 Rabin 树定理，是逻辑可判定性领域最强结果之一。作者构造了一个完备演绎系统，其公理集可在多项式时间内识别；系统包含把二阶逻辑视为双排序一阶逻辑的通常规则，以及刻画某类奇偶博弈位置确定性的公理模式。由于 MSO 语言表达力有限，作者提出函数式（一元）二阶逻辑 FSO 作为扩展，可统一处理（遗传）有限集及相应的带标号树，并获得更高抽象。由此，通过对形式推导的朴素枚举，可形式地得到 Rabin 树定理的一个证明。
This paper presents a complete axiomatization of Monadic Second-Order Logic (MSO) over infinite trees. MSO on infinite trees is a rich system, and its decidability ("Rabin's Tree Theorem") is one of the most powerful known results concerning the decidability of logics. By a complete axiomatization we mean a complete deduction system with a polynomial-time recognizable set of axioms. By naive enumeration of formal derivations, this formally gives a proof of Rabin's Tree Theorem. The deduction system consists of the usual rules for second-order logic seen as two-sorted first-order logic, together with the natural adaptation In addition, it contains an axiom scheme expressing the (positional) determinacy of certain parity games. The main difficulty resides in the limited expressive power of the language of MSO. We actually devise an extension of MSO, called Functional (Monadic) Second-Order Logic (FSO), which allows us to uniformly manipulate (hereditarily) finite sets and corresponding labeled trees, and whose language allows for higher abstraction than that of MSO.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1903-05878,
title = {A Functional (Monadic) Second-Order Theory of Infinite Trees},
author = {Anupam Das and Colin Riba},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 4},
year = {2020},
doi = {10.23638/lmcs-16(4:6)2020}
}