Lax Lean Archive

The edges of a definable flip are quantifier-free definable

Lax185574.DefinableFlipFormula · concepts/Lax185574/DefinableFlipFormula.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

    Observation

    The edges of a definable flip can be defined in the original graph. More precisely, for every s ∈ ℕ and symmetric relation R ⊆ Π^s × Π^s there exists a quantifier-free formula E_{⊕R}(x, y, z̄) such that for every graph G, tuple p̄ ∈ V(G)^s, and vertices u, v ∈ V(G),

    G ⊕ (p̄, R) ⊨ E(u, v) ⟺ G ⊨ E_{⊕R}(u, v, p̄).

    Concept map
    12 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 20 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.DefinableFlips
    2import Mathlib.ModelTheory.Complexity
    3
    4/-!
    5---
    6title: The edges of a definable flip are quantifier-free definable
    7type: observation
    8---
    9The edges of a definable flip can be defined in the original graph. More
    10precisely, for every s ∈ ℕ and symmetric relation R ⊆ Π^s × Π^s there
    11exists a quantifier-free formula E_{⊕R}(x, y, z̄) such that for every
    12graph G, tuple p̄ ∈ V(G)^s, and vertices u, v ∈ V(G),
    13
    14G ⊕ (p̄, R) ⊨ E(u, v) ⟺ G ⊨ E_{⊕R}(u, v, p̄).
    15
    16# Formalization notes
    17
    18The formula is in mathlib's language of graphs with the free variables
    19`Fin 2 ⊕ Fin s`: the left summand is (x, y) and the right summand is z̄.
    20Quantifier-free is mathlib's `IsQF`. The formula is chosen before the
    21graph, so one formula works for all graphs on all vertex types of a
    22fixed universe, finite or infinite. G ⊕ (p̄, R) ⊨ E(u, v) is adjacency
    23in `DefinableFlips.flipOver`.
    24-/
    25
    26namespace Lax185574.DefinableFlipFormula
    27
    28open FirstOrder FirstOrder.Language
    29open Lax185574.AtomicTypes Lax185574.DefinableFlips
    30
    31universe u
    32
    33/-- **Definable flips are quantifier-free definable.** For a symmetric
    34relation `R` on atomic types over `s`-tuples, one quantifier-free
    35formula `E_{⊕R}(x, y, z̄)` defines the edges of `G ⊕ (p̄, R)` in `G`, for
    36every graph `G` and tuple `p̄`. -/
    37axiom exists_isQF_flipOver_formula (s : ℕ)
    38 (R : (Fin s → PairType) → (Fin s → PairType) → Prop)
    39 (hR : ∀ P Q, R P Q → R Q P) :
    40 ∃ φ : Language.graph.Formula (Fin 2 ⊕ Fin s), φ.IsQF ∧
    41 ∀ (V : Type u) (G : SimpleGraph V) (p : Fin s → V) (x y : V),
    42 (flipOver G p R).Adj x y ↔
    43 @Formula.Realize Language.graph V G.structure _ φ (Sum.elim ![x, y] p)
    44
    45end Lax185574.DefinableFlipFormula
    46
    Show Proof
    Formalization notes

    The formula is in mathlib's language of graphs with the free variables Fin2⊕FinsFin 2 ⊕ Fin s: the left summand is (x, y) and the right summand is z̄. Quantifier-free is mathlib's IsQFIsQF. The formula is chosen before the graph, so one formula works for all graphs on all vertex types of a fixed universe, finite or infinite. G ⊕ (p̄, R) ⊨ E(u, v) is adjacency in DefinableFlips.flipOverDefinableFlips.flipOver.

    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…