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.

@[reducible, inline]

abbrev DescriptiveComplexity.sfMemSym : setFamilySOLang.Relations 2

The mem symbol over the sum.

Equations

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

inductive DescriptiveComplexity.FamilyGuessBlockIx : Type

The relation variables of the block.

• guess : FamilyGuessBlockIx

  The guessed subfamily.

• inj : FamilyGuessBlockIx

  The injection witnessing the threshold.

@[reducible, inline]

abbrev DescriptiveComplexity.sfInjSym : setFamilySOLang.Relations 2

The inj symbol over the sum.

Equations

• DescriptiveComplexity.sfInjSym = Sum.inr DescriptiveComplexity.sfInjRel

def DescriptiveComplexity.sfGuessRel : familyGuessBlock.lang.Relations 1

The guess relation variable.

Equations

• DescriptiveComplexity.sfGuessRel = ⟨DescriptiveComplexity.FamilyGuessBlockIx.guess, DescriptiveComplexity.sfGuessRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.sfElemSym : setFamilySOLang.Relations 1

The elem symbol over the sum.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.setFamilySOLang : FirstOrder.Language

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

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.sfGuessSym : setFamilySOLang.Relations 1

The guess symbol over the sum.

Equations

• DescriptiveComplexity.sfGuessSym = Sum.inr DescriptiveComplexity.sfGuessRel

def DescriptiveComplexity.sfInjRel : familyGuessBlock.lang.Relations 2

The inj relation variable.

Equations

• DescriptiveComplexity.sfInjRel = ⟨DescriptiveComplexity.FamilyGuessBlockIx.inj, DescriptiveComplexity.sfInjRel._proof_1⟩

@[instance_reducible]

instance DescriptiveComplexity.instFintypeFamilyGuessBlockIx : Fintype FamilyGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.sfFamSym : setFamilySOLang.Relations 1

The fam symbol over the sum.

Equations

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

def DescriptiveComplexity.familyGuessBlock : SOBlock

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

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqFamilyGuessBlockIx : DecidableEq FamilyGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.sfMarkedSym : setFamilySOLang.Relations 1

The marked symbol over the sum.

Equations

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

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 colored 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 uncolored 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 color 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 color class and check first-order that every set of the family meets it and its complement.