Reductions between Clique, Independent Set and Vertex Cover

The classical reductions inside the clique family, as quantifier-free first-order reductions on marked graphs (all of tag Unit and dimension 1):

• DescriptiveComplexity.indSet_fo_reduction_clique and DescriptiveComplexity.clique_fo_reduction_indSet: complementing the edges (off the diagonal) exchanges cliques and independent sets, keeping the marked set;
• DescriptiveComplexity.vertexCover_fo_reduction_indSet and DescriptiveComplexity.indSet_fo_reduction_vertexCover: complementing the marked set exchanges vertex covers and independent sets, keeping the edges – a set is a vertex cover iff its complement is independent, and (on a finite universe) it is at most as large as the marked set iff its complement is at least as large as the complement of the marked set;
• composites DescriptiveComplexity.vertexCover_fo_reduction_clique and DescriptiveComplexity.clique_fo_reduction_vertexCover.

The counting step of the vertex-cover reductions (DescriptiveComplexity.coverOn_iff_indepOn_not) is the only place where finiteness is used; it enters through the finiteness conjunct of the problems themselves. That step is pure unary-representation arithmetic – complementing a marked set subtracts its decoded number from the size of the universe, hence reverses comparisons – and is discharged by DescriptiveComplexity.ncard_compl_le_ncard_compl_iff and DescriptiveComplexity.ncard_compl_le_iff of DescriptiveComplexity.Numbers.Unary.

Complementation lemmas for the generic properties

theorem DescriptiveComplexity.cliqueOn_iff_indepOn_compl {A : Type} (Adjp : A → A → Prop) (Kp : A → Prop) : CliqueOn Adjp Kp ↔ IndepOn (fun (x y : A) => x ≠ y ∧ ¬Adjp x y) Kp

A clique is an independent set of the complement graph (loops removed).

theorem DescriptiveComplexity.indepOn_iff_cliqueOn_compl {A : Type} (Adjp : A → A → Prop) (Kp : A → Prop) : IndepOn Adjp Kp ↔ CliqueOn (fun (x y : A) => x ≠ y ∧ ¬Adjp x y) Kp

An independent set is a clique of the complement graph (loops removed).

theorem DescriptiveComplexity.coverOn_iff_indepOn_not {A : Type} [Finite A] (Adjp : A → A → Prop) (Kp : A → Prop) : CoverOn Adjp Kp ↔ IndepOn Adjp fun (x : A) => ¬Kp x

On a finite universe, a vertex cover at most as large as the marked set exists iff an independent set at least as large as the complement of the marked set does: complementation exchanges the two.

theorem DescriptiveComplexity.indepOn_iff_coverOn_not {A : Type} [Finite A] (Adjp : A → A → Prop) (Kp : A → Prop) : IndepOn Adjp Kp ↔ CoverOn Adjp fun (x : A) => ¬Kp x

On a finite universe, an independent set at least as large as the marked set exists iff a vertex cover at most as large as the complement of the marked set does.

The two interpretations

def DescriptiveComplexity.complEdgeInterp : FOInterpretation FirstOrder.Language.markedGraph FirstOrder.Language.markedGraph Unit 1

The edge-complementing interpretation: adjacency becomes off-diagonal non-adjacency, marks are kept.

Equations

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

def DescriptiveComplexity.complMarkInterp : FOInterpretation FirstOrder.Language.markedGraph FirstOrder.Language.markedGraph Unit 1

The mark-complementing interpretation: adjacency is kept, marks are complemented.

Equations

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

theorem DescriptiveComplexity.complEdgeInterp_isQuantifierFree : complEdgeInterp.IsQuantifierFree

Both interpretations are quantifier-free.

theorem DescriptiveComplexity.complMarkInterp_isQuantifierFree : complMarkInterp.IsQuantifierFree

Both interpretations are quantifier-free.

Characterizations of the interpreted relations

@[simp]

theorem DescriptiveComplexity.complEdge_adj {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgAdj ![((), w₁), ((), w₂)] ↔ w₁ 0 ≠ w₂ 0 ∧ ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgAdj ![w₁ 0, w₂ 0]

@[simp]

theorem DescriptiveComplexity.complEdge_marked {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgMarked ![((), w)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgMarked ![w 0]

@[simp]

theorem DescriptiveComplexity.complMark_adj {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgAdj ![((), w₁), ((), w₂)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgAdj ![w₁ 0, w₂ 0]

@[simp]

theorem DescriptiveComplexity.complMark_marked {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgMarked ![((), w)] ↔ ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgMarked ![w 0]

Correctness

theorem DescriptiveComplexity.hasLargeIndependentSet_iff_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasLargeIndependentSet A ↔ HasLargeClique (complEdgeInterp.Map A)

Correctness of the edge complementation, independent-set-to-clique direction.

theorem DescriptiveComplexity.hasLargeClique_iff_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasLargeClique A ↔ HasLargeIndependentSet (complEdgeInterp.Map A)

Correctness of the edge complementation, clique-to-independent-set direction.

theorem DescriptiveComplexity.hasSmallVertexCover_iff_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasSmallVertexCover A ↔ HasLargeIndependentSet (complMarkInterp.Map A)

Correctness of the mark complementation, vertex-cover-to-independent-set direction.

theorem DescriptiveComplexity.hasLargeIndependentSet_iff_cover_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasLargeIndependentSet A ↔ HasSmallVertexCover (complMarkInterp.Map A)

Correctness of the mark complementation, independent-set-to-vertex-cover direction.

The reductions

def DescriptiveComplexity.indSet_fo_reduction_clique : FOReduction IndependentSet Clique

Independent Set FO-reduces to Clique, by complementing the edges.

Equations

• DescriptiveComplexity.indSet_fo_reduction_clique = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.complEdgeInterp, correct := ⋯ }

def DescriptiveComplexity.clique_fo_reduction_indSet : FOReduction Clique IndependentSet

Clique FO-reduces to Independent Set, by complementing the edges.

Equations

• DescriptiveComplexity.clique_fo_reduction_indSet = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.complEdgeInterp, correct := ⋯ }

def DescriptiveComplexity.vertexCover_fo_reduction_indSet : FOReduction VertexCover IndependentSet

Vertex Cover FO-reduces to Independent Set, by complementing the marked set.

Equations

• DescriptiveComplexity.vertexCover_fo_reduction_indSet = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.complMarkInterp, correct := ⋯ }

def DescriptiveComplexity.indSet_fo_reduction_vertexCover : FOReduction IndependentSet VertexCover

Independent Set FO-reduces to Vertex Cover, by complementing the marked set.

Equations

• DescriptiveComplexity.indSet_fo_reduction_vertexCover = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.complMarkInterp, correct := ⋯ }