PH ⊆ PSPACE

The theorem: every level of the polynomial hierarchy is inside polynomial space (DescriptiveComplexity.PH_subset_PSPACE). A Σₖ sentence is not a walk, so this is not a syntactic inclusion; it is two closure properties of SO(TC) put together, alternated along the quantifier prefix:

• complement (DescriptiveComplexity.SOTCDefinable.compl, i.e. PSPACE = coPSPACE, proved in DescriptiveComplexity.PSpaceCompl), which turns a universal block into an existential one;
• prefixing an existential block (DescriptiveComplexity.SOTCDefinable.exBlock): a walk can carry a guessed block in its own state and never touch it again, so ∃R̄. (SO(TC) condition) is again an SO(TC) condition.

The second is the construction of this file. The state of DescriptiveComplexity.SOTCSpec.exBlock is an assignment of the merged block DescriptiveComplexity.SOBlock.cons; its transition sentence is the conjunction of DescriptiveComplexity.fixedS – the guessed component is unchanged, one universally quantified equivalence per relation variable of it – with the inner transition sentence read through DescriptiveComplexity.consTwoLHom; and its endpoints are the inner ones read through DescriptiveComplexity.consOneLHom. Because a step never moves the guessed component, a whole walk keeps it fixed (DescriptiveComplexity.exBlock_reach), so accepting is accepting the inner walk under some assignment of it (DescriptiveComplexity.exBlock_accepts_iff).

The prefix is then peeled one block at a time (DescriptiveComplexity.sotcDefinable_soProblem), the base case being that a first-order sentence is a walk with a trivial block and no step. Level 0 of the hierarchy is not second-order at all and goes through PTIME ⊆ NP ⊆ PSPACE.

Reading a spec over a block expansion through the merge

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

The renaming of a one-copy expansion: the symbols of the guessed block B land in the left component of the merged block.

Equations

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

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

The renaming of a two-copy expansion: the symbols of the guessed block land in the left component of the first copy of the merged block.

Equations

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

theorem DescriptiveComplexity.consOneLHom_isExpansionOn {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ₀ : B.Assignment A) (ρ₁ : M.Assignment A) : (consOneLHom L B M).IsExpansionOn A

theorem DescriptiveComplexity.consTwoLHom_isExpansionOn {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ₀ σ₀ : B.Assignment A) (ρ₁ σ₁ : M.Assignment A) : (consTwoLHom L B M).IsExpansionOn A

The guessed block does not change

@[reducible, inline]

abbrev DescriptiveComplexity.fstSym (L : FirstOrder.Language) (B M : SOBlock) (i : B.ι) : (((L.sum FirstOrder.Language.order).sum (B.cons M).lang).sum (B.cons M).lang).Relations (B.arity i)

The relation variable i of the guessed block, in the first copy of the merged block.

Equations

• DescriptiveComplexity.fstSym L B M i = Sum.inl (Sum.inr ⟨Sum.inl i, ⋯⟩)

@[reducible, inline]

abbrev DescriptiveComplexity.sndSym (L : FirstOrder.Language) (B M : SOBlock) (i : B.ι) : (((L.sum FirstOrder.Language.order).sum (B.cons M).lang).sum (B.cons M).lang).Relations (B.arity i)

The relation variable i of the guessed block, in the second copy.

Equations

• DescriptiveComplexity.sndSym L B M i = Sum.inr ⟨Sum.inl i, ⋯⟩

noncomputable def DescriptiveComplexity.fixedAtS (L : FirstOrder.Language) (B M : SOBlock) (i : B.ι) : (((L.sum FirstOrder.Language.order).sum (B.cons M).lang).sum (B.cons M).lang).Sentence

The relation variable i of the guessed block has the same value in the two copies of the merged block.

Equations

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

noncomputable def DescriptiveComplexity.fixedS (L : FirstOrder.Language) (B M : SOBlock) : (((L.sum FirstOrder.Language.order).sum (B.cons M).lang).sum (B.cons M).lang).Sentence

The whole guessed block is unchanged by a step.

Equations

• DescriptiveComplexity.fixedS L B M = DescriptiveComplexity.listInf (List.map (DescriptiveComplexity.fixedAtS L B M) Finset.univ.toList)

theorem DescriptiveComplexity.realize_fixedAtS {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ₀ σ₀ : B.Assignment A) (ρ₁ σ₁ : M.Assignment A) (i : B.ι) : A ⊨ fixedAtS L B M i ↔ ∀ (x : Fin (B.arity i) → A), ρ₀ i x ↔ σ₀ i x

theorem DescriptiveComplexity.realize_fixedS {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ₀ σ₀ : B.Assignment A) (ρ₁ σ₁ : M.Assignment A) : A ⊨ fixedS L B M ↔ ρ₀ = σ₀

Prefixing a specification with a guessed block

noncomputable def DescriptiveComplexity.SOTCSpec.exBlock {L : FirstOrder.Language} (B : SOBlock) (spec : SOTCSpec (L.sum B.lang)) : SOTCSpec L

The walk that guesses a block first: its state is an assignment of the merged block, its transition sentence says that the guessed part does not change and that the rest takes a step of spec, and its endpoints are those of spec.

Equations

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

theorem DescriptiveComplexity.exBlock_isSrc_iff {L : FirstOrder.Language} {B : SOBlock} {spec : SOTCSpec (L.sum B.lang)} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ₀ : B.Assignment A) (ρ₁ : spec.B.Assignment A) : (SOTCSpec.exBlock B spec).IsSrc (consAssign ρ₀ ρ₁) ↔ spec.IsSrc ρ₁

