Trees,grids, and MSO decidability: From graphs to matroids

Monadic second order (MSO) logic has proved to be a useful tool in many areas of application, reaching from decidability and complexity to picture processing, correctness of programs and parallel processes. To characterize the structural borderline between decidability and undecidability is a classical research problem here. This problem is related to questions in computational complexity, especially to the model checking problem, for which many tools developed in the area of decidability have proved to be useful. For more than two decades it was conjectured in [D. Seese, The structure of the models of decidable monadic theories of graphs, Ann. Pure Appl. Logic 53 (1991) 169–195] that decidability of monadic theories of countable structures implies that the theory can be reduced via interpretability to a theory of trees.