pith. sign in

arxiv: 2606.11993 · v1 · pith:G7PPVOD6new · submitted 2026-06-10 · 💻 cs.LO · math.LO

A Rank-Preserving Gaifman Normal Form

Martin Grohe , Nicole Schweikardt This is my paper

Pith reviewed 2026-06-27 08:13 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords first-order logicGaifman's theoremlocalityrank measurenowhere-dense structuresmodel checkingalgorithmic meta-theorems
0
0 comments X

The pith

First-order logic admits a rank measure under which Gaifman's theorem produces the classic normal form without increasing rank.

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

The paper defines a numerical rank for first-order formulas. It proves that any formula can be rewritten into a Gaifman normal form sentence that has exactly the same rank as the original. The normal form matches the syntactic shape of the 1960s result exactly. This yields a simpler proof that first-order properties on nowhere-dense structures can be decided in almost linear time.

Core claim

We introduce a rank measure for first-order logic and prove a rank-preserving version of Gaifman's theorem that yields formulas in exactly the same normal form as Gaifman's original theorem. As an application of this theorem, we give a simplified proof of the main result that first-order properties of nowhere-dense structures can be decided in almost linear time.

What carries the argument

A rank measure on first-order formulas that remains invariant under the quantifier movements and neighborhood expansions used to reach Gaifman normal form.

If this is right

  • Gaifman normal forms can be obtained while exactly preserving rank.
  • The decision procedure for first-order properties on nowhere-dense structures runs in almost linear time via a simpler argument.
  • Locality transformations can be applied without raising the tracked complexity of the formula.

Where Pith is reading between the lines

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

  • The rank measure may extend to other syntactic transformations in first-order logic beyond Gaifman locality.
  • Tracking this rank could give finer bounds on the resources needed for model checking on sparse inputs.

Load-bearing premise

The new rank measure stays the same or decreases when formulas undergo the syntactic steps that produce the Gaifman normal form.

What would settle it

A first-order formula for which every equivalent sentence in Gaifman normal form has strictly higher rank than the original under the defined measure.

Figures

Figures reproduced from arXiv: 2606.11993 by Martin Grohe, Nicole Schweikardt.

Figure 3.1
Figure 3.1. Figure 3.1: Structure G “ G7 of Example 3.2. Undirected edges represent directed edges in both directions, and redG “ t3, 7, 16u and blueG “ t17u. of the formulas in S Y L. The inner quantifier rank (the width, respectively) of φ 1 is the maximum of the inner quantifier ranks (the widths, respectively) of all sentences in S. The outer quantifier rank of φ 1 is the maximum of the quantifier ranks of all the formulas … view at source ↗
read the original abstract

We introduce a rank measure for first-order logic and prove a "rank-preserving'" version of Gaifman's theorem. Compared to earlier "rank-preserving locality theorems'" (in particular, [Grohe, Kreutzer, Siebertz, JACM 2017]), our theorem is not only much simpler, but also yields formulas in exactly the same normal form as Gaifman's original theorem. As an application of this theorem, we give a simplified proof of the main result of [Grohe, Kreutzer, Siebertz, JACM 2017] that first-order properties of nowhere-dense structures can be decided in almost linear time.

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

0 major / 2 minor

Summary. The manuscript introduces a rank measure on first-order logic formulas and proves a rank-preserving version of Gaifman's theorem that produces formulas in exactly the same normal form as the original Gaifman theorem. It then applies the result to give a simplified proof that first-order properties of nowhere-dense structures are decidable in almost linear time, re-proving the main theorem of Grohe, Kreutzer and Siebertz (JACM 2017).

Significance. If the rank measure and preservation property hold, the work supplies a direct and simpler route to Gaifman normal forms that remains compatible with existing applications. The explicit construction of the rank and the fact that the normal form is identical to Gaifman's original are concrete strengths. The application demonstrates utility by streamlining the decision procedure for nowhere-dense classes.

