Pith. sign in

REVIEW 1 major objections 5 minor 1 cited by

Low rank MSO

T0 review · 1 major / 5 minor · reviewed 2026-08-08 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper introduces low rank MSO, a fragment of monadic second-order logic that restricts set quantification to vertex sets of bounded cutrank, and proves it equivalent over all undirected graphs to flip-reachability logic—so every…

desk verdict Strong, well-proved logic paper: low rank MSO is a genuine new fragment with clean equivalences and a polynomial-time corollary; worth a careful referee. read the letter →

arxiv 2502.08476 v1 pith:MYLRYGDB submitted 2025-02-12 cs.LO

Miko{l}aj Bojańczyk , Micha{l} Pilipczuk , Wojciech Przybyszewski , Marek Soko{l}owski , Giannos Stamoulis This is my paper · ORCID
classification cs.LO MSC 03B7003C1305C8568Q19
keywords lowrankMSOcutrankmonadicsecond-orderlogicflip-reachabilityseparatordefinableflipsVCdimensionpolynomial-timemodelchecking
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Low rank MSO is a fragment of monadic second-order logic in which set quantifiers may range only over vertex sets whose cut—the bipartite adjacency matrix between the set and its complement—has bounded rank over the two-element field. The paper's central claim is that on undirected graphs this logic has exactly the expressive power of flip-reachability logic, the first-order extension with reachability predicates evaluated after flipping adjacency patterns around a bounded tuple of parameter vertices. If that claim is right, then every graph property definable in low rank MSO is decidable in polynomial time, giving a completely new tractable island inside MSO on dense graphs. The paper also shows that over weakly sparse classes low rank MSO coincides with the known separator logic, and over classes of bounded VC dimension it coincides with the symmetric flip-connectivity logic—but that on all graphs it is strictly stronger than flip-connectivity logic. A sympathetic reading of the proof places the weight on a structure theorem: every low-rank set can be represented as the span of a 'seed' partition defined by three flip-reachability formulas from a bounded parameter tuple.

What carries the argument

The load-bearing object is the seed: a partition of the vertex set into a forced-in part X+, a forced-out part X−, and free parts X∼, whose span is X+ plus any union of free parts. A seed is a-uniform when vertices that are twins with respect to the parameter tuple a are also twins with respect to everything outside their own parts; this uniformity is what lets a flip defined by atomic types behave correctly. The Low Rank Structure Theorem (Theorem 6.1) states that for each r, the family of all rank-≤r vertex sets is exactly the union, over all parameter tuples of length k(r), of spans of a-uniform seeds defined by three fixed flip-reachability formulas. The proof chain runs: low-rank sets become suffixes of a definable flip (Lemma 6.2, using representatives of size at most 2^r supplied by the cutrank literature), suffixes are covered by seeds anchored at a bounded antichain of strongly connected components (Lemma 6.8), and the antichain can be witnessed by a bounded tuple of vertices because a minimal cover has size at most |atp_{k+1}|^2 (Lemma 6.11).

What would settle it

A concrete refutation would be a graph G and a vertex set X of cutrank at most r that, for every parameter tuple a of length k(r), lies outside Span(Seed(φ+, φ−, φ∼, a)) for the formulas constructed in Theorem 6.1; a brute-force search over all undirected graphs on up to ten vertices with r = 1 or r = 2 would settle this directly. A second independent check: fix a low-rank MSO sentence and its claimed flip-reachability translation, and search for a graph on which the two disagree.

Watch

Extended reading notes

Core claim

On every undirected graph, the sets of vertices of cutrank at most r are exactly the spans of seeds defined by fixed flip-reachability formulas from a parameter tuple of length k(r). This Low Rank Structure Theorem is proved by first showing that low-rank sets are precisely the suffixes of a directed graph obtained from the original graph by a definable flip around a bounded tuple (Lemma 6.2), and then showing that the family of suffixes of any such flip is covered by spans of seeds parameterized by a bounded antichain of strongly connected components (Lemma 6.8). From this characterization the paper derives the equivalence of low rank MSO with flip-reachability logic, and hence Corollary 1.5: every low-rank-MSO-definable graph property is decidable in polynomial time. On weakly sparse classes the same framework yields equality with separator logic, and on bounded-VC-dimension classes with flip-connectivity logic; a separate construction shows low rank MSO strictly exceeds flip-connectivity logic on all graphs.

