Compositionality of the MSO+U Logic

TL;DR

This paper demonstrates the compositional nature of MSO+U logic on trees, showing that its truth depends only on properties of roots and subtrees, and that formulas with finite set variables can be rewritten using MSO properties of subtrees.

Contribution

It establishes the compositionality of MSO+U logic and provides a method to rewrite formulas with finite set variables into MSO formulas referencing subtree properties.

Findings

MSO+U logic is compositional on trees.

Formulas with finite set variables can be rewritten into MSO formulas.

The approach simplifies reasoning about MSO+U properties on trees.

Abstract

We prove that the MSO+U logic is compositional in the following sense: whether an MSO+U formula holds in a tree T depends only on MSO+U-definable properties of the root of T and of subtrees of T starting directly below the root. Another kind of compositionality follows: every MSO+U formula whose all free variables range only over finite sets of nodes (in particular, whose all free variables are first-order) can be rewritten into an MSO formula having access to properties of subtrees definable by MSO+U sentences (without free variables).