Dominating Set is in NP

The Σ₁ definition of DescriptiveComplexity.DominatingSet: guess the dominating set and an injection of it into the marked set, then check first-order that every vertex is dominated and that the injection is one.

def DescriptiveComplexity.dominatingGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Dominating Set: the dominating set (unary) and an injection of it into the marked set (binary).

Equations

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

def DescriptiveComplexity.dsSetRel : dominatingGuessBlock.lang.Relations 1

The symbol of the dominating-set relation variable.

Equations

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

def DescriptiveComplexity.dsInjRel : dominatingGuessBlock.lang.Relations 2

The symbol of the injection relation variable.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.dsSOLang : FirstOrder.Language

The vocabulary of the kernel.

Equations

• DescriptiveComplexity.dsSOLang = FirstOrder.Language.markedGraph.sum DescriptiveComplexity.dominatingGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.dsAdjSym : dsSOLang.Relations 2

The adjacency symbol in the kernel's vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.dsMarkedSym : dsSOLang.Relations 1

The mark symbol in the kernel's vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.dsSetSym : dsSOLang.Relations 1

The dominating-set symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.dsSetSym = Sum.inr DescriptiveComplexity.dsSetRel

@[reducible, inline]

abbrev DescriptiveComplexity.dsInjSym : dsSOLang.Relations 2

The injection symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.dsInjSym = Sum.inr DescriptiveComplexity.dsInjRel

noncomputable def DescriptiveComplexity.dominatingKernel : dsSOLang.Sentence

The first-order kernel of the Σ₁ definition of Dominating Set.

Equations

• DescriptiveComplexity.dominatingKernel = DescriptiveComplexity.dsDomClause✝ ⊓ (DescriptiveComplexity.dsTotalClause✝ ⊓ DescriptiveComplexity.dsInjClause✝)

theorem DescriptiveComplexity.dominatingSet_sigmaSODefinable : SigmaSODefinable 1 DominatingSet

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