Pulling second-order definability back through an interpretation

If P ≤ᶠᵒ Q and Q is Σₖ- (resp. Πₖ-) definable, then so is P (DescriptiveComplexity.SigmaSODefinable.of_foReduction, DescriptiveComplexity.PiSODefinable.of_foReduction): the levels of the polynomial hierarchy, defined by second-order alternation, are closed under first-order reductions.

The proof pulls the defining second-order sentence back through the interpretation I underlying the reduction, block by block:

• a second-order quantifier over an n-ary relation on the interpreted universe Tag × A^d becomes a family of second-order quantifiers over (n·d)-ary relations on A, one per n-tuple of tags (DescriptiveComplexity.SOBlock.pull; assignments transfer bijectively via DescriptiveComplexity.SOBlock.pullAssign / DescriptiveComplexity.SOBlock.mergeAssign);
• the interpretation extends to the languages expanded by a block (DescriptiveComplexity.FOInterpretation.extendSO): relation variables of the block are interpreted by the corresponding pulled relation variables, reading the tag tuple off statically; interpreting-then-expanding agrees with expanding-then-interpreting (DescriptiveComplexity.FOInterpretation.extendSOEquiv);
• the first-order kernel is pulled back by DescriptiveComplexity.FOInterpretation.pull from DescriptiveComplexity.Composition, packaged at the sentence level as DescriptiveComplexity.FOInterpretation.pullSentence.

DescriptiveComplexity.sorealize_pullSO puts these together: alternating second-order satisfaction in the interpreted structure coincides with alternating second-order satisfaction of the pulled sentence (over the pulled blocks) in the base structure.

Pulling back a sentence

noncomputable def DescriptiveComplexity.FOInterpretation.pullSentence {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} [L₂.IsRelational] [Finite Tag] (I : FOInterpretation L₁ L₂ Tag d) (φ : L₂.Sentence) : L₁.Sentence

The pullback of an L₂-sentence through the interpretation I: an L₁-sentence that holds in A exactly when the original sentence holds in I.Map A (see FOInterpretation.realize_pullSentence).

Equations

• I.pullSentence φ = FirstOrder.Language.Formula.relabel (fun (p : (Empty ⊕ Fin 0) × Fin d) => isEmptyElim p.1) (I.pull φ fun (a : Empty ⊕ Fin 0) => isEmptyElim a)

theorem DescriptiveComplexity.FOInterpretation.realize_pullSentence {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} [L₂.IsRelational] [Finite Tag] (I : FOInterpretation L₁ L₂ Tag d) (φ : L₂.Sentence) (A : Type) [L₁.Structure A] : A ⊨ I.pullSentence φ ↔ I.Map A ⊨ φ

Pulling back a block

def DescriptiveComplexity.SOBlock.pull (Tag : Type) [Finite Tag] (d : ℕ) (B : SOBlock) : SOBlock

The pullback of a second-order quantifier block through a tagged d-dimensional interpretation: an n-ary relation variable on the interpreted universe Tag × A^d becomes one (n·d)-ary relation variable on A per n-tuple of tags.

Equations

• DescriptiveComplexity.SOBlock.pull Tag d B = { ι := (i : B.ι) × (Fin (B.arity i) → Tag), ιFinite := ⋯, arity := fun (p : (i : B.ι) × (Fin (B.arity i) → Tag)) => B.arity p.fst * d }

def DescriptiveComplexity.SOBlock.pullAssign {Tag : Type} [Finite Tag] {d : ℕ} {A : Type} (B : SOBlock) (ρ : B.Assignment (Tag × (Fin d → A))) : (pull Tag d B).Assignment A

Transfer of an assignment on the interpreted universe to an assignment of the pulled block on the base universe.

Equations

• B.pullAssign ρ p x = ρ p.fst fun (k : Fin (B.arity p.fst)) => (p.snd k, fun (j : Fin d) => x (finProdFinEquiv (k, j)))

def DescriptiveComplexity.SOBlock.mergeAssign {Tag : Type} [Finite Tag] {d : ℕ} {A : Type} (B : SOBlock) (σ : (pull Tag d B).Assignment A) : B.Assignment (Tag × (Fin d → A))

Transfer of an assignment of the pulled block on the base universe to an assignment on the interpreted universe.

Equations

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

