A Rank-Preserving Gaifman Normal Form for First-Order Logic on Weighted Structures

Steffen van Bergerem; Martin Grohe; Charlotte Lenz; Nicole Schweikardt

Source-linked AI summary

A Rank-Preserving Gaifman Normal Form for First-Order Logic on Weighted Structures

Steffen van Bergerem, Martin Grohe, Charlotte Lenz, Nicole Schweikardt

arXiv:2609.37337v1Sep 29, 2026cs.LOmath.LO

TL;DR

Standard Gaifman normal forms can increase quantifier rank, creating difficulty for recursive applications to nowhere-dense algorithmic meta-theorems. The paper gives a rank-preserving normal form for weighted logic and its first-order and modulo-counting cases, and applies it to simplify a nowhere-dense algorithmic meta-theorem proof.

Problem
Standard Gaifman normal forms may increase quantifier rank, a serious obstacle for recursive proofs of algorithmic meta-theorems for nowhere-dense classes.
Source: §1 · p. 2
Method
The paper proves a rank-preserving Gaifman normal form for neighbourhood-guarded first-order logic on weighted structures, with an approach based on a refined syntactic proof and a Feferman–Vaught decomposition.
Source: §1 · p. 3, §5 · p. 8
Results
Every formula in the specified ngFOW+ fragments has an equivalent Gaifman normal form preserving quantifier rank and distance-atom bounds, with corresponding results for FO+ and FO+MOD+.
Source: §1 · p. 3, §7.1 · p. 14, §7.2 · p. 15
Takeaways & Limitations
The theorem yields a simplified proof that first-order properties of nowhere-dense structures can be decided in almost-linear time and is a step toward a meta-theorem for ngFOW+.
Source: §1 · p. 2, §6 · p. 13
For a particular choice of weight ranges and predicates, ngFOW+ model checking is AW[*]-hard even on vertex-weighted trees of height 1.
Source: §6 · p. 13

Abstract

from arXiv · show

We 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 much simpler and yields formulas in exactly the same normal form as Gaifman's original theorem. Furthermore, it holds not only for first-order logic, but also for first-order logic with modulo-counting quantifiers and, more generally, for the first-order logic on weighted structures ngFOW+ that is introduced in this article. As an application of our theorem, we give a simplified proof of the algorithmic meta-theorem of [Grohe, Kreutzer, Siebertz, JACM 2017] stating that first-order properties of nowhere dense structures can be decided in almost-linear time. Our locality theorem for the weight logic ngFOW+ can be seen as an essential step toward such a meta-theorem for this logic.

1 Introduction

Standard Gaifman normal forms may increase quantifier rank, complicating recursive applications such as nowhere-dense algorithmic meta-theorems. The paper develops a simpler rank-preserving form for a broader logic on weighted structures.

1 Introduction

Rank increases in standard Gaifman normal forms complicate recursive applications to nowhere-dense algorithmic meta-theorems [3, 18, 19, 35].Earlier rank-preserving locality theorems, including Grohe, Kreutzer, and Siebertz [18], were complex; the paper also arose from an attempt to fix an error in [19].Source: §1 · p. 2
The paper also gives a simplified proof of the nowhere-dense first-order algorithmic meta-theorem and develops the result for FO and modulo-counting logic.The paper outlines applications and further research directions, including a possible path toward a meta-theorem for the weight logic.Source: §1 · pp. 2–3
Earlier locality results for weighted or counting logics cover restricted fragments, while long-range shared numeric values can create virtual connections that undermine locality.The paper targets a larger neighbourhood-guarded fragment that permits comparisons between terms associated with variables only when they are close together.Source: §1 · pp. 2–3
The authors stratify ngFOW+ into fragments F(q, k, d), separating quantifier rank, free variables, and permitted distance-atom bounds.The permitted distances also depend on each atom’s position in the formula.Source: §1 · p. 3
Every formula in F(q, k, d) has an equivalent Gaifman normal form preserving both quantifier rank and distance-atom bounds.The form combines local formulas, basic local sentences, and local aggregation sentences; the theorem also has a refined syntactic version.Source: §1 · p. 3
The proof combines Ehrenfeucht–Fraïssé and syntactic Gaifman ideas, extending them with a parameter-compatible Feferman–Vaught decomposition.Its construction differs from Gaifman’s original proof, which enables avoiding a quantifier-rank increase.Source: §1 · p. 3