minor comments (2)
  1. A brief explicit comparison (e.g., a short list or table) of the new proof steps versus the 2017 JACM argument would help readers assess the claimed simplification.
  2. Notation for the rank function r(·) and the distance predicates could be introduced with a small example in the preliminaries section to aid readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of the manuscript, the recognition of the explicit rank construction and the fact that the normal form matches Gaifman's original, and the recommendation for minor revision. No major comments appear in the report.

Circularity Check

0 steps flagged

Minor self-citation to 2017 overlapping-author paper used only for comparison and application; new rank measure and theorem proved independently.

full rationale

The paper introduces a new rank measure on FO formulas and proves a rank-preserving Gaifman normal form that matches the original syntactic shape. It cites the 2017 Grohe-Kreutzer-Siebertz JACM paper solely to contrast simplicity and to derive a simplified proof of that paper's main result on nowhere-dense structures. No equation or definition in the given text reduces the new theorem to the 2017 result, to a fitted parameter, or to a self-referential construction. The central derivation therefore remains self-contained; the self-citation is not load-bearing for the new claim.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

Review limited to abstract; no explicit free parameters, axioms, or invented entities beyond the new rank definition are stated.

axioms (1)
  • standard math Standard syntax and semantics of first-order logic
    The theorem is stated inside FO logic, so background FO axioms are presupposed.
invented entities (1)
  • Rank measure on FO formulas no independent evidence
    purpose: To track complexity while preserving locality normal form
    Newly introduced in the paper; no independent evidence outside the claimed theorem.

pith-pipeline@v0.9.1-grok · 5628 in / 1147 out tokens · 23621 ms · 2026-06-27T08:13:40.736879+00:00 · methodology

discussion (0)

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

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. A Rank-Preserving Locality Theorem

    cs.LO 2026-06 unverdicted novelty 5.0

    Proves a rank-preserving locality theorem for a syntactic first-order logic variant with weak scatter sentences, applied to bounded merge-width graphs.

Reference graph

Works this paper leans on

