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.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqDominatingGuessBlockIx : DecidableEq DominatingGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.dsInjSym : dsSOLang.Relations 2

The inj symbol over the sum.

Equations

• DescriptiveComplexity.dsInjSym = Sum.inr DescriptiveComplexity.dsInjRel

inductive DescriptiveComplexity.DominatingGuessBlockIx : Type

The relation variables of the block.

• set : DominatingGuessBlockIx

  The guessed dominating set.

• inj : DominatingGuessBlockIx

  The guessed injection of the dominating set into the marked set.

def DescriptiveComplexity.dsSetRel : dominatingGuessBlock.lang.Relations 1

The set relation variable.

Equations

• DescriptiveComplexity.dsSetRel = ⟨DescriptiveComplexity.DominatingGuessBlockIx.set, DescriptiveComplexity.dsSetRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.dsAdjSym : dsSOLang.Relations 2

The adj symbol over the sum.

Equations

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

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

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

@[reducible, inline]

abbrev DescriptiveComplexity.dsMarkedSym : dsSOLang.Relations 1

The marked symbol over the sum.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.dsSOLang : FirstOrder.Language

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

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instFintypeDominatingGuessBlockIx : Fintype DominatingGuessBlockIx

Equations

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

def DescriptiveComplexity.dsInjRel : dominatingGuessBlock.lang.Relations 2

The inj relation variable.

Equations

• DescriptiveComplexity.dsInjRel = ⟨DescriptiveComplexity.DominatingGuessBlockIx.inj, DescriptiveComplexity.dsInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.dsSetSym : dsSOLang.Relations 1

The set symbol over the sum.

Equations

• DescriptiveComplexity.dsSetSym = Sum.inr DescriptiveComplexity.dsSetRel

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.