arxiv: 2605.10841 · v1 · submitted 2026-05-11 · 💻 cs.LO · math.LO

Recognition: 2 theorem links

· Lean Theorem

Constant time testability of first-order logic with modulo counting on finitary graphs

Isolde Adler, Jenny Stimpson

Pith reviewed 2026-05-12 03:42 UTC · model grok-4.3

classification 💻 cs.LO math.LO

keywords property testingfirst-order logic with modulo countingHanf normal formbounded degree graphsfinitary graphsconstant time testersalgorithmic meta-theoremspatchability condition

0 comments

The pith

Properties expressible in first-order logic with modulo counting are testable with constant query complexity on graphs of bounded degree and bounded component size.

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

The paper aims to prove that any property definable in first-order logic with modulo counting admits a tester that uses only a constant number of queries, independent of the total graph size, whenever the input is restricted to graphs whose maximum degree is d and whose components have size at most c. This would matter because constant-time testers give a uniform, scalable guarantee for verifying logical statements on arbitrarily large structures, improving on earlier polylogarithmic bounds that still grew with input size. The argument proceeds by adapting Hanf normal forms to the logic and showing that a number-theoretic condition called patchability lets one combine information from a fixed-size local sample into a correct global decision. If the result holds, then testers for a wide range of counting properties become practical even when only tiny portions of the input can be examined.

Core claim

The central claim is that first-order logic with modulo counting is constant-time testable on the class C^c_d of graphs with degree at most d and component size at most c. The proof works by tailoring the Hanf normal form of this logic to the finitary setting and establishing a number-theoretic patchability condition that allows global information about the input graph to be recovered from a local sample of constant size. The step from first-order logic with modulo counting to monadic second-order logic with counting then follows from the known expressive-power relation between these logics on classes of bounded treedepth.

What carries the argument

The number-theoretic patchability condition on Hanf normal forms of FOMOD, which converts constant-size local samples into correct global decisions on graphs with bounded component size.

If this is right

Every FOMOD-definable property on C^c_d admits a constant-query tester in the bounded-degree model.
The same constant-time guarantee extends to CMSO on the same graph classes via the cited reduction to order-invariant logics.
Local samples of fixed radius suffice to determine whether a global FOMOD sentence holds whenever the patchability condition is satisfied.
Hanf normal forms can be specialised to finitary graphs so that number-theoretic patching replaces size-dependent global counting.

Where Pith is reading between the lines

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

The patchability technique might be reusable for other counting extensions of first-order logic beyond modulo arithmetic.
If component sizes grow slowly rather than being strictly bounded, analogous number-theoretic conditions could still yield sublinear testers.
The separation between local structure and global counting constraints may inform query complexity results for related problems in distributed or streaming models.

Load-bearing premise

The input graphs must have both maximum degree and maximum component size fixed in advance so that patchability can reliably lift local observations to global correctness.

What would settle it

A concrete counterexample would be a fixed FOMOD sentence together with two infinite families of graphs in C^c_d that agree on every constant-radius neighborhood yet one family satisfies the sentence while the other does not, so that no constant-query tester can separate them with high probability.

Figures

Figures reproduced from arXiv: 2605.10841 by Isolde Adler, Jenny Stimpson.

