Where First-Order and Monadic Second-Order Logic Coincide

TL;DR

This paper characterizes when first-order logic and monadic second-order logic have equal expressive power on graph classes, showing it occurs precisely for classes with bounded tree depth.

Contribution

It establishes a precise condition linking bounded tree depth to the equivalence of FO and MSO expressive power on graph classes.

Findings

FO and MSO coincide on classes with bounded tree depth

For classes closed under induced subgraphs, GSO and MSO coincide

Constructive Feferman-Vaught-type theorem developed

Abstract

We study on which classes of graphs first-order logic (FO) and monadic second-order logic (MSO) have the same expressive power. We show that for all classes C of graphs that are closed under taking subgraphs, FO and MSO have the same expressive power on C if, and only if, C has bounded tree depth. Tree depth is a graph invariant that measures the similarity of a graph to a star in a similar way that tree width measures the similarity of a graph to a tree. For classes just closed under taking induced subgraphs, we show an analogous result for guarded second-order logic (GSO), the variant of MSO that not only allows quantification over vertex sets but also over edge sets. A key tool in our proof is a Feferman-Vaught-type theorem that is constructive and still works for unbounded partitions.