2 Preliminaries

The preliminaries establish the structures, graph distances, and logical notions used to state locality and quantifier-rank results.

2 Preliminaries

A relational structure has a finite non-empty universe and interprets each signature relation as a set of tuples of its specified arity.The signature may include 0-ary relation symbols.Source: §2 · p. 4
The Gaifman graph connects distinct elements that occur together in a relation tuple, and structure distance is shortest-path distance in that graph.The r-neighbourhood of an element consists of those at distance at most r.Source: §2 · p. 4
First-order formulas use relational atoms, Boolean combinations, and existential quantification; quantifier rank is the maximum nesting depth of quantifiers.A formula is r-local when its truth is determined by the r-neighbourhood of its assigned variables.Source: §2 · p. 4

3 Gaifman’s Theorem for FO is Not Rank-Preserving

The section demonstrates that ordinary Gaifman normal form need not preserve the quantifier rank of a formula. A constructed example shows that rank-2 local formulas cannot always express the required equivalence.

3 Gaifman’s Theorem for FO is Not Rank-Preserving

The section defines basic local sentences using pairwise distance conditions and a one-free-variable local formula; Gaifman normal forms combine these with local formulas.Distances at most d can be expressed by FO formulas whose quantifier rank depends on d and the signature’s maximum relation arity.Source: §3 · p. 5
An FO formula of quantifier rank 2 can fail to be equivalent to any Boolean combination of local formulas of quantifier rank at most 2 and basic local sentences.This establishes that Gaifman’s theorem does not generally preserve outer quantifier rank.Source: §3 · p. 5
The example formula asks for an orange node unreachable from x by a walk of length 2 that has no blue neighbour.The displayed formula uses the signature with edge, orange, and blue relations.Source: §3 · p. 5
For every r ≥ 7, the example structure satisfies the formula at v but not v′, although their r-neighbourhoods coincide.A winning two-round Ehrenfeucht–Fraïssé strategy on those neighbourhoods supports the non-equivalence result.Source: §3 · p. 5

4 First-Order Logic on Weighted Structures: FOW+ and ngFOW+

FOW+ combines first-order logic with weight terms, aggregation, and distance atoms on weighted structures. The neighbourhood-guarded variant ngFOW+ supports locality and includes distance-atom FO+ and modulo-counting extensions.

FOW+

FOW+ adds weight atoms and aggregation over tuples satisfying a formula, while weighted structures assign tuples group- or ring-valued weights subject to a locality condition.FOW+ also permits distance atoms dist(x, y) ⩽d.Source: §4 · p. 6

ngFOW+

General FOW+ can express that a vertex shares its weight with a distinct vertex, a property not expressible as a Boolean combination of sentences and local formulas.ngFOW+ restricts predicate use to a neighbourhood-guarded form.Source: §4 · p. 6
In a vertex-weighted digraph, an ngFOW+ sentence can express that every edge points toward the endpoint with the larger weight.Source: §4 · pp. 6–7

FO+

When weight symbols and predicates are unavailable, ngFOW+ coincides with FO+ with distance atoms.Source: §4 · p. 7

FO+MOD

FO+MOD with distance atoms embeds in ngFOW+ by representing each modulo count with a unary weight valued in Z/mZ.The construction assigns weight 1 to each element for each modulus.Source: §4 · p. 7

5 A Rank-Preserving Gaifman Normal Form for ngFOW+

The section establishes a computable, rank-preserving Gaifman normal form for ngFOW+ formulas, with bounds on its outer and inner complexity. It completes the equivalence proof by constructing witnesses that contradict failure of the local condition and establish that μ′(x̄_I) is equivalent to μ(x̄_I).

5 A Rank-Preserving Gaifman Normal Form for ngFOW+

Every φ∈F(q,k,d) has an equivalent computable Gaifman normal form preserving free variables, with bounded outer and inner rank, radius, width, and inner distance.The bounds are outer/inner quantifier rank at most qr(φ)/qr(φ)−1; outer/inner radius at most r(q,k,d)/r(q−1,k+ω,d); width at most k+1+(q−1)ω; and inner distance at most r(q,k,d)+2r(q−1,k+ω,d). Every ngFOW+ formula belongs to some F(q,k,d).Source: §5 · pp. 7–8
The normal form is rank-preserving because its local formulas remain in F(q,k,d) with rank at most qr(φ), yielding forms for FO+ and FO+MOD+ and a simplified proof of [18].The FO+ normal form is used in Appendix E for the simplified proof of the algorithmic meta-theorem [18].Source: §5 · p. 8
The refined theorem makes the conversion a Boolean combination of formulas from S(q,k,d) and L(q,k,d), preserves free variables and rank bounds, and is algorithmic.The sets are constructed so the normal form uses local formulas and basic local or local aggregation sentences.Source: §5 · p. 9
The witnesses b0 and (bj)j∈J would certify ξ(c−1), contradicting its assumed negation and completing the proof that µ′(x̄_I) is equivalent to µ(x̄_I).The construction uses elements bj near separated aj and shows their pairwise distances exceed the required threshold.Source: §5 · p. 12

6 Applications and Outlook

The theorem extends rank-preserving Gaifman normal forms to FO+ and FO+MOD+, and the FO+ form supplies a simplified proof of the nowhere-dense first-order model-checking meta-theorem. The section also identifies limits on extending efficient model checking to weighted logics and outlines further directions.

6 Applications and Outlook

FO+ and FO+MOD+ are special cases of ngFOW+, so Theorem 8 yields rank-preserving Gaifman normal forms for both logics.For FO+, the weight vocabulary is empty; for FO+MOD+, it contains unary weight symbols.Source: §6 · p. 12
The FO+ normal form gives a simplified proof of the algorithmic meta-theorem for first-order model checking on nowhere dense classes [18].The authors suggest that the proof may generalize to FO+MOD+ model checking on nowhere dense classes.Source: §6 · p. 13
For ngFOW+ with integer-valued vertex weights and weight equality, model checking is AW[∗]-hard even on vertex-weighted trees of height 1.The authors conclude that efficient model checking on nowhere dense classes requires suitable restrictions on ngFOW+ and its vocabulary.Source: §6 · p. 13
The section illustrates the FO-to-ngFOW+ translation by encoding a graph as a vertex-weighted tree of height 1 while preserving the formula’s truth on assignments.The construction uses a tree structure with weights that encode vertex and edge information.Source: §6 · p. 13

7 Application: Rank-Preserving Gaifman Normal Forms for FO+ and FO+MOD+

The section derives rank-preserving Gaifman normal forms for FO+ and FO+MOD+ by viewing them as special cases of ngFOW+. The resulting forms retain quantifier-rank bounds and provide explicit bounds on radii and widths.

7 Application: Rank-Preserving Gaifman Normal Forms for FO+ and FO+MOD+

FO+ and FO+MOD+ with distance atoms are treated as special cases of ngFOW+, with no weight symbols for FO+ and unary weight symbols for FO+MOD+.Both settings have parameter ω = 1.Source: §7 · pp. 13–14

7.1 A Rank-Preserving Gaifman Normal Form for FO+

FO+(q, k, d) organizes FO+ formulas by quantifier rank q, at most k free variables, and distance-atom depth d.Its Gaifman normal form is a Boolean combination of local formulas and basic local sentences.Source: §7.1 · p. 14
Every FO+(q, k, d) formula has an equivalent Gaifman-normal-form formula with the same free variables and outer rank at most qr(φ), and inner rank at most qr(φ)−1.The outer and inner radii are bounded by r1(q, k, d) and r1(q−1, k+1, d), respectively; the formula is computable from φ, q, k, d.Source: §7.1 · p. 14

7.2 A Rank-Preserving Gaifman Normal Form for FO+MOD+

