Recursion Schemes, the MSO Logic, and the U quantifier

TL;DR

This paper extends the decidability of model-checking for recursion schemes to a logic with an unbounding quantifier U, enabling analysis of properties involving arbitrarily large finite sets within trees generated by higher-order recursion schemes.

Contribution

It introduces a decidable extension of MSO logic with the U quantifier for recursion schemes, preserving key logical properties.

Findings

Decidability established for the extended logic with U quantifier.

The logic retains reflection and effective selection properties.

Applicable to trees generated by higher-order recursion schemes.

Abstract

We study the model-checking problem for recursion schemes: does the tree generated by a given higher-order recursion scheme satisfy a given logical sentence. The problem is known to be decidable for sentences of the MSO logic. We prove decidability for an extension of MSO in which we additionally have an unbounding quantifier U, saying that a subformula is true for arbitrarily large finite sets. This quantifier can be used only for subformulae in which all free variables represent finite sets (while an unrestricted use of the quantifier leads to undecidability). We also show that the logic has the properties of reflection and effective selection for trees generated by recursion schemes.