PSPACE, by second-order transitive closure

The class PSPACE: the problems definable in SO(TC), second-order logic with a transitive closure taken over assignments of a relation block (DescriptiveComplexity.SOTCDefinable), which captures polynomial space on ordered structures (Immerman 1999, ch. 10). This is the same move as defining PTIME by the Horn fragment, NL by the Krom fragment and NP by Σ₁-definability: the class is a definition, not an axiom, and it is a bona fide DescriptiveComplexity.ComplexityClass because SO(TC) definability is closed under (ordered) first-order reductions – the block and the three sentences all survive the pullback, see DescriptiveComplexity.SecondOrderTransitiveClosurePull.

Why the states are relations

An SO(TC) walk remembers an assignment of relations, i.e. n^a bits on a universe of size n, and may take exponentially many steps to reach its target. That is precisely a polynomially space-bounded computation: the configuration is the remembered assignment, and the (first-order) transition sentence is one step of the machine. Immerman's capture theorem is the statement that nothing is lost either way; here, as everywhere in this library, the logic is taken as the definition of the class and the capture theorem is a statement about machines, to be proved against a machine model rather than assumed (see DescriptiveComplexity.Machines).

What is not free here

• PSPACE = coPSPACE is not the definitional duality that gives PiP k from SigmaP k: the complement of an SO(TC) definable problem is not obviously SO(TC) definable. It is a genuine theorem, and it is proved – downstream, in DescriptiveComplexity.PSpaceCompl, once QSAT is available: every SO(TC) definable problem reduces to QSAT, complementing a reduction is free, and the walk that decides QSAT is deterministic, so reading its answer the other way round decides the complement.
• PH ⊆ PSPACE is not a syntactic inclusion either: a Σₖ sentence is not a walk. It too is proved downstream, in DescriptiveComplexity.PSpaceHierarchy, by alternating that complement with the other closure property of SO(TC) – a walk can guess a block into its own state and never touch it again – along the quantifier prefix. What is immediate here is the bottom of the tower, NP ⊆ PSPACE (DescriptiveComplexity.NP_subset_PSPACE): an existential block is a walk that guesses its state in one step and then stops, so Σ₁-definability is SO(TC) definability with an empty transition relation. Everything below NP follows by composition.

noncomputable def DescriptiveComplexity.PSPACE : ComplexityClass

The class PSPACE: the problems definable in SO(TC), second-order logic with a transitive closure over assignments of a relation block, which captures polynomial space on ordered structures (Immerman 1999).

Hardness is stated cofinally, exactly as for the other classes of this library (DescriptiveComplexity.CofinalHard); over a relational vocabulary it is the usual notion, DescriptiveComplexity.hard_PSPACE_iff.

Equations

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

theorem DescriptiveComplexity.mem_PSPACE_iff {L : FirstOrder.Language} (P : DecisionProblem L) : PSPACE.Mem P ↔ SOTCDefinable P

Membership in PSPACE is exactly SO(TC) definability, by definition.

theorem DescriptiveComplexity.hard_PSPACE_iff {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : PSPACE.Hard P ↔ ∀ {L'' : FirstOrder.Language} (Q : DecisionProblem L''), SOTCDefinable Q → Nonempty (RelOrderedFOReduction Q P)

Over a relational vocabulary, PSPACE-hardness is the usual notion: every SO(TC) definable problem reduces to P.

theorem DescriptiveComplexity.PSPACE_hard_of_sotcDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) (h : ∀ {L'' : FirstOrder.Language} (Q : DecisionProblem L''), SOTCDefinable Q → Nonempty (RelOrderedFOReduction Q P)) : PSPACE.Hard P

A problem is PSPACE-hard as soon as every SO(TC) definable problem reduces to it; the discharge shape shared by every PSPACE-hardness proof of the catalog.

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.coPSPACE : ComplexityClass

coPSPACE, the complement class of PSPACE. That it coincides with PSPACE (Savitch) is not proved here (see the module docstring).

Equations

• DescriptiveComplexity.coPSPACE = DescriptiveComplexity.PSPACE.compl

NP ⊆ PSPACE: an existential block is a one-step walk

A Σ₁ definition ∃ R̄. φ(R̄) is the SO(TC) specification whose states are the assignments of the block, whose transition relation is empty, and whose starting and accepting states are both the ones satisfying φ. Its walks are the one-state walks, so it accepts exactly when some assignment satisfies φ.

The only work is that an SO(TC) specification's sentences live over the ordered expansion of the vocabulary, so the kernel has to be moved along the language map that inserts the order symbol.

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

The language map inserting the order vocabulary underneath a block expansion: the kernel of a Σ₁ definition, which does not see the order, read as a sentence of the vocabulary an SO(TC) specification uses.

Equations

• DescriptiveComplexity.blockOrderLift L B = FirstOrder.Language.LHom.sumInl.sumMap (FirstOrder.Language.LHom.id B.lang)

theorem DescriptiveComplexity.blockOrderLift_isExpansionOn {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (B : SOBlock) (ρ : B.Assignment A) : (blockOrderLift L B).IsExpansionOn A

Inserting the order symbol does not change how anything is interpreted.

theorem DescriptiveComplexity.realize_blockOrderLift {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (B : SOBlock) (ρ : B.Assignment A) (φ : (L.sum B.lang).Sentence) : A ⊨ (blockOrderLift L B).onSentence φ ↔ A ⊨ φ

The lifted kernel realizes over the ordered expansion exactly as the original kernel realizes over the base expansion.

def DescriptiveComplexity.sigmaOneSpec (L : FirstOrder.Language) (B : SOBlock) (φ : (L.sum B.lang).Sentence) : SOTCSpec L

The specification of a Σ₁ definition: the states are the assignments of the block, there are no transitions, and the accepting states are the ones satisfying the kernel.

Equations

• DescriptiveComplexity.sigmaOneSpec L B φ = { B := B, step := ⊥, src := (DescriptiveComplexity.blockOrderLift L B).onSentence φ, tgt := (DescriptiveComplexity.blockOrderLift L B).onSentence φ }

theorem DescriptiveComplexity.sigmaOneSpec_accepts_iff {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (B : SOBlock) (φ : (L.sum B.lang).Sentence) : (sigmaOneSpec L B φ).Accepts A ↔ ∃ (ρ : B.Assignment A), A ⊨ φ

The one-step walk of a Σ₁ definition accepts exactly when the kernel is satisfiable in the block.

theorem DescriptiveComplexity.SOTCDefinable.of_sigmaSODefinable {L : FirstOrder.Language} {P : DecisionProblem L} (h : SigmaSODefinable 1 P) : SOTCDefinable P

Every Σ₁-definable problem is SO(TC) definable: guess the block in the state, take no step.

theorem DescriptiveComplexity.NP_subset_PSPACE : NP ⊆ PSPACE

NP ⊆ PSPACE: NP is Σ₁-definability (Fagin) and PSPACE is SO(TC) definability, and an existential block is a walk that guesses its state and stops.