Pith. sign in

REVIEW 4 minor 13 references

A Dichotomy Theorem for Ordinal Ranks in MSO

T0 review · 0 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

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

Pith's one-line read MSO witness ranks are tiny or maximal—and you can tell which

desk verdict 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. read the letter →

arxiv 2501.05385 v4 pith:AUIVGFOL submitted 2025-01-09 cs.LO

Damian Niwiński , Pawe{l} Parys , Micha{l} Skrzypczak This is my paper · ORCID
classification cs.LO MSC 03D0503B1568Q4503E10
keywords ordinalranksmonadicsecond-orderlogicfullbinarytreewell-foundedsetsparityautomatadichotomytheoremclosureordinalslayereddepth
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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 ω².

Reading between the lines

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

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

0 major / 4 minor

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.

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.

minor comments (4)
  1. [Section 2, Fact 2.4] 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).
  2. [Section 7] 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.
  3. [Section 8, Lemma 4.4] 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.
  4. [Section 4, Lemma 4.5] In the proof of Lemma 4.5, 'loosing' should be 'losing'.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the game equivalence is proven in both directions, and the dichotomy does not reduce to its inputs.

full rationale

The paper's central claim, Theorem 1.1, is reduced to Proposition 3.2 via the rank estimates of Fact 2.4, and then to the dichotomy game G^N_A. The three parts of Proposition 4.2 are not assumed but proved: Lemma 4.3 proves soundness by unravelling a winning strategy of ∃ into a tree t whose witnesses all have layered depth at least N (or arbitrarily large countable depth when N=∞), via Claims 6.2–6.4; Lemma 4.4 proves completeness by using the uniform positional strategy of Pathfinder from Lemma 7.1 to convert a tree t with val_t(ε,q_I,R) ≥ N into a winning strategy of ∃ in G^N_A; and Lemma 4.5 proves the finitary collapse from G^∞_A to G^N_A by a self-contained pigeonhole argument over the finite memory of ∀'s Büchi–Landweber winning strategy. The external theorems used—Büchi–Landweber finite-memory determinacy, positional determinacy of parity games, and Rabin's theorem—are standard results cited as evidence, and none of them is replaced by a self-citation of the present authors. The authors' prior work is invoked for motivation, technique, or comparison, not as the source of the dichotomy: the paper explicitly constructs the games and proves both directions of the equivalence between rankR(Γ) ≥ N and ∃ winning G^N_A. No fitted parameter is renamed as a prediction, no uniqueness theorem by the same authors is imported to force the chosen construction, and no ansatz is smuggled in via citation. The application in Section 10 uses Theorem 1.1 after a separate translation into MSO, so the closure-ordinal dichotomy is a consequence rather than an input. Thus the derivation chain is self-contained; at most there are minor self-citations that are not load-bearing, giving a low score.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The paper introduces new definitions (rankR, rankT, the game GN_A, selectors, back-markings) but these are explicit mathematical objects with proofs, not unexplained postulated entities. They do not require independent empirical evidence. The central claim rests on standard set theory and established theorems in automata and games.

assumptions (6)
  • standard math ZFC and standard ordinal arithmetic below ω1
    The paper uses ordinals, transfinite induction, and the well-founded rank of trees throughout (Section 2).
  • domain assumption Rabin's Tree Theorem: every MSO-definable tree language is regular
    Invoked in Section 2 (Theorem 2.1) to translate MSO formulae to parity tree automata, the main working formalism.
  • domain assumption Büchi-Landweber determinacy and finite-memory winning strategies for ω-regular games
    Used in Remark 4.1 to solve the games GN_A and in Lemma 4.5 to derive a finite bound N from a winning strategy of ∀ in G∞_A.
  • domain assumption Positional determinacy of parity games
    Used in Section 7 to obtain a uniform positional strategy for Pathfinder in the auxiliary game HA,t,N.
  • domain assumption The derivative-based ordinal rank characterizes well-foundedness (Kechris)
    Section 2 states rank(x) is well-defined iff x is well-founded; this standard result underlies the definition of rank(φ).
  • domain assumption Tree-model property, bisimulation invariance, and MSO translation of µ-calculus
    Section 10 uses these to reduce closure ordinals of fixed-point formulae to ranks of MSO-definable relations (citing [BW18]).

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Dichotomy Theorem for Ordinal Ranks in MSO." pith.science (2026). https://pith.science/paper/AUIVGFOL

