Order Invariance on Decomposable Structures

TL;DR

This paper investigates the expressive power of order-invariant MSO and FO logics on classes of structures with certain tree decompositions, revealing equivalences and extensions of known results in graph theory and logic.

Contribution

It extends existing results by showing that order-invariant MSO and CMSO are equally expressive on graphs with bounded tree width and planar graphs, and that FO properties are captured by MSO on these classes.

Findings

Order-invariant MSO and CMSO are equally expressive on bounded tree width graphs.

Order-invariant MSO is more expressive than MSO and CMSO in general.

All order-invariant FO properties are definable in MSO on certain classes.

Abstract

Order-invariant formulas access an ordering on a structure's universe, but the model relation is independent of the used ordering. Order invariance is frequently used for logic-based approaches in computer science. Order-invariant formulas capture unordered problems of complexity classes and they model the independence of the answer to a database query from low-level aspects of databases. We study the expressive power of order-invariant monadic second-order (MSO) and first-order (FO) logic on restricted classes of structures that admit certain forms of tree decompositions (not necessarily of bounded width). While order-invariant MSO is more expressive than MSO and, even, CMSO (MSO with modulo-counting predicates), we show that order-invariant MSO and CMSO are equally expressive on graphs of bounded tree width and on planar graphs. This extends an earlier result for trees due to Courcelle. Moreover, we show that all properties definable in order-invariant FO are also definable in MSO on these classes. These results are applications of a theorem that shows how to lift up definability results for order-invariant logics from the bags of a graph's tree decomposition to the graph itself.