Invariance of formulas and inductions under pebble games
Lax945089.PebbleInvariance · concepts/Lax945089/PebbleInvariance.lean · lax-945089
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
A first-order formula that fits in variables, its free variables and its quantifier depth together, cannot separate two tuples related by the -pebble equivalence generated by agreement on atomic types. On bare sets with at least elements each, two -tuples with the same equalities between coordinates are -pebble equivalent, whatever the two sizes: pebbles cannot count past . And an inflationary induction with variable budget takes the same value on two structures that have -pebble equivalent tuples.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Order |
| 2 | import Mathlib.Order.Defs.LinearOrder |
| 3 | import Lax904597.Problems |
| 4 | import Lax904597.Interpretations |
| 5 | import Lax904597.Relativized |
| 6 | import Lax904597.SecondOrder |
| 7 | import Lax904597.Classes |
| 8 | import Lax485149.Problems |
| 9 | import Lax485149.FirstOrderDefinability |
| 10 | import Lax485149.TransitiveClosure |
| 11 | import Lax485149.DeterministicTransitiveClosure |
| 12 | import Lax485149.ClassNL |
| 13 | import Lax485149.ClassL |
| 14 | import Lax535992.InflationaryFixedPoint |
| 15 | import Lax535992.ClassPTIME |
| 16 | import Lax134656.PartialFixedPoint |
| 17 | import Lax895169.ArithmeticLogic |
| 18 | import Lax945089.OrderFreeFirstOrder |
| 19 | import Lax945089.EhrenfeuchtGames |
| 20 | import Lax945089.PebbleGames |
| 21 | import Lax945089.Even |
| 22 | import Lax945089.Parity |
| 23 | import Lax945089.TransitiveClosureReductions |
| 24 | |
| 25 | /-! |
| 26 | --- |
| 27 | title: Invariance of formulas and inductions under pebble games |
| 28 | type: theorem |
| 29 | --- |
| 30 | A first-order formula that fits in variables, its free variables and |
| 31 | its quantifier depth together, cannot separate two tuples related by the |
| 32 | -pebble equivalence generated by agreement on atomic types. On bare |
| 33 | sets with at least elements each, two -tuples with the same |
| 34 | equalities between coordinates are -pebble equivalent, whatever the two |
| 35 | sizes: pebbles cannot count past . And an inflationary induction |
| 36 | with variable budget takes the same value on two structures that have |
| 37 | -pebble equivalent tuples. |
| 38 | -/ |
| 39 | |
| 40 | namespace Lax945089.PebbleInvariance |
| 41 | |
| 42 | open FirstOrder FirstOrder.Language |
| 43 | open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.SecondOrder |
| 44 | open Lax904597.Classes |
| 45 | open Lax485149.Problems Lax485149.FirstOrderDefinability Lax485149.TransitiveClosure |
| 46 | open Lax485149.DeterministicTransitiveClosure Lax485149.ClassNL Lax485149.ClassL |
| 47 | open Lax535992.InflationaryFixedPoint Lax535992.ClassPTIME |
| 48 | open Lax134656.PartialFixedPoint Lax895169.ArithmeticLogic |
| 49 | open Lax945089.OrderFreeFirstOrder Lax945089.EhrenfeuchtGames Lax945089.PebbleGames |
| 50 | open Lax945089.Even Lax945089.Parity |
| 51 | open Lax945089.TransitiveClosureReductions |
| 52 | |
| 53 | /-- A formula within `k` variables cannot separate `k`-pebble equivalent tuples. -/ |
| 54 | axiom realize_equivK₂ : |
| 55 | ∀ {L : Language.{0, 0}} {M N : Type} {k : ℕ} [L.IsRelational] [L.Structure M] [L.Structure N] |
| 56 | [Finite M] [Finite N] {S : Set ((n : ℕ) × L.Relations n)} {α : Type} [Fintype α] {n : ℕ} |
| 57 | (φ : L.BoundedFormula α n) (g : α → Fin k) (h : Fin n → Fin k), Function.Injective h → |
| 58 | (∀ (i : α) (j : Fin n), g i ≠ h j) → |
| 59 | (Finset.image g Finset.univ ∪ Finset.image h Finset.univ).card + qdepth φ ≤ k → |
| 60 | RelsIn S φ → ∀ (v : Fin k → M) (w : Fin k → N), EquivK₂ (atomicAgreeOn₂ S M N k) v w → |
| 61 | ((φ.Realize (fun i => v (g i)) fun j => v (h j)) ↔ |
| 62 | φ.Realize (fun i => w (g i)) fun j => w (h j)) |
| 63 | |
| 64 | /-- On bare sets, tuples with the same equalities are `k`-pebble equivalent. -/ |
| 65 | axiom equivK₂_bare : |
| 66 | ∀ {M N : Type} {k : ℕ} [Language.empty.Structure M] [Language.empty.Structure N] [Finite M] |
| 67 | [Finite N] |
| 68 | {S : Set ((n : ℕ) × Language.empty.Relations n)}, k ≤ Nat.card M → k ≤ Nat.card N → |
| 69 | ∀ {v : Fin k → M} {w : Fin k → N}, (∀ (p q : Fin k), v p = v q ↔ w p = w q) → |
| 70 | EquivK₂ (atomicAgreeOn₂ S M N k) v w |
| 71 | |
| 72 | /-- An inflationary induction cannot separate two structures with `k`-pebble |
| 73 | equivalent tuples. -/ |
| 74 | axiom ifpHolds_equivK₂ : |
| 75 | ∀ {L : Language.{0, 0}} {M N : Type} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} |
| 76 | [L.Structure M] [L.Structure N] [L.IsRelational] [Finite M] [Finite N] (d : StepDef L), |
| 77 | StepDef.VarBound d k → StepDef.UsesRels d S → qdepth d.out ≤ k → |
| 78 | ∀ {v : Fin k → M} {w : Fin k → N}, EquivK₂ (atomicAgreeOn₂ S M N k) v w → |
| 79 | (d.IFPHolds M ↔ d.IFPHolds N) |
| 80 | |
| 81 | end Lax945089.PebbleInvariance |
| 82 |
Builds on
Lax134656.PartialFixedPointLax485149.ClassLLax485149.ClassNLLax485149.DeterministicTransitiveClosureLax485149.FirstOrderDefinabilityLax485149.ProblemsLax485149.TransitiveClosureLax535992.ClassPTIMELax535992.InflationaryFixedPointLax895169.ArithmeticLogicLax904597.ClassesLax904597.InterpretationsLax904597.ProblemsLax904597.RelativizedLax904597.SecondOrderLax945089.EhrenfeuchtGamesLax945089.EvenLax945089.OrderFreeFirstOrderLax945089.ParityLax945089.PebbleGamesLax945089.TransitiveClosureReductions
Used by
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments