Hardness of the set family: graphs as incidence systems

One interpretation, read twice. DescriptiveComplexity.edgeIncidenceInterp maps a marked graph to the incidence system of its edges: the ground elements are the (oriented) edges, the sets are the vertices, and a vertex-set contains the edges it is an endpoint of. It has tag Unit and dimension 2, and splits the pairs of vertices in three: an off-diagonal adjacent pair is the ground element for that edge, a diagonal pair (v, v) is the vertex-set of v, and any other pair is junk that no relation of the output mentions. The threshold is transported to the marked diagonal, so the interpreted marked set is in bijection with the input one and encodes the same number.

Under this reading,

• a set of vertices meets every edge iff the family of its vertex-sets covers every ground element, giving DescriptiveComplexity.vertexCover_fo_reduction_setCover;
• two distinct vertices are non-adjacent iff their vertex-sets are disjoint (DescriptiveComplexity.exists_elem_mem_both_iff), giving DescriptiveComplexity.indSet_fo_reduction_setPacking.

Each edge gives two ground elements, one per orientation, and this is harmless: the two carry the same constraint in both readings. The cardinality bookkeeping – the interpreted family and marked set are diagonal, hence in bijection with their vertex counterparts – is DescriptiveComplexity.ncard_diag_eq below, the unary representation's counting step for both reductions.

The vertex-sets are named (DescriptiveComplexity.diagPt) and characterized by an iff lemma (DescriptiveComplexity.eq_diagPt_iff) rather than handled by projections. The reason is that FOInterpretation.Map is a non-reducible definition: a statement phrased over the raw Tag × (Fin d → A) is ill-typed at the transparency rw/simp match at, even though exact accepts it, and destructuring an element of the interpreted universe inside a set-builder membership goal produces exactly such a statement. Keeping every hypothesis in the shape ∀ p, Q p → ∃ v, p = diagPt v avoids the issue outright.

The interpretation

def DescriptiveComplexity.edgeIncidenceInterp : FOInterpretation FirstOrder.Language.markedGraph FirstOrder.Language.setSystem Unit 2

The edge-incidence interpretation of a marked graph as a set system: the ground elements are the (oriented) edges, the sets are the vertices, sitting on the diagonal, and a vertex-set contains the edges it is an endpoint of. The threshold moves to the marked diagonal, encoding the same number.

Equations

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

theorem DescriptiveComplexity.edgeIncidenceInterp_isQuantifierFree : edgeIncidenceInterp.IsQuantifierFree

The edge-incidence interpretation is quantifier-free.

@[simp]

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

@[simp]

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

@[simp]

theorem DescriptiveComplexity.edgeIncidence_mem {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 2 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssMem ![((), w₁), ((), w₂)] ↔ w₂ 0 = w₂ 1 ∧ (w₂ 0 = w₁ 0 ∨ w₂ 0 = w₁ 1)

@[simp]

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

The counting step

Both the interpreted family and the interpreted marked set live on the diagonal, which is in bijection with the vertex set; so the numbers they encode are the numbers encoded by their vertex counterparts.

def DescriptiveComplexity.diagPt {A : Type} (v : A) : edgeIncidenceInterp.Map A

A vertex, as a set of the interpreted set system: the diagonal pair.

Equations

• DescriptiveComplexity.diagPt v = ((), ![v, v])

theorem DescriptiveComplexity.eq_diagPt_iff {A : Type} (t : Unit) (w : Fin 2 → A) (v : A) : (t, w) = diagPt v ↔ w 0 = v ∧ w 1 = v

A tagged pair is the vertex-set of v exactly when both its coordinates are v. Stating the diagonal condition this way, rather than by projections, is what keeps the proofs about the interpreted structure free of destructuring (see the module docstring above).

theorem DescriptiveComplexity.diagPt_injective {A : Type} : Function.Injective diagPt

Distinct vertices give distinct vertex-sets.

theorem DescriptiveComplexity.ncard_diag_eq {A : Type} (P : A → Prop) (Q : edgeIncidenceInterp.Map A → Prop) (hdiag : ∀ (p : edgeIncidenceInterp.Map A), Q p → ∃ (v : A), p = diagPt v) (hP : ∀ (v : A), Q (diagPt v) ↔ P v) : {p : edgeIncidenceInterp.Map A | Q p}.ncard = {v : A | P v}.ncard

A predicate that only holds of diagonal pairs encodes the same number as its restriction to the diagonal, read as a predicate on vertices.

def DescriptiveComplexity.vertexFamily {A : Type} (C : A → Prop) : edgeIncidenceInterp.Map A → Prop

The subfamily of vertex-sets attached to a set of vertices: the diagonal pairs of its members. Shared by the reductions of Vertex Cover to Set Cover and of Independent Set to Set Packing, which both send a set of vertices to the family of its vertex-sets.

Equations

• DescriptiveComplexity.vertexFamily C p = ∃ (v : A), C v ∧ p = DescriptiveComplexity.diagPt v

theorem DescriptiveComplexity.ncard_vertexFamily {A : Type} (C : A → Prop) : {p : edgeIncidenceInterp.Map A | vertexFamily C p}.ncard = {v : A | C v}.ncard

The family of vertex-sets of a set of vertices encodes the same number as the set itself.

theorem DescriptiveComplexity.marked_diag (A : Type) [FirstOrder.Language.markedGraph.Structure A] (p : edgeIncidenceInterp.Map A) : SSMarked p → ∃ (v : A), p = diagPt v

The interpreted marked set lives on the diagonal.

theorem DescriptiveComplexity.ncard_marked (A : Type) [FirstOrder.Language.markedGraph.Structure A] : {p : edgeIncidenceInterp.Map A | SSMarked p}.ncard = {v : A | MGMarked v}.ncard

The interpreted marked set encodes the same number as the input one.

theorem DescriptiveComplexity.hasSmallVertexCover_iff_setCover_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasSmallVertexCover A ↔ HasSmallSetCover (edgeIncidenceInterp.Map A)

Correctness of the edge-incidence interpretation: a graph has a vertex cover at most as large as its marked set iff the associated set system has a cover at most as large as its marked set.

def DescriptiveComplexity.vertexCover_fo_reduction_setCover : FOReduction VertexCover SetCover

Vertex Cover FO-reduces to Set Cover: the edges are the ground elements, the vertices the sets that cover them.

Equations

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

Independent Set reduces to Set Packing

The same interpretation, read again: a set of vertices is independent exactly when the family of their vertex-sets is pairwise disjoint.

theorem DescriptiveComplexity.exists_elem_mem_both_iff {A : Type} [FirstOrder.Language.markedGraph.Structure A] {u v : A} (huv : u ≠ v) : (∃ (x : edgeIncidenceInterp.Map A), SSElem x ∧ SSMem x (diagPt u) ∧ SSMem x (diagPt v)) ↔ MGAdj u v ∨ MGAdj v u

Two distinct vertices have intersecting sets of incident edges exactly when they are adjacent (in either direction). This is the whole content of the reduction; note that only ground elements, i.e. genuine edges, count as witnesses of an intersection.

theorem DescriptiveComplexity.hasLargeIndependentSet_iff_setPacking_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasLargeIndependentSet A ↔ HasLargeSetPacking (edgeIncidenceInterp.Map A)

Correctness of the edge-incidence interpretation as a reduction of Independent Set: a graph has an independent set at least as large as its marked set iff the associated set system has a packing at least as large as its marked set.

def DescriptiveComplexity.indSet_fo_reduction_setPacking : FOReduction IndependentSet SetPacking

Independent Set FO-reduces to Set Packing: the vertices become the sets of edges they are incident to, and independence becomes disjointness.

Equations

• DescriptiveComplexity.indSet_fo_reduction_setPacking = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 2, toInterpretation := DescriptiveComplexity.edgeIncidenceInterp, correct := ⋯ }