The set family is existential second-order definable

The membership half of the NP-completeness of Set Cover and Set Packing: both are Σ₁-definable in the sense of DescriptiveComplexity.SecondOrder (DescriptiveComplexity.setCover_sigmaSODefinable, DescriptiveComplexity.setPacking_sigmaSODefinable). Hitting Set needs no definition of its own: it FO-reduces to Set Cover (DescriptiveComplexity.Problems.SetFamily.Reductions).

The two definitions share everything but their goal clause. A single existential block (DescriptiveComplexity.familyGuessBlock) guesses a unary relation – the subfamily – and a binary one – an injection witnessing the threshold – and the first-order kernel is a conjunction of clauses built from a common kit:

• DescriptiveComplexity.sfFamClause: the guessed subfamily consists of sets of the family (shared);
• the goal clause: DescriptiveComplexity.sfCoverClause (every ground element belongs to a guessed set) for Set Cover, DescriptiveComplexity.sfDisjClause (no ground element belongs to two distinct guessed sets) for Set Packing;
• the threshold clauses DescriptiveComplexity.sfGuessToMarkedClause (Set Cover, an upper bound: the subfamily injects into the marked set) or DescriptiveComplexity.sfMarkedToGuessClause (Set Packing, a lower bound: the marked set injects into the subfamily), together with the shared injectivity clause DescriptiveComplexity.sfInjClause.

The direction of the injection is the only semantic difference the threshold makes, which is exactly what the embedding forms of DescriptiveComplexity.Problems.SetFamily.Defs (DescriptiveComplexity.coversOn_iff_embedding, DescriptiveComplexity.packsOn_iff_embedding) say. This mirrors DescriptiveComplexity.clique_sigmaSODefinable, whose threshold is a lower bound like Set Packing's.

def DescriptiveComplexity.familyGuessBlock : SOBlock

The single existential block shared by the Σ₁ definitions of the set family: a unary relation variable (true: the guessed subfamily) and a binary one (false: the injection witnessing the threshold).

Equations

• DescriptiveComplexity.familyGuessBlock = { ι := Bool, ιFinite := Bool.instFinite, arity := fun (i : Bool) => bif i then 1 else 2 }

def DescriptiveComplexity.sfGuessRel : familyGuessBlock.lang.Relations 1

The symbol of the subfamily relation variable.

Equations

• DescriptiveComplexity.sfGuessRel = ⟨true, DescriptiveComplexity.sfGuessRel._proof_1⟩

def DescriptiveComplexity.sfInjRel : familyGuessBlock.lang.Relations 2

The symbol of the injection relation variable.

Equations

• DescriptiveComplexity.sfInjRel = ⟨false, DescriptiveComplexity.sfInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.setFamilySOLang : FirstOrder.Language

The vocabulary of the kernels: set systems together with the two guessed relation variables.

Equations

• DescriptiveComplexity.setFamilySOLang = FirstOrder.Language.setSystem.sum DescriptiveComplexity.familyGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.sfElemSym : setFamilySOLang.Relations 1

The ground-element symbol in the kernels' vocabulary.

Equations

• DescriptiveComplexity.sfElemSym = Sum.inl FirstOrder.Language.ssElem

@[reducible, inline]

abbrev DescriptiveComplexity.sfFamSym : setFamilySOLang.Relations 1

The family symbol in the kernels' vocabulary.

Equations

• DescriptiveComplexity.sfFamSym = Sum.inl FirstOrder.Language.ssFam

@[reducible, inline]

abbrev DescriptiveComplexity.sfMemSym : setFamilySOLang.Relations 2

The incidence symbol in the kernels' vocabulary.

Equations

• DescriptiveComplexity.sfMemSym = Sum.inl FirstOrder.Language.ssMem

@[reducible, inline]

abbrev DescriptiveComplexity.sfMarkedSym : setFamilySOLang.Relations 1

The mark symbol in the kernels' vocabulary.

Equations

• DescriptiveComplexity.sfMarkedSym = Sum.inl FirstOrder.Language.ssMarked

@[reducible, inline]

abbrev DescriptiveComplexity.sfGuessSym : setFamilySOLang.Relations 1

The subfamily symbol in the kernels' vocabulary.

Equations

