The sum of two witness counts, as one witness count

Two kernels over two blocks are combined into one kernel over one block with a selector, a relation variable of arity zero (DescriptiveComplexity.boolBlock): when the selector holds, the first kernel must hold of the first block and the second block must be empty; otherwise the second kernel must hold of the second block and the first block must be empty (DescriptiveComplexity.pairKernel). The witnesses of the pair kernel are, bijectively, the witnesses of one kernel or the other (DescriptiveComplexity.pairWitnessEquiv), so

• its witness count is the sum of the two (DescriptiveComplexity.witnessCount_pairKernel),
• and the selector reads the two summands back (DescriptiveComplexity.card_pairWitness_sel, DescriptiveComplexity.card_pairWitness_not_sel).

The first is what adding a constant to a witness count takes – the second kernel being ⊤ over the block without variables, with exactly one witness (DescriptiveComplexity.witnessCount_trivial_top) – and so what the closure under complement of ⊕P and PP rests on. The second is what the completeness of a problem comparing two counts rests on: a single formula, whose models are told apart by the value of the selector's variable.

The selector block and the lifting of kernels

@[reducible]

def DescriptiveComplexity.boolBlock : SOBlock

The block with one relation variable of arity zero: a Boolean.

Equations

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

def DescriptiveComplexity.boolSel {A : Type} (ζ : boolBlock.Assignment A) : Prop

The Boolean an assignment of the selector block holds.

Equations

• DescriptiveComplexity.boolSel ζ = ζ () finZeroElim

def DescriptiveComplexity.SOBlock.consAssignEquiv (B M : SOBlock) (A : Type) : (B.cons M).Assignment A ≃ B.Assignment A × M.Assignment A

Assignments of a merged block are pairs of assignments.

Equations

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

noncomputable def DescriptiveComplexity.liftFst {L : FirstOrder.Language} (B M : SOBlock) (φ : (L.sum B.lang).Sentence) : (L.sum (B.cons M).lang).Sentence

A sentence over the expansion by B, read over the expansion by the merged block SOBlock.cons B M.

Equations

• DescriptiveComplexity.liftFst B M φ = (DescriptiveComplexity.mergeStep L B M).onSentence (FirstOrder.Language.LHom.sumInl.onSentence φ)

noncomputable def DescriptiveComplexity.liftSnd {L : FirstOrder.Language} (B M : SOBlock) (φ : (L.sum M.lang).Sentence) : (L.sum (B.cons M).lang).Sentence

A sentence over the expansion by M, read over the expansion by the merged block SOBlock.cons B M.

Equations

• DescriptiveComplexity.liftSnd B M φ = (DescriptiveComplexity.mergeStep L B M).onSentence ((FirstOrder.Language.LHom.sumInl.sumMap (FirstOrder.Language.LHom.id M.lang)).onSentence φ)

noncomputable def DescriptiveComplexity.emptyBlockS {L : FirstOrder.Language} (B : SOBlock) : (L.sum B.lang).Sentence

“Every relation variable of the block is empty.”

Equations

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

noncomputable def DescriptiveComplexity.selectorS {L : FirstOrder.Language} (B : SOBlock) : (L.sum (B.cons boolBlock).lang).Sentence

“The selector holds.”

Equations

• DescriptiveComplexity.selectorS B = FirstOrder.Language.Relations.formula (Sum.inr ⟨Sum.inr (), ⋯⟩) finZeroElim

The pair kernel

@[reducible, inline]

abbrev DescriptiveComplexity.pairBlock (B B' : SOBlock) : SOBlock

The block of a pair of kernels: the two blocks and the selector.

Equations

• DescriptiveComplexity.pairBlock B B' = B.cons (B'.cons DescriptiveComplexity.boolBlock)

noncomputable def DescriptiveComplexity.pairKernel {L : FirstOrder.Language} (B B' : SOBlock) (φ : (L.sum B.lang).Sentence) (φ' : (L.sum B'.lang).Sentence) : (L.sum (pairBlock B B').lang).Sentence

The pair kernel: the first kernel of the first block when the selector holds, the second block being empty; the second kernel of the second block otherwise, the first block being empty.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Witness {L : FirstOrder.Language} (M : SOBlock) (ψ : (L.sum M.lang).Sentence) (A : Type) [L.Structure A] : Type