Load-bearing premise

The argument stands or falls on the Low Rank Structure Theorem: that every vertex set of cutrank at most r can be captured as the span of a seed defined by flip-reachability formulas from a parameter tuple whose length depends only on r. If the antichain/cover argument in Lemma 6.11 has a hidden gap, the equivalence with flip-reachability logic—and the polynomial-time corollary—loses its foundation. The bounded-VC-dimension equivalence additionally takes a cited duality-based structure theorem (Theorem 5.9) as a black box.

Editorial extensions

If this is right

  • Every graph property expressible in low rank MSO can be decided in polynomial time, and the translation is effective, yielding a uniform XP model-checking algorithm.
  • Over weakly sparse graph classes, low rank MSO is no more expressive than separator logic, confirming that the new logic is a faithful dense analogue of the sparse connectivity logic.
  • Over classes of bounded VC dimension, low rank MSO coincides with flip-connectivity logic, but not over all graphs, where low rank MSO is strictly stronger.
  • Since flip-reachability predicates are themselves expressible in low rank MSO, the two logics have exactly equal expressive power on all undirected graphs.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the structure theorem's proof pattern generalizes, the seed/span machinery may yield polynomial-time model checking for low rank MSO on binary relational structures and matroids, where the paper sketches natural definitions but proves nothing.
  • The strict separation between flip-connectivity and flip-reachability logic shows that allowing directed, asymmetric flips adds genuine expressive power even on undirected inputs; a directed-graph analogue of Theorem 1.4, which the paper leaves open, would be a natural test of whether flip-reachability logic is the 'right' dense counterpart of separator logic.
  • The equivalence collapses bounded-rank set quantification into first-order reachability queries; replacing reachability with other non-first-order transitive closures, such as parity reachability, would probe whether the polynomial-time corollary is robust or fragile.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 5 minor

Summary. The paper introduces low rank MSO, the fragment of MSO over undirected vertex-colored graphs in which set quantifiers range over vertex sets of bounded cutrank. It proves three expressive completeness theorems: equality with separator logic on weakly sparse classes (Theorem 1.1), equality with flip-connectivity logic on classes of bounded VC dimension plus a separation on all graphs (Theorems 1.2 and 1.3), and equality with flip-reachability logic on all undirected graphs (Theorem 1.4). The final equivalence yields Corollary 1.5 stating that every property expressible in low rank MSO is decidable in polynomial time. The central technical contribution is the Low Rank Structure Theorem (Theorem 6.1), which represents every low-rank set as an element of the span of an a-uniform seed defined by flip-reachability formulas from a bounded tuple of parameters.

Significance. If the proof is correct, this is a substantial contribution: it provides a dense analogue of separator logic, a transfer principle from a rank-restricted fragment of MSO to an FO-like logic, and a polynomial-time meta-theorem for arbitrary undirected graphs. The proof architecture is modular: a general low-rank definability framework (Section 3), a sparse case built on a separation characterization (Section 4), a bounded-VC case using duality (Section 5), and an all-graphs case via suffixes of flips (Section 6). The paper is careful about what is proved and what is imported: the external duality theorem (Theorem 5.9) is used only for Theorem 1.3, and the effective translation underlying uniform XP is explicitly flagged as omitted. The construction in Theorem 6.1 is concrete and checkable, and the negative result of Theorem 1.2 is itself informative. No circularity or parameter fitting is involved.