Modulo-counting quantifiers are represented using unary weights with ranges Z/mZ, so modulo-counting corresponds to aggregation quantification in the chosen ngFOW+ setting.The translation preserves satisfaction between the original structure and its weighted expansion.Source: §7.2 · p. 14
The FO+MOD+ normal form uses local formulas, basic local sentences, and local modulo-counting sentences.The local modulo-counting sentences test whether the number of local witnesses is congruent to a specified residue.Source: §7.2 · p. 15
Every FO+MOD+(q, k, d) formula has an equivalent Gaifman-normal-form formula preserving its free variables, with outer rank at most qr(φ) and inner rank at most qr(φ)−1.Its radii are bounded by r1(q, k, d) and r1(q−1, k+1, d), and its width and inner distance have the stated bounds; the formula is computable from φ, q, k, d.Source: §7.2 · p. 15
The FO+MOD+ result is presented as a rank-preserving version of the Gaifman normal form for FO+MODM in [28].Source: §7.2 · p. 15

A Details Omitted in Section 2

Lemma 18 shows that locality does not depend on which non-empty tuple of variables is used to list the free variables of a formula. Its proof handles extra variables by assigning them a common value before applying the locality assumption.

A Details Omitted in Section 2

If φ(x̄) is r-local, then φ(ȳ) is r-local for any non-empty tuple ȳ whose variables include all free variables of φ.Source: A Details Omitted in Section 2 · p. 17
The proof assigns a common element to variables in the tuples that are not free in φ, then uses the coincidence lemma and the assumed r-locality.It applies locality in the original structure and the induced neighborhood structure to establish the result.Source: A Details Omitted in Section 2 · pp. 17–18

B Details Omitted in Section 3

The appendix details a counterexample showing that Gaifman normal forms need not preserve outer quantifier rank, then specifies the syntax and semantics of FOW+ and ngFOW+. It defines weighted structures, term comparisons, aggregation quantification, and locality-related rank conventions.

B Details Omitted in Section 3

For r ≥ 7, Duplicator wins the 2-round EF game on the two pointed structures, so local FO formulas of rank at most 2 cannot distinguish the corresponding vertices.The proof supplies good vertex pairs to establish the game strategy.Source: B Details Omitted in Section 3 · pp. 18–19
The appendix concludes that the example formula is not equivalent to any Boolean combination of local formulas of quantifier rank at most 2 and basic local sentences.Source: B Details Omitted in Section 3 · p. 19

C.1 Detailed Definition of Syntax and Semantics of FOW+

A (σ, W)-structure expands a relational structure with typed weight functions, subject to a locality condition requiring nonzero-weight tuples to lie within a relation tuple or have all entries equal.This condition makes the entries of any nonzero-weight tuple form a clique in the Gaifman graph.Source: §C.1 · p. 19
FOW+ terms combine weight values and constants using the available group or ring operations, while predicate atoms test tuples of term values against designated predicates.Ring types also permit multiplication.Source: §C.1 · p. 20
Aggregation quantification sums weights over tuples satisfying a formula and tests whether the result equals a specified value.The quantified weight symbol must have a finite range.Source: §C.1 · pp. 20–21
FOW+ quantifier rank counts nested existential and aggregation quantifiers, while distance atoms are available as quantifier-free formulas.Source: §C.1 · pp. 20–22
ngFOW+ uses a neighbourhood-guarded term-comparison rule, while ngFOW replaces distance atoms with equivalent FO formulas.FOW omits distance atoms altogether.Source: §C.1 · p. 22

C.2 Details Omitted in Example 4

Claim 21 shows that the formula from Example 4 cannot be expressed as a Boolean combination of sentences and local FOW+ formulas. The proof constructs structures with indistinguishable local views but different truth values for that formula.

C.2 Details Omitted in Example 4

No formula equivalent to the Example 4 formula is a Boolean combination of sentences and local FOW+ formulas.The proof assumes such a combination exists and derives a contradiction.Source: §C.2 · pp. 22–23
Among the constructed structures, two satisfy the same sentences in the proposed combination, so its sentence components can be fixed to obtain a local formula.The structures are chosen by the pigeonhole principle, and the resulting local formula has some radius r.Source: §C.2 · p. 23
The selected points have isomorphic radius-r neighborhoods, yet the Example 4 formula holds at one and not the other.The structures have edgeless Gaifman graphs, making the radius-r neighborhoods around the selected points isomorphic.Source: §C.2 · p. 23

D.1 Proof of Lemma 9

