Peeling a quantifier into a block

The semantic core of the translation lemma. Two facts, both independent of any syntax.

A guarded block is a point. A second-order quantifier ranges over all assignments of DescriptiveComplexity.ExpExpansion.pointBlock; the quantifier being translated ranges over the points of the expanded universe, which are the assignments the point guard admits. The two match up (DescriptiveComplexity.ExpExpansion.exists_point_iff, DescriptiveComplexity.ExpExpansion.forall_point_iff): a guarded block is a point, existentially with the guard as a conjunct and universally with the guard as a hypothesis, which is the usual shape of relativized quantification.

A guard can be pulled through the rest of the prefix. The guard of round i sits at nesting depth i in the kernel, so peeling round i first has to move it out past the quantifiers that remain (DescriptiveComplexity.altBlockQuant_and_const, DescriptiveComplexity.altBlockQuant_const_imp). Both directions need the block assignments to be inhabited, which they are – DescriptiveComplexity.SOBlock.botAssign – and the existential case of the implication needs excluded middle, as relativized quantification always does.

Moving a constant through the prefix

theorem DescriptiveComplexity.altBlockQuant_and_const {B : SOBlock} {A : Type} (g : Prop) (k : ℕ) (P : (Fin k → B.Assignment A) → Prop) (pol : Bool) : altBlockQuant A B k (fun (ρs : Fin k → B.Assignment A) => g ∧ P ρs) pol ↔ g ∧ altBlockQuant A B k P pol

A conjunct not depending on the rounds moves out of the prefix.

theorem DescriptiveComplexity.altBlockQuant_const_imp {B : SOBlock} {A : Type} (g : Prop) (k : ℕ) (P : (Fin k → B.Assignment A) → Prop) (pol : Bool) : altBlockQuant A B k (fun (ρs : Fin k → B.Assignment A) => g → P ρs) pol ↔ g → altBlockQuant A B k P pol

A hypothesis not depending on the rounds moves out of the prefix. The existential case is where excluded middle enters: with the hypothesis false, any round will do, and there is one.

A guarded block is a point

def DescriptiveComplexity.ExpExpansion.pointAssign {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (p : X.Map A) : X.pointBlock.Assignment A

The block assignment carrying a point.

Equations

• DescriptiveComplexity.ExpExpansion.pointAssign p = DescriptiveComplexity.SOBlock.tagAssign (↑p).1 (↑p).2

@[simp]

theorem DescriptiveComplexity.ExpExpansion.roundAssign_apply {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (pts : Fin m → X.Map A) (i : Fin m) : roundAssign pts i = pointAssign (pts i)

def DescriptiveComplexity.ExpExpansion.IsPointAssign {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (σ : X.pointBlock.Assignment A) : Prop

The condition the point guard expresses, semantically.

Equations

• DescriptiveComplexity.ExpExpansion.IsPointAssign σ = ∃ (t : X.Tag) (ρ : X.B.Assignment A), σ = DescriptiveComplexity.SOBlock.tagAssign t ρ ∧ DescriptiveComplexity.ExpExpansion.DomHolds (t, ρ)

theorem DescriptiveComplexity.ExpExpansion.isPointAssign_pointAssign {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (p : X.Map A) : IsPointAssign (pointAssign p)

theorem DescriptiveComplexity.ExpExpansion.exists_point_iff {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (P : X.pointBlock.Assignment A → Prop) : (∃ (σ : X.pointBlock.Assignment A), IsPointAssign σ ∧ P σ) ↔ ∃ (p : X.Map A), P (pointAssign p)

A guarded block is a point, existentially.

theorem DescriptiveComplexity.ExpExpansion.forall_point_iff {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (P : X.pointBlock.Assignment A → Prop) : (∀ (σ : X.pointBlock.Assignment A), IsPointAssign σ → P σ) ↔ ∀ (p : X.Map A), P (pointAssign p)

A guarded block is a point, universally.

The peel steps

Peeling the outermost quantifier of the prefix: the guard of the leading round moves out past the rounds that remain (DescriptiveComplexity.altBlockQuant_and_const, DescriptiveComplexity.altBlockQuant_const_imp), and what is left of it turns the round into a point (exists_point_iff, forall_point_iff).

theorem DescriptiveComplexity.ExpExpansion.altBlockQuant_peel_ex {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {k : ℕ} (R : X.pointBlock.Assignment A → (Fin k → X.pointBlock.Assignment A) → Prop) : altBlockQuant A X.pointBlock (k + 1) (fun (ρs : Fin (k + 1) → X.pointBlock.Assignment A) => IsPointAssign (ρs 0) ∧ R (ρs 0) (Fin.tail ρs)) true ↔ ∃ (p : X.Map A), altBlockQuant A X.pointBlock k (R (pointAssign p)) false

Peeling an existential quantifier.

theorem DescriptiveComplexity.ExpExpansion.altBlockQuant_peel_all {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {k : ℕ} (R : X.pointBlock.Assignment A → (Fin k → X.pointBlock.Assignment A) → Prop) : altBlockQuant A X.pointBlock (k + 1) (fun (ρs : Fin (k + 1) → X.pointBlock.Assignment A) => IsPointAssign (ρs 0) → R (ρs 0) (Fin.tail ρs)) false ↔ ∀ (p : X.Map A), altBlockQuant A X.pointBlock k (R (pointAssign p)) true

Peeling a universal quantifier.