major comments (1)
  1. [§6.1.2, Claim 6.13] In the proof of Claim 6.13, the final contradiction in the case u′1v′2 ∈ E(H) is not derived correctly as printed. From the path u1 → v2 and the fact that ¬(u1 < v2), one gets v2 ⩽ u1; combined with u2 < v2 this yields u2 ⩽ u1, with u1 ∼ u2 excluded by the choice of v1 (otherwise u2 < v1 would follow). Hence u2 < u1, contradicting either the choice of v1 (since u2 < v1 would then hold by transitivity) or the minimality of B+. The sentence "since u1 < v1 and u2 < v2, we find that u1 < v2" should be corrected, and the symmetric case should be checked against the same repair. This step is load-bearing for the bound |B+| ≤ |atpk+1|² and therefore for Lemma 6.11 and Theorem 6.1.
minor comments (5)
  1. [§6.2, Claim 6.17] The text refers several times to "q-flip-connectivity type" and "r-flip-connectivity type" in a proof about flip-reachability logic; these should be "q-flip-reachability type" and "r-flip-reachability type". The EF transfer also deserves one sentence explaining that vertices in one part have identical flip-reachability behavior because they lie in the same strongly connected component of the relevant flip.
  2. [§2, Lemma 2.2] The formula φk,F(X) is said to "existentially quantify C and D as sets"; since φ is claimed to be an FO formula, the intended meaning must be quantification over a bounded tuple of vertices with a disjunction over possible partitions. Please make this explicit.
  3. [§5.1] The proof that Gn and G′n are indistinguishable by FO sentences of quantifier rank o(log n) is invoked as "standard" without a proof or reference; given the iterated-exponential size of the layers, an explicit EF argument or citation would help.
  4. [Footnote 2 and end of §1] The claim that the translation in Theorem 1.4 can be made effective, yielding uniform XP, is stated without details. Since Corollary 1.5 only needs non-uniform XP this does not affect the main theorem, but the uniform claim should either be proved in an appendix or explicitly labeled as an open point.
  5. [§4, Lemma 4.2 (Claim 4.3)] The "standard argument involving Ehrenfeucht–Fraïssé games" for separator logic is not detailed. The paper would be easier to verify if the type-counting argument were sketched, especially since the same argument is reused in Lemma 5.11.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the low rank MSO/flip-reachability equivalence is established by independent structural theorems.

full rationale

The paper's central claim, Theorem 1.4, is obtained through the general framework of Theorem 3.2, which reduces the task to verifying the low rank definability property for flip-reachability logic. This property is established in Lemma 6.16 using the Low Rank Structure Theorem (Theorem 6.1). The structure theorem itself is proved from Lemma 6.2, which characterizes low-rank sets as suffixes of definable flips, and Lemma 6.8, which parameterizes suffixes of definable flips by spans of seeds. These are genuine two-way inclusions proved in Lemmas 6.6, 6.7, 6.9, 6.10, and 6.11, not identities true by definition. The flip-reachability predicates are defined syntactically, independently of low rank MSO; Lemma 2.5 (their expressibility in low rank MSO) is used only for the converse inclusion and does not feed back into the main translation. The external duality-based theorem, Theorem 5.9, is cited from [2], whose authors do not overlap with the present paper, and it supports only Theorem 1.3 (bounded VC dimension), not Theorem 1.4 or Corollary 1.5. Self-citations, such as [1] for separator logic and [16] for a survey, are background and not load-bearing. The intricate claims in Lemma 6.11, including the counting argument in Claim 6.13 and the antichain/cover construction, are genuine combinatorial arguments rather than renamed assumptions. No fitted parameter is renamed as a prediction, and no cited uniqueness theorem is used to forbid alternatives. The derivation is therefore self-contained with respect to its central equivalence and polynomial-time corollary.

Assumptions & free parameters 0 free parameters · 5 assumptions · 3 invented entities

This paper introduces three new logics; their formal definitions are precise and the internal proofs give strong support (the equivalence theorems), but no independent external validation exists, so the invented-entities flag is set to False. The central theorems additionally rely on two cited external results from [2] (duality and small-set approximation) and one from [15] (representatives), plus standard finite-type/EF-game facts.

