Lax Lean Archive

Positive Ehrenfeucht–Fraïssé games

Lax503819.PositiveGames · concepts/Lax503819/PositiveGames.lean · lax-503819

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

    Duplicator must preserve the order and equality of selected positions in both directions, and the letter order from the first word to the second. In each round Spoiler selects a position in either word; Duplicator responds in the other. SurvivesSurvives expresses existence of a winning strategy recursively. A move in an empty word is unavailable, while inability to respond loses.

    The two statements are the word versions of Theorem 3.7 and Corollary 3.8. The formula characterization includes previously selected positions. The language characterization requires a finite alphabet and a single uniform round bound for all pairs of words.

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

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 definable_iff_bounded_games proven

    2 survives_iff_formulas proven

    Lean source view on GitHub

    1import Lax503819.PositiveLogic
    2
    3/-!
    4---
    5title: Positive Ehrenfeucht–Fraïssé games
    6type: theorem
    7---
    8Duplicator must preserve the order and equality of selected positions in both
    9directions, and the letter order from the first word to the second. In each
    10round Spoiler selects a position in either word; Duplicator responds in the
    11other. `Survives` expresses existence of a winning strategy recursively.
    12A move in an empty word is unavailable, while inability to respond loses.
    13
    14The two statements are the word versions of Theorem 3.7 and Corollary 3.8.
    15The formula characterization includes previously selected positions. The
    16language characterization requires a finite alphabet and a single uniform
    17round bound for all pairs of words.
    18-/
    19
    20namespace Lax503819.PositiveGames
    21
    22open Lax503819.Words Lax503819.PositiveLogic
    23
    24def Valid {A : Type} [LE A] {u v : List A} {k : ℕ}
    25 (α : Fin k → Position u) (β : Fin k → Position v) : Prop :=
    26 (∀ i, u.get (α i) ≤ v.get (β i)) ∧
    27 (∀ i j, α i ≤ α j ↔ β i ≤ β j)
    28
    29def Survives {A : Type} [LE A] (u v : List A) :
    30 ℕ → {k : ℕ} → (Fin k → Position u) → (Fin k → Position v) → Prop
    31 | 0, _, α, β => Valid α β
    32 | r + 1, _, α, β => Valid α β ∧
    33 (∀ x : Position u, ∃ y : Position v,
    34 Survives u v r (Fin.cons x α) (Fin.cons y β)) ∧
    35 (∀ y : Position v, ∃ x : Position u,
    36 Survives u v r (Fin.cons x α) (Fin.cons y β))
    37
    38def DuplicatorWins {A : Type} [LE A] (r : ℕ) (u v : List A) : Prop :=
    39 Survives u v r (k := 0) Fin.elim0 Fin.elim0
    40
    41axiom survives_iff_formulas {A : Type} [PartialOrder A] [Fintype A]
    42 (u v : List A) (r k : ℕ)
    43 (α : Fin k → Position u) (β : Fin k → Position v) :
    44 Survives u v r α β ↔
    45 ∀ φ : Formula A k, φ.rank ≤ r → φ.Realize u α → φ.Realize v β
    46
    47axiom definable_iff_bounded_games {A : Type} [PartialOrder A] [Fintype A]
    48 (L : Language A) :
    49 Definable L ↔ ∃ r : ℕ, ∀ u v, u ∈ L → v ∉ L → ¬ DuplicatorWins r u v
    50
    51end Lax503819.PositiveGames
    52
    Show ProofShow Proof
    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…