3-dimensional matching is existential second-order definable

The membership half of its NP-completeness (DescriptiveComplexity.threeDimMatching_sigmaSODefinable): a matching is a relation, so a single existential block guesses it – ternary, the first of the catalog – and the kernel spells out the seven conditions of DescriptiveComplexity.IsMatchingOn: that the guessed triples are available ones inside the three classes, that every marked element is covered, and that no two triples share a coordinate.

def DescriptiveComplexity.tdmGuessBlock : SOBlock

The single existential block of the Σ₁ definition: the matching, a ternary relation.

Equations

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

def DescriptiveComplexity.tdmMatchRel : tdmGuessBlock.lang.Relations 3

The symbol of the guessed matching.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.tdmSOLang : FirstOrder.Language

The vocabulary of the kernel: triple systems together with the guessed matching.

Equations

• DescriptiveComplexity.tdmSOLang = FirstOrder.Language.tripleSys.sum DescriptiveComplexity.tdmGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.tXSym : tdmSOLang.Relations 1

The first-class symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tXSym = Sum.inl FirstOrder.Language.tsX

@[reducible, inline]

abbrev DescriptiveComplexity.tYSym : tdmSOLang.Relations 1

The second-class symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tYSym = Sum.inl FirstOrder.Language.tsY

@[reducible, inline]

abbrev DescriptiveComplexity.tZSym : tdmSOLang.Relations 1

The third-class symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tZSym = Sum.inl FirstOrder.Language.tsZ

@[reducible, inline]

abbrev DescriptiveComplexity.tTripSym : tdmSOLang.Relations 3

The triple symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tTripSym = Sum.inl FirstOrder.Language.tsTrip

@[reducible, inline]

abbrev DescriptiveComplexity.tMatchSym : tdmSOLang.Relations 3

The matching symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tMatchSym = Sum.inr DescriptiveComplexity.tdmMatchRel

noncomputable def DescriptiveComplexity.tdmKernel : tdmSOLang.Sentence

The first-order kernel of the Σ₁ definition: the guessed relation is a matching.

Equations

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

theorem DescriptiveComplexity.threeDimMatching_sigmaSODefinable : SigmaSODefinable 1 ThreeDimMatching

3-dimensional matching is Σ₁-definable: existentially guess the matching – a ternary relation – then check first-order that it is one. Since NP is defined as Σ₁-definability, this is the membership half of its NP-completeness.