The Hamilton circuit problems are existential second-order definable

The membership half of the NP-completeness of both problems: DescriptiveComplexity.dirHamCircuit_sigmaSODefinable and DescriptiveComplexity.hamCircuit_sigmaSODefinable.

Being a Hamilton circuit is not a first-order property of a graph, but a circuit is a first-order object: a linear order of the universe (DescriptiveComplexity.TourOn). So a single existential block guesses one binary relation, and the kernel checks

• that it is a linear order – reflexive, transitive, antisymmetric, total;
• that every element is adjacent to its immediate successor, “immediate” being the first-order “nothing strictly in between”;
• that the last element is adjacent to the first.

The two problems share the block and the four order clauses, and differ only in how the last two read the arc relation: as it stands for the directed problem, symmetrized for the undirected one.

def DescriptiveComplexity.hamGuessBlock : SOBlock

The single existential block of the Σ₁ definitions: the circuit, guessed as a linear order of the universe.

Equations

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

def DescriptiveComplexity.hLeRel : hamGuessBlock.lang.Relations 2

The le relation variable.

Equations

• DescriptiveComplexity.hLeRel = ⟨DescriptiveComplexity.HamGuessBlockIx.le, DescriptiveComplexity.hLeRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.hArcSym : hamSOLang.Relations 2

The arc symbol over the sum.

Equations

• DescriptiveComplexity.hArcSym = Sum.inl FirstOrder.Language.dgArc

@[reducible, inline]

abbrev DescriptiveComplexity.hamSOLang : FirstOrder.Language

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

Equations

• DescriptiveComplexity.hamSOLang = FirstOrder.Language.digraph.sum DescriptiveComplexity.hamGuessBlock.lang

inductive DescriptiveComplexity.HamGuessBlockIx : Type

The relation variables of the block.

• le : HamGuessBlockIx

  The guessed order.

@[instance_reducible]

instance DescriptiveComplexity.instFintypeHamGuessBlockIx : Fintype HamGuessBlockIx

Equations

• DescriptiveComplexity.instFintypeHamGuessBlockIx = { elems := [DescriptiveComplexity.HamGuessBlockIx.le].toFinset, complete := DescriptiveComplexity.instFintypeHamGuessBlockIx._proof_1 }

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqHamGuessBlockIx : DecidableEq HamGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.hLeSym : hamSOLang.Relations 2

The le symbol over the sum.

Equations

• DescriptiveComplexity.hLeSym = Sum.inr DescriptiveComplexity.hLeRel

noncomputable def DescriptiveComplexity.hamKernel (dir : Bool) : hamSOLang.Sentence

The first-order kernel of the Σ₁ definitions: the guessed relation is a linear order carrying a tour.

Equations

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

The two definability theorems

theorem DescriptiveComplexity.dirHamCircuit_sigmaSODefinable : SigmaSODefinable 1 DirHamCircuit

Directed Hamilton Circuit is Σ₁-definable: existentially guess the circuit as a linear order of the universe, then check first-order that it is one and that it follows the arcs.

theorem DescriptiveComplexity.hamCircuit_sigmaSODefinable : SigmaSODefinable 1 HamCircuit

Hamilton Circuit is Σ₁-definable: the same certificate, the two adjacency clauses reading the arc relation symmetrically.