pith. sign in

arxiv: 2510.00139 · v3 · submitted 2025-09-30 · 🧮 math.CO · math.LO

Myhill-Nerode for hypergraphs and an application to gain-graphic matroids

Daryl Funk , Angus Matthews , Dillon Mayhew This is my paper

Pith reviewed 2026-05-18 11:15 UTC · model grok-4.3

classification 🧮 math.CO math.LO
keywords Myhill-Nerode theoremhypergraphscounting monadic second-order logicgain-graphic matroidsuniformly locally finite groupsconviviality graphmatroid definability
0
0 comments X

The pith

A Myhill-Nerode theorem for hypergraphs shows definable classes have finite index and that gain-graphic matroids over non-uniformly locally finite groups are not monadically definable.

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

The paper develops a Myhill-Nerode theorem tailored to hypergraphs by introducing an operation that merges two structures into a single hypergraph and using it to define an equivalence relation. It proves that any class of hypergraphs definable in counting monadic second-order logic induces an equivalence with only finitely many classes. The authors apply this to gain-graphic matroids to conclude that when the gain group is not uniformly locally finite the corresponding class of matroids cannot be defined in monadic logic. They further define the conviviality graph of a group and link its infiniteness to the same non-definability result.

Core claim

The central claim is that there exists an operation producing a hypergraph from two input structures such that the induced Myhill-Nerode equivalence relation has finite index for every class definable in the counting monadic second-order logic of hypergraphs. Applying the theorem yields that for a group Γ that is not uniformly locally finite the class of Γ-gain-graphic matroids is not monadically definable, and likewise if the conviviality graph of Γ is infinite.

What carries the argument

The operation that combines two input structures to produce a hypergraph, which defines the Myhill-Nerode-type equivalence relation on hypergraphs.

If this is right

  • If a class of hypergraphs is definable in counting monadic second-order logic then its Myhill-Nerode equivalence has finite index.
  • The class of Γ-gain-graphic matroids is not monadically definable whenever Γ is not uniformly locally finite.
  • If the conviviality graph of Γ is infinite then the class of Γ-gain-graphic matroids is not monadically definable.

Where Pith is reading between the lines

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

  • This theorem provides a general method to prove non-definability results for classes of hypergraphs and derived structures like matroids.
  • The conviviality graph can serve as a new invariant for detecting when classes of gain-graphic matroids lie outside monadic definability.

Load-bearing premise

The operation producing the hypergraph from two structures interacts with counting monadic second-order logic so that the equivalence relation distinguishes exactly the definable properties.

What would settle it

A concrete counterexample would be a class of hypergraphs definable in counting monadic second-order logic whose Myhill-Nerode equivalence relation has infinite index, or a specific non-uniformly locally finite group for which the gain-graphic matroids turn out to be monadically definable.

Figures

Figures reproduced from arXiv: 2510.00139 by Angus Matthews, Daryl Funk, Dillon Mayhew.