theorem DescriptiveComplexity.SOBlock.pullAssign_mergeAssign {Tag : Type} [Finite Tag] {d : ℕ} {A : Type} (B : SOBlock) (σ : (pull Tag d B).Assignment A) : B.pullAssign (B.mergeAssign σ) = σ

The two assignment transfers are inverse (in the direction needed to biject the second-order quantifiers).

Extending an interpretation along a block

def DescriptiveComplexity.SOBlock.pullSym (B : SOBlock) (Tag : Type) [Finite Tag] (d : ℕ) {n : ℕ} (r : B.lang.Relations n) (τ : Fin n → Tag) : (pull Tag d B).lang.Relations (B.arity ↑r * d)

The relation symbol of the pulled block corresponding to a relation variable of the original block and a tuple of tags.

Equations

• B.pullSym Tag d r τ = ⟨⟨↑r, fun (k : Fin (B.arity ↑r)) => τ (Fin.cast ⋯ k)⟩, ⋯⟩

def DescriptiveComplexity.FOInterpretation.extendSO {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} [Finite Tag] (I : FOInterpretation L₁ L₂ Tag d) (B : SOBlock) : FOInterpretation (L₁.sum (SOBlock.pull Tag d B).lang) (L₂.sum B.lang) Tag d

Extension of an interpretation along a second-order quantifier block: an interpretation of the target language expanded by the block in the source language expanded by the pulled block. Symbols of the target language keep their defining formulas; a relation variable of the block is interpreted by the pulled relation variable selected by the (static) tag tuple, its argument positions decoded by finProdFinEquiv.

Equations

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

def DescriptiveComplexity.FOInterpretation.extendSOEquiv {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} [L₂.IsRelational] [Finite Tag] (I : FOInterpretation L₁ L₂ Tag d) (B : SOBlock) (A : Type) [instA : L₁.Structure A] (ρ : B.Assignment (I.Map A)) : (L₂.sum B.lang).Equiv ((I.extendSO B).Map A) (I.Map A)

Interpreting and then expanding by a block agrees with expanding by the pulled block and then interpreting through the extended interpretation: the identity map is an isomorphism over the expanded target language, when the block is interpreted by an assignment on the interpreted universe on one side and by its pulled transfer on the other.

Equations

• I.extendSOEquiv B A ρ = { toEquiv := Equiv.refl ((I.extendSO B).Map A), map_fun' := ⋯, map_rel' := ⋯ }

Pulling back an alternating second-order sentence

def DescriptiveComplexity.pullBlocks (Tag : Type) [Finite Tag] (d : ℕ) (Bs : List SOBlock) : List SOBlock

The blockwise pullback of a list of blocks.

Equations

• DescriptiveComplexity.pullBlocks Tag d Bs = List.map (fun (B : DescriptiveComplexity.SOBlock) => DescriptiveComplexity.SOBlock.pull Tag d B) Bs

noncomputable def DescriptiveComplexity.pullSO {Tag : Type} {d : ℕ} [Finite Tag] (Bs : List SOBlock) (L₁ L₂ : FirstOrder.Language) [L₂.IsRelational] (_I : FOInterpretation L₁ L₂ Tag d) : (soLang L₂ Bs).Sentence → (soLang L₁ (pullBlocks Tag d Bs)).Sentence

The pullback of a sentence over the block expansion of the target language: pull each block, then pull the first-order kernel through the (iteratively extended) interpretation.

Equations

• DescriptiveComplexity.pullSO [] x✝⁴ x✝³ x✝¹ x✝ = x✝¹.pullSentence x✝
• DescriptiveComplexity.pullSO (B :: Bs) x✝⁴ x✝³ x✝¹ x✝ = DescriptiveComplexity.pullSO Bs (x✝⁴.sum (DescriptiveComplexity.SOBlock.pull Tag d B).lang) (x✝³.sum B.lang) (x✝¹.extendSO B) x✝

theorem DescriptiveComplexity.sorealize_pullSO {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} [Finite Tag] [instRel : L₂.IsRelational] (I : FOInterpretation L₁ L₂ Tag d) (A : Type) [L₁.Structure A] (Bs : List SOBlock) (φ : (soLang L₂ Bs).Sentence) (pol : Bool) : SORealize L₂ (I.Map A) Bs φ pol ↔ SORealize L₁ A (pullBlocks Tag d Bs) (pullSO Bs L₁ L₂ I φ) pol

