Lax Lean Archive

First-Order Model Checking on Monadically Dependent Graph Classes

lax-185574·formalized by Jan Dreier @jan3er · Nikolas Mählmann @nmaehlmann · Szymon Toruńczyk @szymtor·registered·created ·GitHub @2184fc6·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    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)|U|^{O(1)} types of fixed quantifier rank over any set of parameters UU.

    View annotated paper

    65 pages · 151 marked passages

    Concepts

    Concept map
    96 concepts
    100%
    Algorithms and their running timesAtomically matched tuplesAtomic types of vertices and of pairsA definable flip separating a ball one stepfurtherFew atomic types in balls avoiding a closureMerge sequences with definable stages fromchainsA four-part flip of a bipartite graph withshort edges in both polaritiesBipartite graphs and bipartite complementsHomogeneous rectangles for colorings of pairsof tuplesBounded VC-dimension of monadicallydependent classesCanonical formLocally definable construction sequencesfrom chainsChains of vertex sets with few atomic typesin flip-metric ballsChains and their radius-r widthClosure theoremClosure theorem for tuplesClustering of a tupleColorings of graphsA graph or its complement has diameter atmost 3Computing the scatter typeComputing chains of small widthModel checking along a constructionsequenceConstruction sequencesRadius-r width of a construction sequenceThe edges of a definable flip arequantifier-free definableTransitivity of definable flipsDefinable flipsComputing locally definable constructionsequencesLocal definability bounds the widthDistance logic over partial graphs anddistance rankThe distance matrix of a partial graphEncoding data as lists of numbersHow inputs are given to algorithmsEvaluation of distance formulas on type treesFar composition of type treesThe far treeConstruction sequences with few realizedtypesFirst-order logic on colored graphsTypes of bounded quantifier rankRefining a partition increases the flip metricFlips and flip metricsDefinable flips preserve monadic dependenceMonadically dependent classes exclude largeφ-patternsMonadically dependent classes exclude large(φ, ψ)-patternsGaifman graph, distances, balls and inducedsubstructuresGaifman's locality theorem with a rankboundBalls around vertex sets in a graphGraphs and graph classesSplitting by a transversal gives a partitionhomogeneous modulo the pair relationMonadic dependence through theindependence propertyLocally definable construction sequencesLocal formulas and basic local sentencesLocal formulas are evaluated in any supersetof the ballTypes are determined by types in aneighborhoodMany atomic types force atomically matchedtuplesLifting type trees through a mergeMerge sequences and their radius-r widthFrom merge sequences to locally definableconstruction sequencesFirst-order model checking on monadicallydependent graph classesMonadically dependent graph classesPolynomial neighborhood complexity frombounded VC-dimensionPairs at distance at most 5 in both polaritiesBalls of the pair relation lie in flip-metricballsThe pair relation of atomic types is definableThe pair relation grows under coarseningPartial graphsConverting the flip metric of a partition intoa single flipPartitions, transversals and the partition intoatomic typesφ-patterns(φ, ψ)-patternsRank shift of type treesLifting type trees through a resolveOrdered coordinate restriction of type treesRestriction of scatter typesScatter typesFew types far from a parameter setFew types far from a parameter set, with afixed tuple of parametersSplitting by a transversal keeps few parts inflip-metric ballsSplitting by minimal representativespreserves coarseningComputing the far treeType trees are distance typesLocality of type treesPolynomial bound on the number of typesover a parameter setSplitting the parts of a partition by atomictypes over a setType tree sizesType trees and their canonical representationNeighborhood complexity and VC-dimensionBounded-VC dualityRadius-r depth-q width of a constructionsequenceGraph classesNeighborhood complexityColored graphs and walk distanceDistance logic and distance rankFirst-order logic on graphsFirst-order transductionsThe word RAM
    Proven claimDefinitionThis submissionOther submissionA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Proofs

    Proof networkview on GitHub

    100%
    premise files concept fileProven claimClaim from this submission / another submissionAll proofs of one concept — hover for individual statements and proofs
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on AA → B: only B's proofs build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-185574,
  author = {Jan Dreier and Nikolas Mählmann and Szymon Toruńczyk},
  title = {First-Order Model Checking on Monadically Dependent Graph Classes},
  year = {2026},
  howpublished = {Lax Archive, lax-185574},
  url = {https://laxarchive.org/lax-185574/},
}

    References

    1. Jan Dreier, Nikolas Mählmann and Szymon Toruńczyk. First-Order Model Checking on Monadically Dependent Graph Classes. 2026. arXiv:2611.08143
    2. Jan Dreier, Nikolas Mählmann, Michał Pilipczuk and Szymon Toruńczyk. Monadically Dependent Graph Classes Have Almost Bounded Merge-Width. 2026. arXiv:2611.06804

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…