The coloring family is existential second-order definable

Membership for the three problems, in two flavours dictated by where the number of colors lives.

• For DescriptiveComplexity.KCol k, the number k is fixed by the problem, so the definition can guess the k color classes as k unary relation variables and check first-order that they cover the vertices and that no edge stays inside a class (DescriptiveComplexity.kCol_sigmaSODefinable); the kernel is built with Formula.iSup/iInf over Fin k.
• For DescriptiveComplexity.ChromaticNumber and DescriptiveComplexity.CliqueCover, the number is the size of the marked set, so it is not available to the formulas – there is no “k classes” to write down. The palette form (DescriptiveComplexity.paletteColorableOn_iff) removes the problem: colouring with as many colors as the marked set has elements is colouring by the marked set, which a single binary relation variable Col x y, read as “x has color y”, expresses. The kernel then has two clauses: every vertex gets some marked color, and two conflicting vertices never share a color. Note that the guessed relation need not be functional: choosing one color per vertex is enough, and the second clause already forbids a shared one.

The two threshold problems differ only in the sign of the adjacency atom in that second clause, so their kernels come from one builder (DescriptiveComplexity.paletteProperClause) parameterized by that sign.

Membership: the color classes as guessed relations

def DescriptiveComplexity.colorGuessBlock (k : ℕ) : SOBlock

The single existential block of the Σ₁ definition of k-colorability: one unary relation variable per color.

Equations

• DescriptiveComplexity.colorGuessBlock k = { ι := Fin k, ιFinite := ⋯, arity := fun (x : Fin k) => 1 }

def DescriptiveComplexity.cgColorSym {k : ℕ} (i : Fin k) : (colorGuessBlock k).lang.Relations 1

The symbol of the i-th color class.

Equations

• DescriptiveComplexity.cgColorSym i = ⟨i, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.kColSOLang (k : ℕ) : FirstOrder.Language

The vocabulary of the kernel: graphs together with the guessed color classes.

Equations

• DescriptiveComplexity.kColSOLang k = FirstOrder.Language.graph.sum (DescriptiveComplexity.colorGuessBlock k).lang

@[reducible, inline]

abbrev DescriptiveComplexity.kcAdjSym (k : ℕ) : (kColSOLang k).Relations 2

The adjacency symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kcAdjSym k = Sum.inl FirstOrder.Language.adj

@[reducible, inline]

abbrev DescriptiveComplexity.kcColorSym {k : ℕ} (i : Fin k) : (kColSOLang k).Relations 1

The symbol of the i-th color class in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kcColorSym i = Sum.inr (DescriptiveComplexity.cgColorSym i)

noncomputable def DescriptiveComplexity.kColKernel (k : ℕ) : (kColSOLang k).Sentence

The first-order kernel of the Σ₁ definition of k-colorability: every vertex belongs to some color class, and no edge has both endpoints in the same class.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.kCol_sigmaSODefinable (k : ℕ) : SigmaSODefinable 1 (KCol k)

k-colorability is Σ₁-definable: existentially guess the k color classes, then check first-order that they cover the vertices and that no edge stays inside a class. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of k-colorability.

Chromatic Number and Clique Cover: the palette as a binary relation

def DescriptiveComplexity.paletteGuessBlock : SOBlock

The single existential block of the Σ₁ definitions of the two threshold problems: one binary relation variable, read as “this vertex has that color”, the colors being the marked elements.

Equations

• DescriptiveComplexity.paletteGuessBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 2 }

def DescriptiveComplexity.pcColRel : paletteGuessBlock.lang.Relations 2

The symbol of the coloring relation variable.

Equations

• DescriptiveComplexity.pcColRel = ⟨(), DescriptiveComplexity.pcColRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.paletteSOLang : FirstOrder.Language

The vocabulary of the kernels: marked graphs together with the guessed coloring.

Equations

• DescriptiveComplexity.paletteSOLang = FirstOrder.Language.markedGraph.sum DescriptiveComplexity.paletteGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.pcAdjSym : paletteSOLang.Relations 2

The adjacency symbol in the kernels' vocabulary.

Equations

• DescriptiveComplexity.pcAdjSym = Sum.inl FirstOrder.Language.mgAdj

@[reducible, inline]

abbrev DescriptiveComplexity.pcMarkedSym : paletteSOLang.Relations 1

The mark symbol in the kernels' vocabulary.

Equations

• DescriptiveComplexity.pcMarkedSym = Sum.inl FirstOrder.Language.mgMarked

@[reducible, inline]

abbrev DescriptiveComplexity.pcColSym : paletteSOLang.Relations 2

The coloring symbol in the kernels' vocabulary.

Equations

• DescriptiveComplexity.pcColSym = Sum.inr DescriptiveComplexity.pcColRel

noncomputable def DescriptiveComplexity.paletteKernel (positive : Bool) : paletteSOLang.Sentence

The kernel of the Σ₁ definition of a threshold coloring problem.

Equations

• DescriptiveComplexity.paletteKernel positive = DescriptiveComplexity.paletteTotalClause✝ ⊓ DescriptiveComplexity.paletteProperClause✝ positive

theorem DescriptiveComplexity.chromaticNumber_sigmaSODefinable : SigmaSODefinable 1 ChromaticNumber

Chromatic Number is Σ₁-definable: guess a coloring of the vertices by the marked elements, and check first-order that every vertex has a marked color and that no two adjacent vertices share one.

theorem DescriptiveComplexity.cliqueCover_sigmaSODefinable : SigmaSODefinable 1 CliqueCover

Clique Cover is Σ₁-definable: the same definition with the adjacency atom negated – covering by cliques is coloring the complement.