QSAT is PSPACE-hard

The reduction of SUCCINCT-REACH to QSAT is correct (DescriptiveComplexity.qsatHolds_iff), so the interpretation of DescriptiveComplexity.Problems.Qsat.Interp is an ordered first-order reduction (DescriptiveComplexity.succinctReach_ordered_fo_reduction_qsat) and QSAT is PSPACE-complete (DescriptiveComplexity.QSAT_PSPACE_complete).

Peeling the first block – the two endpoints of the walk – opens the position of the first level, which DescriptiveComplexity.game_level says computes reachability in at most 2 ^ m moves for m the number of state variables; and that is reachability, by DescriptiveComplexity.succinctReachable_iff_savPow. An instance with no state variable has no level at all: the first block and every level block are empty, so the initial position is the position of the last block, and DescriptiveComplexity.game_aux answers directly.

def DescriptiveComplexity.endVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (S T : A → Prop) : QM A → Prop

The assignment of the first block made of the two endpoints of the walk.

Equations

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

theorem DescriptiveComplexity.stS_over_endVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ : QM A → Prop) (S T : A → Prop) {a : A} (ha : IsSV a) : stS (qOver (QBlk (tEnds A)) τ (endVal S T)) a ↔ S a

theorem DescriptiveComplexity.stT_over_endVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ : QM A → Prop) (S T : A → Prop) {a : A} (ha : IsSV a) : stT (qOver (QBlk (tEnds A)) τ (endVal S T)) a ↔ T a

theorem DescriptiveComplexity.qPlayed_tAux_of_isEmpty {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (h : ∀ (x : A), ¬IsSV x) : QPlayed (tAux A) = fun (x : QM A) => False

With no state variable, the auxiliary block is the first one: every other variable would need a state variable for one of its coordinates.

theorem DescriptiveComplexity.stCls_subsingleton {A : Type} [FirstOrder.Language.transSys.Structure A] (h : ∀ (x : A), ¬IsSV x) (S S' : A → Prop) : stCls S = stCls S'

With no state variable, all states have the same class.

theorem DescriptiveComplexity.qsatHolds_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : QsatHolds (QM A) ↔ SuccinctReachable A

Correctness of the Savitch reduction.

noncomputable def DescriptiveComplexity.succinctReach_ordered_fo_reduction_qsat : OrderedFOReduction SUCCINCTREACH QSAT

The Savitch reduction, as an ordered first-order reduction.

Equations

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

theorem DescriptiveComplexity.qsat_PSPACE_hard : PSPACE.Hard QSAT

QSAT is PSPACE-hard, by Savitch's recursive doubling from SUCCINCT-REACH.

theorem DescriptiveComplexity.QSAT_PSPACE_complete : PSPACE.Complete QSAT

QSAT is PSPACE-complete (Stockmeyer–Meyer 1973).