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.

inductive DescriptiveComplexity.TdmGuessBlockIx : Type

The relation variables of the block.

• matching : TdmGuessBlockIx

  The guessed matching.

def DescriptiveComplexity.tMatchingRel : tdmGuessBlock.lang.Relations 3

The matching relation variable.

Equations

• DescriptiveComplexity.tMatchingRel = ⟨DescriptiveComplexity.TdmGuessBlockIx.matching, DescriptiveComplexity.tMatchingRel._proof_1⟩

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqTdmGuessBlockIx : DecidableEq TdmGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.tTripSym : tdmSOLang.Relations 3

The trip symbol over the sum.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.tYElSym : tdmSOLang.Relations 1

The yEl symbol over the sum.

Equations

• DescriptiveComplexity.tYElSym = Sum.inl FirstOrder.Language.tsYEl

def DescriptiveComplexity.tdmGuessBlock : SOBlock

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

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.tdmSOLang : FirstOrder.Language

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

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.tZElSym : tdmSOLang.Relations 1

The zEl symbol over the sum.

Equations

• DescriptiveComplexity.tZElSym = Sum.inl FirstOrder.Language.tsZEl

@[reducible, inline]

abbrev DescriptiveComplexity.tMatchingSym : tdmSOLang.Relations 3

The matching symbol over the sum.

Equations

• DescriptiveComplexity.tMatchingSym = Sum.inr DescriptiveComplexity.tMatchingRel

@[reducible, inline]

abbrev DescriptiveComplexity.tXElSym : tdmSOLang.Relations 1

The xEl symbol over the sum.

Equations

• DescriptiveComplexity.tXElSym = Sum.inl FirstOrder.Language.tsXEl

@[instance_reducible]

instance DescriptiveComplexity.instFintypeTdmGuessBlockIx : Fintype TdmGuessBlockIx

Equations

• DescriptiveComplexity.instFintypeTdmGuessBlockIx = { elems := [DescriptiveComplexity.TdmGuessBlockIx.matching].toFinset, complete := DescriptiveComplexity.instFintypeTdmGuessBlockIx._proof_1 }

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.