The role of counting quantifiers in laminar set systems

Noleen K\"ohler; Rutger Campbell

arxiv: 2512.02617 · v2 · pith:GSVUA4EMnew · submitted 2025-12-02 · 💻 cs.LO · cs.FL

The role of counting quantifiers in laminar set systems

Rutger Campbell , Noleen K\"ohler This is my paper

Pith reviewed 2026-05-21 19:02 UTC · model grok-4.3

classification 💻 cs.LO cs.FL

keywords laminar set systemsmonadic second-order logicMSO transductionlaminar treegraph decompositionscounting quantifiers

0 comments

The pith

From any laminar set system one can recover its laminar tree using only an MSO transduction.

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

Laminar set systems are collections of non-crossing subsets whose inclusions line up with the ancestor-descendant relation of a tree. The paper shows that a monadic second-order logic transduction can build this tree directly from the family when the family is presented as a relational structure. This settles an open question from Courcelle about whether counting quantifiers are needed for the step. The result upgrades several well-known graph decompositions, including modular, split, and bi-join decompositions, from CMSO to plain MSO. The authors also map out some situations inside laminar systems where counting quantifiers still add expressive power.

Core claim

The authors prove that there exists an MSO transduction which, given a laminar family of sets as input structure, outputs the tree whose nodes are the sets and whose descendant relation is exactly the inclusion relation of the family. The transduction is defined without counting quantifiers. Using earlier results, the same approach yields MSO transductions for modular decompositions, co-trees, split decompositions, and bi-join decompositions. The work also supplies partial results on when counting quantifiers can be eliminated inside laminar set systems and when they cannot.

What carries the argument

MSO transduction that interprets the descendant relation of the laminar tree from the inclusion relation of the input sets.

If this is right

Modular decompositions of graphs can be obtained via MSO transductions rather than CMSO.
Split decompositions and bi-join decompositions admit MSO transductions.
Co-trees can be recovered from their underlying structures by MSO alone.
Counting quantifiers are unnecessary for the passage from a laminar family to its tree representation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The result hints that MSO may capture more structure than expected once the input is restricted to laminar families.
Similar simplifications might apply to other graph decompositions built on non-crossing set families.
It would be natural to classify precisely which properties of laminar systems require counting quantifiers and which do not.

Load-bearing premise

The laminar set system is supplied as a relational structure whose membership and inclusion relations can be directly addressed by monadic second-order formulas.

What would settle it

A concrete laminar family of sets on which every possible MSO transduction fails to produce a tree whose relations match the inclusion structure of the family.

read the original abstract

Laminar set systems consist of non-crossing subsets of a universe with set inclusion essentially corresponding to the descendant relationship of a tree, the so-called laminar tree. Laminar set systems lie at the core of many graph decompositions such as modular decompositions, split decompositions, and bi-join decompositions. We show that from a laminar set system we can obtain the corresponding laminar tree by means of a monadic second order logic (MSO) transduction. This resolves an open question originally asked by Courcelle and is a satisfying resolution as MSO is the natural logic for set systems and is sufficient to define the property ``laminar''. Using results from Campbell et al. [STACS 2025], we can now obtain transductions for obtaining modular decompositions, co-trees, split decompositions and bi-join decompositions using MSO instead of CMSO. We further gain some insight into the expressive power of counting quantifiers and provide some results towards determining when counting quantifiers can be simulated in MSO in laminar set systems and when they cannot.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Resolves Courcelle's open question via an MSO transduction from laminar set systems to trees, which cleans up several decompositions but puts the core construction in a companion paper.

read the letter

Hi colleague, the main takeaway is that this paper constructs an MSO transduction that recovers the laminar tree from a given laminar set system. That directly settles Courcelle's question and lets modular, split, and bi-join decompositions move from CMSO to plain MSO by building on their STACS 2025 results. They also note that MSO can define the laminarity property itself, which lines up with the natural logic for set systems. The side discussion on when counting quantifiers can be simulated inside MSO for these structures adds a bit of extra context. What they do well is keep the logic clean and show a concrete payoff for several standard decompositions without adding extra machinery. The construction appears to stay inside MSO by working directly with the inclusion relation on the relational structure, so the stress-test worry about hidden cardinality tests for non-crossing sets or maximal chains does not seem to apply here. The paper treats the input as a straightforward two-sorted incidence structure and defines descendant via inclusion without extra quantifiers. One soft spot is that the detailed transduction and its verification live in the companion STACS paper rather than here, so this manuscript functions more as an application and extension note. That makes the central claim harder to check in isolation and leaves the simulation results on counting quantifiers feeling preliminary rather than fully worked out. The work is aimed at logicians and graph theorists who track the MSO-CMSO boundary in decomposition problems. A reader who follows Courcelle-style results or needs simpler logical characterizations for laminar structures will find direct value. It deserves a serious referee because it closes a known open question with clear downstream uses, even if the presentation splits the proof across papers. I would recommend sending it out for peer review.