assumptions (5)
  • domain assumption Duality theorem for set systems of bounded VC dimension (Theorem 5.8, from [2]).
    Used to show that in bounded-VC-dimension graphs the edge relation has a duality of order k, a prerequisite for Lemma 5.10.
  • domain assumption Small-set approximation theorem for edges under a pseudometric (Theorem 5.9, [2, Theorem 3.5]).
    Used in Lemma 5.10 to find a small set S such that edges between far-apart vertices depend only on adjacency to S.
  • domain assumption Representative existence for sets of bounded rank (Proposition 6.3, from Oum and Seymour [15]).
    Used to pick representatives R+ and R- of size at most 2^r for a low-rank set and its complement, the starting point for the suffix characterization in Lemma 6.2.
  • standard math Standard Ehrenfeucht-Fraisse game characterization of FO equivalence and finiteness of types of bounded quantifier rank.
    Invoked in Lemmas 4.2, 5.11, and Claim 6.17 to show that formulas are invariant under replacing sets that agree up to a bounded number of components/parts of each type.
  • standard math Basic linear algebra facts about rank over finite fields (Lemma 2.1).
    Used to argue that the choice of field for cutrank is immaterial and that rank is FO-definable (Lemma 2.2).
invented entities (3)
  • Low rank MSO
    purpose: A new logic: MSO with set quantification restricted to vertex sets of cutrank at most r. Central object of study.
    New formalism, precisely defined. The paper gives internal evidence of robustness via equivalence theorems with existing logics, but there is no external (outside-the-paper) confirmation.
  • Flip-connectivity logic
    purpose: FO extension with flip-connectivity predicates; intended as a dense analogue of separator logic. Used to characterize low rank MSO on bounded-VC-dimension classes.
    New logic introduced by the authors; the paper proves equivalence with low rank MSO on bounded VC dimension and a strict separation on all graphs (Theorem 1.2). No external evidence.
  • Flip-reachability logic
    purpose: FO extension with flip-reachability predicates; proved equivalent to low rank MSO on all undirected graphs, yielding the polynomial-time model checking corollary.
    New logic introduced by the authors. Internal proof of equivalence; no external confirmation known.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Low rank MSO." pith.science (2026). https://pith.science/paper/MYLRYGDB

@misc{pith2026250208476,
  author       = {Pith},
  title        = {Pith review of: Low rank MSO},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MYLRYGDB}},
  note         = {Machine review of arXiv:2502.08476}
}
read the original abstract

We introduce a new logic for describing properties of graphs, which we call low rank MSO. This is the fragment of monadic second-order logic in which set quantification is restricted to vertex sets of bounded cutrank. We prove the following statements about the expressive power of low rank MSO. - Over any class of graphs that is weakly sparse, low rank MSO has the same expressive power as separator logic. This equivalence does not hold over all graphs. - Over any class of graphs that has bounded VC dimension, low rank MSO has the same expressive power as flip-connectivity logic. This equivalence does not hold over all graphs. - Over all graphs, low rank MSO has the same expressive power as flip-reachability logic. Here, separator logic is an extension of first-order logic by basic predicates for checking connectivity, which was proposed by Boja\'nczyk [ArXiv 2107.13953] and by Schirrmacher, Siebertz, and Vigny [ACM ToCL 2023]. Flip-connectivity logic and flip-reachability logic are analogues of separator logic suited for non-sparse graphs, which we propose in this work. In particular, the last statement above implies that every property of undirected graphs expressible in low rank MSO can be decided in polynomial time.

Figures

Figures reproduced from arXiv: 2502.08476 by the authors.

