Steiner Tree is existential second-order definable

The membership half of its NP-completeness (DescriptiveComplexity.steinerTree_sigmaSODefinable). The existential block guesses four relations – the chosen set, a root, a strict partial order certifying connectivity, and an injection of the chosen non-terminals into the marked set – and the first-order kernel checks the eight conditions of DescriptiveComplexity.steinerOn_iff_certificate.

The interesting one is connectivity, which is a transitive-closure condition and hence not first-order. What is guessed instead is a root – as a relation constrained to hold of at most one element, since the empty set is connected and has no root – together with an order in which every other chosen vertex has a chosen neighbour strictly below it. Walking down the order reaches the root; that is the same certificate idea as for acyclicity in DescriptiveComplexity.Problems.Feedback, run in the opposite direction.

inductive DescriptiveComplexity.SteinerGuess : Type

The four relation variables guessed by the Σ₁ definition of Steiner Tree.

• set : SteinerGuess

  The chosen set of vertices.

• root : SteinerGuess

  The root of the chosen set.

• order : SteinerGuess

  The order certifying connectivity.

• inj : SteinerGuess

  The injection witnessing the threshold.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSteinerGuess : DecidableEq SteinerGuess

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instFintypeSteinerGuess : Fintype SteinerGuess

Equations

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

def DescriptiveComplexity.steinerGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Steiner Tree.

Equations

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

def DescriptiveComplexity.sgSetRel : steinerGuessBlock.lang.Relations 1

The symbol of the chosen-set relation variable.

Equations

• DescriptiveComplexity.sgSetRel = ⟨DescriptiveComplexity.SteinerGuess.set, DescriptiveComplexity.sgSetRel._proof_1⟩

def DescriptiveComplexity.sgRootRel : steinerGuessBlock.lang.Relations 1

The symbol of the root relation variable.

Equations

• DescriptiveComplexity.sgRootRel = ⟨DescriptiveComplexity.SteinerGuess.root, DescriptiveComplexity.sgRootRel._proof_1⟩

def DescriptiveComplexity.sgOrderRel : steinerGuessBlock.lang.Relations 2

The symbol of the order relation variable.

Equations

• DescriptiveComplexity.sgOrderRel = ⟨DescriptiveComplexity.SteinerGuess.order, DescriptiveComplexity.sgOrderRel._proof_1⟩

def DescriptiveComplexity.sgInjRel : steinerGuessBlock.lang.Relations 2

The symbol of the injection relation variable.

Equations

• DescriptiveComplexity.sgInjRel = ⟨DescriptiveComplexity.SteinerGuess.inj, DescriptiveComplexity.sgInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.steinerSOLang : FirstOrder.Language

The vocabulary of the kernel.

Equations

• DescriptiveComplexity.steinerSOLang = FirstOrder.Language.steinerGraph.sum DescriptiveComplexity.steinerGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.kStAdjSym : steinerSOLang.Relations 2

The adjacency symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kStAdjSym = Sum.inl FirstOrder.Language.stAdj

@[reducible, inline]

abbrev DescriptiveComplexity.kStTermSym : steinerSOLang.Relations 1

The terminal symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kStTermSym = Sum.inl FirstOrder.Language.stTerminal

@[reducible, inline]

abbrev DescriptiveComplexity.kStMarkedSym : steinerSOLang.Relations 1

The mark symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kStMarkedSym = Sum.inl FirstOrder.Language.stMarked

@[reducible, inline]

abbrev DescriptiveComplexity.kStSetSym : steinerSOLang.Relations 1

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

Equations

• DescriptiveComplexity.kStSetSym = Sum.inr DescriptiveComplexity.sgSetRel

@[reducible, inline]

abbrev DescriptiveComplexity.kStRootSym : steinerSOLang.Relations 1

The root symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kStRootSym = Sum.inr DescriptiveComplexity.sgRootRel

@[reducible, inline]

abbrev DescriptiveComplexity.kStLtSym : steinerSOLang.Relations 2

The order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kStLtSym = Sum.inr DescriptiveComplexity.sgOrderRel

@[reducible, inline]

abbrev DescriptiveComplexity.kStInjSym : steinerSOLang.Relations 2

The injection symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kStInjSym = Sum.inr DescriptiveComplexity.sgInjRel

The clauses

noncomputable def DescriptiveComplexity.steinerKernel : steinerSOLang.Sentence

The first-order kernel of the Σ₁ definition of Steiner Tree.

Equations

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

Realization

theorem DescriptiveComplexity.steinerTree_sigmaSODefinable : SigmaSODefinable 1 SteinerTree

Steiner Tree is Σ₁-definable: guess the chosen set, its root, an order certifying that it is connected, and an injection of its non-terminals into the marked set, then check the eight conditions first-order.

The edge-weighted variant

The same certificate, plus the edge set itself, and with the threshold injection mapping pairs to elements – hence a ternary relation variable, for which DescriptiveComplexity.realize_rel₃ (DescriptiveComplexity.Interpretation) plays the role Mathlib's Formula.realize_rel₁/₂ play at lower arity.

inductive DescriptiveComplexity.EdgeSteinerGuess : Type

The five relation variables guessed by the Σ₁ definition of the edge-weighted Steiner tree.

• tree : EdgeSteinerGuess

  The chosen set of edges.

• set : EdgeSteinerGuess

  The chosen set of vertices.

• root : EdgeSteinerGuess

  The root of the chosen set.