@misc{pith2026250105385,
  author       = {Pith},
  title        = {Pith review of: A Dichotomy Theorem for Ordinal Ranks in MSO},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AUIVGFOL}},
  note         = {Machine review of arXiv:2501.05385}
}
abstract

We focus on formulae $\exists X.\, \varphi(\vec{Y}, X)$ of monadic second-order logic over the full binary tree, such that the witness $X$ is a well-founded set. The ordinal rank $\mathrm{rank}(X) < \omega_1$ of such a set $X$ measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula $\varphi$. Let $\mathrm{rank}(\varphi)$ be the minimal ordinal such that, whenever an instance $\vec{Y}$ satisfies the formula, there is a witness $X$ with $\mathrm{rank}(X) \leq \mathrm{rank}(\varphi)$. Then $\mathrm{rank}(\varphi)$ is either strictly smaller than $\omega^2$ or it reaches the maximal possible value $\omega_1$. Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.

Figures

Figures reproduced from arXiv: 2501.05385 by the authors.

Figure 4.1
Figure 4.1. Depiction of the four types of selectors. [PITH_FULL_IMAGE:figures/full_fig_p011_4_1.png] view at source ↗
Figure 4
Figure 4. depicts the four types of selectors for ( [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 4.2
Figure 4.2. A depiction of a round of the game G N A . The first two lemmata are proven in the subsequent sections: soundness (Lemma 4.3) in Section 6 and completeness (Lemma 4.4) in Section 8. Lemma 4.5 is proven below. Proof of Lemma 4.5. Recall that Remark 4.1 gives a bound M on the number of memory states needed by either of the players to win the game G∞ A . As N we take the number of positions in the game G∞ A , times M, … view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: depicts an example of a round of the game [PITH_FULL_IMAGE:figures/full_fig_p014_4.png]
Figure 9.1
Figure 9.1. Figure 9.1: An illustration of the tree x used in the proof of Lemma 9.2 Definability of this predicate in MSO boils down to checking if the following language is regular: L≤η def =  x ∈ Tr{0,1} | rank(x) ≤ η [PITH_FULL_IMAGE:figures/full_fig_p027_9_1.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

13 extracted references · 9 canonical work pages

  1. [9]

    [Fon08] Ga¨ elle Fontaine

    doi:10.1109/LICS.2013.56. [Fon08] Ga¨ elle Fontaine. Continuous fragment of the mu-calculus. InCSL, volume 5213 ofLecture Notes in Computer Science, pages 139–153. Springer, 2008.doi:10.1007/978-3-540-87531-4_12. [FT13] Olivier Finkel and Stevo Todorcevic. Automatic ordinals.Int. J. Unconv. Comput., 9(1-2):61–70,

    work page doi:10.1109/lics.2013.56 2013

  2. [10]

    Mostowski Index via extended register games

    URL: http://www.oldcitypublishing.com/journals/ijuc-home/ijuc-issue-contents/ ijuc-volume-9-number-1-2-2013/ijuc-9-1-2-p-61-70/. [GS19] Maria J. Gouveia and Luigi Santocanale. ℵ1 and the modal µ-calculus.Log. Methods Comput. Sci., 15(4), 2019.doi:10.23638/LMCS-15(4:1)2019. [IL24] Olivier Idir and Karoliina Lehtinen. Mostowski index via extended register g...

    work page Pith review arXiv doi:10.48550/arxiv.2412.16793 2013

  3. [13]

    [SW16] Micha l Skrzypczak and Igor Walukiewicz

    doi:10.1007/978-3-662-52947-8. [SW16] Micha l Skrzypczak and Igor Walukiewicz. Deciding the topological complexity of B¨ uchi languages. InICALP, volume 55 ofLIPIcs, pages 99:1–99:13. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2016.doi:10.4230/LIPICS.ICALP.2016.99. [Tho97] Wolfgang Thomas. Languages, automata, and logic. InHandbook of Formal Lan...

    work page doi:10.1007/978-3-662-52947-8

  4. [1983]

    [Mos91] Andrzej W

    doi:10.1016/0304-3975(82)90125-6. [Mos91] Andrzej W. Mostowski. Games with forbidden positions. Technical report, University of Gda´ nsk,

    doi:10.1016/0304-3975(82)90125-6

  5. [1991]

    [NPS25] Damian Niwi´ nski, Pawe l Parys, and Micha l Skrzypczak

    doi:10.1007/3-540-54345-7_80. [NPS25] Damian Niwi´ nski, Pawe l Parys, and Micha l Skrzypczak. A dichotomy theorem for ordinal ranks in MSO. InSTACS, volume 327 ofLIPIcs, pages 69:1–69:18. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2025.doi:10.4230/LIPICS.STACS.2025.69. [NW03] Damian Niwi´ nski and Igor Walukiewicz. A gap property of determinist...

    work page doi:10.1007/3-540-54345-7_80

  6. [1998]

    [BW18] Julian C

    doi:10.1007/BFB0028547. [BW18] Julian C. Bradfield and Igor Walukiewicz. The mu-calculus and model checking. InHandbook of Model Checking, pages 871–919. Springer, 2018.doi:10.1007/978-3-319-10575-8_26. [CKL V13] Thomas Colcombet, Denis Kuperberg, Christof L¨ oding, and Michael Vanden Boom. Deciding the weak definability of B¨ uchi definable tree language...

    work page doi:10.1007/bfb0028547 2018

  7. [2001]

    Bradfield, Jacques Duparc, and Sandra Quickert

    [BDQ05] Julian C. Bradfield, Jacques Duparc, and Sandra Quickert. Transfinite extension of the mu- calculus. InCSL, volume 3634 ofLecture Notes in Computer Science, pages 384–396. Springer, 2005.doi:10.1007/11538363_27. [Bek84] Hans Beki´ c. Definable operation in general algebras, and the theory of automata and flowcharts. In Programming Languages and Th...

    work page doi:10.1007/11538363_27 2005

  8. [2010]

    [BL69] Julius R

    doi:10.3233/ FI-2010-260. [BL69] Julius R. B¨ uchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295–311,

    work page 2010

Show all 13 references
  1. [2011]

    2011.03.020

    doi:10.1016/J.TCS. 2011.03.020. [FBB+23] Nathana¨ el Fijalkow, Nathalie Bertrand, Patricia Bouyer-Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotn´ y, Mickael Randour, Ocan ...

    2011 arXiv

  2. [2013]

    [AN01] Andr´ e Arnold and Damian Niwi´ nski.Rudiments of mu-calculus

    doi:10.4230/LIPICS.CSL.2013.30. [AN01] Andr´ e Arnold and Damian Niwi´ nski.Rudiments of mu-calculus. Studies in Logic and the Founda- tions of Mathematics. Elsevier,

    2013 doi

  3. [2016]

    Tree automata, mu-calculus and determinacy

    [EJ91] Allen Emerson and Charanjit Jutla. Tree automata, mu-calculus and determinacy. InFOCS, pages 368–377. IEEE Computer Society, 1991.doi:10.1109/SFCS.1991.185392. [EKL11] Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixe...

    1991

  4. [2023]

    [FMS13] Alessandro Facchini, Filip Murlak, and Micha l Skrzypczak

    doi:10.48550/ ARXIV.2305.10546. [FMS13] Alessandro Facchini, Filip Murlak, and Micha l Skrzypczak. Rabin-Mostowski index problem: A step beyond deterministic automata. InLICS, pages 499–508. IEEE Computer Society,

    doi arXiv

  5. [2024]

    [AL13] Bahareh Afshari and Graham E

    URL: https://www.irif.fr/_media/users/saurin/fics2024/ pre-proceedings/fics-2024-afshari-etal.pdf. [AL13] Bahareh Afshari and Graham E. Leigh. On closure ordinals for the modal mu-calculus. InCSL, volume 23 ofLIPIcs, pages 30–44. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik,

    2024

Pith tools

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