Lemma 9 establishes that every formula in L(q, k, d) belongs to F(q, k, d) and is r(q, k, d)-local. Its proof proceeds by induction on quantifier rank, using locality of the constituent atoms and formulas.

D.1 Proof of Lemma 9

Every formula in L(q, k, d) belongs to F(q, k, d) and is r(q, k, d)-local.The proof establishes the claim by induction on q.Source: §D.1 · pp. 23, 25
At quantifier rank zero, the formulas are quantifier-free Boolean combinations of relational, distance, weight, and neighbourhood-guarded term-comparison atoms, which have bounded locality radii.The stated atom radii include 0-locality for relational atoms, d-locality for distance atoms, and 1-locality for weight atoms.Source: §D.1 · p. 23
For the induction step, formulas with added variables remain local by bounding their neighborhoods within the larger radius r(q+1, k, d).The proof applies the induction hypothesis to extended variable tuples and uses the locality condition on weighted structures.Source: §D.1 · pp. 24–25

D.2 Properties of S(q, k, d)

The proof characterizes formulas in S(q, k, d) using atomic sentences, local aggregation sentences, and basic local sentences with bounded parameters. It obtains the characterization by induction, with the quantifier-free case consisting of atomic sentences.

D.2 Properties of S(q, k, d)

Every formula in S(q, k, d) is an atomic sentence, a local aggregation sentence, or a basic local sentence with the stated radius, width, and inner-distance bounds.The local aggregation inner radius is at most r(q−1, k+ω, d); basic local sentences have inner radius at most that bound, width at most k+1+(q−1)ω, and inner distance at most r(q, k, d) + 2 r(q−1, k+ω, d).Source: §D.2 · p. 25
At quantifier rank zero, S(q, k, d) consists of the atomic sentences true, false, nullary relation or weight atoms, and closed term-comparison atoms.The proof identifies these as exactly the atomic sentences in S(0, 0, 0), which is the same set as S(0, k, d).Source: §D.2 · p. 25
The induction step derives local aggregation and basic local sentences from formulas in L, preserving the specified radius bounds and, for basic local sentences, the width and inner-distance bounds.The proof treats the sentence, basic-local-sentence, and local-aggregation cases separately.Source: §D.2 · pp. 25–26

D.3 Proof of Lemma 11 (Feferman–Vaught Decomposition)

This section proves Lemma 11’s Feferman–Vaught decomposition by induction on quantifier rank, using exclusivity normalization and separating Boolean reasoning from the weighted existential step across separated variable sets; the decomposition preserves quantifier-rank bounds through finite sets of formula pairs.

D.3 Proof of Lemma 11 (Feferman–Vaught Decomposition)

Lemma 24 algorithmically replaces any finite set of formula pairs by Boolean combinations whose first entries are mutually exclusive; the construction can instead make the second entries mutually exclusive.The proof constructs disjoint Boolean cases from the original first entries, and the symmetric version handles the second entries.Source: §D.3 · p. 27
Lemma 11 decomposes each formula into finitely many pairs over the two variable blocks, preserving quantifier rank and ensuring mutually exclusive first entries, with an algorithm to compute the pairs.The blocks are indexed by I and K\I, and the decomposition applies when they are nonempty and separated by more than the prescribed radius.Source: §D.3 · pp. 27–28
For a weighted atom using variables from both blocks, if distA(āI; āK\I) > r′, its output is 0S, so the atom holds exactly when s = 0S.Source: §D.3 · p. 29
In the quantifier-rank step, an existential witness is assigned to one side or the other according to which block contains the nearby variable, yielding two inductive decompositions.The proof uses enlarged variable sets and a reduced separation radius, then forms new component formulas while keeping their quantifier rank at most that of the original formula.Source: §D.3 · pp. 31–32
Claim 25 shows that adjoining a nonzero-weight tuple close to one side of a sufficiently separated split leaves the enlarged sides separated by more than r′.The tuple’s coordinates are mutually close under the weighted-structure locality condition, which supports the separation argument.Source: §D.3 · p. 34
Under the separation condition, Claim 26 replaces ψ with an equivalent formula ˆψ built from component formulas whose weight values sum to the target value.The equivalence is immediate when the relevant indices lie on only one side; otherwise it follows by splitting the sum over pairs (t1, t2) with t1 +S t2 = s.Source: §D.3 · p. 34
For each t, Claim 27 constructs a finite, non-empty set of formula pairs that characterizes ϱt across the split, with component quantifier rank bounded by qr(ϱt).The proof applies the induction hypothesis to λ1 and uses mutually exclusive second components to establish the characterization.Source: §D.3 · pp. 34–36
Claim 28 gives the analogous finite, non-empty formula-pair decomposition for ϑt, with component quantifier rank bounded by qr(ϑt).It applies the induction hypothesis to λ2; the proof follows the same lines as Claim 27.Source: §D.3 · pp. 36–37
The proof finishes the weighted existential case by combining the finite decompositions for both sides, then handles disjunctions and negations as in the induction base to complete Lemma 11.When one side of the split is empty, the replacement formula is already covered by one of the two decomposition claims.Source: §D.3 · p. 37

