Merging a quantifier prefix into a single second-order block

A second-order sentence with k alternating blocks quantifies over a list of blocks Bs, and its kernel lives over the iterated expansion DescriptiveComplexity.soLang L Bs. Constructions that must read the kernel – above all the Tseitin translation of DescriptiveComplexity.Problems.Sat.Tseitin, which turns it into a CNF instance – are stated for a single block, over L.sum B.lang.

This file bridges the two: DescriptiveComplexity.mergeBlocks collects a list of blocks into one block whose relation variables are the disjoint union of theirs, and DescriptiveComplexity.mergeHom transports the kernel accordingly. The alternation is not lost – it moves from the block list to DescriptiveComplexity.altAssign, which quantifies the components of a merged assignment alternately – so DescriptiveComplexity.sorealize_iff_altAssign rewrites alternating second-order satisfaction as an alternating quantification over the pieces of a single assignment, with a single-block kernel.

The only mathematical content is the re-association (L ⊕ B) ⊕ M ≅ L ⊕ (B ⊕ M) of DescriptiveComplexity.mergeStep, applied once per block.

Merging blocks

@[reducible]

def DescriptiveComplexity.SOBlock.cons (B M : SOBlock) : SOBlock

Prepending a block to another: the relation variables are the disjoint union of both families. Reducible, so that (SOBlock.cons B M).ι unfolds to a sum type when elaborating index literals.

Equations

• B.cons M = { ι := B.ι ⊕ M.ι, ιFinite := ⋯, arity := Sum.elim B.arity M.arity }

def DescriptiveComplexity.mergeBlocks : List SOBlock → SOBlock

The single block merging a whole list of blocks: one relation variable per relation variable of one of the blocks.

Equations

• DescriptiveComplexity.mergeBlocks [] = DescriptiveComplexity.SOBlock.trivial
• DescriptiveComplexity.mergeBlocks (B :: Bs) = B.cons (DescriptiveComplexity.mergeBlocks Bs)

def DescriptiveComplexity.consAssign {A : Type} {B M : SOBlock} (ρ : B.Assignment A) (μ : M.Assignment A) : (B.cons M).Assignment A

An assignment of the merged block SOBlock.cons B M, assembled from an assignment of B and one of M.

Equations

• DescriptiveComplexity.consAssign ρ μ (Sum.inl i) = ρ i
• DescriptiveComplexity.consAssign ρ μ (Sum.inr i) = μ i

def DescriptiveComplexity.nilAssign (A : Type) : (mergeBlocks []).Assignment A

The unique assignment of the merged block of the empty list.

Equations

• DescriptiveComplexity.nilAssign A i = Empty.elim i

Re-associating an expansion

def DescriptiveComplexity.mergeStep (L : FirstOrder.Language) (B M : SOBlock) : (L.sum B.lang).sum M.lang →ᴸ L.sum (B.cons M).lang

Re-association of language expansions: expanding L by a block B and then by a block M is expanding L by the merged block SOBlock.cons B M.

Equations

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

theorem DescriptiveComplexity.mergeStep_isExpansionOn (L : FirstOrder.Language) {A : Type} (instL : L.Structure A) (B M : SOBlock) (ρ : B.Assignment A) (μ : M.Assignment A) : (mergeStep L B M).IsExpansionOn A

The re-association is an expansion: it does not change how any symbol is interpreted, when the two block assignments on one side are assembled into a single merged assignment on the other.

Transporting the kernel

def DescriptiveComplexity.mergeHom (Bs : List SOBlock) (L : FirstOrder.Language) : soLang L Bs →ᴸ L.sum (mergeBlocks Bs).lang

The morphism transporting a kernel over the iterated block expansion into one over the single merged block.

Equations

