Documentation

Complexity.Logics.SecondOrder.Coloring

Colorability is existential second-order definable #

A structure for Mathlib's language of graphs FirstOrder.Language.graph is a directed graph, possibly with loops. It is n-colorable (Cslib.Logic.FO.graph.Colorable) when its vertices can be colored with n colors so that the two ends of every edge have different colors. This is expressed by the existential second-order sentence ∃ C₀ … Cₙ₋₁, (∀ x, C₀ x ∨ ⋯ ∨ Cₙ₋₁ x) ∧ ∀ x y, E x y → ¬ (C₀ x ∧ C₀ y) ∧ ⋯ ∧ ¬ (Cₙ₋₁ x ∧ Cₙ₋₁ y) with one unary relation variable for each color Fagin, Section 1, Example 1, Immerman, Section 7.1. On the structure of a simple graph it says that the graph is n-colorable in the sense of SimpleGraph.Colorable; in particular bipartiteness (n = 2) and three-colorability (n = 3) are existential second-order definable.

Main definitions #

Main results #

References #

source
theorem Cslib.Logic.FO.Definable.simpleGraph :
Definable {M : CategoryTheory.Bundled FirstOrder.Language.graph.Structure | ↑M ⊨ FirstOrder.Language.Theory.simpleGraph}

The class of finite simple graphs, the models of FirstOrder.Language.Theory.simpleGraph, is first-order definable.

source
@[reducible, inline]
abbrev Cslib.Logic.ESO.Sentence.color {n : ℕ} (c : Fin n) :
(FirstOrder.Language.graph.sum (varLanguage fun (x : Fin n) => 1)).Relations 1

The relation symbol of the color c, a unary relation variable.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Logic.ESO.Sentence.edge (n : ℕ) :
    (FirstOrder.Language.graph.sum (varLanguage fun (x : Fin n) => 1)).Relations 2

    The edge relation symbol, among the symbols of the colorability sentence.

    Instances For
      source
      noncomputable def Cslib.Logic.ESO.Sentence.colorableMatrix (n : ℕ) :
      (FirstOrder.Language.graph.sum (varLanguage fun (x : Fin n) => 1)).Sentence

      The first-order part of the colorability sentence: every vertex has one of the colors, and no edge joins two vertices of the same color.

      Instances For
        source
        noncomputable def Cslib.Logic.ESO.Sentence.colorable (n : ℕ) :
        Sentence FirstOrder.Language.graph

        Colorability: the existential second-order sentence saying that every vertex has one of n colors and that no edge joins two vertices of the same color.

        Instances For
          source
          theorem Cslib.Logic.ESO.Sentence.realize_colorable_iff {n : ℕ} {M : Type w} [FirstOrder.Language.graph.Structure M] :
          (colorable n).Realize M ↔ ∃ (f : M → Fin n), ∀ (x y : M), FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y] → f x ≠ f y

          A directed graph satisfies the colorability sentence exactly when it has a coloring with n colors in which the two ends of every edge have different colors.

          source
          theorem Cslib.Logic.ESO.Sentence.realize_colorable_structure_iff {n : ℕ} {V : Type w} (G : SimpleGraph V) :
          (colorable n).Realize V ↔ G.Colorable n

          A simple graph satisfies the colorability sentence exactly when it is n-colorable.

          source
          theorem Cslib.Logic.ESO.Definable.colorable (n : ℕ) :
          Definable {M : CategoryTheory.Bundled FirstOrder.Language.graph.Structure | ∃ (f : ↑M → Fin n), ∀ (x y : ↑M), FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y] → f x ≠ f y}

          Colorability is existential second-order definable: the class of finite directed graphs that are n-colorable is a generalized spectrum Fagin, Section 1, Example 1.

          source
          theorem Cslib.Logic.ESO.Definable.colorable_simpleGraph (n : ℕ) :
          Definable {M : CategoryTheory.Bundled FirstOrder.Language.graph.Structure | ↑M ⊨ FirstOrder.Language.Theory.simpleGraph ∧ ∃ (f : ↑M → Fin n), ∀ (x y : ↑M), FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y] → f x ≠ f y}

          Colorability of simple graphs is existential second-order definable: the class of finite simple graphs that are n-colorable, such as the bipartite (n = 2) or three-colorable (n = 3) ones, is the intersection of a first-order definable class with an existential second-order definable one.

          source
          theorem Cslib.Logic.FO.graph.definable_ThreeColorable :
          ESO.Definable ThreeColorable

          3COL is existential second-order definable.

          source
          theorem Cslib.Logic.FO.graph.definable_SimpleThreeColorable :
          ESO.Definable SimpleThreeColorable

          Classical 3COL is existential second-order definable.