First-Order Model Checking on Monadically Dependent Graph Classes
Abstract
Monadically dependent graph classes are those in which first-order logic cannot encode all graphs. They include all nowhere dense classes and all classes of bounded twin-width. We show that first-order model checking is fixed-parameter tractable on every monadically dependent graph class. Together with the known hardness result for hereditary classes that are not monadically dependent, this gives a complete characterization of the hereditary graph classes with fixed-parameter tractable first-order model checking. This resolves a central open problem in algorithmic model theory. Our proof combines ideas from structural graph theory (graph decompositions), finite model theory (locality of first-order logic), and model theory (counting types). In particular, we show that in monadically dependent classes, tuples of fixed length have only |U|O(1) types of fixed quantifier rank over any set of parameters U.
Related
- Monadically Dependent Graph Classes Have Almost Bounded Merge-Width
- On first-order limiting probabilities for small permutation classes
- FOSLS-deRhaNN: native de Rham neural classes for H(div) and H(curl) with applications to first-order system least-squares neural network methods for partial differential equations
- A Logic for Minor-Free Graph Classes: Model Checking, Dependence, and Combinatorial Reconfiguration
- MIXSim: A multiclass first order traffic model with composition-dependent dynamics for mixed-autonomy urban networks
BibTeX
@misc{dreier2026firstorder,
title = {{First-Order Model Checking on Monadically Dependent Graph Classes}},
author = {Jan Dreier and Nikolas Mählmann and Szymon Toruńczyk},
howpublished = {arXiv},
year = {2026},
month = nov,
doi = {10.48550/arxiv.2611.08143},
eprint = {2611.08143},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2611.08143},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - First-Order Model Checking on Monadically Dependent Graph Classes
AU - Jan Dreier
AU - Nikolas Mählmann
AU - Szymon Toruńczyk
PY - 2026
DA - 2026/11/05
PB - arXiv
DO - 10.48550/arxiv.2611.08143
UR - https://arxiv.org/abs/2611.08143
AB - Monadically dependent graph classes are those in which first-order logic cannot encode all graphs. They include all nowhere dense classes and all classes of bounded twin-width. We show that first-order model checking is fixed-parameter tractable on every monadically dependent graph class. Together with the known hardness result for hereditary classes that are not monadically dependent, this gives a complete characterization of the hereditary graph classes with fixed-parameter tractable first-order model checking. This resolves a central open problem in algorithmic model theory. Our proof combines ideas from structural graph theory (graph decompositions), finite model theory (locality of first-order logic), and model theory (counting types). In particular, we show that in monadically dependent classes, tuples of fixed length have only |U|^O(1) types of fixed quantifier rank over any set of parameters U.
ER -