Lax Lean Archive

Monadic dependence through the independence property

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

    A formula Ο†(x, y) in the signature of colored graphs has the independence property on a graph class π’ž if for every n there are a coloring G⁺ of a graph G ∈ π’ž, vertices a₁, …, aβ‚™, and vertices b_J for J βŠ† [n] such that G⁺ ⊨ Ο†(aα΅’, b_J) holds exactly when i ∈ J. A class is monadically dependent if and only if no formula has the independence property on it.

    By a result of Baldwin and Shelah, one may equivalently allow formulas Ο†(xΜ„, Θ³) with tuples of variables, and tuples āᡒ and bΜ„_J. On a monadically dependent class, no such formula has the independence property either.

    Concept map
    4 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 monadicallyDependent_iff_forall_not_hasIP proven

    2 not_hasIP_of_monadicallyDependent proven

    In the paper

    • page 60 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.MonadicDependence
    2
    3/-!
    4---
    5title: Monadic dependence through the independence property
    6type: theorem
    7---
    8A formula Ο†(x, y) in the signature of colored graphs has the
    9*independence property* on a graph class π’ž if for every n there are a
    10coloring G⁺ of a graph G ∈ π’ž, vertices a₁, …, aβ‚™, and vertices b_J for
    11J βŠ† [n] such that G⁺ ⊨ Ο†(aα΅’, b_J) holds exactly when i ∈ J. A class is
    12monadically dependent if and only if no formula has the independence
    13property on it.
    14
    15By a result of Baldwin and Shelah, one may equivalently allow formulas
    16Ο†(xΜ„, Θ³) with tuples of variables, and tuples āᡒ and bΜ„_J. On a
    17monadically dependent class, no such formula has the independence
    18property either.
    19
    20# Formalization notes
    21
    22The paper defines monadic dependence by transductions, like
    23`Lax185574.MonadicDependence`, and states the characterization by the
    24independence property as a theorem of Baldwin and Shelah, in its
    25appendix on forbidden patterns. The first statement of this concept is
    26this characterization for formulas in two single variables. The second
    27is the tuple form, in the direction the paper uses.
    28
    29Formulas and colorings are those of `Lax185574.FirstOrderLogic`. A
    30formula Ο†(xΜ„, Θ³) has the free variables xβ‚€, …, x_{p+p'βˆ’1}. The first p
    31of them form the tuple xΜ„ and the last p' form Θ³. The assignment
    32`Fin.append ā bΜ„` gives xΜ„ the values ā and Θ³ the values bΜ„, which is the
    33paper's Ο†(ā, bΜ„). A formula Ο†(x, y) in two single variables is the case
    34p = p' = 1, written `1 + 1`.
    35-/
    36
    37namespace Lax185574.IndependenceProperty
    38
    39open Lax185574.Graphs Lax185574.FirstOrderLogic Lax185574.MonadicDependence
    40
    41/-- The formula `Ο†(xΜ„, Θ³)` with `k` colors, whose free variables are a
    42tuple `xΜ„` of `p` variables followed by a tuple `Θ³` of `p'` variables,
    43has the *independence property* on `C`: for every `m` there are a graph
    44`G ∈ C`, a coloring of `G`, tuples `a i` for `i < m` and tuples `b J`
    45for `J βŠ† {0, …, m - 1}` such that `Ο†(a i, b J)` holds exactly when
    46`i ∈ J`. -/
    47def HasIP (C : GraphClass) {k p p' : β„•} (Ο† : Formula (Fin k) (p + p')) : Prop :=
    48 βˆ€ m : β„•, βˆƒ G ∈ C, βˆƒ (col : Fin k β†’ Set (Fin G.n)) (a : Fin m β†’ Fin p β†’ Fin G.n)
    49 (b : Finset (Fin m) β†’ Fin p' β†’ Fin G.n),
    50 βˆ€ (i : Fin m) (J : Finset (Fin m)), Ο†.Holds G col (Fin.append (a i) (b J)) ↔ i ∈ J
    51
    52/-- A graph class is monadically dependent if and only if no formula
    53`Ο†(x, y)` of colored graphs, in two single variables, has the
    54independence property on it. -/
    55axiom monadicallyDependent_iff_forall_not_hasIP (C : GraphClass) :
    56 MonadicallyDependent C ↔ βˆ€ (k : β„•) (Ο† : Formula (Fin k) (1 + 1)), Β¬ HasIP C Ο†
    57
    58/-- On a monadically dependent class, no formula `Ο†(xΜ„, Θ³)` of colored
    59graphs, in tuples of variables, has the independence property
    60(Baldwin–Shelah). -/
    61axiom not_hasIP_of_monadicallyDependent (C : GraphClass) (hC : MonadicallyDependent C)
    62 {k p p' : β„•} (Ο† : Formula (Fin k) (p + p')) : Β¬ HasIP C Ο†
    63
    64end Lax185574.IndependenceProperty
    65
    Show ProofShow Proof
    Formalization notes

    The paper defines monadic dependence by transductions, like Lax185574.MonadicDependenceLax185574.MonadicDependence, and states the characterization by the independence property as a theorem of Baldwin and Shelah, in its appendix on forbidden patterns. The first statement of this concept is this characterization for formulas in two single variables. The second is the tuple form, in the direction the paper uses.

    Formulas and colorings are those of Lax185574.FirstOrderLogicLax185574.FirstOrderLogic. A formula Ο†(xΜ„, Θ³) has the free variables xβ‚€, …, x_{p+p'βˆ’1}. The first p of them form the tuple xΜ„ and the last p' form Θ³. The assignment Fin.append ā bΜ„ gives xΜ„ the values ā and Θ³ the values bΜ„, which is the paper's Ο†(ā, bΜ„). A formula Ο†(x, y) in two single variables is the case p = p' = 1, written 1+11 + 1.

    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…