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 neighbor 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.SteinerGuessBlockIx : Type

The relation variables of the block.

• set : SteinerGuessBlockIx

  The chosen set of vertices.

• root : SteinerGuessBlockIx

  The root of the chosen set.

• order : SteinerGuessBlockIx

  The order certifying connectivity.

• inj : SteinerGuessBlockIx

  The injection witnessing the threshold.

@[reducible, inline]

abbrev DescriptiveComplexity.kStOrderSym : steinerSOLang.Relations 2

The order symbol over the sum.

Equations

• DescriptiveComplexity.kStOrderSym = Sum.inr DescriptiveComplexity.kStOrderRel

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSteinerGuessBlockIx : DecidableEq SteinerGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.kStSetSym : steinerSOLang.Relations 1

The set symbol over the sum.

Equations

• DescriptiveComplexity.kStSetSym = Sum.inr DescriptiveComplexity.kStSetRel

@[instance_reducible]

instance DescriptiveComplexity.instFintypeSteinerGuessBlockIx : Fintype SteinerGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.kStInjSym : steinerSOLang.Relations 2

The inj symbol over the sum.

Equations

• DescriptiveComplexity.kStInjSym = Sum.inr DescriptiveComplexity.kStInjRel

@[reducible, inline]

abbrev DescriptiveComplexity.kStAdjSym : steinerSOLang.Relations 2

The adj symbol over the sum.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.steinerSOLang : FirstOrder.Language

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

Equations

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

def DescriptiveComplexity.kStRootRel : steinerGuessBlock.lang.Relations 1

The root relation variable.

Equations

• DescriptiveComplexity.kStRootRel = ⟨DescriptiveComplexity.SteinerGuessBlockIx.root, DescriptiveComplexity.kStRootRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.kStTerminalSym : steinerSOLang.Relations 1

The terminal symbol over the sum.

Equations

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

def DescriptiveComplexity.kStOrderRel : steinerGuessBlock.lang.Relations 2

The order relation variable.

Equations

• DescriptiveComplexity.kStOrderRel = ⟨DescriptiveComplexity.SteinerGuessBlockIx.order, DescriptiveComplexity.kStOrderRel._proof_1⟩

def DescriptiveComplexity.steinerGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Steiner Tree: its four relation variables.

Equations

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

def DescriptiveComplexity.kStSetRel : steinerGuessBlock.lang.Relations 1

The set relation variable.

Equations

• DescriptiveComplexity.kStSetRel = ⟨DescriptiveComplexity.SteinerGuessBlockIx.set, DescriptiveComplexity.kStSetRel._proof_1⟩

def DescriptiveComplexity.kStInjRel : steinerGuessBlock.lang.Relations 2

The inj relation variable.

Equations

• DescriptiveComplexity.kStInjRel = ⟨DescriptiveComplexity.SteinerGuessBlockIx.inj, DescriptiveComplexity.kStInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.kStRootSym : steinerSOLang.Relations 1

The root symbol over the sum.

Equations

• DescriptiveComplexity.kStRootSym = Sum.inr DescriptiveComplexity.kStRootRel

@[reducible, inline]

abbrev DescriptiveComplexity.kStMarkedSym : steinerSOLang.Relations 1

The marked symbol over the sum.

Equations

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

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.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqEdgeSteinerGuessBlockIx : DecidableEq EdgeSteinerGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.kEsRootSym : edgeSteinerSOLang.Relations 1

The root symbol over the sum.

Equations

• DescriptiveComplexity.kEsRootSym = Sum.inr DescriptiveComplexity.kEsRootRel

@[reducible, inline]

abbrev DescriptiveComplexity.kEsAdjSym : edgeSteinerSOLang.Relations 2

The adj symbol over the sum.

Equations

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

def DescriptiveComplexity.kEsInjRel : edgeSteinerGuessBlock.lang.Relations 3

The inj relation variable.

Equations

• DescriptiveComplexity.kEsInjRel = ⟨DescriptiveComplexity.EdgeSteinerGuessBlockIx.inj, DescriptiveComplexity.kEsInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.kEsInjSym : edgeSteinerSOLang.Relations 3

The inj symbol over the sum.

Equations

• DescriptiveComplexity.kEsInjSym = Sum.inr DescriptiveComplexity.kEsInjRel

def DescriptiveComplexity.kEsTreeRel : edgeSteinerGuessBlock.lang.Relations 2

The tree relation variable.

Equations

• DescriptiveComplexity.kEsTreeRel = ⟨DescriptiveComplexity.EdgeSteinerGuessBlockIx.tree, DescriptiveComplexity.kEsTreeRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.kEsTerminalSym : edgeSteinerSOLang.Relations 1

The terminal symbol over the sum.

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instFintypeEdgeSteinerGuessBlockIx : Fintype EdgeSteinerGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.kEsMarkedSym : edgeSteinerSOLang.Relations 1

The marked symbol over the sum.

Equations

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

def DescriptiveComplexity.edgeSteinerGuessBlock : SOBlock

The single existential block of the Σ₁ definition of the edge-weighted Steiner tree: its five relation variables.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.edgeSteinerSOLang : FirstOrder.Language

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

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.kEsOrderSym : edgeSteinerSOLang.Relations 2

The order symbol over the sum.

Equations

• DescriptiveComplexity.kEsOrderSym = Sum.inr DescriptiveComplexity.kEsOrderRel

@[reducible, inline]

abbrev DescriptiveComplexity.kEsTreeSym : edgeSteinerSOLang.Relations 2

The tree symbol over the sum.

Equations

• DescriptiveComplexity.kEsTreeSym = Sum.inr DescriptiveComplexity.kEsTreeRel

def DescriptiveComplexity.kEsOrderRel : edgeSteinerGuessBlock.lang.Relations 2

The order relation variable.

Equations

• DescriptiveComplexity.kEsOrderRel = ⟨DescriptiveComplexity.EdgeSteinerGuessBlockIx.order, DescriptiveComplexity.kEsOrderRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.kEsSetSym : edgeSteinerSOLang.Relations 1

The set symbol over the sum.

Equations

• DescriptiveComplexity.kEsSetSym = Sum.inr DescriptiveComplexity.kEsSetRel

def DescriptiveComplexity.kEsRootRel : edgeSteinerGuessBlock.lang.Relations 1

The root relation variable.

Equations

• DescriptiveComplexity.kEsRootRel = ⟨DescriptiveComplexity.EdgeSteinerGuessBlockIx.root, DescriptiveComplexity.kEsRootRel._proof_1⟩

inductive DescriptiveComplexity.EdgeSteinerGuessBlockIx : Type

The relation variables of the block.

• tree : EdgeSteinerGuessBlockIx

  The chosen set of edges.

• set : EdgeSteinerGuessBlockIx

  The chosen set of vertices.

• root : EdgeSteinerGuessBlockIx

  The root of the chosen set.

• order : EdgeSteinerGuessBlockIx

  The order certifying connectivity.

• inj : EdgeSteinerGuessBlockIx

  The injection witnessing the threshold.

def DescriptiveComplexity.kEsSetRel : edgeSteinerGuessBlock.lang.Relations 1

The set relation variable.

Equations

• DescriptiveComplexity.kEsSetRel = ⟨DescriptiveComplexity.EdgeSteinerGuessBlockIx.set, DescriptiveComplexity.kEsSetRel._proof_1⟩

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.