PSPACE = coPSPACE

The theorem: polynomial space is closed under complement. In this library PSPACE is defined by SO(TC) (DescriptiveComplexity.PSPACE), and the complement of a walk is not a walk, so this is not the definitional duality that gives PiP k from SigmaP k. It is assembled from three pieces:

• every SO(TC) definable problem reduces to SUCCINCT-REACH (DescriptiveComplexity.succinctReach_hard_of_sotcDefinable, the Tseitin discharge) and from there to QSAT (DescriptiveComplexity.succinctReach_ordered_fo_reduction_qsat, Savitch's recursive doubling);
• complementing an ordered reduction is free – the same interpretation (DescriptiveComplexity.OrderedFOReduction.compl);
• the complement of QSAT is SO(TC) definable (DescriptiveComplexity.qsatCompl_sotcDefinable), because the walk that decides QSAT is deterministic and computes the value of the formula, so reading its answer the other way round decides the complement.

That third piece is where the content sits, and it is the logical shadow of the machine-theoretic reason PSPACE is closed under complement: a space-bounded computation can be made deterministic (Savitch), and a deterministic decider is complemented by flipping its answer. Savitch's recursive doubling is what DescriptiveComplexity.Problems.Qsat.Hardness spends to turn the nondeterministic walk of an arbitrary SO(TC) specification into the deterministic evaluation of a quantified Boolean formula.

SO(TC) is closed under complement

theorem DescriptiveComplexity.SOTCDefinable.compl {L : FirstOrder.Language} {P : DecisionProblem L} (h : SOTCDefinable P) : SOTCDefinable Pᶜ

SO(TC) is closed under complement: the complement of an SO(TC) definable problem is SO(TC) definable.

Reduce to QSAT – through SUCCINCT-REACH and Savitch's recursive doubling – and read the deterministic evaluation walk of QSAT backwards.

theorem DescriptiveComplexity.sotcDefinable_compl_iff {L : FirstOrder.Language} (P : DecisionProblem L) : SOTCDefinable Pᶜ ↔ SOTCDefinable P

Complementation is a bijection of the SO(TC) definable problems.

PSPACE = coPSPACE

theorem DescriptiveComplexity.PSPACE_eq_coPSPACE : PSPACE = coPSPACE

PSPACE = coPSPACE: polynomial space is closed under complement.

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

Membership in PSPACE is closed under complement.

theorem DescriptiveComplexity.QSAT_coPSPACE_complete : coPSPACE.Complete QSAT

QSAT is coPSPACE-complete, since PSPACE and coPSPACE coincide.