Pulling second-order satisfaction back through an interpretation: alternating second-order satisfaction in the interpreted structure coincides with satisfaction of the pulled sentence, over the pulled blocks, in the base structure.

Closure of the definability levels under FO reductions

theorem DescriptiveComplexity.SigmaSODefinable.of_foReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : FOReduction P Q) (h : SigmaSODefinable k Q) : SigmaSODefinable k P

Σₖ-definability is closed under first-order reductions.

theorem DescriptiveComplexity.PiSODefinable.of_foReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : FOReduction P Q) (h : PiSODefinable k Q) : PiSODefinable k P

Πₖ-definability is closed under first-order reductions.

Pulling back atoms, guards and tag assignments

The clausal fragments (SO-Horn, SO-Krom) pull a clause list back through an interpretation rather than a formula: each clause becomes one clause per static assignment of tags to its universally quantified variables, its guard becoming an ordinary formula pullback and its atoms becoming atoms of the pulled relation variables. The pieces that do not depend on the shape of a clause are collected here, and are shared by DescriptiveComplexity.SecondOrderHornPull and DescriptiveComplexity.SecondOrderKromPull.

def DescriptiveComplexity.SOAtom.pull {Tag : Type} [Finite Tag] {B : SOBlock} {k : ℕ} (a : SOAtom B k) (d : ℕ) (t : Fin k → Tag) : SOAtom (SOBlock.pull Tag d B) (k * d)

The pullback of a second-order atom at a static assignment of tags to the universally quantified variables: the atom of the pulled relation variable selected by the tags, its arguments the d coordinates of each original argument.

Equations

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

def DescriptiveComplexity.tagVal {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d k : ℕ} (I : FOInterpretation L₁ L₂ Tag d) {A : Type} (t : Fin k → Tag) (w : Fin (k * d) → A) : Fin k → I.Map A

The interpreted valuation determined by a tag assignment and a valuation of the coordinates.

Equations

• DescriptiveComplexity.tagVal I t w p = (t p, fun (j : Fin d) => w (finProdFinEquiv (p, j)))

theorem DescriptiveComplexity.SOAtom.pull_holds {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} {A : Type} (I : FOInterpretation L₁ L₂ Tag d) (a : SOAtom B k) (t : Fin k → Tag) (ρ : B.Assignment (I.Map A)) (w : Fin (k * d) → A) : (a.pull d t).Holds (B.pullAssign ρ) w ↔ a.Holds ρ (tagVal I t w)

theorem DescriptiveComplexity.tagVal_split {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d k : ℕ} {A : Type} (I : FOInterpretation L₁ L₂ Tag d) (v : Fin k → I.Map A) : (tagVal I (fun (p : Fin k) => (v p).1) fun (m : Fin (k * d)) => (v (finProdFinEquiv.symm m).1).2 (finProdFinEquiv.symm m).2) = v

Splitting an interpreted valuation into its tags and its coordinates.

noncomputable def DescriptiveComplexity.guardPull {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d k : ℕ} [L₂.IsRelational] (I : FOInterpretation L₁ L₂ Tag d) (φ : L₂.Formula (Fin k)) (t : Fin k → Tag) : L₁.Formula (Fin (k * d))

The pullback of a guard: the ordinary formula pullback at the tag assignment t, its variables re-indexed as coordinates.

Equations

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

theorem DescriptiveComplexity.realize_guardPull {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d k : ℕ} [L₂.IsRelational] {A : Type} [L₁.Structure A] (I : FOInterpretation L₁ L₂ Tag d) (φ : L₂.Formula (Fin k)) (t : Fin k → Tag) (w : Fin (k * d) → A) : (guardPull I φ t).Realize w ↔ φ.Realize (tagVal I t w)

noncomputable def DescriptiveComplexity.allTagAssign (Tag : Type) [Finite Tag] (k : ℕ) : List (Fin k → Tag)

All assignments of tags to the k universally quantified variables, as a list: the pullback of a clause is instantiated at each of them.

Equations

• DescriptiveComplexity.allTagAssign Tag k = Finset.univ.toList

theorem DescriptiveComplexity.mem_allTagAssign {Tag : Type} [Finite Tag] {k : ℕ} (t : Fin k → Tag) : t ∈ allTagAssign Tag k