Figure 1
Figure 1. Figure 1: The graph H∗ n,N . For ease of notation, we will refer to vertices by lower-case Greek letters, and edges by upper-case Roman letters. Let G∗ ℓ,N be the subgraph enclosed by the dotted line, and let ℓ ∗ N be its edge-set. Let T be the collection of bolded edges. Note that each of A, B1, . . . , BN and C are collections of edges: A = {AId, A1, . . . , An, As} Bi = {Bi,Id, Bi,1, . . . , Bi,n} for all 1 ≤ i ≤… view at source ↗
Figure 2
Figure 2. Figure 2: The graph Hn,N \ H∗ n,N . Each Di : 1 ≤ i ≤ 6 is a collection of two edges: Di = {Di,1, Di,2}. Each Qi is a single loop edge. Let Gℓ,N = G∗ ℓ,N ∪ {QN+6, QN+7}, and let ℓN be its edge-set. We will use these new edges at only one point in the argument. Suppose we have some group Γ, a generating set {a1, . . . , an}, some s,M ∈ ⟨a1, . . . , an⟩. Then, H∗ n,N has a Γ-gaining σ ∗ = σ ∗ (Γ, {a1, . . . , an}, s,M… view at source ↗
Figure 3
Figure 3. Figure 3: The graph Λ∗ Γ1,Γ2 For ease of notation, we will refer to vertices by lower-case Greek letters, and edges by upper-case Roman letters. Let ℓ ∗ Γ1 be the edge set of the subgraph enclosed by the dotted line (we will see its structure depends only on Γ1). Let T be the collection of bolded edges. Note that each of A, B1, B2, B3 and C are collections of edges: A = {Ag : g ∈ Γ1} Bi = {Bi,g : g ∈ Γ2} : i = 1, 2,… view at source ↗
Figure 4
Figure 4. Figure 4: The graph ΛΓ1,Γ2 \ Λ ∗ Γ1,Γ2 Each Di : 1 ≤ i ≤ 11 is a collection of two edges: Di = {Di,1, Di,2}. Each Qi is a single loop edge. Let ℓΓ1 = ℓ ∗ Γ1 ∪ {Q8, Q9} ∪ D10. We will use these new edges at only one point in the argument. Suppose we have an infinite group Γ3 containing Γ2, and M some element in Γ3. Then, Λ∗ Γ1,Γ2 has a Γ2-gaining σ ∗ = σ ∗ (Γ1, Γ2,M), defined as follows: σ ∗ (T) = Id ∀ T ∈ T σ ∗ (Ag)… view at source ↗
read the original abstract

We present a Myhill-Nerode theorem for hypergraphs. The theorem involves an operation which takes two input structures and produces a hypergraph as output. Using this operation, we define a Myhill-Nerode-type equivalence relation and show that if a class of hypergraphs is definable in the counting monadic second-order logic of hypergraphs, then the equivalence relation has finite index. We apply this tool to classes of gain-graphic matroids, and show that if the group $\Gamma$ is not uniformly locally finite, then the class of $\Gamma$\dash gain-graphic matroids is not monadically definable. (A group is uniformly locally finite if, for every $k$, there is a maximum size amongst subgroups generated by at most $k$ elements.) In addition, we define the conviviality graph of a group, and show that if the group $\Gamma$ has an infinite conviviality graph, then the class of $\Gamma$\dash gain-graphic matroids is not monadically definable. This will be useful in future constructions.

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.

Referee Report

2 major / 2 minor

Summary. The paper presents a Myhill-Nerode theorem for hypergraphs. It defines an operation that takes two input structures and produces a hypergraph, then uses this to define a Myhill-Nerode-type equivalence relation. The central result shows that if a class of hypergraphs is definable in counting monadic second-order logic (CMSO), then the equivalence has finite index. This is applied to gain-graphic matroids: if the group Γ is not uniformly locally finite, the class of Γ-gain-graphic matroids is not monadically definable. The paper also defines the conviviality graph of a group and proves that an infinite conviviality graph implies the class is not monadically definable.

Significance. If the results hold, the work supplies a useful logical tool for establishing non-definability of certain matroid classes in monadic second-order logic, bridging hypergraph logic with algebraic combinatorics. The explicit Myhill-Nerode construction and the new conviviality graph invariant are concrete contributions that support future applications, as the authors note. The paper gives clear theorem statements and applies the tool directly to a natural family of matroids.

major comments (2)
  1. [Section 3] The proof of the finite-index claim for CMSO-definable classes (the Myhill-Nerode theorem) rests on the combining operation preserving the relevant logical distinctions. An explicit lemma or subsection verifying that CMSO formulas translate across the operation without introducing new quantifier alternations or losing the finite-index property would make the argument self-contained.
  2. [Section 5] In the application to Γ-gain-graphic matroids (when Γ is not uniformly locally finite), the argument that the class has infinite index under the equivalence must confirm that the operation on the underlying hypergraphs does not collapse distinctions arising from the group elements. A concrete check against the definition of gain-graphic matroids would strengthen this step.
minor comments (2)
  1. [Introduction] The introduction would benefit from a short concrete example illustrating the combining operation on two small hypergraphs and the resulting equivalence classes.
  2. [Section 4] The definition of the conviviality graph could be placed in a numbered definition environment and its basic properties (e.g., whether it is directed) stated explicitly for reference.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive assessment of the manuscript and for the constructive suggestions that will help strengthen the presentation. We address the two major comments below and will revise the paper to incorporate explicit verifications as requested, thereby improving the self-contained nature of the arguments.

read point-by-point responses

  1. Referee: [Section 3] The proof of the finite-index claim for CMSO-definable classes (the Myhill-Nerode theorem) rests on the combining operation preserving the relevant logical distinctions. An explicit lemma or subsection verifying that CMSO formulas translate across the operation without introducing new quantifier alternations or losing the finite-index property would make the argument self-contained.

    Authors: We agree that an explicit lemma will make the argument more self-contained. In the revised manuscript we will insert a new lemma in Section 3 that explicitly shows how CMSO formulas are interpreted on the output hypergraph produced by the combining operation. The lemma will verify that atomic predicates and quantifiers (including counting quantifiers) translate directly, without introducing additional alternations, and that the finite-index property for definable classes is therefore preserved. This addition directly addresses the concern about logical distinctions being maintained across the operation. revision: yes

  2. Referee: [Section 5] In the application to Γ-gain-graphic matroids (when Γ is not uniformly locally finite), the argument that the class has infinite index under the equivalence must confirm that the operation on the underlying hypergraphs does not collapse distinctions arising from the group elements. A concrete check against the definition of gain-graphic matroids would strengthen this step.

    Authors: We thank the referee for highlighting this point. In the revision we will add a short concrete verification in Section 5. We will explicitly check, using the definition of Γ-gain-graphic matroids, that when two distinct elements of Γ label otherwise identical hyperedges, the resulting structures remain inequivalent under the Myhill-Nerode relation after the combining operation is applied. This verification will confirm that distinctions arising from group elements are not collapsed by the operation, thereby supporting the claim of infinite index when Γ is not uniformly locally finite. revision: yes

Circularity Check

0 steps flagged

Myhill-Nerode theorem for hypergraphs is a direct logical construction with no circular reductions.

full rationale

The derivation defines a Myhill-Nerode-type equivalence via an explicit operation mapping pairs of structures to hypergraphs, then proves finite index for any CMSO-definable class using standard properties of counting monadic second-order logic. This is a self-contained adaptation of the classical theorem, not a renaming or self-referential fit. The non-definability result for Γ-gain-graphic matroids when Γ is not uniformly locally finite follows from the finite-index property combined with an independent group-theoretic argument (existence of arbitrarily large finite subgroups generated by bounded elements). No equation or claim reduces to its own inputs by construction, no load-bearing self-citation chain is present, and the conviviality graph is introduced as an auxiliary definition for future use rather than a circular justification. The entire chain rests on explicit logical translations and external group properties.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on standard background assumptions from logic and group theory with no free parameters or new invented entities introduced.

axioms (2)
  • standard math Standard properties and expressive power of counting monadic second-order logic on hypergraphs
    Invoked as the logical framework in which definability is considered.
  • domain assumption Basic facts about groups and their finitely generated subgroups
    Used in the definition of uniformly locally finite and the application to matroids.

pith-pipeline@v0.9.0 · 5721 in / 1420 out tokens · 40348 ms · 2026-05-18T11:15:40.362920+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

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

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

17 extracted references · 17 canonical work pages

  1. [1]

    Reprint of the 1979 original

    Martin Aigner,Combinatorial theory, Classics in Mathematics, Springer-Verlag, Berlin, 1997. Reprint of the 1979 original

    work page 1997

  2. [2]

    Downey, Michael R

    Ren´ e van Bevern, Rodney G. Downey, Michael R. Fellows, Serge Gaspers, and Frances A. Rosamond,Myhill-Nerode methods for hypergraphs, Algorithmica73(2015), no. 4, 696–729

    work page 2015

  3. [3]

    IX, Megara, c

    Euclid,Elements, Vol. IX, Megara, c. 300BCE

    work page

  4. [4]

    Daryl Funk,On excluded minors and biased graph representations of frame matroids, PhD thesis, Simon Fraser University, 2015

    work page 2015

  5. [5]

    Daryl Funk, Dillon Mayhew, and Mike Newman,Defining bicircular matroids in monadic logic, Q. J. Math.73(2022), no. 1, 65–92

    work page 2022

  6. [6]

    Sci., vol

    Petr Hlinˇ en´ y,Branch-width, parse trees, and monadic second-order logic for matroids (extended abstract), STACS 2003, Lecture Notes in Comput. Sci., vol. 2607, Springer, Berlin, 2003, pp. 319–330

    work page 2003

  7. [7]

    Sci., vol

    ,On matroid properties definable in the MSO logic, Mathematical foundations of computer science 2003, Lecture Notes in Comput. Sci., vol. 2747, Springer, Berlin, 2003, pp. 470–479

    work page 2003

  8. [8]

    Wilfrid Hodges,A shorter model theory, Cambridge University Press, 1997

    work page 1997

  9. [9]

    Hopcroft and Jeffrey D

    John E. Hopcroft and Jeffrey D. Ullman,Introduction to automata theory, languages, and computation, Addison-Wesley series in computer science, Addison-Wesley, 1979

    work page 1979

  10. [10]

    Makowsky,Connection matrices and the definability of graph parameters, Log

    Tomer Kotek and Johann A. Makowsky,Connection matrices and the definability of graph parameters, Log. Methods Comput. Sci.10(2014), no. 4, 4:1, 33

    work page 2014

  11. [11]

    Dillon Mayhew, Mike Newman, and Geoff Whittle,Yes, the ‘missing axiom’ of ma- troid theory is lost forever, Trans. Amer. Math. Soc.370(2018), no. 8, 5907–5929

    work page 2018

  12. [12]

    John Myhill,Finite automata and the representation of events, WADD Technical Report57(1957), 112–137

    work page 1957

  13. [13]

    Nerode,Linear automaton transformations, Proc

    A. Nerode,Linear automaton transformations, Proc. Amer. Math. Soc.9(1958), 541–544

    work page 1958

  14. [14]

    21, Oxford University Press, Oxford, 2011

    James Oxley,Matroid theory, 2nd ed., Oxford Graduate Texts in Mathematics, vol. 21, Oxford University Press, Oxford, 2011

    work page 2011

  15. [15]

    Thomas Zaslavsky,Biased graphs. I. Bias, balance, and gains, J. Combin. Theory Ser. B47(1989), no. 1, 32–52

    work page 1989

  16. [16]

    E. I. Zel ′manov,Solution of the restricted Burnside problem for groups of odd expo- nent, Izv. Akad. Nauk SSSR Ser. Mat.54(1990), no. 1, 42–59, 221 (Russian); English transl., Math. USSR-Izv.36(1991), no. 1, 41–60

    work page 1990

  17. [17]

    Sb.182(1991), no

    ,Solution of the restricted Burnside problem for2-groups, Mat. Sb.182(1991), no. 4, 568–592 (Russian); English transl., Math. USSR-Sb.72(1992), no. 2, 543–565

    work page 1991