**Figure 1.** Figure 1: The graphs G2n+1 and G2n of Example 5. isolated vertex and an isolated edge. Consider the graphs G2n+1 and G2n on 2n+ 1 and 2n vertices, respectively, shown in [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗

read the original abstract

This paper studies algorithmic meta theorems for property testing with \emph{constant running time} in the bounded degree model. In (Adler, Harwath 2018) it was shown that on graph classes $\mathcal C^{w}_d$ consisting of all graphs with both degree at most $d$ and treewidth at most $w$, every problem expressible in monadic second-order logic with counting (CMSO) is testable with \emph{polylogarithmic} running time (where $d,w\in \mathbb N$ are fixed). It was left open whether this can be improved to \emph{constant} running time. In this paper we give a positive answer for testing CMSO on classes $\mathcal C^{c}_d$, where $d$ bounds the degree and $c$ bounds the component size. Our main result shows constant time testability of first-order logic with modulo counting (FOMOD) on $\mathcal C^{c}_d$. For our proof we tailor Hanf normal form of FOMOD to our setting, and we exhibit a number-theoretic `patchability' condition that allows to infer global information on the input graph from a local sample of constant size. We believe that our `patchability' might be of independent interest. The step from FOMOD to CMSO then follows from a result by (Eickmeyer, Elberfeld, Harwath, 2017) on the expressive power of order invariant monadic second-order logic on classes of bounded treedepth.

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

The paper closes the 2018 open question by showing constant-time testability for FOMOD on C^c_d via a tailored Hanf form plus a new patchability condition.

read the letter

The main takeaway is that Adler and Stimpson have resolved the open question from their earlier work: FOMOD properties are constant-time testable on graphs with bounded degree and bounded component size. They do this by adapting Hanf normal form to FOMOD and defining a number-theoretic patchability condition on the coefficients that is supposed to let local constant-radius samples determine the global truth value, including for modulo counts. The step to CMSO then follows from the existing Eickmeyer et al. 2017 result on order-invariant MSO and bounded treedepth. This is a clean technical move that directly targets the gap left in 2018 rather than a broad generalization. The patchability notion is presented as potentially reusable, which is a modest but concrete addition to the toolkit for locality-based arguments on graphs. The proof outline in the abstract is coherent and avoids obvious circularity by building on prior normal-form theorems. The soft spot is the lifting step itself. The stress-test note correctly flags that FOMOD can talk about global size modulo m, and on C^c_d it is possible to vary total order while preserving the multiset of small components and thus the local type counts seen in any fixed-radius sample. If the patchability condition is stated strongly enough to rule out or compensate for those residue-class flips, the claim goes through; if it only works for certain coefficient patterns, the result may be narrower than stated. The full derivation of the condition and the exact class of FOMOD sentences it covers will need checking. This paper is for people already working on algorithmic meta-theorems, property testing in the bounded-degree model, or locality results for logics on graphs. A reader following the Adler-Harwath line or interested in constant-time testers will get direct value from the new condition. It deserves a serious referee because it settles an explicit open problem with a new technical device, even if the details of patchability require scrutiny.

Referee Report

1 major / 0 minor

Summary. The paper claims that every property definable in first-order logic with modulo counting (FOMOD) is testable with constant running time in the bounded-degree model on the classes C^c_d of graphs with maximum degree at most d and maximum component size at most c (for fixed d, c). The proof adapts Hanf normal forms for FOMOD to this finitary setting and introduces a number-theoretic 'patchability' condition on the normal-form coefficients that is asserted to allow recovery of global information, including modular cardinalities, from constant-size local samples. The extension to CMSO then follows from the cited result of Eickmeyer et al. (2017) on order-invariant MSO over bounded treedepth.

Significance. If correct, the result would strengthen existing polylogarithmic-time meta-theorems for CMSO on bounded-treewidth graphs to constant time for the weaker FOMOD fragment on the more restrictive bounded-component-size classes, and the patchability notion could be of independent interest for other local-to-global arguments in logic and testing. The manuscript does not, however, supply machine-checked proofs or reproducible code.

major comments (1)

[Abstract and main result] Abstract and proof outline: The central claim that patchability lifts local samples to global correctness for all FOMOD sentences is contradicted by the fact that FOMOD can express the sentence 'universe size ≡ r (mod m)'. On the subclass C^1_0 (edgeless graphs consisting of isolated vertices), every constant-radius neighborhood is a single isolated vertex; the observed local-type distribution is therefore identical for all sufficiently large even and odd orders, yet the truth value of the sentence differs. No number-theoretic condition on the Hanf coefficients can eliminate this n-mod-m ambiguity while preserving the reduction to a congruence on local-type counts, so the patchability argument does not establish constant-time testability for the full logic.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the thorough review and for highlighting a potential issue with the patchability condition in the context of global cardinality properties. We believe the main result remains valid and address the concern directly below. The tester operates in the standard bounded-degree model where the input size n is known, which resolves the apparent ambiguity.

read point-by-point responses

Referee: [Abstract and main result] Abstract and proof outline: The central claim that patchability lifts local samples to global correctness for all FOMOD sentences is contradicted by the fact that FOMOD can express the sentence 'universe size ≡ r (mod m)'. On the subclass C^1_0 (edgeless graphs consisting of isolated vertices), every constant-radius neighborhood is a single isolated vertex; the observed local-type distribution is therefore identical for all sufficiently large even and odd orders, yet the truth value of the sentence differs. No number-theoretic condition on the Hanf coefficients can eliminate this n-mod-m ambiguity while preserving the reduction to a congruence on local-type counts, so the patchability argument does not establish constant-time testability for the full logic.

Authors: The referee's counterexample does not contradict the claim because the property-testing algorithm is given the vertex set size n as part of the input (standard in the bounded-degree model). For the sentence expressing |V| ≡ r (mod m), the Hanf normal form reduces it to a modular condition on the count of the single local type (the isolated vertex). Although the observed distribution is uniform, the tester computes the implied count as n (or proportion × n) and checks the congruence directly using the known n. This eliminates the ambiguity without requiring any additional number-theoretic patch on the coefficients beyond what is already stated. When n ≡ r (mod m) the property holds for every graph in C^1_0; otherwise it holds for none, and the tester rejects immediately. In both cases the procedure uses only constant time (in fact, zero queries when the type is uniform). The patchability condition is therefore not required to 'guess' n mod m; it combines the locally observed proportions with the globally known n to recover the necessary modular information. The same mechanism applies to any FOMOD sentence whose normal-form coefficients involve total cardinality. revision: no

Circularity Check

0 steps flagged

Derivation is self-contained via new Hanf tailoring and external citation

full rationale

The paper derives constant-time testability for FOMOD on C^c_d by tailoring Hanf normal forms to the bounded-component setting and introducing a fresh number-theoretic patchability condition that lifts local samples to global properties. This construction is presented as original and does not reduce any claimed prediction or theorem to a fitted parameter or prior definition by construction. The subsequent step to CMSO invokes an independent external result (Eickmeyer et al. 2017) on order-invariant MSO, which is not a self-citation load-bearing step and carries no definitional circularity. No equations or steps in the provided abstract or description exhibit self-definition, renaming of known results, or ansatz smuggling.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The proof relies on the existence of Hanf normal form for FOMOD (standard in finite model theory) and on the 2017 expressive-power result for order-invariant MSO; the patchability condition is introduced as a new technical device but is not an invented entity with independent evidence.

axioms (2)

standard math Hanf normal form exists and can be tailored for FOMOD on bounded-degree graphs
Invoked to reduce the testing problem to local neighborhood counts.
domain assumption Eickmeyer-Elberfeld-Harwath 2017 result on order-invariant MSO over bounded treedepth
Used to lift the FOMOD result to CMSO.

invented entities (1)

patchability condition no independent evidence
purpose: Number-theoretic condition allowing global information to be inferred from a constant-size local sample
Introduced in the paper to bridge local and global views; no independent falsifiable prediction is given.

pith-pipeline@v0.9.0 · 5582 in / 1590 out tokens · 59107 ms · 2026-05-12T03:42:32.346355+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 recovery theorem unclear
k-capped component histogram vector... rare types... frequent types... g | n' ... conical combination

Reference graph

Works this paper leans on

17 extracted references · 17 canonical work pages

[1]

Faster property testers in a variation of the bounded degree model.ACM Trans

Isolde Adler and Polly Fahey. Faster property testers in a variation of the bounded degree model.ACM Trans. Comput. Log., 24(3):25:1– 25:24, 2023.doi:10.1145/3584948

work page doi:10.1145/3584948 2023
[2]

Property testing for bounded de- gree databases

Isolde Adler and Frederik Harwath. Property testing for bounded de- gree databases. In35th Symposium on Theoretical Aspects of Com- puter Science, STACS 2018, volume 96, pages 6:1–6:14, 2018.doi: 10.4230/LIPICS.STACS.2018.6

work page doi:10.4230/lipics.stacs.2018.6 2018
[3]

On testability of first-order properties in bounded-degree graphs

Isolde Adler, Noleen K¨ ohler, and Pan Peng. On testability of first-order properties in bounded-degree graphs. In D´ aniel Marx, editor,Pro- ceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, SODA 2021, Virtual Conference, January 10 - 13, 2021, pages 1578–

work page 2021
[4]

SIAM, 2021.doi:10.1137/1.9781611976465.96. 17

work page doi:10.1137/1.9781611976465.96 2021
[5]

On testability of first-order properties in bounded-degree graphs and connections to proximity- oblivious testing.SIAM J

Isolde Adler, Noleen K¨ ohler, and Pan Peng. On testability of first-order properties in bounded-degree graphs and connections to proximity- oblivious testing.SIAM J. Comput., 53(4):825–883, 2024. URL: https://doi.org/10.1137/23m1556253,doi:10.1137/23M1556253

work page doi:10.1137/23m1556253 2024
[6]

Ef- ficient testing of large graphs.Combinatorica, 20(4):451–476, 2000

Noga Alon, Eldar Fischer, Michael Krivelevich, and Mario Szegedy. Ef- ficient testing of large graphs.Combinatorica, 20(4):451–476, 2000. URL:http://dx.doi.org/10.1007/s004930070001,doi:10.1007/ s004930070001

work page doi:10.1007/s004930070001 2000
[7]

Every minor-closed property of sparse graphs is testable.Advances in Mathematics, 223(6):2200 – 2218, 2010

Itai Benjamini, Oded Schramm, and Asaf Shapira. Every minor-closed property of sparse graphs is testable.Advances in Mathematics, 223(6):2200 – 2218, 2010. URL:http://www. sciencedirect.com/science/article/pii/S0001870809003466, doi:http://dx.doi.org/10.1016/j.aim.2009.10.018

work page doi:10.1016/j.aim.2009.10.018 2010
[8]

Testing hereditary properties of nonexpanding bounded-degree graphs.SIAM J

Artur Czumaj, Asaf Shapira, and Christian Sohler. Testing hereditary properties of nonexpanding bounded-degree graphs.SIAM J. Comput., 38(6):2499–2510, 2009.doi:10.1137/070681831

work page doi:10.1137/070681831 2009
[9]

Succinct- ness of order-invariant logics on depth-bounded structures.ACM Trans

Kord Eickmeyer, Michael Elberfeld, and Frederik Harwath. Succinct- ness of order-invariant logics on depth-bounded structures.ACM Trans. Comput. Log., 18(4):33:1–33:25, 2017.doi:10.1145/3152770

work page doi:10.1145/3152770 2017
[10]

Where first-order and monadic second-order logic coincide.ACM Trans

Michael Elberfeld, Martin Grohe, and Till Tantau. Where first-order and monadic second-order logic coincide.ACM Trans. Comput. Log., 17(4):25, 2016.doi:10.1145/2946799

work page doi:10.1145/2946799 2016
[11]

Solomon Feferman and Robert L. Vaught. The first order properties of products of algebraic systems.Fundamenta Mathematicae, 47(1):57– 103, 1959. URL:http://eudml.org/doc/213526

work page 1959
[12]

Property testing in bounded degree graphs.Algorithmica, 32(2):302–343, 2002

Oded Goldreich and Dana Ron. Property testing in bounded degree graphs.Algorithmica, 32(2):302–343, 2002. URL:http://dx.doi.org/ 10.1007/s00453-001-0078-7,doi:10.1007/s00453-001-0078-7

work page doi:10.1007/s00453-001-0078-7 2002
[13]

Hanf normal form for first-order logic with unary counting quantifiers

Lucas Heimberg, Dietrich Kuske, and Nicole Schweikardt. Hanf normal form for first-order logic with unary counting quantifiers. 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 277–286. ACM, 2016.doi:10.1145/2933...

work page doi:10.1145/2933575.2934571 2016
[14]

Jones and J

Gareth A. Jones and J. Mary Jones.Elementary Number Theory. Springer, 1998

work page 1998
[15]

Lattice translates of a polytope and the frobenius prob- lem.Comb., 12(2):161–177, 1992.doi:10.1007/BF01204720

Ravi Kannan. Lattice translates of a polytope and the frobenius prob- lem.Comb., 12(2):161–177, 1992.doi:10.1007/BF01204720

work page doi:10.1007/bf01204720 1992
[16]

Every property of hyperfinite graphs is testable.SIAM J

Ilan Newman and Christian Sohler. Every property of hyperfinite graphs is testable.SIAM J. Comput., 42(3):1095–1112, 2013. Con- ference version published at STOC 2011. URL:http://dx.doi.org/ 10.1137/120890946,doi:10.1137/120890946

work page doi:10.1137/120890946 2013
[17]

≥m”}andY 2 :={0} ∪[ℓ−1]. We define two sets ofs-tuples B1 = ( b∈Y X 1 | sX i=1 b[i]≥mor b[i] = “≥m

Juha Nurmonen. Counting modulo quantifiers on finite structures. Inf. Comput., 160(1-2):62–87, 2000. URL:https://doi.org/10.1006/ inco.1999.2842,doi:10.1006/INCO.1999.2842. A Proof of lemma 11 Letd∈N. For every sentenceφof FOMOD there exist anr max ∈Nand an FOMOD sentenceψsuch thatφ≡ d ψ, whereψis in HNF and every Hanf sentence has radiusr max. Proof.Appl...

work page doi:10.1006/inco.1999.2842 2000