A Functional (Monadic) Second-Order Theory of Infinite Trees

摘要

This paper presents a complete axiomatization of Monadic Second-Order Logic(MSO) over infinite trees. MSO on infinite trees is a rich system, and itsdecidability ("Rabin's Tree Theorem") is one of the most powerful known resultsconcerning the decidability of logics. By a complete axiomatization we mean acomplete deduction system with a polynomial-time recognizable set of axioms. Bynaive enumeration of formal derivations, this formally gives a proof of Rabin'sTree Theorem. The deduction system consists of the usual rules for second-orderlogic seen as two-sorted first-order logic, together with the naturaladaptation In addition, it contains an axiom scheme expressing the (positional)determinacy of certain parity games. The main difficulty resides in the limitedexpressive power of the language of MSO. We actually devise an extension ofMSO, called Functional (Monadic) Second-Order Logic (FSO), which allows us touniformly manipulate (hereditarily) finite sets and corresponding labeledtrees, and whose language allows for higher abstraction than that of MSO.