• order : EdgeSteinerGuess

  The order certifying connectivity.

• inj : EdgeSteinerGuess

  The injection witnessing the threshold.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqEdgeSteinerGuess : DecidableEq EdgeSteinerGuess

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instFintypeEdgeSteinerGuess : Fintype EdgeSteinerGuess

Equations

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

def DescriptiveComplexity.edgeSteinerGuessBlock : SOBlock

The single existential block of the Σ₁ definition of the edge-weighted Steiner tree.

Equations

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

def DescriptiveComplexity.esTreeRel : edgeSteinerGuessBlock.lang.Relations 2

The symbol of the edge-set relation variable.

Equations

• DescriptiveComplexity.esTreeRel = ⟨DescriptiveComplexity.EdgeSteinerGuess.tree, DescriptiveComplexity.esTreeRel._proof_1⟩

def DescriptiveComplexity.esSetRel : edgeSteinerGuessBlock.lang.Relations 1

The symbol of the chosen-set relation variable.

Equations

• DescriptiveComplexity.esSetRel = ⟨DescriptiveComplexity.EdgeSteinerGuess.set, DescriptiveComplexity.esSetRel._proof_1⟩

def DescriptiveComplexity.esRootRel : edgeSteinerGuessBlock.lang.Relations 1

The symbol of the root relation variable.

Equations

• DescriptiveComplexity.esRootRel = ⟨DescriptiveComplexity.EdgeSteinerGuess.root, DescriptiveComplexity.esRootRel._proof_1⟩

def DescriptiveComplexity.esOrderRel : edgeSteinerGuessBlock.lang.Relations 2

The symbol of the order relation variable.

Equations

• DescriptiveComplexity.esOrderRel = ⟨DescriptiveComplexity.EdgeSteinerGuess.order, DescriptiveComplexity.esOrderRel._proof_1⟩

def DescriptiveComplexity.esInjRel : edgeSteinerGuessBlock.lang.Relations 3

The symbol of the injection relation variable.

Equations

• DescriptiveComplexity.esInjRel = ⟨DescriptiveComplexity.EdgeSteinerGuess.inj, DescriptiveComplexity.esInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.edgeSteinerSOLang : FirstOrder.Language

The vocabulary of the edge-weighted kernel.

Equations

• DescriptiveComplexity.edgeSteinerSOLang = FirstOrder.Language.steinerGraph.sum DescriptiveComplexity.edgeSteinerGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.kEsAdjSym : edgeSteinerSOLang.Relations 2

The adjacency symbol in the edge-weighted kernel's vocabulary.

Equations

• DescriptiveComplexity.kEsAdjSym = Sum.inl FirstOrder.Language.stAdj

@[reducible, inline]

abbrev DescriptiveComplexity.kEsTermSym : edgeSteinerSOLang.Relations 1

The terminal symbol in the edge-weighted kernel's vocabulary.

Equations

• DescriptiveComplexity.kEsTermSym = Sum.inl FirstOrder.Language.stTerminal

@[reducible, inline]

abbrev DescriptiveComplexity.kEsMarkedSym : edgeSteinerSOLang.Relations 1

The mark symbol in the edge-weighted kernel's vocabulary.

Equations

• DescriptiveComplexity.kEsMarkedSym = Sum.inl FirstOrder.Language.stMarked

@[reducible, inline]

abbrev DescriptiveComplexity.kEsTreeSym : edgeSteinerSOLang.Relations 2

The edge-set symbol in the edge-weighted kernel's vocabulary.

Equations

• DescriptiveComplexity.kEsTreeSym = Sum.inr DescriptiveComplexity.esTreeRel

@[reducible, inline]

abbrev DescriptiveComplexity.kEsSetSym : edgeSteinerSOLang.Relations 1

The chosen-set symbol in the edge-weighted kernel's vocabulary.

Equations

• DescriptiveComplexity.kEsSetSym = Sum.inr DescriptiveComplexity.esSetRel

@[reducible, inline]

abbrev DescriptiveComplexity.kEsRootSym : edgeSteinerSOLang.Relations 1

The root symbol in the edge-weighted kernel's vocabulary.

Equations

• DescriptiveComplexity.kEsRootSym = Sum.inr DescriptiveComplexity.esRootRel

@[reducible, inline]

abbrev DescriptiveComplexity.kEsLtSym : edgeSteinerSOLang.Relations 2

The order symbol in the edge-weighted kernel's vocabulary.

Equations

• DescriptiveComplexity.kEsLtSym = Sum.inr DescriptiveComplexity.esOrderRel

@[reducible, inline]

abbrev DescriptiveComplexity.kEsInjSym : edgeSteinerSOLang.Relations 3

The injection symbol in the edge-weighted kernel's vocabulary.

Equations

• DescriptiveComplexity.kEsInjSym = Sum.inr DescriptiveComplexity.esInjRel

noncomputable def DescriptiveComplexity.edgeSteinerKernel : edgeSteinerSOLang.Sentence

The first-order kernel of the Σ₁ definition of the edge-weighted Steiner tree.

Equations

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

theorem DescriptiveComplexity.edgeSteinerTree_sigmaSODefinable : SigmaSODefinable 1 EdgeSteinerTree

The edge-weighted Steiner Tree is Σ₁-definable: guess the edge set, the vertices it spans, a root, an order certifying connectivity, and an injection of the chosen edges into the marked set.