D.4 Detailed Proof of Theorem 10 (Rank-Preserving Gaifman Normal Form)

This section proves the effective rank-preserving Gaifman normal form by induction, handling existential and weighted quantifiers while preserving free variables and quantifier-rank bounds. It then applies the locality theorem to give a simplified proof of the almost-linear-time algorithmic result for first-order properties of nowhere dense structures.

D.4 Detailed Proof of Theorem 10 (Rank-Preserving Gaifman Normal Form)

Every formula in F(q, k, d) is effectively equivalent to a Boolean combination of formulas in S(q, k, d) ∪ L(q, k, d), with the same free variables and the stated quantifier-rank bounds.The outer rank is at most qr(φ), and the inner rank is at most qr(φ)−1.Source: §D.4 · p. 37
The proof inducts on q: the q = 0 base case follows directly from the definitions, and the step reduces formulas to five cases.For k ≥ 1, F(0, k, d) equals L(0, k, d); for k = 0, formulas are Boolean combinations of sentences in S(0, k, d).Source: §D.4 · pp. 37–38
For existential quantification, the inductive normal form is put in disjunctive normal form, separating sentence conditions from local formulas before handling each quantified local formula.If the original formula has no free variables, the quantified local formula is itself a basic local sentence.Source: §D.4 · pp. 38, 39, 42
Lemma 11 decomposes a local formula into conditions on the free-variable tuple and quantified variable, with the latter required to lie beyond distance r′.The proof then expresses the resulting conditions using formulas in the target local and sentence classes while preserving the rank bounds.Source: §D.4 · p. 39
For the selected bj, the choice of π yields distA(āI; bj) > r′; hence bj ∈ B is a witness to A |= μ(ā), as claimed in this step.Source: §D.4 · p. 40
When the witness set has bounded packing, a plateau in its decreasing separation counts supplies c and ℓ for matching the normal-form conditions to existential truth or falsity.The proof uses distance inequalities to transfer separated witnesses between the predicate set and the free-variable tuple.Source: §D.4 · pp. 40–41
For weighted quantifiers, the proof follows the analogous case of [1, Theorem 4.6] but uses Lemma 11 instead of its Feferman–Vaught decompositions.Disjunctive normal form yields mutually exclusive sentence conditions, which partition the cases for the remaining local formulas.Source: §D.4 · p. 42
Case (v) reduces the formula to a Boolean combination in L(q+1, k, d) ∪ S(q+1, k, d), with outer rank at most qr(φ) and inner rank at most qr(φ) − 1.The construction uses a finite family of formula pairs whose first entries are mutually exclusive.Source: §D.4 · pp. 43, 45
The weighted-sum step recovers the weight of far tuples by subtracting the near-tuple sum from the total, using inverses in the finite abelian group S.The resulting formula ˆµ is equivalent to µ.Source: §D.4 · pp. 44–45

Deciding First-Order Properties of Nowhere Dense Structures

