Functoriality of block expansion, and padding with trivial blocks

Infrastructure for the second-order definability layer of DescriptiveComplexity.SecondOrder:

• Functoriality: a language morphism Φ : L →ᴸ L' lifts through the expansion by a list of blocks (DescriptiveComplexity.soLangLift), and alternating second-order satisfaction is invariant when the base structure is expanded along Φ (DescriptiveComplexity.sorealize_soLangLift).
• Embedded first-order sentences: a sentence of the base language, embedded into the block expansion (DescriptiveComplexity.soLangEmbed), can be pulled out of the second-order quantification when it appears as a conjunct or as the premise of an implication (DescriptiveComplexity.sorealize_inf_embed, DescriptiveComplexity.sorealize_imp_embed). This is how the auxiliary order of an ordered reduction is eliminated: the order becomes a second-order variable of the first block, guarded by the first-order sentence “it is a linear order”.
• Padding: appending or prepending the trivial (empty) block (DescriptiveComplexity.SOBlock.trivial) does not change alternating second-order satisfaction (DescriptiveComplexity.sorealize_append_trivial), so Σₖ- and Πₖ-definability satisfy the level inclusions of the polynomial hierarchy: Σₖ ⊆ Σₖ₊₁ ∩ Πₖ₊₁ and dually (DescriptiveComplexity.SigmaSODefinable.succ, DescriptiveComplexity.SigmaSODefinable.piSucc, DescriptiveComplexity.PiSODefinable.succ, DescriptiveComplexity.PiSODefinable.sigmaSucc).

Languages vary through all the inductions, so the recursive definitions and statements take them as explicit arguments.

Assignments always exist

instance DescriptiveComplexity.SOBlock.instNonemptyAssignment (B : SOBlock) (A : Type) : Nonempty (B.Assignment A)

Functoriality of block expansion

def DescriptiveComplexity.soLangLift (Bs : List SOBlock) (L L' : FirstOrder.Language) : (L →ᴸ L') → (soLang L Bs →ᴸ soLang L' Bs)

Lift of a language morphism through the expansion by blocks: symbols of the base language are mapped by the morphism, relation variables of the blocks to themselves.

Equations

• DescriptiveComplexity.soLangLift [] x✝² x✝¹ x✝ = x✝
• DescriptiveComplexity.soLangLift (B :: Bs) x✝² x✝¹ x✝ = DescriptiveComplexity.soLangLift Bs (x✝².sum B.lang) (x✝¹.sum B.lang) (x✝.sumMap (FirstOrder.Language.LHom.id B.lang))

theorem DescriptiveComplexity.sorealize_soLangLift (Bs : List SOBlock) (L L' : FirstOrder.Language) (Φ : L →ᴸ L') (A : Type) (instL : L.Structure A) (instL' : L'.Structure A) : Φ.IsExpansionOn A → ∀ (φ : (soLang L Bs).Sentence) (pol : Bool), SORealize L' A Bs ((soLangLift Bs L L' Φ).onSentence φ) pol ↔ SORealize L A Bs φ pol

Alternating second-order satisfaction only depends on the base structure through the symbols the kernel mentions: it is invariant under transporting the kernel along a language morphism whose expansion the structure is.

Embedding the base language into a block expansion

def DescriptiveComplexity.soLangEmbed (Bs : List SOBlock) (L : FirstOrder.Language) : L →ᴸ soLang L Bs

The embedding of the base language into its expansion by blocks.

Equations

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

theorem DescriptiveComplexity.sorealize_inf_embed (Bs : List SOBlock) (L : FirstOrder.Language) (A : Type) (instL : L.Structure A) (χ : L.Sentence) (φ : (soLang L Bs).Sentence) (pol : Bool) : SORealize L A Bs ((soLangEmbed Bs L).onSentence χ ⊓ φ) pol ↔ A ⊨ χ ∧ SORealize L A Bs φ pol

A conjunct that is (the embedding of) a sentence of the base language can be pulled out of the second-order quantification.

theorem DescriptiveComplexity.sorealize_imp_embed (Bs : List SOBlock) (L : FirstOrder.Language) (A : Type) (instL : L.Structure A) (χ : L.Sentence) (φ : (soLang L Bs).Sentence) (pol : Bool) : SORealize L A Bs (FirstOrder.Language.BoundedFormula.imp ((soLangEmbed Bs L).onSentence χ) φ) pol ↔ A ⊨ χ → SORealize L A Bs φ pol

A premise that is (the embedding of) a sentence of the base language can be pulled out of the second-order quantification.

The trivial block, and padding

def DescriptiveComplexity.SOBlock.trivial : SOBlock

The trivial second-order quantifier block, with no relation variables. Quantifying over it (in either polarity) does not change satisfaction; it pads a quantifier prefix to a larger number of alternations.

Equations

• DescriptiveComplexity.SOBlock.trivial = { ι := Empty, ιFinite := ⋯, arity := Empty.elim }

def DescriptiveComplexity.soLangAppendOne (C : SOBlock) (L : FirstOrder.Language) (Bs : List SOBlock) : soLang L Bs →ᴸ soLang L (Bs ++ [C])

Extension of the block expansion under appending one more block at the end of the list.

Equations

• DescriptiveComplexity.soLangAppendOne C x✝ [] = FirstOrder.Language.LHom.sumInl
• DescriptiveComplexity.soLangAppendOne C x✝ (B :: Bs) = DescriptiveComplexity.soLangAppendOne C (x✝.sum B.lang) Bs

theorem DescriptiveComplexity.sorealize_append_trivial (Bs : List SOBlock) (L : FirstOrder.Language) (A : Type) (instL : L.Structure A) (φ : (soLang L Bs).Sentence) (pol : Bool) : SORealize L A (Bs ++ [SOBlock.trivial]) ((soLangAppendOne SOBlock.trivial L Bs).onSentence φ) pol ↔ SORealize L A Bs φ pol

Appending the trivial block does not change alternating second-order satisfaction.

Level inclusions at the definability level

theorem DescriptiveComplexity.SigmaSODefinable.succ {L : FirstOrder.Language} {k : ℕ} {P : DecisionProblem L} (h : SigmaSODefinable k P) : SigmaSODefinable (k + 1) P

Σₖ ⊆ Σₖ₊₁: pad by appending the trivial block.

theorem DescriptiveComplexity.PiSODefinable.succ {L : FirstOrder.Language} {k : ℕ} {P : DecisionProblem L} (h : PiSODefinable k P) : PiSODefinable (k + 1) P

Πₖ ⊆ Πₖ₊₁: pad by appending the trivial block.

theorem DescriptiveComplexity.SigmaSODefinable.piSucc {L : FirstOrder.Language} {k : ℕ} {P : DecisionProblem L} (h : SigmaSODefinable k P) : PiSODefinable (k + 1) P

Σₖ ⊆ Πₖ₊₁: pad by prepending the trivial block.

theorem DescriptiveComplexity.PiSODefinable.sigmaSucc {L : FirstOrder.Language} {k : ℕ} {P : DecisionProblem L} (h : PiSODefinable k P) : SigmaSODefinable (k + 1) P

Πₖ ⊆ Σₖ₊₁: pad by prepending the trivial block.