Seese's theorem

Statement

The satisfiability problem for a sentence of monadic second-order logic is the problem of determining whether there exists at least one graph (possibly within a restricted family of graphs) for which the sentence is true. For arbitrary graph families, and arbitrary sentences, this problem is undecidable. However, satisfiability of MSO₂ sentences is decidable for the graphs of bounded treewidth, and satisfiability of MSO₁ sentences is decidable for graphs of bounded clique-width. The proof involves using Courcelle's theorem to build an automaton that can test the property, and then examining the automaton to determine whether there is any graph it can accept. As a partial converse, (Seese 1991) proved that, whenever a family of graphs has a decidable MSO₂ satisfiability problem, the family must have bounded treewidth. The proof is based on a theorem of Robertson and Seymour that the families of graphs with unbounded treewidth have arbitrarily large grid minors. Seese also conjectured that every family of graphs with a decidable MSO₁ satisfiability problem must have bounded clique-width. This has not been proven, but a weakening of the conjecture that extends MSO₁ with modular counting predicates is true.