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

• DescriptiveComplexity.hamGuessBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 2 }

def DescriptiveComplexity.hamLeRel : hamGuessBlock.lang.Relations 2

The symbol of the guessed order.

Equations

• DescriptiveComplexity.hamLeRel = ⟨(), DescriptiveComplexity.hamLeRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.hamSOLang : FirstOrder.Language

The vocabulary of the kernel: digraphs together with the guessed order.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.hArcSym : hamSOLang.Relations 2

The arc symbol in the kernel's vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.hLeSym : hamSOLang.Relations 2

The order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.hLeSym = Sum.inr DescriptiveComplexity.hamLeRel

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.