18 extracted references · 16 canonical work pages · cited by 1 Pith paper

  1. [1]

    Homomorphism preservation on quasi-wide classes

    Anuj Dawar. “Homomorphism preservation on quasi-wide classes”. In:Journal of Computer and System Sciences76.5 (2010), pp. 324–332.doi:10.1016/J.JCSS. 2009.10.005

    work page doi:10.1016/j.jcss 2010

  2. [2]

    First-Order Model Check- ing on Structurally Sparse Graph Classes

    Jan Dreier, Nikolas M¨ ahlmann, and Sebastian Siebertz. “First-Order Model Check- ing on Structurally Sparse Graph Classes”. In:Proceedings of the 55th Annual ACM Symposium on Theory of Computing (STOC’23). 2023, pp. 567–580.doi: 10.1145/3564246.3585186

    work page doi:10.1145/3564246.3585186 2023

  3. [3]

    2nd edition

    Heinz-Dieter Ebbinghaus and J¨ org Flum.Finite Model Theory. 2nd edition. Springer, 1999.doi:10.1007/3-540-28788-4

    work page doi:10.1007/3-540-28788-4 1999

  4. [4]

    3rd edition

    Heinz-Dieter Ebbinghaus, J¨ org Flum, and Wolfgang Thomas.Mathematical Logic. 3rd edition. Springer, 2021.doi:10.1007/978-3-030-73839-6

    work page doi:10.1007/978-3-030-73839-6 2021

  5. [5]

    Monadic Generalized Spectra

    Ronald Fagin. “Monadic Generalized Spectra”. In:Zeitschrift f¨ ur mathematische Logik und Grundlagen der Mathematik21 (1975), pp. 89–96.doi:10.1002/malq. 19750210112

    work page doi:10.1002/malq 1975

  6. [6]

    Deciding first-order properties of locally tree- decomposable structures

    Markus Frick and Martin Grohe. “Deciding first-order properties of locally tree- decomposable structures”. In:Journal of the ACM48.6 (2001), pp. 1184–1206. doi:10.1145/504794.504798

    work page doi:10.1145/504794.504798 2001

  7. [7]

    On local and non-local properties

    Haim Gaifman. “On local and non-local properties”. In:Proceedings of the Her- brand Symposium, Logic Colloquium ‘81. Ed. by J. Stern. Vol. 107. Studies in Logic and the Foundations of Mathematics. North Holland, 1982, pp. 105–135. doi:10.1016/S0049-237X(08)71879-2

    work page doi:10.1016/s0049-237x(08)71879-2 1982

  8. [8]

    Deciding First-Order Properties of Nowhere Dense Graphs

    Martin Grohe, Stephen Kreutzer, and Sebastian Siebertz. “Deciding First-Order Properties of Nowhere Dense Graphs”. In:Journal of the ACM64.3 (2017).doi: 10.1145/3051095. 38

    work page doi:10.1145/3051095 2017

  9. [9]

    First-Order Query Evaluation with Cardi- nality Conditions

    Martin Grohe and Nicole Schweikardt. “First-Order Query Evaluation with Cardi- nality Conditions”. In:Proceedings of the 37th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS’18).2018, pp. 253-266. doi:10.1145/3196959.3196970. Full version: ArXiv 1707.05945,doi:10.48550/arXiv.1707.05945

    work page doi:10.1145/3196959.3196970 2018

  10. [10]

    Model-theoretic methods in the study of elementary logic

    William Hanf. “Model-theoretic methods in the study of elementary logic”. In:The Theory of Models. Ed. by J. Addison, L. Henkin, and A. Tarski. North Holland, 1965, pp. 132–145.doi:10.1016/B978-0-7204-2233-7.50020-4

    work page doi:10.1016/b978-0-7204-2233-7.50020-4 1965

  11. [11]

    Shrinking games and local formu- las

    H. Jerome Keisler and Wafik Boulos Lotfallah. “Shrinking games and local formu- las”. In:Ann. Pure Appl. Log.128.1-3 (2004), pp. 215–225.doi:10.1016/J.APAL. 2004.01.004

    work page doi:10.1016/j.apal 2004

  12. [12]

    First-order logic with counting

    Dietrich Kuske and Nicole Schweikardt. “First-order logic with counting”. In:Pro- ceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’17). 2017, pp. 1–12.doi:10.1109/LICS.2017.8005133

    work page doi:10.1109/lics.2017.8005133 2017

  13. [13]

    Texts in Theoretical Computer Science

    Leonid Libkin.Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.isbn: 3-540-21202-7.doi:10.1007/ 978-3-662-07003-1

    2004

  14. [14]

    Logics with counting and local properties

    Leonid Libkin. “Logics with counting and local properties”. In:ACM Transactions on Computational Logic1 (2000), pp. 33–59.doi:10.1145/343369.343376

    work page doi:10.1145/343369.343376 2000

  15. [15]

    On forms of locality over finite models

    Leonid Libkin. “On forms of locality over finite models”. In:Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS’97). 1997, pp. 204–215.doi:10.1109/LICS.1997.614948

    work page doi:10.1109/lics.1997.614948 1997

  16. [16]

    and Carta, J.A

    Jaroslav Nesetril and Patrice Ossona de Mendez. “On nowhere dense graphs”. In: European Journal of Combinatorics32.4 (2011), pp. 600–617.doi:10.1016/J. EJC.2011.01.006

    work page doi:10.1016/j 2011

  17. [17]

    Enumeration for FO queries over nowhere dense graphs

    Nicole Schweikardt, Luc Segoufin, and Alexandre Vigny. “Enumeration for FO queries over nowhere dense graphs”. In:Journal of the ACM69.3 (2022), pp. 1– 37.doi:10.1145/3517035

    work page doi:10.1145/3517035 2022

  18. [18]

    Linear time computable problems and first-order descriptions

    Detlef Seese. “Linear time computable problems and first-order descriptions”. In: Mathematical Structures in Computer Science6 (1996), pp. 505–526.doi:10 . 1017/S0960129500070079. 39

    1996