The witnesses of a kernel.

Equations

• DescriptiveComplexity.Witness M ψ A = { ρ : M.Assignment A // A ⊨ ψ }

def DescriptiveComplexity.SOBlock.emptyAssign (M : SOBlock) (A : Type) : M.Assignment A

The empty assignment of a block.

Equations

• M.emptyAssign A x✝¹ x✝ = False

@[reducible, inline]

abbrev DescriptiveComplexity.pairFst {B B' : SOBlock} {A : Type} (ρ : (pairBlock B B').Assignment A) : B.Assignment A

The first component of an assignment of the pair block.

Equations

• DescriptiveComplexity.pairFst ρ i = ρ (Sum.inl i)

@[reducible, inline]

abbrev DescriptiveComplexity.pairSnd {B B' : SOBlock} {A : Type} (ρ : (pairBlock B B').Assignment A) : B'.Assignment A

The second component of an assignment of the pair block.

Equations

• DescriptiveComplexity.pairSnd ρ i = ρ (Sum.inr (Sum.inl i))

@[reducible, inline]

abbrev DescriptiveComplexity.pairSel {B B' : SOBlock} {A : Type} (ρ : (pairBlock B B').Assignment A) : Prop

The selector of an assignment of the pair block.

Equations

• DescriptiveComplexity.pairSel ρ = DescriptiveComplexity.boolSel fun (i : DescriptiveComplexity.boolBlock.ι) => ρ (Sum.inr (Sum.inr i))

theorem DescriptiveComplexity.witnessCount_pairKernel {L : FirstOrder.Language} {B B' : SOBlock} {φ : (L.sum B.lang).Sentence} {φ' : (L.sum B'.lang).Sentence} {A : Type} [L.Structure A] [Finite A] : witnessCount (pairBlock B B') (pairKernel B B' φ φ') A = witnessCount B φ A + witnessCount B' φ' A

The witness count of the pair kernel is the sum of the two witness counts.

def DescriptiveComplexity.subtypeIsLeftEquiv {X Y : Type} : { s : X ⊕ Y // s.isLeft = true } ≃ X

The left summands of a sum type.

Equations

• DescriptiveComplexity.subtypeIsLeftEquiv = { toFun := fun (s : { s : X ⊕ Y // s.isLeft = true }) => (↑s).getLeft ⋯, invFun := fun (x : X) => ⟨Sum.inl x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def DescriptiveComplexity.subtypeIsRightEquiv {X Y : Type} : { s : X ⊕ Y // s.isLeft = false } ≃ Y

The right summands of a sum type.

Equations

• DescriptiveComplexity.subtypeIsRightEquiv = { toFun := fun (s : { s : X ⊕ Y // s.isLeft = false }) => (↑s).getRight ⋯, invFun := fun (y : Y) => ⟨Sum.inr y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem DescriptiveComplexity.card_pairWitness_sel {L : FirstOrder.Language} {B B' : SOBlock} {φ : (L.sum B.lang).Sentence} {φ' : (L.sum B'.lang).Sentence} {A : Type} [L.Structure A] : Nat.card { w : Witness (pairBlock B B') (pairKernel B B' φ φ') A // pairSel ↑w } = witnessCount B φ A

The witnesses of the pair kernel with the selector are the witnesses of the first kernel.

theorem DescriptiveComplexity.card_pairWitness_not_sel {L : FirstOrder.Language} {B B' : SOBlock} {φ : (L.sum B.lang).Sentence} {φ' : (L.sum B'.lang).Sentence} {A : Type} [L.Structure A] : Nat.card { w : Witness (pairBlock B B') (pairKernel B B' φ φ') A // ¬pairSel ↑w } = witnessCount B' φ' A

The witnesses of the pair kernel without the selector are the witnesses of the second kernel.

theorem DescriptiveComplexity.witnessCount_trivial_top {L : FirstOrder.Language} {A : Type} [L.Structure A] : witnessCount SOBlock.trivial ⊤ A = 1

The kernel ⊤ over the block without variables has exactly one witness.