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.

@[reducible, inline]

abbrev DescriptiveComplexity.kMarkedSym : cliqueSOLang.Relations 1

The marked symbol over the sum.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.kCliqueSym : cliqueSOLang.Relations 1

The clique symbol over the sum.

Equations

• DescriptiveComplexity.kCliqueSym = Sum.inr DescriptiveComplexity.kCliqueRel

@[instance_reducible]

instance DescriptiveComplexity.instFintypeCliqueGuessBlockIx : Fintype CliqueGuessBlockIx

Equations

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

inductive DescriptiveComplexity.CliqueGuessBlockIx : Type

The relation variables of the block.

• clique : CliqueGuessBlockIx

  The guessed clique.

• inj : CliqueGuessBlockIx

  The guessed injection of the marked set into the clique.

@[reducible, inline]

abbrev DescriptiveComplexity.kInjSym : cliqueSOLang.Relations 2

The inj symbol over the sum.

Equations

• DescriptiveComplexity.kInjSym = Sum.inr DescriptiveComplexity.kInjRel

@[reducible, inline]

abbrev DescriptiveComplexity.cliqueSOLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

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

def DescriptiveComplexity.kCliqueRel : cliqueGuessBlock.lang.Relations 1

The clique relation variable.

Equations

• DescriptiveComplexity.kCliqueRel = ⟨DescriptiveComplexity.CliqueGuessBlockIx.clique, DescriptiveComplexity.kCliqueRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.kAdjSym : cliqueSOLang.Relations 2

The adj symbol over the sum.

Equations

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

def DescriptiveComplexity.kInjRel : cliqueGuessBlock.lang.Relations 2

The inj relation variable.

Equations

• DescriptiveComplexity.kInjRel = ⟨DescriptiveComplexity.CliqueGuessBlockIx.inj, DescriptiveComplexity.kInjRel._proof_1⟩

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCliqueGuessBlockIx : DecidableEq CliqueGuessBlockIx

Equations

• DescriptiveComplexity.instDecidableEqCliqueGuessBlockIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DescriptiveComplexity.cliqueGuessBlock : SOBlock

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

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.