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.

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)

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_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_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} [L.IsRelational] {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) [L.IsRelational] (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 (Bs : List SOBlock) (L : FirstOrder.Language) [L.IsRelational] (φ : (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.sigmaP_subset_PSPACE (k : ℕ) : SigmaP k ⊆ PSPACE

Every level of the polynomial hierarchy is inside PSPACE. Registered in the Lax archive as Lax134656.HierarchyInPSPACE.sigmaP_subset_PSPACE.

theorem DescriptiveComplexity.PH_subset_PSPACE : PH ⊆ PSPACE

PH ⊆ PSPACE: the polynomial hierarchy is inside polynomial space. Registered in the Lax archive as Lax134656.HierarchyInPSPACE.PH_subset_PSPACE.

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

Πₖᵖ ⊆ PSPACE as well, since PSPACE is closed under complement. Registered in the Lax archive as Lax134656.HierarchyInPSPACE.piP_subset_PSPACE.