The paper applies its new locality theorem, specifically Corollary 16, to give a simplified proof of Theorem 33 [18].The result is stated for the non-uniform version, and the proof can also be adapted to the uniform version.Source: Deciding First-Order Properties of… · p. 45
For every nowhere dense class C, first-order sentence φ, and ε > 0, Theorem 33 [18] decides A |= φ for A ∈ C in time O_C,φ,ε(|A|^(1+ε)).The theorem’s constants may depend on C, φ, and ε.Source: Deciding First-Order Properties of… · p. 45
The simplified proof is not self-contained because it relies on several substantial results from [18], which are stated without proof.Source: Deciding First-Order Properties of… · p. 45
For fixed signature σ, the Gaifman graph of a σ-structure A can be computed from A in time O(∥A∥).This lets the proof compute the Gaifman graphs it uses within the permitted time bounds.Source: Deciding First-Order Properties of… · p. 45

E.1 The Splitter Game and Nowhere Dense Classes

The splitter game characterizes nowhere-dense classes, and a bounded-round strategy underlies efficient algorithmic tools used for these classes. The section also presents neighborhood covers and algorithms for finding distance-independent sets.

E.1 The Splitter Game and Nowhere Dense Classes

A graph class is nowhere dense exactly when, for every radius, Splitter has a winning strategy within a class-wide bounded number of rounds.A structure class is nowhere dense when its Gaifman graphs form a nowhere-dense graph class.Source: §E.1 · p. 46
On nowhere-dense classes, Splitter can force a win within t(C, r) rounds even when Connector may restrict each round to a subgraph.The lemma’s strategy removes neighborhoods around chosen vertices; its generalized-game interpretation is stated explicitly.Source: §E.1 · pp. 46–47

E.2 Neighbourhood Covers

For nowhere-dense graphs, the cited neighborhood-cover construction runs in O(n^1+ε) time and yields covers of radius at most 2r and maximum degree O(n^ε).The cover also has a centre function locating each cluster within distance 2r of its centre.Source: §E.2 · p. 48

E.3 Distance Independent Sets

For nowhere-dense structure classes, an algorithm decides in O(n^1+ε) time whether a given set contains a d-independent subset of size at least m.A d-independent set has pairwise distances greater than d.Source: §E.3 · p. 48

E.4 The Removal Lemma

The removal lemma translates formulas to structures after elements are deleted, while retaining the formula’s bounded logical parameters. Its iterated form handles multiple deletions and distinguishes evaluations on surviving and removed elements.

E.4 The Removal Lemma

The algorithm applies the removal lemma repeatedly while following Splitter’s strategy, translating formulas between the original and reduced structures.The removal operation preserves the Gaifman graph as the induced graph on the remaining elements.Source: §E.4 · p. 48
The removal lemma translates a formula after deleting selected variables’ assigned elements into the expanded signature, without changing its FO+ parameters q, k, and d.The expansion records relation tuples after dropping occurrences of removed elements and adds unary predicates for their distance neighborhoods.Source: §E.4 · p. 48
After deleting s distinct elements, the iterated lemma supplies a formula for surviving elements and a sentence for each deleted element’s evaluation.An algorithm computes these formulas from the original formula and s.Source: §E.4 · p. 50

E.5 The Main Algorithm

The algorithm evaluates first-order formulas on nowhere dense structures by recursively computing local formula sets over neighborhood covers. Its running time is O_C,φ,ε(|A|^(1+ε)).

E.5 The Main Algorithm

O_C,φ,ε(|A|^(1+ε)) time suffices to compute φ(A) for FO+ formulas on structures in a nowhere dense class.The running-time analysis derives this bound at the root of the recursion.Source: §E.5 · pp. 50, 54
The algorithm first converts φ into a Boolean combination of local formulas and basic local sentences, then evaluates their local formula sets and sentence truth values.For a basic local sentence, evaluation reduces to finding a sufficiently large independent set within the relevant formula set.Source: §E.5 · p. 51
It recursively computes local formula sets on structures induced by clusters in bounded-radius neighborhood covers, using locality to recover membership in the original structure.The recursion has bounded depth, and small clusters are handled by brute force.Source: §E.5 · pp. 51–52
When a cluster requires removing vertices, the algorithm extends the signature and transforms formulas so their evaluations can be recovered from recursive computations on smaller cover clusters.The accumulated removed sets are bounded by ℓ, and the resulting signature size depends on the input formula and class, not the structure size.Source: §E.5 · pp. 52–53