The complement of QSAT is in PSPACE

The walk of DescriptiveComplexity.Problems.Qsat.Membership does not search for an accepting computation: it is deterministic, and its single run computes the value of the quantified formula. That is what makes the complement of QSAT as cheap as QSAT itself – the walk is the same, only the accepting condition changes.

DescriptiveComplexity.qsSpecCo therefore reuses DescriptiveComplexity.qsSpec's transition sentence verbatim and accepts the returning state at the empty branch carrying the value false. One point needs care: a malformed instance is a no-instance of QSAT, hence a yes-instance of its complement, and the run of the walk says nothing about it – on a malformed prefix neither the next nor the last variable of a position need exist. So the source sentence has a second disjunct, which starts a malformed instance directly in an accepting state.

This is the whole content of PSPACE = coPSPACE (DescriptiveComplexity.PSpaceCompl): every SO(TC) definable problem reduces to QSAT, and complementing a reduction is free.

The complementary specification

noncomputable def DescriptiveComplexity.qsFalseS : qsLang₁.Sentence

The accepting states of the complementary walk: back at the empty branch, returning the value false.

Equations

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

noncomputable def DescriptiveComplexity.qsSpecCo : SOTCSpec FirstOrder.Language.qsat

The complementary specification: the depth-first evaluation of the game tree again – the same transition sentence – accepting when the value computed is false, or when the instance is malformed, in which case the walk starts where it would have ended.

Equations

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

Reading the specification back

theorem DescriptiveComplexity.qsRealize_sup₁ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ : qsBlock.Assignment A) (φ ψ : qsLang₁.Sentence) : A ⊨ φ ⊔ ψ ↔ A ⊨ φ ∨ A ⊨ ψ

theorem DescriptiveComplexity.qsSpecCo_step_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ σ : qsBlock.Assignment A) : qsSpecCo.Step ρ σ ↔ qsSpec.Step ρ σ

The complementary walk is the same walk.

theorem DescriptiveComplexity.qsSpecCo_reach_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ σ : qsBlock.Assignment A) : qsSpecCo.Reach ρ σ ↔ qsSpec.Reach ρ σ

theorem DescriptiveComplexity.realize_qsFalseS {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ : qsBlock.Assignment A) : A ⊨ qsFalseS ↔ (∀ (y : A), ¬qsSet ρ y) ∧ qsUp ρ ∧ ¬qsRes ρ

theorem DescriptiveComplexity.qsSpecCo_isTgt_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ : qsBlock.Assignment A) : qsSpecCo.IsTgt ρ ↔ (∀ (y : A), ¬qsSet ρ y) ∧ qsUp ρ ∧ ¬qsRes ρ

The accepting states: back at the initial position, returning false.

theorem DescriptiveComplexity.qsSpecCo_isSrc_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ : qsBlock.Assignment A) : qsSpecCo.IsSrc ρ ↔ QsatWf A ∧ (∀ (y : A), ¬qsSet ρ y) ∧ ¬qsUp ρ ∨ ¬QsatWf A ∧ (∀ (y : A), ¬qsSet ρ y) ∧ qsUp ρ ∧ ¬qsRes ρ

The starting states: the initial position of a well-formed instance, or – on a malformed one – an accepting state outright.

Correctness

theorem DescriptiveComplexity.not_qsatHolds_iff_accepts {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] : ¬QsatHolds A ↔ qsSpecCo.Accepts A

The complementary specification is correct: its walk accepts an instance exactly when the instance is not a yes-instance of QSAT.

theorem DescriptiveComplexity.qsatCompl_sotcDefinable : SOTCDefinable QSATᶜ

The complement of QSAT is SO(TC) definable: the walk that decides QSAT is deterministic, so reading its answer the other way round decides the complement.

theorem DescriptiveComplexity.qsatCompl_mem_PSPACE : PSPACE.Mem QSATᶜ

The complement of QSAT is in PSPACE, i.e. QSAT ∈ coPSPACE.