{"id":"84f70a85-b994-4e3a-89f3-e009f2ebec85","arxiv_id":"2501.13903","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A hereditary graph class has bounded shrub-depth if and only if it forbids flipped half-graphs and flipped unions of long paths, which happens exactly when MSO is no more expressive than FO.","lead":"This paper identifies the exact substructures that force a hereditary graph class to be logically complex, and shows when monadic second-order logic has no extra power over first-order logic. It resolves open questions about bounded shrub-depth and the expressive power of MSO.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 6.10 is false as stated: for G=2P_3, t=3, q=1, nibble1 has an isolated vertex while nibble2 does not, so FO_1 types differ; this flaw is load-bearing for the FO/MSO separation on flipped tP_t classes.","rationale":"The central theorem 1.1 requires showing that every hereditary class of unbounded shrub-depth has MSO more expressive than FO. The proof splits into two cases: classes with arbitrarily large flipped half-graphs (Lemma 6.8) and classes with arbitrarily large flipped tP_t (Lemma 6.9). Lemma 6.9 relies on Lemma 6.10, which asserts an FO-equivalence between two nibbles of a flipped mP_t. I found a concrete counterexample: for q=1, t=3, m=2, the two nibbles of 2P_3 are distinguished by the FO_1 sentence 'there exists an isolated vertex'. This falsifies Lemma 6.10 as stated. The flaw also appears in the proof: the bijection f in the Hanf argument does not preserve balls of radius 3q−1 when t=3q, because balls from the swapped middle reach the missing endpoints. The lemma is likely repairable by strengthening the bound to t ≥ 6q+1 (so no ball meets both a swapped segment and a modified end) and adjusting the threshold in f accordingly. Since the paper's theorem may still be true, I recommend a CONDITIONAL verdict: the manuscript must correct Lemma 6.10 and its use in Lemma 6.9. The previously noted δ2 typo in Lemma 4.9 is minor by comparison. I do not find a flaw in the black-box Theorem 2.11 that the reader flagged; that reliance is legitimate, though it should be stated prominently. The new concrete error is more load-bearing because it is internal to the main proof.","tokens_in":27009,"tokens_out":39909,"duration_ms":314876,"concrete_test":"Verify the counterexample: for G=2P_3 (unflipped), compute nibble1 and nibble2 and check that the FO_1 sentence ∃x∀y¬E(x,y) distinguishes them. Then inspect the Hanf bijection in Lemma 6.10 for q=2, t=6: show that the 5-ball around (1,4) in G+_1 has 4 vertices while its image (2,4) in G+_2 has a 5-vertex ball, confirming the bijection does not preserve ball types. This demonstrates the proof of Lemma 6.10 is invalid; a corrected proof should use the larger threshold t ≥ 6q+1.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Lemma 6.10 claims that for every q≥1 and every flipped mP_t with m≥2 and t≥3q, tp(nibble1(G), FO_q) = tp(nibble2(G), FO_q). This is false. Take q=1, t=3, m=2, and G=2P_3 with no flips. nibble1 removes (1,1) and (1,3), leaving the isolated vertex (1,2) plus a P_3. nibble2 removes (1,1) and (2,3), leaving two P_2 components. The FO_1 sentence α=∃x∀y¬E(x,y) holds in nibble1 but fails in nibble2, contradicting the lemma. This lemma is essential: Lemma 6.9 uses it to prove that MSO is more expressive than FO on hereditary classes containing flipped tP_t for all t, and sets t=3q, m=9. The counterexample persists for m=9, so the proof of Lemma 6.9 fails at least for q=1. More broadly, the Hanf-locality bijection f in the proof of Lemma 6.10 does not preserve (3q−1)-balls when t=3q: a vertex near position 3q/2 has a ball reaching the modified left end (missing (1,1)) in one nibble but not in the other, changing the ball type. The argument can likely be repaired by requiring t ≥ 6q+1 (so no ball reaches both a swapped segment and a modified end) and adjusting the swap threshold accordingly, but as written the paper contains a false lemma in a central step.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper characterizes hereditary graph classes of bounded shrub-depth by explicit forbidden induced subgraphs: for some t, all flipped half-graphs H_t and all flipped tP_t (or equivalently flipped 3P_t) are excluded. From this it derives a chain of equivalences with MSO-stability, monadic CMSO-stability, failure to 1-dimensionally FO-interpret the class of all paths, and equality of the expressive power of FO and MSO. The proof strategy goes through flip-flatness: pattern-free classes are shown to be ∞-flip-flat using the author's earlier stability/flatness characterizations, and classes with unbounded shrub-depth are shown to FO-interpret all paths. The FO/MSO separation is proved separately for flipped half-graphs and for flipped tP_t, using pairs of 'nibbled' graphs that are claimed to be FO-indistinguishable but MSO-distinguishable.","tokens_in":27379,"tokens_out":33289,"duration_ms":298350,"significance":"If correct, Theorem 1.1 would resolve the Elberfeld–Grohe–Tantau question on hereditary classes where FO and MSO coincide, confirm a conjecture of Gajarský and Hliněný, and give the first explicit forbidden-induced-subgraph characterization of bounded shrub-depth. The strengthening from FO-transductions to 1-dimensional FO-interpretations in Theorem 1.7 is a substantial improvement over prior work. The paper is carefully written and the main non-structure arguments are largely self-contained, with explicit interpretations and locality arguments. However, the proof contains a false central lemma in Section 6.3, so the claimed separation of FO and MSO on classes containing flipped tP_t is not established as submitted; this affects Theorem 1.9 and item 9 of Theorem 1.1.","major_comments":[{"comment":"Lemma 6.10 is false as stated. Take q=1, t=3, m=2, and G=2P_3 with no flips. Then nibble1(G) is P_1 ∪ P_3, while nibble2(G) is 2P_2; the FO_1 sentence ∃x∀y¬E(x,y) holds in the former and fails in the latter, contradicting the claimed equality of FO_1 types. The failure is not an isolated edge case: for t=3q, the (3q−1)-balls used in the Hanf argument have different size counts in G+1 and G+2, because G+1 has a P_t component while G+2 has only two P_{t−1} components. In the proof's bijection f, for example with q=2 and t=9, the ball of radius 5 at (1,4) in G+1 has 7 vertices, while its image (2,4) in G+2 has 8 vertices, so f does not preserve ball isomorphism types. Since Lemma 6.9 chooses t=3q and relies on Lemma 6.10 to equate the FO_q types of the two nibbles, the proof of Lemma 6.9, and hence the flipped-tP_t case of Proposition 6.1, is incomplete. A repair may be possible by taking t≥6q+1 and moving the swap threshold to 3q+1, but the statement and proof as written are incorrect.","section":"Section 6.3, Lemma 6.10"}],"minor_comments":[{"comment":"In the definition of δ2(x), the formula quantifies y3 and y4 but then refers to twins(y1,y2), which is outside the scope of those quantifiers; it should read twins(y3,y4).","section":"Section 4.2, Lemma 4.9"},{"comment":"The definition of M∞(m) appears to contain a typo: it is written as M_{2t}(max(2m, 2k_t^{2t}·t)), but the application of Corollary 3.11 to the k_{2t}-flip H requires the quantity 2k_{2t}^t·t. Please replace k_t^{2t} with k_{2t}^t and check the exponent against the statement of Corollary 3.11.","section":"Section 3.2, Proposition 3.1"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nQuick take: the paper has a real main result and a false lemma. The characterization of hereditary classes of bounded shrub-depth by forbidden flipped half-graphs and flipped tP_t is new and answers the Elberfeld-Grohe-Tantau question; the FO-interpretation of all paths (Prop 4.1) improving the transduction result is genuinely valuable. Sections 3-5 are careful and mostly check out. Credit where due: the flip-flatness argument, the definability claims in Lemmas 4.4 and 4.9 (modulo one typo), and the use of stability are all sound as far as I checked.\n\nSoft spots. First, Lemma 6.10 is false as stated. Take q=1, t=3, m=2, G=2P_3 with no flips. nibble1 leaves an isolated vertex; nibble2 leaves two P_2s. The FO_1 sentence \"exists x forall y not E(x,y)\" separates them. This is not a corner case: Lemma 6.9 uses Lemma 6.10 at exactly t=3q with m=9, so that proof fails for q=1. The Hanf-type bijection in 6.4 cannot work because the 3q-1 ball around the isolated vertex has no matching ball in the other nibble. The lemma might be repairable with t >= 6q+1 and a shifted swap, but as written it is false.\n\nSecond, Lemma 4.9 has a formula typo: delta2 quantifies y3,y4 but then says twins(y1,y2); it should be twins(y3,y4). That one is minor.\n\nThe bigger question is whether the false lemma is load-bearing. In the paper as written, yes: it is the proof of Lemma 6.9. But the same paper already contains a sound route to the same conclusion: Proposition 4.1 plus Lemma 6.7. If a hereditary class contains arbitrarily large flipped tP_t, Prop 4.1 FO-interprets all paths, and Lemma 6.7 gives the MSO/FO separation. So Theorem 1.1 is very likely correct; the nibble section should be rewritten or deleted, and a referee should request that.\n\nCitation pattern: several key black boxes are from the author's own group (Theorem 2.11 from [13,14], Theorem 3.4 from [11]), but those are published, and the new work builds on them transparently. Not a problem by itself.\n\nVerdict: the central theorem is important and probably right, but the manuscript contains a demonstrably false lemma in a proof of a main application. It deserves a serious referee and a major revision, not a desk reject. I would not cite it until the nibble argument is fixed or removed.\n\nBest.","headline":"Main characterization likely correct and important, but Lemma 6.10 is false as stated and the nibble-based proof of Lemma 6.9 needs replacing.","tokens_in":27883,"tokens_out":8365,"would_cite":false,"duration_ms":72463,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03C45","05C75","68Q19","03B70"],"pacs":[],"model":"deepseek-v4-flash","headline":"For hereditary graph classes, this paper proves that bounded shrub-depth is equivalent to MSO-stability and to FO and MSO having the same expressive power, via a forbidden-induced-subgraph characterization.","keywords":["forbidden induced subgraphs","shrub-depth","MSO-stability","monadic stability","FO and MSO expressive power","flip-flatness","half-graphs","FO-interpretations"],"falsifier":"Exhibit a hereditary graph class that, for some fixed t, contains no induced flipped half-graph H_t and no induced flipped tP_t, yet has unbounded shrub-depth; Theorem 1.6 says no such class exists. Equivalently, find a hereditary class of unbounded shrub-depth on which FO and MSO define exactly the same sentences, contradicting Theorem 1.9.","tokens_in":26821,"feed_emoji":"🌳","tokens_out":6955,"duration_ms":60918,"temperature":0.7,"pith_summary":"This paper establishes a sharp dividing line for hereditary graph classes: bounded shrub-depth is equivalent to a cluster of logical properties, including MSO-stability, CMSO-stability, and equality of expressive power between first-order logic and monadic second-order logic. The new combinatorial core is a forbidden induced subgraph characterization: a hereditary class has unbounded shrub-depth exactly when it contains arbitrarily large flipped half-graphs or flipped disjoint unions of many paths. Combined with an earlier result that FO and MSO coincide on bounded shrub-depth classes, this fully answers the question of which hereditary classes have the same FO and MSO theories. It also strengthens a known result by showing that every hereditary class of unbounded shrub-depth FO-interprets the class of all paths.","feed_headline":"Unbounded shrub-depth makes MSO stronger than FO","feed_subtitle":"Hereditary classes where first-order and monadic second-order logic coincide are exactly those of bounded shrub-depth.","key_machinery":"The load-bearing objects are flipped half-graphs and flipped tP_t: graphs obtained from half-graphs or from disjoint unions of t-vertex paths by complementing edges between parts of a fixed vertex partition. The proof proceeds through ∞-flip-flatness, the property that every sufficiently large vertex set contains a large subset that can be made pairwisely disconnected by a bounded number of flips. A technical engine is the uniqueness of irreducible flip-witnesses, which lets the construction detect which edges were flipped and undo them; this yields a single FO-interpretation that recovers all paths from any hereditary class containing arbitrarily large flipped patterns.","core_discovery":"The paper claims Theorem 1.1: for every hereditary graph class C, bounded shrub-depth is equivalent to excluding all flipped half-graphs of a fixed order and all flipped tP_t; to MSO-stability, monadic MSO-stability, CMSO-stability, and monadic CMSO-stability; to not 1-dimensionally FO-interpreting the class of all paths; and to FO and MSO having the same expressive power on C. The central new step is showing that any class containing arbitrarily large flipped half-graphs or flipped tP_t can FO-interpret all paths, and conversely that any class avoiding these patterns is ∞-flip-flat, hence of bounded shrub-depth.","pith_inferences":["Editorial inference: the uniform interpretation constructed in Proposition 4.1 suggests that lower bounds or inexpressibility results proved for paths may transfer automatically to every hereditary class of unbounded shrub-depth, without needing to know the class's specific structure.","Editorial inference: the 3P_t variant raises a natural testable next step: determine whether replacing 3P_t by 2P_t still characterizes bounded shrub-depth, or whether 2P_t already allows unbounded shrub-depth.","Editorial inference: the dependence analog stated in the appendix points toward a possible clique-width or rank-width characterization of MSO-dependence in hereditary classes, a direction the paper raises as a conjecture rather than a proved theorem."],"forward_implications":["On every hereditary class of bounded shrub-depth, FO and MSO have exactly the same expressive power, and on every hereditary class of unbounded shrub-depth, MSO is strictly more expressive than FO.","For hereditary graph classes, MSO-stability, monadic MSO-stability, CMSO-stability, and monadic CMSO-stability all coincide with bounded shrub-depth.","Every hereditary class of unbounded shrub-depth 1-dimensionally FO-interprets the class of all paths, improving the earlier FO-transduction result.","For monotone graph classes, MSO-stability coincides with bounded tree-depth."],"supporting_citations":[{"why":"Supplies the ∞-flip-flatness characterization of bounded shrub-depth and the flip-flatness characterization of FO-stability that the proof uses as a black box in Sections 2.8 and 3.2.","marker":"[14]"},{"why":"Establishes the forward direction that FO and MSO coincide on bounded shrub-depth classes, completing the equivalence in Theorem 1.9.","marker":"[18]"},{"why":"Shows every class of unbounded shrub-depth FO-transduces the class of all paths; this paper strengthens that result to 1-dimensional FO-interpretations.","marker":"[32]"},{"why":"Characterizes monadic FO-stability through flip-flatness and supplies flatness tools used in proving pattern-free classes are flip-flat.","marker":"[13]"},{"why":"Gives the forbidden-subgraph characterization of monadic FO-stability that yields Lemma 3.6 about flipped crossings and half-graphs.","marker":"[11]"},{"why":"Provides the finite Hanf locality theorem used to prove that the two nibbled graphs in Lemma 6.10 have equal FO-types.","marker":"[16]"},{"why":"Supplies the singleton-variable reduction for the order property that the appendix adapts to finite classes and richer logics in Lemma 5.3.","marker":"[36]"},{"why":"Introduces shrub-depth and the equivalent SC-depth parameter used throughout the paper.","marker":"[20]"}],"fun_headline_variants":["Forbidden flips pinpoint bounded shrub-depth classes","MSO outruns FO on exactly the unbounded shrub-depth hereditary classes","Hereditary classes: MSO stronger than FO iff shrub-depth unbounded","Conjecture confirmed: MSO outruns FO exactly when shrub-depth unbounded","New proof: unbounded shrub-depth lets FO interpret all paths"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The argument treats as a black box the prior theorem that a class has bounded shrub-depth exactly when every sufficiently large vertex set contains a large subset that can be made pairwisely disconnected by a bounded number of flips; if that theorem is flawed, the new equivalences no longer follow even if every new lemma is correct.","fun_headline_variants_meta":{"raw":{"variants":["Forbidden flips pinpoint bounded shrub-depth classes","MSO outruns FO on exactly the unbounded shrub-depth hereditary classes","Hereditary classes: MSO stronger than FO iff shrub-depth unbounded","Conjecture confirmed: MSO outruns FO exactly when shrub-depth unbounded","New proof: unbounded shrub-depth lets FO interpret all paths"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00068,"raw_usage":{"total_tokens":3099,"prompt_tokens":967,"completion_tokens":2132,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":583,"completion_tokens_details":{"reasoning_tokens":2039}},"tokens_in":583,"tokens_out":2132,"duration_ms":12530,"temperature":1.0,"reasoning_tokens":2039,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T15:29:01.674699+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a hereditary graph class that, for some fixed t, contains no induced flipped half-graph H_t and no induced flipped tP_t, yet has unbounded shrub-depth; Theorem 1.6 says no such class exists. Equivalently, find a hereditary class of unbounded shrub-depth on which FO and MSO define exactly the same sentences, contradicting Theorem 1.9.","supporting_citations":[{"cited_title":"Flip-breakability: A combinatorial dichotomy for monadically dependent graph classes","cited_arxiv_id":null,"evidence_quote":"Supplies the ∞-flip-flatness characterization of bounded shrub-depth and the flip-flatness characterization of FO-stability that the proof uses as a black box in Sections 2.8 and 3.2."},{"cited_title":"Kernelizing mso properties of trees of fixed height, and some consequences","cited_arxiv_id":null,"evidence_quote":"Establishes the forward direction that FO and MSO coincide on bounded shrub-depth classes, completing the equivalence in Theorem 1.9."},{"cited_title":"Transducing paths in graph classes with unbounded shrubdepth","cited_arxiv_id":null,"evidence_quote":"Shows every class of unbounded shrub-depth FO-transduces the class of all paths; this paper strengthens that result to 1-dimensional FO-interpretations."},{"cited_title":"Indiscernibles and flatness in monadically stable and monadically NIP classes","cited_arxiv_id":null,"evidence_quote":"Characterizes monadic FO-stability through flip-flatness and supplies flatness tools used in proving pattern-free classes are flip-flat."},{"cited_title":"First-Order Model Checking on Monadically Stable Graph Classes","cited_arxiv_id":null,"evidence_quote":"Gives the forbidden-subgraph characterization of monadic FO-stability that yields Lemma 3.6 about flipped crossings and half-graphs."},{"cited_title":"Stockmeyer, and Moshe Y","cited_arxiv_id":null,"evidence_quote":"Provides the finite Hanf locality theorem used to prove that the two nibbled graphs in Lemma 6.10 have equal FO-types."},{"cited_title":"When trees grow low: Shrubs and fast MSO1","cited_arxiv_id":null,"evidence_quote":"Introduces shrub-depth and the equivalent SC-depth parameter used throughout the paper."}],"review_version":1}