Referee Report

1 major / 3 minor

Summary. The manuscript shows that a laminar set system given as a relational structure admits an MSO transduction producing the corresponding laminar tree (with descendant relation matching set inclusion). This resolves Courcelle's open question. Combining the result with Campbell et al. (STACS 2025) yields MSO transductions for modular decompositions, co-trees, split decompositions and bi-join decompositions. The paper further analyzes the expressive power of counting quantifiers, identifying cases where they can be simulated in MSO on laminar families and cases where they cannot.

Significance. If the construction is correct, the result is significant: it demonstrates that MSO alone suffices for laminar set systems and their trees, replacing CMSO in several decomposition transductions. This clarifies the boundary between MSO and CMSO on non-crossing set families and supplies concrete logical constructions for important graph decompositions. The explicit resolution of the cited open question and the accompanying analysis of counting quantifiers constitute a clear contribution to logical graph theory.

major comments (1)

§3.2, transduction construction: the claim that the descendant relation is MSO-definable without counting relies on the precise input signature (two-sorted incidence structure versus one-sorted). The manuscript should explicitly verify that selecting covering relations or maximal chains does not require cardinality tests that would force CMSO; a counter-example family where non-crossing detection needs |A| comparisons would undermine the MSO claim.

minor comments (3)

§2: the relational signature for the laminar set system is introduced informally; an explicit list of predicates and an example structure would improve readability.
Figure 2: the laminar-tree diagram lacks node labels corresponding to the original sets, making it harder to verify the inclusion-to-descendant mapping.
References: the Campbell et al. citation should include the full title and arXiv identifier of the STACS 2025 paper.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment and the recommendation for minor revision. The major comment raises a valid point about the precise input signature and the need for explicit verification that the transduction avoids counting quantifiers. We address the comment directly below and will revise the manuscript accordingly.

read point-by-point responses

Referee: §3.2, transduction construction: the claim that the descendant relation is MSO-definable without counting relies on the precise input signature (two-sorted incidence structure versus one-sorted). The manuscript should explicitly verify that selecting covering relations or maximal chains does not require cardinality tests that would force CMSO; a counter-example family where non-crossing detection needs |A| comparisons would undermine the MSO claim.

Authors: We appreciate this observation. The input is the two-sorted incidence structure with universe elements and laminar sets as distinct sorts, connected by an incidence relation. In this signature, set inclusion (which defines the descendant relation in the laminar tree) is expressed by the first-order formula ∀x (Inc(x,S) → Inc(x,T)). The covering relation is defined by proper inclusion together with the universal statement that no other set U in the given family lies strictly between S and T; this quantifies only over the second sort and requires no cardinality tests. Non-crossing detection is likewise first-order: two sets cross only if they intersect but neither is included in the other, again using only incidence and Boolean combinations. Because the laminar family is provided explicitly as the second sort, no auxiliary counting over element cardinalities is invoked. We are not aware of a counter-example family in which these relations would require |A| comparisons, as the definitions are purely inclusion-based. In the revised manuscript we will insert a short clarifying paragraph in §3.2 that spells out these formulas and confirms that the transduction stays inside MSO. revision: yes

Circularity Check

0 steps flagged

Minor self-citation for extensions; core MSO transduction independently resolves Courcelle question

full rationale

The paper's central derivation defines an MSO transduction that maps a laminar set system (given as a relational structure) to the laminar tree whose descendant relation matches set inclusion. This construction is presented as a direct logical argument that resolves Courcelle's open question and is self-contained within the MSO framework for set systems; laminarity itself is definable in MSO without external parameters. The reference to Campbell et al. [STACS 2025] is used only to extend the result to modular, split, and bi-join decompositions, replacing prior CMSO transductions with MSO ones, but does not serve as the load-bearing justification for the laminar-tree transduction itself. No fitted quantities, self-definitional loops, or ansatzes imported via citation reduce the primary claim to its inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on the standard definition of MSO transductions and the background fact that laminar set systems correspond to trees under inclusion. No free parameters, new entities, or ad-hoc axioms are introduced in the abstract.

