The feedback problems are existential second-order definable

The membership half of the NP-completeness of both feedback problems: DescriptiveComplexity.feedbackVertexSet_sigmaSODefinable and DescriptiveComplexity.feedbackArcSet_sigmaSODefinable.

Acyclicity is not first-order, but its certificate is (DescriptiveComplexity.acyclicRel_iff_exists_order), so both definitions have the same five-clause shape. A single existential block guesses

• the removed object – a set of vertices for Feedback Vertex Set (arity 1), a set of arcs for Feedback Arc Set (arity 2);
• a strict partial order certifying that what survives is acyclic (arity 2);
• an injection of the removed object into the marked set, witnessing the threshold – arity 2 for Feedback Vertex Set, where it maps vertices to vertices, and arity 4 for Feedback Arc Set, where it maps pairs to pairs, the threshold living one arity up (the unary encoding read at arity 2, see DescriptiveComplexity.nonempty_embedding_iff_ncard_le₂);

and the kernel checks transitivity, irreflexivity, that every surviving arc goes forward in the order, and that the injection is total and injective. The arity-4 atom is the only thing the second definition needs beyond the first, and it costs nothing beyond DescriptiveComplexity.realize_rel₄ (DescriptiveComplexity.Interpretation), Mathlib's Formula.realize_rel₁/₂ stopping at arity 2.

def DescriptiveComplexity.feedbackGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Feedback Vertex Set: the removed set (unary), a strict partial order certifying acyclicity (binary), and an injection of the removed set into the marked set (binary).

Equations

• DescriptiveComplexity.feedbackGuessBlock = { ι := Option Bool, ιFinite := ⋯, arity := fun (i : Option Bool) => match i with | none => 1 | some val => 2 }

def DescriptiveComplexity.fvsSetSym : feedbackGuessBlock.lang.Relations 1

The symbol of the removed-set relation variable.

Equations

• DescriptiveComplexity.fvsSetSym = ⟨none, DescriptiveComplexity.fvsSetSym._proof_1⟩

def DescriptiveComplexity.fvsLtSym : feedbackGuessBlock.lang.Relations 2

The symbol of the order relation variable.

Equations

• DescriptiveComplexity.fvsLtSym = ⟨some true, DescriptiveComplexity.fvsLtSym._proof_1⟩

def DescriptiveComplexity.fvsInjSym : feedbackGuessBlock.lang.Relations 2

The symbol of the injection relation variable.

Equations

• DescriptiveComplexity.fvsInjSym = ⟨some false, DescriptiveComplexity.fvsInjSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.fvsSOLang : FirstOrder.Language

The vocabulary of the kernel: marked graphs together with the three guessed relation variables.

Equations

• DescriptiveComplexity.fvsSOLang = FirstOrder.Language.markedGraph.sum DescriptiveComplexity.feedbackGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.fAdjSym : fvsSOLang.Relations 2

The adjacency symbol in the kernel's vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.fMarkedSym : fvsSOLang.Relations 1

The mark symbol in the kernel's vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.fSetSym : fvsSOLang.Relations 1

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

Equations

• DescriptiveComplexity.fSetSym = Sum.inr DescriptiveComplexity.fvsSetSym

@[reducible, inline]

abbrev DescriptiveComplexity.fLtSym : fvsSOLang.Relations 2

The order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.fLtSym = Sum.inr DescriptiveComplexity.fvsLtSym

@[reducible, inline]

abbrev DescriptiveComplexity.fInjSym : fvsSOLang.Relations 2

The injection symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.fInjSym = Sum.inr DescriptiveComplexity.fvsInjSym

noncomputable def DescriptiveComplexity.feedbackKernel : fvsSOLang.Sentence

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

Equations

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

theorem DescriptiveComplexity.feedbackVertexSet_sigmaSODefinable : SigmaSODefinable 1 FeedbackVertexSet

Feedback Vertex Set is Σ₁-definable: existentially guess the removed set, a strict partial order certifying that the rest is acyclic, and an injection of the removed set into the marked set, then check all five conditions first-order. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Feedback Vertex Set.

Feedback Arc Set

def DescriptiveComplexity.feedbackArcGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Feedback Arc Set: the removed set of arcs (binary), a strict partial order certifying acyclicity (binary), and an injection of the removed arcs into the marked relation (quaternary: it maps pairs to pairs).

Equations

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

def DescriptiveComplexity.fasCutRel : feedbackArcGuessBlock.lang.Relations 2

The symbol of the removed-arc relation variable.

Equations

• DescriptiveComplexity.fasCutRel = ⟨none, DescriptiveComplexity.fasCutRel._proof_1⟩

def DescriptiveComplexity.fasLtRel : feedbackArcGuessBlock.lang.Relations 2

The symbol of the order relation variable.

Equations

• DescriptiveComplexity.fasLtRel = ⟨some true, DescriptiveComplexity.fasLtRel._proof_1⟩

def DescriptiveComplexity.fasInjRel : feedbackArcGuessBlock.lang.Relations 4

The symbol of the injection relation variable.

Equations

• DescriptiveComplexity.fasInjRel = ⟨some false, DescriptiveComplexity.fasInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.fasSOLang : FirstOrder.Language

The vocabulary of the kernel: arc-marked digraphs together with the three guessed relation variables.

Equations

• DescriptiveComplexity.fasSOLang = FirstOrder.Language.markedArcGraph.sum DescriptiveComplexity.feedbackArcGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.fasAdjSym : fasSOLang.Relations 2

The adjacency symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.fasAdjSym = Sum.inl FirstOrder.Language.magAdj

@[reducible, inline]

abbrev DescriptiveComplexity.fasMarkedSym : fasSOLang.Relations 2

The mark symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.fasMarkedSym = Sum.inl FirstOrder.Language.magMarked

@[reducible, inline]

abbrev DescriptiveComplexity.fasCutSym : fasSOLang.Relations 2

The removed-arc symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.fasCutSym = Sum.inr DescriptiveComplexity.fasCutRel

@[reducible, inline]

abbrev DescriptiveComplexity.fasLtSym : fasSOLang.Relations 2

The order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.fasLtSym = Sum.inr DescriptiveComplexity.fasLtRel

@[reducible, inline]

abbrev DescriptiveComplexity.fasInjSym : fasSOLang.Relations 4

The injection symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.fasInjSym = Sum.inr DescriptiveComplexity.fasInjRel

noncomputable def DescriptiveComplexity.feedbackArcKernel : fasSOLang.Sentence

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

Equations

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

theorem DescriptiveComplexity.feedbackArcSet_sigmaSODefinable : SigmaSODefinable 1 FeedbackArcSet

Feedback Arc Set is Σ₁-definable: existentially guess the removed arcs, a strict partial order certifying that the rest is acyclic, and an injection of the removed arcs into the marked relation – a quaternary relation variable, the threshold being carried by pairs. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Feedback Arc Set.