• DescriptiveComplexity.mergeHom [] x✝ = FirstOrder.Language.LHom.sumInl
• DescriptiveComplexity.mergeHom (B :: Bs) x✝ = (DescriptiveComplexity.mergeStep x✝ B (DescriptiveComplexity.mergeBlocks Bs)).comp (DescriptiveComplexity.mergeHom Bs (x✝.sum B.lang))

Alternating quantification over a merged assignment

def DescriptiveComplexity.altAssign (A : Type) (Bs : List SOBlock) : ((mergeBlocks Bs).Assignment A → Prop) → Bool → Prop

Alternating quantification over the components of an assignment of the merged block: the component of the first block is quantified outermost, existentially if pol is true, and the polarities alternate inwards.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.altAssign A [] P x✝ = P (DescriptiveComplexity.nilAssign A)

theorem DescriptiveComplexity.altAssign_congr {A : Type} (Bs : List SOBlock) (P Q : (mergeBlocks Bs).Assignment A → Prop) : (∀ (μ : (mergeBlocks Bs).Assignment A), P μ ↔ Q μ) → ∀ (pol : Bool), altAssign A Bs P pol ↔ altAssign A Bs Q pol

Alternating quantification over a merged assignment only depends on the quantified predicate up to pointwise equivalence.

The merging theorem

theorem DescriptiveComplexity.sorealize_iff_altAssign (Bs : List SOBlock) (L : FirstOrder.Language) (A : Type) (instL : L.Structure A) (φ : (soLang L Bs).Sentence) (pol : Bool) : SORealize L A Bs φ pol ↔ altAssign A Bs (fun (μ : (mergeBlocks Bs).Assignment A) => A ⊨ (mergeHom Bs L).onSentence φ) pol

Merging a quantifier prefix: alternating second-order satisfaction over a list of blocks is the alternating quantification, over the components of a single merged assignment, of the transported kernel.

Enlarging the innermost block

The Tseitin translation of a kernel introduces auxiliary gate variables, which have to be quantified together with the relation variables of the innermost block. The constructions below enlarge the last block of a prefix by a further block Gt, and show that quantifying the enlarged prefix is quantifying the original one with an extra quantifier – of the innermost polarity – over Gt inside. Lists are given as a head and a tail, so that “nonempty” is built into the syntax and the recursion has no overlapping patterns.

def DescriptiveComplexity.quantB (pol : Bool) {α : Type} (P : α → Prop) : Prop

Quantification with a polarity: existential if pol is true.

Equations

• DescriptiveComplexity.quantB true P = ∃ (a : α), P a
• DescriptiveComplexity.quantB false P = ∀ (a : α), P a

def DescriptiveComplexity.innerPol : ℕ → Bool → Bool

The polarity of the innermost quantifier of a prefix whose tail has length n and whose outermost polarity is pol.

Equations

• DescriptiveComplexity.innerPol 0 x✝ = x✝
• DescriptiveComplexity.innerPol n.succ x✝ = DescriptiveComplexity.innerPol n !x✝

theorem DescriptiveComplexity.innerPol_eq (n : ℕ) (pol : Bool) : innerPol n pol = (decide (n % 2 = 1) ^^ pol)

The innermost polarity in closed form: it flips with the parity of the number of blocks below it.

@[reducible]

def DescriptiveComplexity.consLast (Gt : SOBlock) : SOBlock → List SOBlock → List SOBlock

The prefix B :: Bs with its innermost block enlarged by Gt. Reducible, so that (consLast Gt B Bs).length computes and Fin numerals over it elaborate.

Equations