Figure 1
Figure 1. A separation. 4 Relation to separator logic In this section we prove Theorem 1.1. By Theorem 3.2, it suffices to show that for every weakly sparse graph class C , separator logic has low rank definability property on C . The plan is as follows. We first prove a combinatorial characterization of low rank sets in weakly sparse graph classes. Next, we use this characterization to prove low rank definability property. F… view at source ↗
Figure 2
Figure 2. Example graph G and construction of the digraph Ha¯ from an admissible tuple a¯. We first show that Ha¯ is indeed a flip of G with parameters a¯: Lemma 6.5. There exists a binary relation A ⊆ atpk+1 × atpk+1 such that, for any undirected graph G and any tuple a¯ ∈ V (G) k , we have Ha¯ = G ⊕a¯ A. 21 [PITH_FULL_IMAGE:figures/full_fig_p022_2.png] view at source ↗
Figure 3
Figure 3. Situation in the proof of Claim 6.13. Since p > | atpk+1 | 2 , we may assume, without loss of generality, that atp(u ′ 1 , a¯) = atp(u ′ 2 , a¯) and atp(v ′ 1 , a¯) = atp(v ′ 2 , a¯). Let us now define two boolean variables λuv, λvu ∈ {0, 1}: λuv = [(atp(u ′ 1 , a¯), atp(v ′ 1 , a¯)) ∈ A], λvu = [(atp(v ′ 1 , a¯), atp(u ′ 1 , a¯)) ∈ A]. By the definition of a flip, for all i, j ∈ [2], we have ⃗u ′ i v ′ j ∈ E(H) ⇐⇒ … view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. A combinatorial framework for clustering graph states: Algorithms and hardness for rank-integrity

    cs.DS 2026-07 accept novelty 7.0 of 10

    Rank integrity is XP in the rank parameter k yet W[1]-hard, and is equivalent up to a factor of two to ancilla integrity of graph states for clustering entanglement.

Reference graph

Works this paper leans on

23 extracted references · 21 canonical work pages · cited by 1 Pith paper

  1. [1]

    Separator logic and star-free expressions for graphs

    Mikołaj Boja ´nczyk. Separator logic and star-free expressions for graphs. ArXiv preprint , abs/2107.13953, 2021

    work page Pith review arXiv 2021

  2. [2]

    Model checking on interpretations of classes of bounded local cliquewidth

    ´Edouard Bonnet, Jan Dreier, Jakub Gajarsk´y, Stephan Kreutzer, Nikolas M¨ahlmann, Pierre Simon, and Szymon Toru´nczyk. Model checking on interpretations of classes of bounded local cliquewidth. In 30 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022 , pages 54:1–54:13. ACM, 2022

    work page 2022

  3. [3]

    The monadic second-order logic of graphs

    Bruno Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Information and Computation, 85(1):12–75, March 1990

    work page 1990

  4. [4]

    Makowsky, and Udi Rotics

    Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width. Theory of Computing Systems , 33(2):125–150, 2000

    work page 2000

  5. [5]

    First-Order model checking on monadically stable graph classes

    Jan Dreier, Ioannis Eleftheriadis, Nikolas M ¨ahlmann, Rose McCarty, Michał Pilipczuk, and Szymon Toru´nczyk. First-Order model checking on monadically stable graph classes. In 65th IEEE Annual Symposium on Foundations of Computer Science, FOCS2024 , pages 21–30. IEEE, 2024

    work page 2024

  6. [6]

    Indiscernibles and flatness in monadically stable and monadically NIP classes

    Jan Dreier, Nikolas M¨ahlmann, Sebastian Siebertz, and Szymon Toru´nczyk. Indiscernibles and flatness in monadically stable and monadically NIP classes. In 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, volume 261 ofLIPIcs, pages 125:1–125:18. Schloss Dagstuhl — Leibniz-Zentrum f¨ur Informatik, 2023

    work page 2023

  7. [7]

    Flip-breakability: A combinatorial dichotomy for monadically dependent graph classes

    Jan Dreier, Nikolas M¨ahlmann, and Szymon Toru´nczyk. Flip-breakability: A combinatorial dichotomy for monadically dependent graph classes. In 56th Annual ACM Symposium on Theory of Computing, STOC 2024, pages 1550–1560. ACM, 2024

    work page 2024

  8. [8]

    Flipper games for monad- ically stable graph classes

    Jakub Gajarsk ´y, Nikolas M¨ahlmann, Rose McCarty, Pierre Ohlmann, Michał Pilipczuk, Wojciech Przy- byszewski, Sebastian Siebertz, Marek Sokołowski, and Szymon Toru´nczyk. Flipper games for monad- ically stable graph classes. In 50th International Colloquium on Automata, Languages, and Program- ming, ICALP 2023, volume 261 of LIPIcs, pages 128:1–128:16. S...

    work page 2023