theorem DescriptiveComplexity.exBlock_isTgt_iff {L : FirstOrder.Language} {B : SOBlock} {spec : SOTCSpec (L.sum B.lang)} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ₀ : B.Assignment A) (ρ₁ : spec.B.Assignment A) : (SOTCSpec.exBlock B spec).IsTgt (consAssign ρ₀ ρ₁) ↔ spec.IsTgt ρ₁

theorem DescriptiveComplexity.exBlock_step_iff {L : FirstOrder.Language} {B : SOBlock} {spec : SOTCSpec (L.sum B.lang)} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ₀ σ₀ : B.Assignment A) (ρ₁ σ₁ : spec.B.Assignment A) : (SOTCSpec.exBlock B spec).Step (consAssign ρ₀ ρ₁) (consAssign σ₀ σ₁) ↔ ρ₀ = σ₀ ∧ spec.Step ρ₁ σ₁

theorem DescriptiveComplexity.exBlock_step_split {L : FirstOrder.Language} {B : SOBlock} {spec : SOTCSpec (L.sum B.lang)} {A : Type} [instL : L.Structure A] [LinearOrder A] (c d : (B.cons spec.B).Assignment A) (h : (SOTCSpec.exBlock B spec).Step c d) : ((fun (i : B.ι) => c (Sum.inl i)) = fun (i : B.ι) => d (Sum.inl i)) ∧ spec.Step (fun (j : spec.B.ι) => c (Sum.inr j)) fun (j : spec.B.ι) => d (Sum.inr j)

theorem DescriptiveComplexity.exBlock_reach {L : FirstOrder.Language} {B : SOBlock} {spec : SOTCSpec (L.sum B.lang)} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ σ : (B.cons spec.B).Assignment A) (h : (SOTCSpec.exBlock B spec).Reach ρ σ) : ((fun (i : B.ι) => ρ (Sum.inl i)) = fun (i : B.ι) => σ (Sum.inl i)) ∧ spec.Reach (fun (j : spec.B.ι) => ρ (Sum.inr j)) fun (j : spec.B.ι) => σ (Sum.inr j)

The guessed block is the same all along a walk, and the rest of the state walks in the inner specification.

theorem DescriptiveComplexity.exBlock_reach_of {L : FirstOrder.Language} {B : SOBlock} {spec : SOTCSpec (L.sum B.lang)} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ₀ : B.Assignment A) {ρ₁ σ₁ : spec.B.Assignment A} (h : spec.Reach ρ₁ σ₁) : (SOTCSpec.exBlock B spec).Reach (consAssign ρ₀ ρ₁) (consAssign ρ₀ σ₁)

theorem DescriptiveComplexity.exBlock_accepts_iff {L : FirstOrder.Language} {B : SOBlock} {spec : SOTCSpec (L.sum B.lang)} {A : Type} [instL : L.Structure A] [LinearOrder A] : (SOTCSpec.exBlock B spec).Accepts A ↔ ∃ (ρ₀ : B.Assignment A), spec.Accepts A

What the guessing walk accepts: exactly what the inner walk accepts, under some assignment of the guessed block.

theorem DescriptiveComplexity.SOTCDefinable.exBlock {L : FirstOrder.Language} {B : SOBlock} {Q : DecisionProblem (L.sum B.lang)} (hQ : SOTCDefinable Q) {P : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A], P.Holds A ↔ ∃ (ρ : B.Assignment A), Q.Holds A) : SOTCDefinable P

SO(TC) is closed under prefixing an existential second-order block: the walk carries the guessed block in its own state and never touches it again.

Down the quantifier prefix

def DescriptiveComplexity.soProblem (L : FirstOrder.Language) (Bs : List SOBlock) (φ : (soLang L Bs).Sentence) (pol : Bool) : DecisionProblem L

The decision problem defined by a second-order sentence with a given quantifier prefix: isomorphism-invariant by DescriptiveComplexity.sorealize_iso.

Equations

• DescriptiveComplexity.soProblem L Bs φ pol = { Holds := fun (A : Type) (inst : L.Structure A) => DescriptiveComplexity.SORealize L A Bs φ pol, iso_invariant := ⋯ }

theorem DescriptiveComplexity.sotcDefinable_soProblem_nil (L : FirstOrder.Language) (φ : (soLang L []).Sentence) (pol : Bool) : SOTCDefinable (soProblem L [] φ pol)

The base case: a first-order sentence is an SO(TC) condition – a walk with a trivial block and no step.

theorem DescriptiveComplexity.sotcDefinable_soProblem (Bs : List SOBlock) (L : FirstOrder.Language) (φ : (soLang L Bs).Sentence) (pol : Bool) : SOTCDefinable (soProblem L Bs φ pol)

Every second-order sentence defines an SO(TC) condition: peel the prefix one block at a time, guessing an existential block into the state of the walk and complementing at a universal one.

PH ⊆ PSPACE

theorem DescriptiveComplexity.SOTCDefinable.of_sigmaSODefinable_any {L : FirstOrder.Language} {k : ℕ} {P : DecisionProblem L} (h : SigmaSODefinable k P) : SOTCDefinable P

Every Σₖ-definable problem is SO(TC) definable.

theorem DescriptiveComplexity.sigmaP_subset_PSPACE (k : ℕ) : SigmaP k ⊆ PSPACE

Every level of the polynomial hierarchy is inside PSPACE.

theorem DescriptiveComplexity.PH_subset_PSPACE : PH ⊆ PSPACE

PH ⊆ PSPACE: the polynomial hierarchy is inside polynomial space.

theorem DescriptiveComplexity.piP_subset_PSPACE (k : ℕ) : PiP k ⊆ PSPACE

Πₖᵖ ⊆ PSPACE as well, since PSPACE is closed under complement.