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.sfInjSym : setFamilySOLang.Relations 2

The inj symbol over the sum.

Equations

• DescriptiveComplexity.sfInjSym = Sum.inr DescriptiveComplexity.sfInjRel

@[reducible, inline]

abbrev DescriptiveComplexity.sfFamSym : setFamilySOLang.Relations 1

The fam symbol over the sum.

Equations

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

inductive DescriptiveComplexity.FamilyGuessBlockIx : Type

The relation variables of the block.

• guess : FamilyGuessBlockIx

  The guessed subfamily.

• inj : FamilyGuessBlockIx

  The injection witnessing the threshold.

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.instDecidableEqFamilyGuessBlockIx : DecidableEq FamilyGuessBlockIx

Equations

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

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.instFintypeFamilyGuessBlockIx : Fintype FamilyGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.sfMarkedSym : setFamilySOLang.Relations 1

The marked symbol over the sum.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.sfMemSym : setFamilySOLang.Relations 2

The mem symbol over the sum.

Equations

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

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.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.sfNoInjClause : setFamilySOLang.Sentence

Kernel clause: the binary relation variable of the block is empty. Exact Cover does not use it, and a definition that counts the witnesses has to say so, or each exact cover would be counted once per binary relation.

Equations

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

noncomputable def DescriptiveComplexity.sharpExactCoverKernel : setFamilySOLang.Sentence

The kernel of the witness-counting definition of Exact Cover: the kernel of its Σ₁ definition, with the unused relation variable pinned.

Equations

• DescriptiveComplexity.sharpExactCoverKernel = DescriptiveComplexity.exactCoverKernel ⊓ DescriptiveComplexity.sfNoInjClause

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.sfGuessElemClause : setFamilySOLang.Sentence

Kernel clause: the guessed relation holds only of ground elements.

Equations

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

noncomputable def DescriptiveComplexity.sharpSetSplittingKernel : setFamilySOLang.Sentence

The kernel of the witness-counting definition of Set Splitting: a color class of ground elements splitting every set, the unused relation variable pinned.

Equations

• DescriptiveComplexity.sharpSetSplittingKernel = DescriptiveComplexity.setSplittingKernel ⊓ (DescriptiveComplexity.sfGuessElemClause ⊓ DescriptiveComplexity.sfNoInjClause)

Realization of the clauses

@[reducible, inline]

abbrev DescriptiveComplexity.SFRealize {A : Type} [FirstOrder.Language.setSystem.Structure A] (ρ : familyGuessBlock.Assignment A) (φ : setFamilySOLang.Sentence) : Prop

Realization at a set system expanded by an assignment of the block.

Equations

• DescriptiveComplexity.SFRealize ρ φ = A ⊨ φ

theorem DescriptiveComplexity.realize_sharpExactCoverKernel {A : Type} [FirstOrder.Language.setSystem.Structure A] (ρ : familyGuessBlock.Assignment A) : A ⊨ sharpExactCoverKernel ↔ (ExactCoverBy SSElem SSFam SSMem fun (s : A) => ρ FamilyGuessBlockIx.guess ![s]) ∧ ∀ (x y : A), ¬ρ FamilyGuessBlockIx.inj ![x, y]

Realization of the counting kernel of Exact Cover: the guessed subfamily is an exact cover, and the unused relation variable is empty.

theorem DescriptiveComplexity.realize_sharpSetSplittingKernel {A : Type} [FirstOrder.Language.setSystem.Structure A] (ρ : familyGuessBlock.Assignment A) : A ⊨ sharpSetSplittingKernel ↔ ((∀ (f : A), SSFam f → ∃ (x : A), SSElem x ∧ SSMem x f ∧ ρ FamilyGuessBlockIx.guess ![x]) ∧ ∀ (f : A), SSFam f → ∃ (x : A), SSElem x ∧ SSMem x f ∧ ¬ρ FamilyGuessBlockIx.guess ![x]) ∧ (∀ (x : A), ρ FamilyGuessBlockIx.guess ![x] → SSElem x) ∧ ∀ (x y : A), ¬ρ FamilyGuessBlockIx.inj ![x, y]

Realization of the counting kernel of Set Splitting.

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.