axioms (2)

standard math MSO is the logic with quantification over elements and sets of elements
Invoked throughout as the target logic for the transduction.
domain assumption Laminar set systems correspond to trees via the inclusion relation
Stated as the structural correspondence that the transduction must preserve.

pith-pipeline@v0.9.0 · 5712 in / 1290 out tokens · 77628 ms · 2026-05-21T19:02:27.828921+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean logicNat_initial / equivNat unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We show that from a laminar set system we can obtain the corresponding laminar tree by means of a monadic second order logic (MSO) transduction. This resolves an open question originally asked by Courcelle.
IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Theorem 17. ... EVEN-LEAFk(X) ... for rooted trees with down-degree at most k

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

11 extracted references · 11 canonical work pages

[1]

The category of mso transductions

URL:http://arxiv.org/ abs/2305.18039v1,arXiv:2305.18039v1. 2 Mikołaj Bojańczyk, Martin Grohe, and Michał Pilipczuk. Definable decompositions for graphs of bounded linear cliquewidth.Log. Methods Comput. Sci., 17(1),

work page arXiv
[2]

Definability equals recognizability for graphs of bounded treewidth

3 Mikołaj Bojańczyk and Michał Pilipczuk. Definability equals recognizability for graphs of bounded treewidth. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 407–416. ACM, 2016.doi:10.1145/2933575. 2934508. 4 ...

work page doi:10.1145/2933575 2016
[3]

URL:https://doi.org/10.4230/LIPIcs.STACS.2025.22, doi:10.4230/LIPICS.STACS. 2025.22. 5 Rutger Campbell, Bruno Guillon, Mamadou Moustapha Kanté, Eun Jung Kim, and Sang- il Oum. Recognisability equals definability for finitely representable matroids of bounded path-width. In40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, J...

work page doi:10.4230/lipics.stacs.2025.22 2025
[4]

Campbell and N

R. Campbell and N. Köhler 19 9 Bruno Courcelle. The monadic second-order logic of graphs XI: hierarchical decompositions of connected graphs.Theor. Comput. Sci., 224(1-2):35–58, 1999.doi:10.1016/S0304-3975(98) 00306-5. 10 Bruno Courcelle. The monadic second-order logic of graphs XVI: Canonical graph decomposi- tions.Logical Methods in Computer Science, 2,

