Gaifman's normal-form theorem
Lax512892.GaifmanNormalForm · concepts/Lax512892/GaifmanNormalForm.lean · lax-512892
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Every first-order formula over a finite relational vocabulary has an effective, uniform translation into a Boolean combination of formulas local around its free tuple and basic local sentences. For one common radius , a basic local sentence asserts that there are witnesses, pairwise at Gaifman distance greater than , all satisfying the same one-variable -local formula.
If the input has quantifier rank and free variables, the radius can be chosen at most , and every basic local sentence needs at most witnesses. When the input is a sentence, no local formula with free variables occurs: its normal form is a Boolean combination solely of basic local sentences. The equivalence is over all finite structures.
This is the uniform formulation of Gaifman's theorem used in Theorem 4.22 of Libkin's Elements of Finite Model Theory, following Gaifman's original locality theorem.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
No proof in the archive yet — this claim is open.
Lean source view on GitHub
| 1 | import Lax512892.Locality |
| 2 | import Mathlib.Data.Fintype.Basic |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Gaifman's normal-form theorem |
| 7 | type: theorem |
| 8 | --- |
| 9 | Every first-order formula over a finite relational vocabulary has an effective, |
| 10 | uniform translation into a Boolean combination of formulas local around its |
| 11 | free tuple and basic local sentences. For one common radius `r`, a basic local |
| 12 | sentence asserts that there are `s` witnesses, pairwise at Gaifman distance |
| 13 | greater than `2r`, all satisfying the same one-variable `r`-local formula. |
| 14 | |
| 15 | If the input has quantifier rank `q` and `k` free variables, the radius can be |
| 16 | chosen at most `7^q`, and every basic local sentence needs at most `q + k` |
| 17 | witnesses. When the input is a sentence, no local formula with free variables |
| 18 | occurs: its normal form is a Boolean combination solely of basic local |
| 19 | sentences. The equivalence is over all finite structures. |
| 20 | |
| 21 | This is the uniform formulation of Gaifman's theorem used in Theorem 4.22 of |
| 22 | Libkin's *Elements of Finite Model Theory*, following Gaifman's original |
| 23 | locality theorem. |
| 24 | |
| 25 | # Formalization notes |
| 26 | |
| 27 | The output syntax is reified. `NormalForm σ k` stores its common radius and a |
| 28 | Boolean combination whose atoms are either local formulas around the `k` free |
| 29 | variables or basic local sentences. This permits the radius, witness, and |
| 30 | sentence-only conditions to be stated directly about every atom that occurs. |
| 31 | |
| 32 | The theorem quantifies once over a single translation function, before any |
| 33 | input formula or structure. This records uniformity more faithfully than a |
| 34 | separate existential normal form for each formula. It does not assert a running |
| 35 | time bound for the translation. A constructive proof of the axiom supplies the |
| 36 | effective transformation; code extraction is not part of the concept surface. |
| 37 | |
| 38 | The `s = 0` basic sentence is allowed and is vacuously true, exactly as the |
| 39 | displayed first-order sentence with an empty witness tuple. Pairwise separation |
| 40 | is imposed only for distinct witness indices. |
| 41 | -/ |
| 42 | |
| 43 | namespace Lax512892.GaifmanNormalForm |
| 44 | |
| 45 | open Lax512892.RelationalStructures Lax512892.FirstOrder Lax512892.Locality |
| 46 | |
| 47 | universe u |
| 48 | |
| 49 | /-- Boolean combinations of atoms of type `α`. -/ |
| 50 | inductive BooleanCombination (α : Type u) : Type u |
| 51 | /-- An atomic constituent. -/ |
| 52 | | atom (a : α) |
| 53 | /-- Truth, serving also as the empty Boolean combination. -/ |
| 54 | | truth |
| 55 | /-- Negation. -/ |
| 56 | | not (b : BooleanCombination α) |
| 57 | /-- Conjunction. -/ |
| 58 | | and (b c : BooleanCombination α) |
| 59 | |
| 60 | namespace BooleanCombination |
| 61 | |
| 62 | /-- Evaluation of a Boolean combination from an interpretation of its atoms. -/ |
| 63 | def eval {α : Type u} (value : α → Prop) : BooleanCombination α → Prop |
| 64 | | .atom a => value a |
| 65 | | .truth => True |
| 66 | | .not b => ¬ b.eval value |
| 67 | | .and b c => b.eval value ∧ c.eval value |
| 68 | |
| 69 | /-- The atoms occurring in a Boolean combination, with multiplicity. -/ |
| 70 | def atoms {α : Type u} : BooleanCombination α → List α |
| 71 | | .atom a => [a] |
| 72 | | .truth => [] |
| 73 | | .not b => b.atoms |
| 74 | | .and b c => b.atoms ++ c.atoms |
| 75 | |
| 76 | end BooleanCombination |
| 77 | |
| 78 | /-- A basic local sentence at radius `r`: `witnessCount` pairwise far-apart |
| 79 | witnesses all satisfy the same one-variable local formula `property`. -/ |
| 80 | structure BasicLocalSentence (σ : Vocabulary) (r : ℕ) where |
| 81 | /-- The number of witnesses. -/ |
| 82 | witnessCount : ℕ |
| 83 | /-- The uniform local property required of every witness. -/ |
| 84 | property : LocalFormula σ 1 r 0 |
| 85 | |
| 86 | namespace BasicLocalSentence |
| 87 | |
| 88 | /-- Semantics of a basic local sentence. -/ |
| 89 | def Sat {σ : Vocabulary} {M : Type*} {r : ℕ} (A : Structure σ M) |
| 90 | (β : BasicLocalSentence σ r) : Prop := |
| 91 | ∃ witnesses : Fin β.witnessCount → M, |
| 92 | (∀ i, β.property.Sat A (fun _ => witnesses i) Fin.elim0) ∧ |
| 93 | ∀ i j, i ≠ j → |
| 94 | ¬ distanceAtMost A (2 * r) (witnesses i) (witnesses j) |
| 95 | |
| 96 | end BasicLocalSentence |
| 97 | |
| 98 | /-- A Gaifman normal form for a formula with `k` free variables. All its atoms |
| 99 | share the stored locality radius. -/ |
| 100 | structure NormalForm (σ : Vocabulary) (k : ℕ) where |
| 101 | /-- The common locality radius. -/ |
| 102 | radius : ℕ |
| 103 | /-- A Boolean combination of local formulas and basic local sentences. -/ |
| 104 | body : BooleanCombination |
| 105 | (LocalFormula σ k radius 0 ⊕ BasicLocalSentence σ radius) |
| 106 | |
| 107 | namespace NormalForm |
| 108 | |
| 109 | /-- Satisfaction of a normal form under an environment for its free variables. -/ |
| 110 | def Sat {σ : Vocabulary} {M : Type*} {k : ℕ} (A : Structure σ M) |
| 111 | (env : Fin k → M) (nf : NormalForm σ k) : Prop := |
| 112 | nf.body.eval (Sum.elim |
| 113 | (fun ψ => ψ.Sat A env Fin.elim0) |
| 114 | (fun basic => basic.Sat A)) |
| 115 | |
| 116 | /-- Every basic local sentence occurring in `nf` uses at most `bound` |
| 117 | witnesses. -/ |
| 118 | def WitnessesBounded {σ : Vocabulary} {k : ℕ} |
| 119 | (nf : NormalForm σ k) (bound : ℕ) : Prop := |
| 120 | ∀ basic : BasicLocalSentence σ nf.radius, |
| 121 | Sum.inr basic ∈ nf.body.atoms → basic.witnessCount ≤ bound |
| 122 | |
| 123 | /-- No local-formula atom occurs in `nf`. -/ |
| 124 | def ContainsOnlyBasicSentences {σ : Vocabulary} {k : ℕ} |
| 125 | (nf : NormalForm σ k) : Prop := |
| 126 | ∀ ψ : LocalFormula σ k nf.radius 0, Sum.inl ψ ∉ nf.body.atoms |
| 127 | |
| 128 | end NormalForm |
| 129 | |
| 130 | /-- **Gaifman's normal-form theorem.** There is a uniform transformation of |
| 131 | every first-order formula over `σ` into an equivalent Gaifman normal form. For |
| 132 | an input of quantifier rank `q` with `k` free variables, its common radius is at |
| 133 | most `7 ^ q`, each basic local sentence has at most `q + k` witnesses, and a |
| 134 | sentence is translated using basic local sentences only. Equivalence holds in |
| 135 | every finite `σ`-structure. -/ |
| 136 | axiom gaifmanNormalForm (σ : Vocabulary) : |
| 137 | ∃ translate : (k : ℕ) → Formula σ k → NormalForm σ k, |
| 138 | ∀ (k : ℕ) (φ : Formula σ k), |
| 139 | (translate k φ).radius ≤ 7 ^ φ.quantifierRank ∧ |
| 140 | (translate k φ).WitnessesBounded (φ.quantifierRank + k) ∧ |
| 141 | (k = 0 → (translate k φ).ContainsOnlyBasicSentences) ∧ |
| 142 | ∀ {M : Type} [Fintype M] (A : Structure σ M) (env : Fin k → M), |
| 143 | φ.Sat A env ↔ (translate k φ).Sat A env |
| 144 | |
| 145 | end Lax512892.GaifmanNormalForm |
| 146 |
Formalization notes
The output syntax is reified. stores its common radius and a Boolean combination whose atoms are either local formulas around the free variables or basic local sentences. This permits the radius, witness, and sentence-only conditions to be stated directly about every atom that occurs.
The theorem quantifies once over a single translation function, before any input formula or structure. This records uniformity more faithfully than a separate existential normal form for each formula. It does not assert a running time bound for the translation. A constructive proof of the axiom supplies the effective transformation; code extraction is not part of the concept surface.
The basic sentence is allowed and is vacuously true, exactly as the displayed first-order sentence with an empty witness tuple. Pairwise separation is imposed only for distinct witness indices.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments