The clique family is NP-complete

Umbrella file for the problems Clique, Independent Set and Vertex Cover on marked graphs (DescriptiveComplexity.Clique, DescriptiveComplexity.IndependentSet, DescriptiveComplexity.VertexCover, defined in DescriptiveComplexity.Problems.CliqueFamily.Defs), collecting the quantifier-free reductions of DescriptiveComplexity.Problems.CliqueFamily.Reductions and their composites – all three problems are FO-interreducible – and deriving the NP-completeness of all three from

• DescriptiveComplexity.clique_sigmaSODefinable (DescriptiveComplexity.Problems.CliqueFamily.Membership): membership of Clique, by guessing the clique and an injection of the marked set into it;
• DescriptiveComplexity.sat_ordered_fo_reduction_clique : SAT ≤ᶠᵒ[≤] Clique (DescriptiveComplexity.Problems.CliqueFamily.FromSat): hardness of Clique, from the Cook–Levin theorem (DescriptiveComplexity.SAT_NP_complete; Cook 1971; Levin 1973);

with no machine model anywhere. Membership travels backward and hardness forward along the quantifier-free inter-reductions, yielding DescriptiveComplexity.indSet_NP_complete and DescriptiveComplexity.vertexCover_NP_complete. As with any complexity-theoretic statement, these results are about finite marked graphs only (ComplexityClass.mem_congr_finite/hard_congr_finite).

noncomputable def DescriptiveComplexity.vertexCover_fo_reduction_clique : FOReduction VertexCover Clique

Vertex Cover FO-reduces to Clique, by composing the mark and edge complementations.

Equations

• DescriptiveComplexity.vertexCover_fo_reduction_clique = DescriptiveComplexity.vertexCover_fo_reduction_indSet.trans DescriptiveComplexity.indSet_fo_reduction_clique

noncomputable def DescriptiveComplexity.clique_fo_reduction_vertexCover : FOReduction Clique VertexCover

Clique FO-reduces to Vertex Cover, by composing the edge and mark complementations.

Equations

• DescriptiveComplexity.clique_fo_reduction_vertexCover = DescriptiveComplexity.clique_fo_reduction_indSet.trans DescriptiveComplexity.indSet_fo_reduction_vertexCover

NP-completeness

theorem DescriptiveComplexity.clique_mem_NP : NP.Mem Clique

Clique is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.clique_NP_hard : NP.Hard Clique

Clique is NP-hard: SAT, which is NP-hard, reduces to it by an ordered FO reduction.

theorem DescriptiveComplexity.clique_NP_complete : NP.Complete Clique

Clique is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem.

theorem DescriptiveComplexity.indSet_mem_NP : NP.Mem IndependentSet

Independent Set is in NP: it FO-reduces to Clique, which is in NP.

theorem DescriptiveComplexity.indSet_NP_hard : NP.Hard IndependentSet

Independent Set is NP-hard: Clique, which is NP-hard, reduces to it.

theorem DescriptiveComplexity.indSet_NP_complete : NP.Complete IndependentSet

Independent Set is NP-complete.

theorem DescriptiveComplexity.vertexCover_mem_NP : NP.Mem VertexCover

Vertex Cover is in NP: it FO-reduces to Independent Set, which is in NP.

theorem DescriptiveComplexity.vertexCover_NP_hard : NP.Hard VertexCover

Vertex Cover is NP-hard: Independent Set, which is NP-hard, reduces to it.

theorem DescriptiveComplexity.vertexCover_NP_complete : NP.Complete VertexCover

Vertex Cover is NP-complete.