Show all 23 references
  1. [9]

    Twin-width and limits of tractability of FO model checking on geometric graphs

    Petr Hlin ˇen´y and Filip Pokr ´yvka. Twin-width and limits of tractability of FO model checking on geometric graphs. ArXiv preprint, abs/2204.13742, 2022

    2022 arXiv

  2. [10]

    Nondeterministic space is closed under complementation

    Neil Immerman. Nondeterministic space is closed under complementation. SIAM Journal on Com- puting, 17(5):935–938, 1988

    1988

  3. [11]

    Vertex-minors of graphs: A survey

    Donggyu Kim and Sang-il Oum. Vertex-minors of graphs: A survey. Discrete Applied Mathematics, 351:54–73, 2024

    2024

  4. [12]

    Local structure for vertex-minors

    Rose McCarty. Local structure for vertex-minors . PhD thesis, University of Waterloo, 2021. Available at http://hdl.handle.net/10012/17633

    2021

  5. [13]

    Counter-free automata

    Robert McNaughton and Seymour Papert. Counter-free automata. The M.I.T. Press, Cambridge, Mass.- London, 1971

    1971

  6. [14]

    Rank-width and vertex-minors

    Sang-il Oum. Rank-width and vertex-minors. Journal of Combinatorial Theory, Series B, 95(1):79–100, 2005

    2005

  7. [15]

    Sang-il Oum and Paul D. Seymour. Approximating clique-width and branch-width. Journal of Com- binatorial Theory, Series B, 96(4):514–528, 2006

    2006

  8. [16]

    Graph classes through the lens of logic

    Michał Pilipczuk. Graph classes through the lens of logic. ArXiv preprint, abs/2501.04166, 2025. 31

    2025 arXiv

  9. [17]

    Algorithms and data structures for first-order logic with connectivity under vertex failures

    Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Toru´nczyk, and Alexandre Vigny. Algorithms and data structures for first-order logic with connectivity under vertex failures. In49th In- ternational Colloquium on Automata, Languages, and Programming, ICALP 202...

    2022

  10. [18]

    Undirected connectivity in log-space

    Omer Reingold. Undirected connectivity in log-space. Journal of the ACM, 55(4):17:1–17:24, 2008

    2008

  11. [19]

    Flip-width: Cops and Robber on dense graphs

    Szymon Toru ´nczyk. Flip-width: Cops and Robber on dense graphs. In 64th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2023 , pages 663–700. IEEE, 2023

    2023

  12. [20]

    First-order logic with connectivity operators

    Nicole Schirrmacher, Sebastian Siebertz, and Alexandre Vigny. First-order logic with connectivity operators. ACM Transactions on Computational Logic , 24(4):1–23, 2023

    2023

  13. [21]

    On finite monoids having only trivial subgroups

    Marcel-Paul Sch ¨utzenberger. On finite monoids having only trivial subgroups. Information and Con- trol, 8:190–194, 1965

    1965

  14. [22]

    The method of forced enumeration for nondeterministic automata

    R ´obert Szelepcs´enyi. The method of forced enumeration for nondeterministic automata. Acta Infor- matica, 26(3):279–284, 1988

    1988

  15. [23]

    k-NLC graphs and polynomial algorithms

    Egon Wanke. k-NLC graphs and polynomial algorithms. Discrete Applied Mathematics, 54(2-3):251– 266, 1994. 32

    1994

Pith tools

Reviewed August 8, 2026 · model on record in the stance chip above.