• DescriptiveComplexity.consLast Gt x✝ [] = [x✝.cons Gt]
• DescriptiveComplexity.consLast Gt x✝ (B' :: Bs) = x✝ :: DescriptiveComplexity.consLast Gt B' Bs

def DescriptiveComplexity.combineLast (Gt : SOBlock) {A : Type} (B : SOBlock) (Bs : List SOBlock) : (mergeBlocks (B :: Bs)).Assignment A → Gt.Assignment A → (mergeBlocks (consLast Gt B Bs)).Assignment A

An assignment of the enlarged prefix, assembled from an assignment of the original prefix and one of the extra block.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.combineLast Gt x✝¹ [] μ x✝ = DescriptiveComplexity.consAssign (DescriptiveComplexity.consAssign (fun (i : x✝¹.ι) => μ (Sum.inl i)) x✝) (DescriptiveComplexity.nilAssign A)

theorem DescriptiveComplexity.consLast_length (Gt B : SOBlock) (Bs : List SOBlock) : (consLast Gt B Bs).length = Bs.length + 1

Enlarging the innermost block does not change the number of blocks.

def DescriptiveComplexity.splitIdx (Gt B : SOBlock) (Bs : List SOBlock) : (mergeBlocks (consLast Gt B Bs)).ι → (mergeBlocks (B :: Bs)).ι ⊕ Gt.ι

Routing a relation variable of the enlarged prefix: it is either a relation variable of the original prefix, or a variable of the extra block. Note that this is a plain function – no dependent types – so a reading built from it needs no arity cast.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.splitIdx Gt x✝ [] (Sum.inl (Sum.inl i)) = Sum.inl (Sum.inl i)
• DescriptiveComplexity.splitIdx Gt x✝ [] (Sum.inl (Sum.inr j)) = Sum.inr j
• DescriptiveComplexity.splitIdx Gt x✝ [] (Sum.inr e) = Empty.elim e
• DescriptiveComplexity.splitIdx Gt x✝ (head :: tail) (Sum.inl i) = Sum.inl (Sum.inl i)

theorem DescriptiveComplexity.arity_consLast_le (Gt : SOBlock) {D : ℕ} (hGt : ∀ (j : Gt.ι), Gt.arity j ≤ D) (B : SOBlock) (Bs : List SOBlock) : (∀ (i : (mergeBlocks (B :: Bs)).ι), (mergeBlocks (B :: Bs)).arity i ≤ D) → ∀ (i : (mergeBlocks (consLast Gt B Bs)).ι), (mergeBlocks (consLast Gt B Bs)).arity i ≤ D

Arities of the enlarged prefix are bounded by the bounds of its two parts.

theorem DescriptiveComplexity.consAssign_split {A : Type} {B C : SOBlock} (ρ : (B.cons C).Assignment A) : (consAssign (fun (i : B.ι) => ρ (Sum.inl i)) fun (j : C.ι) => ρ (Sum.inr j)) = ρ

Splitting and reassembling an assignment of a merged pair of blocks.

def DescriptiveComplexity.atomPart (Gt : SOBlock) {A : Type} (B : SOBlock) (Bs : List SOBlock) : (mergeBlocks (consLast Gt B Bs)).Assignment A → (mergeBlocks (B :: Bs)).Assignment A

The original part of an assignment of the enlarged prefix.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.atomPart Gt x✝ [] μ = DescriptiveComplexity.consAssign (fun (i : x✝.ι) => μ (Sum.inl (Sum.inl i))) (DescriptiveComplexity.nilAssign A)

def DescriptiveComplexity.gatePart (Gt : SOBlock) {A : Type} (B : SOBlock) (Bs : List SOBlock) : (mergeBlocks (consLast Gt B Bs)).Assignment A → Gt.Assignment A

The gate part of an assignment of the enlarged prefix.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.gatePart Gt x✝ [] μ = fun (j : Gt.ι) => μ (Sum.inl (Sum.inr j))

theorem DescriptiveComplexity.consAssign_nil {A : Type} {B : SOBlock} (μ : (mergeBlocks [B]).Assignment A) : consAssign (fun (i : B.ι) => μ (Sum.inl i)) (nilAssign A) = μ

Reassembling a singleton merged assignment.

theorem DescriptiveComplexity.atomPart_combineLast (Gt : SOBlock) {A : Type} (B : SOBlock) (Bs : List SOBlock) (μ : (mergeBlocks (B :: Bs)).Assignment A) (g : Gt.Assignment A) : atomPart Gt B Bs (combineLast Gt B Bs μ g) = μ

theorem DescriptiveComplexity.gatePart_combineLast (Gt : SOBlock) {A : Type} (B : SOBlock) (Bs : List SOBlock) (μ : (mergeBlocks (B :: Bs)).Assignment A) (g : Gt.Assignment A) : gatePart Gt B Bs (combineLast Gt B Bs μ g) = g

theorem DescriptiveComplexity.altAssign_consLast (Gt : SOBlock) {A : Type} (B : SOBlock) (Bs : List SOBlock) (G : (mergeBlocks (consLast Gt B Bs)).Assignment A → Prop) (pol : Bool) : altAssign A (consLast Gt B Bs) G pol ↔ altAssign A (B :: Bs) (fun (μ : (mergeBlocks (B :: Bs)).Assignment A) => quantB (innerPol Bs.length pol) fun (g : Gt.Assignment A) => G (combineLast Gt B Bs μ g)) pol

Enlarging the innermost block: quantifying a prefix whose innermost block has been enlarged by Gt is quantifying the original prefix, with an extra quantifier over Gt – of the innermost polarity – inside.

The converse transport

For stating that a problem is second-order definable one needs to go the other way: a kernel written over the single merged block has to be turned into a kernel over the iterated expansion. The morphisms below invert those above, and give the same theorem read from right to left (DescriptiveComplexity.sorealize_unmerge).

def DescriptiveComplexity.unmergeStep (L : FirstOrder.Language) (B M : SOBlock) : L.sum (B.cons M).lang →ᴸ (L.sum B.lang).sum M.lang

The inverse of DescriptiveComplexity.mergeStep: splitting the merged block back into the head block and the merged tail.

Equations

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

theorem DescriptiveComplexity.unmergeStep_isExpansionOn (L : FirstOrder.Language) {A : Type} (instL : L.Structure A) (B M : SOBlock) (ρ : B.Assignment A) (μ : M.Assignment A) : (unmergeStep L B M).IsExpansionOn A

def DescriptiveComplexity.unmergeNil (L : FirstOrder.Language) : L.sum SOBlock.trivial.lang →ᴸ L

Discarding the trivial block from an expansion.

Equations

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

theorem DescriptiveComplexity.unmergeNil_isExpansionOn (L : FirstOrder.Language) {A : Type} (instL : L.Structure A) (μ : SOBlock.trivial.Assignment A) : (unmergeNil L).IsExpansionOn A

def DescriptiveComplexity.unmergeHom (Bs : List SOBlock) (L : FirstOrder.Language) : L.sum (mergeBlocks Bs).lang →ᴸ soLang L Bs

The morphism transporting a single-block kernel into the iterated block expansion.

Equations

• DescriptiveComplexity.unmergeHom [] x✝ = DescriptiveComplexity.unmergeNil x✝
• DescriptiveComplexity.unmergeHom (B :: Bs) x✝ = (DescriptiveComplexity.unmergeHom Bs (x✝.sum B.lang)).comp (DescriptiveComplexity.unmergeStep x✝ B (DescriptiveComplexity.mergeBlocks Bs))

theorem DescriptiveComplexity.sorealize_unmerge (Bs : List SOBlock) (L : FirstOrder.Language) (A : Type) (instL : L.Structure A) (ψ : (L.sum (mergeBlocks Bs).lang).Sentence) (pol : Bool) : SORealize L A Bs ((unmergeHom Bs L).onSentence ψ) pol ↔ altAssign A Bs (fun (μ : (mergeBlocks Bs).Assignment A) => A ⊨ ψ) pol

Merging a quantifier prefix, read backwards: a kernel over the single merged block, transported into the iterated expansion, is satisfied alternately exactly when the merged assignment is quantified alternately.