Lax Lean Archive

Gaifman's locality theorem with a rank bound

Lax185574.GaifmanLocality · concepts/Lax185574/GaifmanLocality.lean · lax-185574

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    For all α, q, k ∈ ℕ there is a p = p(α, q, k), computable from α, q, k, with the following property. Let σ be a finite relational signature of arity at most α. Every σ-formula φ(x̄) of quantifier rank at most q and with |x̄| ≤ k free variables is equivalent to a σ-formula φ^loc(x̄), computable from φ, that is a Boolean combination of basic 7^q-local sentences and 7^q-local formulas, each of quantifier rank at most p.

    This is Gaifman's locality theorem. Gaifman's paper does not state the bound p explicitly. An analysis of its proof shows that p depends only on α, q and k, and not on the signature σ, as the rank-preserving locality theorems of Dreier and Toruńczyk and of van Bergerem, Grohe and Schweikardt make explicit for their variants of local formulas. The dependence of p on α comes from expressing the distance predicates in plain first-order logic.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 62 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.FirstOrderTypes
    2import Lax185574.LocalFormulas
    3
    4/-!
    5---
    6title: Gaifman's locality theorem with a rank bound
    7type: theorem
    8---
    9For all α, q, k ∈ ℕ there is a p = p(α, q, k), computable from α, q, k,
    10with the following property. Let σ be a finite relational signature of
    11arity at most α. Every σ-formula φ(x̄) of quantifier rank at most q and
    12with |x̄| ≤ k free variables is equivalent to a σ-formula φ^loc(x̄),
    13computable from φ, that is a Boolean combination of basic 7^q-local
    14sentences and 7^q-local formulas, each of quantifier rank at most p.
    15
    16This is Gaifman's locality theorem. Gaifman's paper does not state the
    17bound p explicitly. An analysis of its proof shows that p depends only
    18on α, q and k, and not on the signature σ, as the rank-preserving locality theorems of Dreier and
    19Toruńczyk and of van Bergerem, Grohe and Schweikardt make explicit for
    20their variants of local formulas. The dependence of p on α comes from expressing the
    21distance predicates in plain first-order logic.
    22
    23# Formalization notes
    24
    25The number p is quantified before the signature, so it depends on α, q
    26and k only. A finite relational signature of arity at most α is a
    27relational language with finitely many relation symbols, none of arity
    28above α. The formula has exactly n free variables for some n ≤ k.
    29
    30The Boolean combinations are those generated from the constituents by
    31falsum and implication, which give all Boolean connectives. A basic
    32local sentence becomes a formula with the free variables x̄ by the
    33evident relabelling of its (absent) free variables. Each constituent,
    34a 7^q-local formula or a basic 7^q-local sentence, has quantifier rank
    35at most p, counting the quantifiers of the dist formulas in the ball
    36guards. Equivalence is over all finite structures with domain in an arbitrary
    37universe, including the empty one. The theorem holds for all structures,
    38but its only use, `Lax185574.LocalToGlobal`, concerns finite ones.
    39
    40The present paper asserts that p is computable from α, q, k and that
    41φ^loc is computable from φ. Here both only exist, since no algorithm uses them.
    42-/
    43
    44namespace Lax185574.GaifmanLocality
    45
    46open FirstOrder FirstOrder.Language
    47open Lax185574.FirstOrderTypes Lax185574.LocalFormulas
    48
    49universe u v w z
    50
    51variable {L : Language.{u, v}}
    52
    53/-- `IsBooleanCombination P φ`: the formula `φ` is a Boolean combination
    54of formulas satisfying `P`, built by falsum and implication. -/
    55inductive IsBooleanCombination {α : Type w} (P : L.Formula α → Prop) :
    56 L.Formula α → Prop
    57 /-- A constituent is a Boolean combination. -/
    58 | atom {φ : L.Formula α} : P φ → IsBooleanCombination P φ
    59 /-- Falsum is a Boolean combination. -/
    60 | falsum : IsBooleanCombination P ⊥
    61 /-- Implications of Boolean combinations are Boolean combinations. -/
    62 | imp {φ ψ : L.Formula α} :
    63 IsBooleanCombination P φ → IsBooleanCombination P ψ →
    64 IsBooleanCombination P (φ.imp ψ)
    65
    66/-- The constituents of a Gaifman normal form with radius `h` and rank
    67bound `p`: `h`-local formulas and basic `h`-local sentences, each of
    68quantifier rank at most `p`. -/
    69def IsLocalConstituent [Finite (Σ l, L.Relations l)] (h p : ℕ) {n : ℕ}
    70 (χ : L.Formula (Fin n)) : Prop :=
    71 (IsLocal h χ ∧ quantifierRank χ ≤ p) ∨
    72 ∃ ψ : L.Sentence, IsBasicLocal h ψ ∧ quantifierRank ψ ≤ p ∧
    73 χ = ψ.relabel Empty.elim
    74
    75/-- **Gaifman's locality theorem.** For all `α, q, k` there is a rank
    76bound `p` such that every formula of quantifier rank at most `q` with at
    77most `k` free variables, over a finite relational signature of arity at
    78most `α`, is equivalent to a Boolean combination of `7^q`-local formulas
    79and basic `7^q`-local sentences of quantifier rank at most `p`. -/
    80axiom exists_local_equivalent (α q k : ℕ) :
    81 ∃ p : ℕ, ∀ (L : Language.{u, v}) [L.IsRelational] [Finite (Σ l, L.Relations l)],
    82 (∀ l, α < l → IsEmpty (L.Relations l)) →
    83 ∀ (n : ℕ), n ≤ k → ∀ φ : L.Formula (Fin n), quantifierRank φ ≤ q →
    84 ∃ ψ : L.Formula (Fin n), FinitelyEquivalent.{u, v, z, 0} φ ψ ∧
    85 IsBooleanCombination (IsLocalConstituent (7 ^ q) p) ψ
    86
    87end Lax185574.GaifmanLocality
    88
    Show Proof
    Formalization notes

    The number p is quantified before the signature, so it depends on α, q and k only. A finite relational signature of arity at most α is a relational language with finitely many relation symbols, none of arity above α. The formula has exactly n free variables for some n ≤ k.

    The Boolean combinations are those generated from the constituents by falsum and implication, which give all Boolean connectives. A basic local sentence becomes a formula with the free variables x̄ by the evident relabelling of its (absent) free variables. Each constituent, a 7^q-local formula or a basic 7^q-local sentence, has quantifier rank at most p, counting the quantifiers of the dist formulas in the ball guards. Equivalence is over all finite structures with domain in an arbitrary universe, including the empty one. The theorem holds for all structures, but its only use, Lax185574.LocalToGlobalLax185574.LocalToGlobal, concerns finite ones.

    The present paper asserts that p is computable from α, q, k and that φ^loc is computable from φ. Here both only exist, since no algorithm uses them.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…