work page doi:10.1016/s0304-3975(98 1999
[5]

Graph structure and monadic second-order logic, a language theoretic approach, Cambridge University Press, 2012

URL:https://doi.org/10.1017%2Fcbo9780511977619, doi:10.1017/cbo9780511977619. 14 Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width.Theory Comput. Syst., 33(2):125–150,

work page doi:10.1017/cbo9780511977619
[6]

Makowsky, and Udi Rotics

URL:https://doi.org/10.1007/s002249910009,doi:10.1007/S002249910009. 15 Daryl Funk, Dillon Mayhew, and Mike Newman. Tree automata and pigeonhole classes of matroids: I.Algorithmica, 84(7):1795–1834,

work page doi:10.1007/s002249910009
[7]

Tree automata and pigeonhole classes of matroids: I

URL: https://doi.org/10.1007/ s00453-022-00939-7,doi:10.1007/S00453-022-00939-7. 16 Tobias Ganzow and Sasha Rubin. Order-invariant MSO is stronger than counting MSO in the finite. In Susanne Albers and Pascal Weil, editors,STACS 2008, 25th Annual Symposium on Theoretical Aspects of Computer Science, Bordeaux, France, February 21-23, 2008, Proceedings, vol...

work page doi:10.1007/s00453-022-00939-7 2008
[8]

Branch-width, parse trees, and monadic second-order logic for matroids

URL:https://doi.org/10.1016/j.jctb.2005.08.005, doi:10.1016/J.JCTB.2005.08.005. 18 Leonid Libkin.Elements of finite model theory. Texts in Theoretical Computer Science. An EATCS Series. Springer-Verlag, Berlin, 2004.doi:10.1007/978-3-662-07003-1. 19 Imre Simon. Factorization forests of finite height.Theor. Comput. Sci., 72(1):65–94,

work page doi:10.1016/j.jctb.2005.08.005 2005
[9]

20 Yann Strozecki

doi:10.1016/0304-3975(90)90047-L. 20 Yann Strozecki. Monadic second-order model-checking on decomposable matroids.Discret. Appl. Math., 159(10):1022–1039,

work page doi:10.1016/0304-3975(90)90047-l
[10]

URL:https://doi.org/10.1016/j.dam.2011.02.005, doi:10.1016/J.DAM.2011.02.005. 21 J. W. Thatcher and J. B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic.Math. Systems Theory, 2:57–81,

work page doi:10.1016/j.dam.2011.02.005 2011
[11]

doi: 10.1007/BF01691346

work page doi:10.1007/bf01691346

[1] [1]

The category of mso transductions

URL:http://arxiv.org/ abs/2305.18039v1,arXiv:2305.18039v1. 2 Mikołaj Bojańczyk, Martin Grohe, and Michał Pilipczuk. Definable decompositions for graphs of bounded linear cliquewidth.Log. Methods Comput. Sci., 17(1),

work page arXiv

[2] [2]

Definability equals recognizability for graphs of bounded treewidth

3 Mikołaj Bojańczyk and Michał Pilipczuk. Definability equals recognizability for graphs of bounded treewidth. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 407–416. ACM, 2016.doi:10.1145/2933575. 2934508. 4 ...

work page doi:10.1145/2933575 2016

[3] [3]

URL:https://doi.org/10.4230/LIPIcs.STACS.2025.22, doi:10.4230/LIPICS.STACS. 2025.22. 5 Rutger Campbell, Bruno Guillon, Mamadou Moustapha Kanté, Eun Jung Kim, and Sang- il Oum. Recognisability equals definability for finitely representable matroids of bounded path-width. In40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, J...

work page doi:10.4230/lipics.stacs.2025.22 2025

[4] [4]

Campbell and N

R. Campbell and N. Köhler 19 9 Bruno Courcelle. The monadic second-order logic of graphs XI: hierarchical decompositions of connected graphs.Theor. Comput. Sci., 224(1-2):35–58, 1999.doi:10.1016/S0304-3975(98) 00306-5. 10 Bruno Courcelle. The monadic second-order logic of graphs XVI: Canonical graph decomposi- tions.Logical Methods in Computer Science, 2,

work page doi:10.1016/s0304-3975(98 1999

[5] [5]

Graph structure and monadic second-order logic, a language theoretic approach, Cambridge University Press, 2012

URL:https://doi.org/10.1017%2Fcbo9780511977619, doi:10.1017/cbo9780511977619. 14 Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width.Theory Comput. Syst., 33(2):125–150,

work page doi:10.1017/cbo9780511977619

[6] [6]

Makowsky, and Udi Rotics

URL:https://doi.org/10.1007/s002249910009,doi:10.1007/S002249910009. 15 Daryl Funk, Dillon Mayhew, and Mike Newman. Tree automata and pigeonhole classes of matroids: I.Algorithmica, 84(7):1795–1834,

work page doi:10.1007/s002249910009

[7] [7]

Tree automata and pigeonhole classes of matroids: I

URL: https://doi.org/10.1007/ s00453-022-00939-7,doi:10.1007/S00453-022-00939-7. 16 Tobias Ganzow and Sasha Rubin. Order-invariant MSO is stronger than counting MSO in the finite. In Susanne Albers and Pascal Weil, editors,STACS 2008, 25th Annual Symposium on Theoretical Aspects of Computer Science, Bordeaux, France, February 21-23, 2008, Proceedings, vol...

work page doi:10.1007/s00453-022-00939-7 2008

[8] [8]

Branch-width, parse trees, and monadic second-order logic for matroids

URL:https://doi.org/10.1016/j.jctb.2005.08.005, doi:10.1016/J.JCTB.2005.08.005. 18 Leonid Libkin.Elements of finite model theory. Texts in Theoretical Computer Science. An EATCS Series. Springer-Verlag, Berlin, 2004.doi:10.1007/978-3-662-07003-1. 19 Imre Simon. Factorization forests of finite height.Theor. Comput. Sci., 72(1):65–94,

work page doi:10.1016/j.jctb.2005.08.005 2005

[9] [9]

20 Yann Strozecki

doi:10.1016/0304-3975(90)90047-L. 20 Yann Strozecki. Monadic second-order model-checking on decomposable matroids.Discret. Appl. Math., 159(10):1022–1039,

work page doi:10.1016/0304-3975(90)90047-l

[10] [10]

URL:https://doi.org/10.1016/j.dam.2011.02.005, doi:10.1016/J.DAM.2011.02.005. 21 J. W. Thatcher and J. B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic.Math. Systems Theory, 2:57–81,

work page doi:10.1016/j.dam.2011.02.005 2011

[11] [11]

doi: 10.1007/BF01691346

work page doi:10.1007/bf01691346