{"id":"272f4d84-13cd-4772-872c-b382c5d81a91","arxiv_id":"2501.05385","paper_version":4,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"For any MSO formula over the infinite binary tree whose existential witness is well-founded, the minimal ordinal rank bound is either strictly below ω² or equal to ω1, and it is decidable which holds.","lead":"This paper proves that the smallest ordinal bound needed to measure well-founded witnesses in monadic second-order logic over the infinite binary tree is either below ω² or as large as possible, and that a computer can decide which case holds. The result clarifies the expressive power of MSO and yields a new, decidable proof that certain fixed-point formulae have closure ordinals below ω².","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified.","rationale":"The reader's verdict is ACCEPT with moderate confidence, and the weakest assumption flagged is the reliance on Büchi-Landweber finite-memory determinacy in Lemma 4.5. I agree that this is the pivotal step where the dichotomy's gap is created: without a finite-memory conversion from G∞_A to G^N_A, one could imagine intermediate countable ordinals filling the gap between ω and ω1. However, the application of Büchi-Landweber is correct. Lemma 4.5's pigeonhole argument is watertight: it tracks the game position, the memory state of ∀'s finite-memory strategy, and the automaton state on a back-marked path just after an R-to-T side change; after sufficiently many changes a repetition occurs, and splicing the intervening fragment forever produces a play consistent with the fixed strategy that satisfies A(∞), contradicting that the strategy is winning. I also checked the other intricate parts of the proof. Lemma 7.1, which provides the uniform positional strategy for Pathfinder in the auxiliary game, initially appears to contain a gap in the s0=R case when claiming that both children of a non-final node labelled 1 are final nodes of type T; but this follows from Property (♣), which guarantees that any move without an immediate victory preserves the side and uses mode 1. Since a move from R to T with label 1 changes the side, it must be an immediate victory, so both children are indeed final. The soundness proof (Lemma 4.3) and the completeness proof (Lemma 4.4) are consistent with the game definitions, and the transfer from rankR to rank via Fact 2.4 is correct. Minor typos, such as the self-referential inequality in the proof of Fact 2.4, do not affect the argument. Overall, I find no load-bearing concern, and the reader's ACCEPT verdict should stand unchanged.","tokens_in":40065,"tokens_out":34224,"duration_ms":327027,"concrete_test":"Implement the game G^N_A and the decision procedure of Proposition 3.2 for small automata: for the automaton of Example 3.3 the procedure should report rankR = ω1; for the relations of Lemma 9.4 with k=1 and k=2 it should report the exact finite values N0 = 1 and N0 = 2. Mismatches would indicate an error in the game characterization (Lemma 4.3 or Lemma 4.4).","verdict_should_be":"UNCHANGED","load_bearing_attack":"The most load-bearing step is indeed the use of Büchi-Landweber finite-memory determinacy in Lemma 4.5, which converts a winning strategy for ∀ in G∞_A into a bound N with ∀ winning G^N_A. I examined this step and found it sound. The periodic-play argument is valid: after N = |Pos|·M·|Q|+1 side changes on a back-marked path, pigeonhole gives two moments with the same game position, memory state, and automaton state; splicing and repeating the intervening fragment yields a play consistent with ∀'s fixed finite-memory strategy that is winning for ∃ via A(∞), a contradiction. The remaining intricate part, the auxiliary game H_{A,t,N} (Lemma 7.1), is also internally consistent: Property (♣) from Claim 7.2 ensures that without an immediate victory the side and mode are unchanged, which justifies the otherwise surprising claim in the s0=R case that both children of a non-final node labelled 1 are final nodes of type T. I identified no significant objection to the central claim.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies the ordinal rank of well-founded witnesses in MSO over the full binary tree. For a formula ∃X.φ(Ȳ,X) in which every satisfying witness X is well-founded, it defines rank(φ) as the least upper bound of the minimal ranks of witnesses over all instances, and proves a dichotomy: rank(φ) is either strictly smaller than ω² or equal to ω1, the two cases are decidable, and in the first case an N with rank(φ)<ω·N is computable. The proof works with a regular relation Γ and the layered ordinal rankR(Γ), constructs a family of finite ω-regular games G^N_A whose winner characterizes whether rankR(Γ)≥N, and uses Büchi–Landweber finite-memory determinacy to convert a ∀-win in G^∞_A into a uniform bound N. The paper also shows that the predicates rank(X)≤η and rankR(X)≤η are MSO-definable only for η<ω, and derives a dichotomy for closure ordinals of vectorial modal µ-calculus fixed points in the fragment where the iteration variables do not occur in the scope of fixed-point operators.","tokens_in":40248,"tokens_out":27784,"duration_ms":268878,"significance":"This is a striking and clean dichotomy: MSO-definable well-founded witnesses either require only bounded finite nesting of combs (rank below ω²) or can require all countable ordinals. The proof is detailed and self-contained, with soundness (Section 6) and completeness (Section 8) of the game characterization proven explicitly in both directions. The use of Büchi–Landweber determinacy is standard and well integrated, and the paper goes beyond the conference version by computing rankR(Γ) exactly and by extending the result to vectorial µ-calculus closure ordinals. The non-definability corollary (Corollary 9.3) and the reduction to Czarnecki's question add further value. The paper relies only on established external results (Rabin's theorem, Büchi–Landweber, positional determinacy of parity games) and does not introduce fitted parameters or ad hoc axioms.","major_comments":[],"minor_comments":[{"comment":"In the proof of Fact 2.4, the displayed inequality 'derω(x′)(u) ≤ derω(x′)(u)' is a typographical self-equality; the intended comparison is between the ordinary derivative der and derω, for instance der^ω(x′)(u) ≤ derω(x′)(u), which is the step needed for the inequality rank(x) ≤ ω·rankR(x).","section":"Section 2, Fact 2.4"},{"comment":"The definition of valt(v,q,s) writes 'ranks(x)', which appears to be a rendering error for rank_s(x), i.e., rankR(x) when s=R and rankT(x) when s=T; the subsequent use of valt(v′,q′,T) as a bound on rankT is clear from context but should be stated explicitly.","section":"Section 7"},{"comment":"The proof of Lemma 4.4 assumes that the parameter k=N−hist_n(q,s) is always positive, which excludes N=0; since the statement includes N=0, the proof should either explicitly restrict to N>0 and treat N=0 separately, or include the easy argument that ∃ always wins G^0_A, as asserted in the proof of Proposition 3.2.","section":"Section 8, Lemma 4.4"},{"comment":"In the proof of Lemma 4.5, 'loosing' should be 'losing'.","section":"Section 4, Lemma 4.5"}],"recommendation":"minor_revision","confidential_remarks":"This is a strong paper. The concern about Lemma 4.5 raised during the stress test does not land: the finite-memory splicing argument is sound, and the periodic-play construction is valid. The only issues found are local: a typo in Fact 2.4, a notation glitch in Section 7, and the N=0 boundary case in the proof of Lemma 4.4. These are easily fixed and do not affect the central dichotomy. I recommend minor revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear [Colleague],\n\nThe thing to know: this is a serious, genuinely new dichotomy result for MSO on the binary tree—rank of an existential well-founded witness is either <ω² or ω1, and you can decide which. The proof is built around a purpose-built parity game G_N^A, adapting the game-based separability technique from Clemente–Skrzypczak and Skrzypczak–Walukiewicz to a new setting. The soundness and completeness arguments are long and notationally heavy, but I read the key step carefully: Lemma 4.5 converts a ∀-strategy in G^∞_A into a finite bound N via Büchi–Landweber finite-memory determinacy, and the periodic-play pigeonhole argument is sound. The stress-test note agrees, and I found no hidden circularity.\n\nWhat's new: the dichotomy itself, the exact computability of the layered rank rankR (Proposition 3.2), and the MSO-undefinability of rank bounds above ω (Corollary 9.3). The paper also gives an alternative proof of the Afshari–Barlucchi–Leigh theorem on closure ordinals for the Σ-fragment of the μ-calculus, with a decision procedure—a nice application, though it does not cover full μ-calculus.\n\nSoft spots: the paper is dense; the reader must absorb a lot of machinery (sides, modes, selectors, back-markings) before the intuition clicks. There are minor typos (e.g., the self-equality in Fact 2.4's proof). The intricate game arguments are not machine-checked; this is a case where formalization would add a lot of confidence. And the exact bound is computed for rankR, not for rank; the paper is upfront that rank(φ) only gets an ω·N bound. These are real but not damaging.\n\nWho this is for: anyone working on MSO expressiveness, tree automata, or transfinite ranks in logic. It deserves serious refereeing. I'd cite it and bring it to a reading group.\n\nRecommendation: send to peer review.","headline":"A dense but sound and genuinely new dichotomy proof for ordinal ranks in MSO; the game construction holds up, and the closure-ordinal application is a real payoff.","tokens_in":40792,"tokens_out":2812,"would_cite":true,"duration_ms":27177,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03D05","03B15","68Q45","03E10"],"pacs":[],"model":"deepseek-v4-flash","headline":"MSO witness ranks are tiny or maximal—and you can tell which","keywords":["ordinal ranks","monadic second-order logic","full binary tree","well-founded sets","parity tree automata","dichotomy theorem","closure ordinals","layered depth"],"falsifier":"Find a regular (MSO-definable) relation Γ ⊆ Tr_A × WF for which the layered depth rank_R(Γ) is exactly ω (or any countable ordinal ≥ ω but < ω₁), meaning that trees t admit witnesses of arbitrarily large finite layered depth but every witness has layered depth below ω₁; the paper proves no such relation exists, so exhibiting one would refute Proposition 3.2 and the dichotomy.","tokens_in":39898,"feed_emoji":"♾️","tokens_out":8686,"duration_ms":77931,"temperature":0.7,"pith_summary":"The paper asks how complex the witness set X must be, in terms of its ordinal rank, in formulae of the form ∃X.φ(Ȳ,X) of monadic second-order logic over the full binary tree, where every witness is well-founded. It proves a dichotomy: the least bound rank(φ) for the rank of a witness is either strictly smaller than ω² (the ordinal of all pairs of natural numbers) or it reaches the maximum ω₁ (the first uncountable ordinal), and it is decidable which case holds. In the small case the proof yields a number N with rank(φ) < ω·N. The argument introduces a companion 'layered depth' that can be computed exactly and encodes the task in a finite ω-regular game whose outcome decides the dichotomy. If correct, the result shows that MSO over the binary tree can only distinguish two extremal regimes of witness complexity, and it implies a corresponding dichotomy for closure ordinals of fixed-point formulae in the modal μ-calculus.","feed_headline":"MSO witness ranks are tiny or maximal—and you can tell which","feed_subtitle":"A new game decides whether well-founded witnesses stay small or reach the uncountable bound.","key_machinery":"The load-bearing object is the two-sided game G^N_A, played on a finite arena, in which ∃ builds a tree letter by letter while ∀ chooses directions and prunes a traced set of automaton states. The play is organized into two sides, R (reach) and T (trunk), and two modes: mode 1 forces a single direction, mode 2 allows branching. Selectors chosen by ∃ determine, for each transition and side, which direction to follow and which side the resulting state lands on; a side switch from R to T marks the discovery of a node labelled 1, i.e., the start of a new nested comb. Player ∀ chooses a back-marking (a sub-flow) at each round, letting him track one history per state and control how many nested combs he demands. The winning condition has two parts: part A(N) requires the back-marked history to switch from R to T at least N times (infinitely often if N = ∞), and part B requires every accepting infinite path in the full flow to see mode 2 infinitely often. The game is ω-regular, so finite-memory determinacy applies, and the dichotomy follows from the fact that when ∀ wins at infinity, his finite memory yields a finite N.","core_discovery":"The central discovery is that ordinal ranks of MSO-definable well-founded witnesses over the full binary tree have no middle ground: rank(Γ), defined as the supremum over all trees t of the minimal rank of a well-founded witness x with (t,x) ∈ Γ, is either strictly below ω² or equal to ω₁. The paper proves this by passing to the layered depth rank_R(Γ), which satisfies rank_R(Γ) ≤ rank(Γ) ≤ ω·rank_R(Γ), and establishing the sharper statement that rank_R(Γ) is either < ω or exactly ω₁, with the exact value computable in the finite case. The proof constructs a family of finite ω-regular games G^N_A parametrized by N ∈ N ∪ {∞}; player ∃ wins G^N_A precisely when rank_R(Γ) ≥ N, and wins G^∞_A exactly when rank_R(Γ) = ω₁. Because the games are determined with finite-memory winning strategies, solving G^∞_A decides the dichotomy, and a memory bound of the winner of ∀ yields the finite N in the small case.","pith_inferences":["The exact computability of rank_R suggests that layered depth is the more robust invariant; one might try to decide whether the exact value of rank(φ) itself can be recovered from rank_R(φ), or whether the factor ω in the inequality rank(φ) ≤ ω·rank_R(φ) is sometimes necessary.","Because the game G^N_A is constructive, the same technique could be applied to other logics or automata classes (e.g., distance automata) to decide similar ordinal bounds, possibly shedding light on the open Mostowski-index problem mentioned in the paper.","The definability threshold is not an invariant of well-foundedness alone: logics like WMSO+U can define ranks up to ω, so the dichotomy should be seen as a feature of MSO's precise expressive power.","One could test whether the finite bound N computed from the memory of ∀ is tight in concrete examples, and whether it can be computed efficiently from the size of the formula or automaton."],"forward_implications":["For every MSO formula of the form ∃X.φ(Ȳ,X) with well-founded witnesses, one can effectively decide whether rank(φ) < ω² or rank(φ) = ω₁, and in the former case compute N with rank(φ) < ω·N.","The rank predicates rank(X) ≤ η and rank_R(X) ≤ η are MSO-definable only for natural numbers η; for η = ω and above they are not regular, so MSO cannot express boundedness of ranks beyond the finite levels.","For each pair (k,ℓ) of natural numbers there are MSO-definable relations with rank exactly ω·k + ℓ, so every ordinal below ω² is attained.","The closure ordinal of a vectorial least fixed point µX̄.F̄(X̄) in the modal μ-calculus, when the fixed-point variables of X̄ never fall under a fixed-point operator, obeys the same dichotomy: either < ω² with a computable bound ω·N, or ≥ ω₁, and it is decidable which.","The dichotomy provides a new proof of the recent theorem that countable closure ordinals of such fixed-point formulae are always below ω²."],"supporting_citations":[{"why":"Supplies the finite-memory determinacy of ω-regular games that makes G^N_A solvable and yields the finite N when ∀ wins.","marker":"[BL69]"},{"why":"Establishes the translation from MSO over trees to finite automata, grounding the automata-based formulation.","marker":"[Rab69]"},{"why":"Constructs MSO-definable relations attaining every rank ω·k + ℓ, fixing the lower edge of the dichotomy and raising the closure-ordinal question.","marker":"[Cza10]"},{"why":"Proves the closure-ordinal theorem for the μ-calculus that the present dichotomy reproves and strengthens with decidability.","marker":"[ABL24]"},{"why":"Introduces the game-based method of characterizing a rank property by an ω-regular game, which the present paper adapts.","marker":"[SW16]"},{"why":"Supplies the standard theory of ranks of well-founded trees via derivative iteration, used in the definition of the ranks.","marker":"[Kec95]"}],"fun_headline_variants":["MSO ranks: tiny or uncountable, and decidable","Deciding whether MSO witness ranks are small or maximal","MSO ordinal ranks: either <ω² or ω₁, decidable","A game decides if MSO ranks are tiny or maximal","For MSO on the binary tree, ranks are small or ω₁"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The dichotomy rests on the classical fact that ω-regular games of the kind constructed here are determined and that the winner can play with only finitely many memory states; if that fact failed, the gap between 'bounded by some natural number' and ω₁ could in principle contain intermediate countable ordinals.","fun_headline_variants_meta":{"raw":{"variants":["MSO ranks: tiny or uncountable, and decidable","Deciding whether MSO witness ranks are small or maximal","MSO ordinal ranks: either <ω² or ω₁, decidable","A game decides if MSO ranks are tiny or maximal","For MSO on the binary tree, ranks are small or ω₁"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000715,"raw_usage":{"total_tokens":3220,"prompt_tokens":958,"completion_tokens":2262,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":574,"completion_tokens_details":{"reasoning_tokens":2175}},"tokens_in":574,"tokens_out":2262,"duration_ms":14677,"temperature":1.0,"reasoning_tokens":2175,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T21:13:45.724525+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find a regular (MSO-definable) relation Γ ⊆ Tr_A × WF for which the layered depth rank_R(Γ) is exactly ω (or any countable ordinal ≥ ω but < ω₁), meaning that trees t admit witnesses of arbitrarily large finite layered depth but every witness has layered depth below ω₁; the paper proves no such relation exists, so exhibiting one would refute Proposition 3.2 and the dichotomy.","supporting_citations":[],"review_version":1}