Anupam Das ; Colin Riba - A Functional (Monadic) Second-Order Theory of Infinite Trees

lmcs:5315 - Logical Methods in Computer Science, October 23, 2020, Volume 16, Issue 4 - https://doi.org/10.23638/LMCS-16(4:6)2020
A Functional (Monadic) Second-Order Theory of Infinite TreesArticle

Authors: Anupam Das ; Colin Riba

    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.


    Volume: Volume 16, Issue 4
    Published on: October 23, 2020
    Accepted on: September 10, 2020
    Submitted on: March 27, 2019
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1263 times.
    This article's PDF has been downloaded 244 times.