• DescriptiveComplexity.sfGuessSym = Sum.inr DescriptiveComplexity.sfGuessRel

@[reducible, inline]

abbrev DescriptiveComplexity.sfInjSym : setFamilySOLang.Relations 2

The injection symbol in the kernels' vocabulary.

Equations

• DescriptiveComplexity.sfInjSym = Sum.inr DescriptiveComplexity.sfInjRel

The clauses

noncomputable def DescriptiveComplexity.sfFamClause : setFamilySOLang.Sentence

Kernel clause: the guessed subfamily consists of sets of the family.

Equations

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

noncomputable def DescriptiveComplexity.sfCoverClause : setFamilySOLang.Sentence

Kernel clause (Set Cover): every ground element belongs to a guessed set.

Equations

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

noncomputable def DescriptiveComplexity.sfDisjClause : setFamilySOLang.Sentence

Kernel clause (Set Packing): no ground element belongs to two distinct guessed sets.

Equations

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

noncomputable def DescriptiveComplexity.sfGuessToMarkedClause : setFamilySOLang.Sentence

Kernel clause (Set Cover's threshold, an upper bound): the guessed injection maps every member of the subfamily to a marked element.

Equations

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

noncomputable def DescriptiveComplexity.sfMarkedToGuessClause : setFamilySOLang.Sentence

Kernel clause (Set Packing's threshold, a lower bound): the guessed injection maps every marked element to a member of the subfamily.

Equations

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

noncomputable def DescriptiveComplexity.sfInjClause : setFamilySOLang.Sentence

Kernel clause: the guessed injection is injective.

Equations

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

noncomputable def DescriptiveComplexity.setCoverKernel : setFamilySOLang.Sentence

The kernel of the Σ₁ definition of Set Cover.

Equations

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

noncomputable def DescriptiveComplexity.exactCoverKernel : setFamilySOLang.Sentence

The first-order kernel of the Σ₁ definition of Exact Cover: the same kit again, this time asking for a subfamily that both covers and is pairwise disjoint – and, exactness replacing the threshold, no injection clause.

Equations

• DescriptiveComplexity.exactCoverKernel = DescriptiveComplexity.sfFamClause ⊓ (DescriptiveComplexity.sfCoverClause ⊓ DescriptiveComplexity.sfDisjClause)

noncomputable def DescriptiveComplexity.sfSplitInClause : setFamilySOLang.Sentence

Kernel clause (Set Splitting): every set of the family contains a coloured ground element.

Equations

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

noncomputable def DescriptiveComplexity.sfSplitOutClause : setFamilySOLang.Sentence

Kernel clause (Set Splitting): every set of the family contains an uncoloured ground element.

Equations

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

noncomputable def DescriptiveComplexity.setSplittingKernel : setFamilySOLang.Sentence

The first-order kernel of the Σ₁ definition of Set Splitting: the guessed relation is read as one colour class, and every set of the family meets it and its complement.

Equations

• DescriptiveComplexity.setSplittingKernel = DescriptiveComplexity.sfSplitInClause ⊓ DescriptiveComplexity.sfSplitOutClause

noncomputable def DescriptiveComplexity.setPackingKernel : setFamilySOLang.Sentence

The kernel of the Σ₁ definition of Set Packing.

Equations

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

Realization of the clauses

The two definitions

theorem DescriptiveComplexity.setCover_sigmaSODefinable : SigmaSODefinable 1 SetCover

Set Cover is Σ₁-definable: existentially guess the covering subfamily and an injection of it into the marked set, then check both first-order. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Set Cover.

theorem DescriptiveComplexity.setPacking_sigmaSODefinable : SigmaSODefinable 1 SetPacking

Set Packing is Σ₁-definable: existentially guess the packing and an injection of the marked set into it, then check both first-order. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Set Packing.

theorem DescriptiveComplexity.exactCover_sigmaSODefinable : SigmaSODefinable 1 ExactCover

Exact Cover is Σ₁-definable: existentially guess the subfamily and check first-order that it covers every ground element and that no element is covered twice. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Exact Cover.

theorem DescriptiveComplexity.setSplitting_sigmaSODefinable : SigmaSODefinable 1 SetSplitting

Set Splitting is Σ₁-definable: existentially guess one colour class and check first-order that every set of the family meets it and its complement.