Second-order definability pulls back through a relativized interpretation

DescriptiveComplexity.SecondOrderPull pulls an alternating second-order sentence back through an interpretation whose universe is all tagged tuples. This file does the same for an interpretation with a definable domain (DescriptiveComplexity.RelFOInterpretation), and concludes that the levels of the polynomial hierarchy are closed under relativized ordered reductions (DescriptiveComplexity.SigmaSODefinable.of_relOrderedReduction, DescriptiveComplexity.PiSODefinable.of_relOrderedReduction) – the membership half of the closure whose hardness half DescriptiveComplexity.Relativized supplies.

Why the transfer of assignments is a retraction, not a bijection

Over the whole universe, assignments of a block on the interpreted structure and assignments of the pulled block on the base structure correspond bijectively (DescriptiveComplexity.SOBlock.pullAssign, DescriptiveComplexity.SOBlock.mergeAssign). Over a definable domain they do not: a pulled relation may hold of tuples that are not points of the target at all, and no condition on the target's assignment says anything about them.

What survives is a retraction: reading a guessed pulled assignment back on the domain (DescriptiveComplexity.SOBlock.readAssignRel) undoes the transfer of a target assignment (DescriptiveComplexity.SOBlock.pullAssignRel), i.e., readAssignRel ∘ pullAssignRel = id (DescriptiveComplexity.SOBlock.readAssignRel_pullAssignRel). That is enough for a quantifier of either polarity: an existential guess is transported forward and read back, a universal one is instantiated at the read-back assignment. The off-domain junk a guess may carry is never looked at, since every atom the kernel evaluates sits at points of the domain.

Reading a pulled assignment back on the definable domain

def DescriptiveComplexity.SOBlock.readAssignRel {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} {A : Type} [L₁.Structure A] (B : SOBlock) (I : RelFOInterpretation L₁ L₂ Tag dm) (σ : (pull Tag dm B).Assignment A) : B.Assignment (I.MapRel A)

Reading an assignment of the pulled block back as an assignment of the original block on the definable domain: a tuple of domain points is packed into its tags and its coordinates. Off-domain tuples are simply not looked at.

Equations

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

theorem DescriptiveComplexity.SOBlock.readAssignRel_iff {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} {A : Type} [L₁.Structure A] (B : SOBlock) (I : RelFOInterpretation L₁ L₂ Tag dm) (σ : (pull Tag dm B).Assignment A) {i : B.ι} (y : Fin (B.arity i) → I.MapRel A) : B.readAssignRel I σ i y ↔ σ ⟨i, fun (k : Fin (B.arity i)) => (↑(y k)).1⟩ fun (m : Fin ((pull Tag dm B).arity ⟨i, fun (k : Fin (B.arity i)) => (↑(y k)).1⟩)) => (↑(y (finProdFinEquiv.symm m).1)).2 (finProdFinEquiv.symm m).2

The read-back of a pulled assignment at a tuple whose components are known.

theorem DescriptiveComplexity.SOBlock.readAssignRel_pullAssignRel {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} {A : Type} [L₁.Structure A] (B : SOBlock) (I : RelFOInterpretation L₁ L₂ Tag dm) (ρ : B.Assignment (I.MapRel A)) : B.readAssignRel I (B.pullAssignRel I ρ) = ρ

The transfer of assignments is a retraction: reading a transferred assignment back on the domain returns it unchanged. (The other composite is not the identity – a guessed pulled assignment may hold of tuples that are not points of the domain.)

The extended interpretation, at an arbitrary pulled assignment

noncomputable def DescriptiveComplexity.RelFOInterpretation.extendSORelEquivAny {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} [L₂.IsRelational] (I : RelFOInterpretation L₁ L₂ Tag dm) (B : SOBlock) (A : Type) [L₁.Structure A] (σ : (SOBlock.pull Tag dm B).Assignment A) : (L₂.sum B.lang).Equiv ((I.extendSORel B).MapRel A) (I.MapRel A)

Interpreting through the extension of a relativized interpretation along a block, at an arbitrary assignment of the pulled block: the block is read on the domain through DescriptiveComplexity.SOBlock.readAssignRel. This is DescriptiveComplexity.RelFOInterpretation.extendSORelEquiv with the assumption that the assignment is transferred from the target dropped – which is what a guessed assignment cannot be assumed to be.

Equations

• I.extendSORelEquivAny B A σ = { toEquiv := DescriptiveComplexity.extendSORelPointEquiv I B A σ, map_fun' := ⋯, map_rel' := ⋯ }

Pulling back an alternating second-order sentence

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

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

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.pullRelSO [] x✝⁴ x✝³ x✝¹ x✝ = x✝¹.pullRelSentence x✝

theorem DescriptiveComplexity.sorealize_pullRelSO {L₁ L₂ : FirstOrder.Language} {Tag : Type} {dm : ℕ} [Finite Tag] [instRel : L₂.IsRelational] (I : RelFOInterpretation L₁ L₂ Tag dm) (A : Type) [L₁.Structure A] (Bs : List SOBlock) (φ : (soLang L₂ Bs).Sentence) (pol : Bool) : SORealize L₂ (I.MapRel A) Bs φ pol ↔ SORealize L₁ A (pullBlocks Tag dm Bs) (pullRelSO Bs L₁ L₂ I φ) pol

Pulling second-order satisfaction back through a relativized interpretation: alternating second-order satisfaction in the interpreted structure – whose universe is the definable domain – coincides with satisfaction of the pulled sentence, over the pulled blocks, in the base structure.

Closure of the hierarchy under relativized ordered reductions

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

Σₖ₊₁-definability is closed under relativized ordered reductions. The blocks pull back with the retraction of assignments above, and the order of the source is re-quantified inside the first block (DescriptiveComplexity.sigmaSODefinable_of_orderPull), exactly as for non-relativized ordered reductions.

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

Πₖ₊₁-definability is closed under relativized ordered reductions.