Clique is existential second-order definable

The membership half of the NP-completeness of Clique: the clique threshold property is Σ₁-definable in the sense of DescriptiveComplexity.SecondOrder (DescriptiveComplexity.clique_sigmaSODefinable). The single existential block guesses two relations – a unary one, the clique itself, and a binary one, an injection of the marked set into the clique – and the first-order kernel checks that the unary relation is a clique and that the binary relation is total on the marked set, lands in the clique, and is injective. On (finite) structures this is equivalent to the existence of an embedding of the marked set into a clique, i.e. to DescriptiveComplexity.HasLargeClique.

Since NP is defined as Σ₁-definability, this is the statement Clique ∈ NP; see DescriptiveComplexity.Problems.CliqueFamily for the NP-completeness theorems of the whole clique family.

def DescriptiveComplexity.cliqueGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Clique: a unary relation variable (true: the clique) and a binary one (false: an injection of the marked set into the clique).

Equations

• DescriptiveComplexity.cliqueGuessBlock = { ι := Bool, ιFinite := Bool.instFinite, arity := fun (i : Bool) => bif i then 1 else 2 }

def DescriptiveComplexity.cgCliqueSym : cliqueGuessBlock.lang.Relations 1

The symbol of the clique relation variable.

Equations

• DescriptiveComplexity.cgCliqueSym = ⟨true, DescriptiveComplexity.cgCliqueSym._proof_1⟩

def DescriptiveComplexity.cgInjSym : cliqueGuessBlock.lang.Relations 2

The symbol of the injection relation variable.

Equations

• DescriptiveComplexity.cgInjSym = ⟨false, DescriptiveComplexity.cgInjSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.cliqueSOLang : FirstOrder.Language

The vocabulary of the kernel: marked graphs together with the two guessed relation variables.

Equations

• DescriptiveComplexity.cliqueSOLang = FirstOrder.Language.markedGraph.sum DescriptiveComplexity.cliqueGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.kAdjSym : cliqueSOLang.Relations 2

The adjacency symbol in the kernel's vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.kMarkedSym : cliqueSOLang.Relations 1

The mark symbol in the kernel's vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.kCliqueSym : cliqueSOLang.Relations 1

The clique symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kCliqueSym = Sum.inr DescriptiveComplexity.cgCliqueSym

@[reducible, inline]

abbrev DescriptiveComplexity.kInjSym : cliqueSOLang.Relations 2

The injection symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kInjSym = Sum.inr DescriptiveComplexity.cgInjSym

noncomputable def DescriptiveComplexity.cliqueKernel : cliqueSOLang.Sentence

The first-order kernel of the Σ₁ definition of Clique: the guessed unary relation is a clique – any two distinct members are adjacent – and the guessed binary relation maps every marked element to some clique member, injectively.

Equations

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

theorem DescriptiveComplexity.clique_sigmaSODefinable : SigmaSODefinable 1 Clique

Clique is Σ₁-definable: existentially guess the clique and an injection of the marked set into it, then check both first-order. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Clique.