The exponential classes: complements and inclusions

Everything in this file is inherited rather than proved. The two facts it rests on are polynomial-level and each cost a large development:

• DescriptiveComplexity.piP_zero_eq – polynomial time is closed under complement, Grädel's capture theorem at level 0, through FO(LFP);
• DescriptiveComplexity.PSPACE_eq_coPSPACE – polynomial space is closed under complement, Savitch, through the deterministic QSAT walk.

DescriptiveComplexity.ComplexityClass.exp_compl carries both one exponential up, and DescriptiveComplexity.ComplexityClass.exp_mono carries every polynomial-level inclusion. Nothing of the two developments above is spent twice; that is the first payoff of making exp an operator on an abstract class.

Read on the definitions, the complement equalities say that SO(LFP) and SO(PFP) are closed under complement, which is the form a reader of the logic will look for; they are stated that way too.

The one construction with content is DescriptiveComplexity.PSPACE_subset_PTIME_exp – an SO(TC) walk is REACH on the expansion whose points are its states – which lives in DescriptiveComplexity.Exponential.Reach and starts the whole tower.

No claim is made for NEXPTIME, which is not expected to be closed under complement.

The two polynomial-level complement facts, in the form used here

theorem DescriptiveComplexity.PTIME_compl_eq : PTIME.compl = PTIME

Polynomial time is closed under complement (DescriptiveComplexity.piP_zero_eq, restated as an equality of classes).

theorem DescriptiveComplexity.PSPACE_compl_eq : PSPACE.compl = PSPACE

Polynomial space is closed under complement (DescriptiveComplexity.PSPACE_eq_coPSPACE, restated the same way).

The complement equalities

theorem DescriptiveComplexity.EXPTIME_eq_coEXPTIME : EXPTIME = coEXPTIME

EXPTIME = coEXPTIME: inherited from PTIME.compl = PTIME through DescriptiveComplexity.ComplexityClass.exp_compl.

theorem DescriptiveComplexity.EXPSPACE_eq_coEXPSPACE : EXPSPACE = coEXPSPACE

EXPSPACE = coEXPSPACE: inherited from Savitch through the same operator.

theorem DescriptiveComplexity.mem_EXPTIME_compl_iff {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : EXPTIME.Mem Pᶜ ↔ EXPTIME.Mem P

A problem is in EXPTIME exactly when its complement is.

theorem DescriptiveComplexity.mem_EXPSPACE_compl_iff {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : EXPSPACE.Mem Pᶜ ↔ EXPSPACE.Mem P

A problem is in EXPSPACE exactly when its complement is.

theorem DescriptiveComplexity.SOLFPDefinable.compl {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : SOLFPDefinable P) : SOLFPDefinable Pᶜ

SO(≤, LFP) is closed under complement – the second-order shadow of DescriptiveComplexity.piP_zero_eq, and the reading of DescriptiveComplexity.EXPTIME_eq_coEXPTIME on the definition.

theorem DescriptiveComplexity.SOPFPDefinable.compl {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : SOPFPDefinable P) : SOPFPDefinable Pᶜ

SO(≤, PFP) is closed under complement – the second-order shadow of Savitch.

The inclusions

Every line but the first is DescriptiveComplexity.ComplexityClass.exp_mono on a polynomial-level inclusion, read through the bridge theorems of DescriptiveComplexity.Exponential.Classes.

theorem DescriptiveComplexity.PSPACE_subset_EXPTIME : PSPACE ⊆ EXPTIME

PSPACE ⊆ EXPTIME: an SO(TC) walk is a reachability question on the expansion whose points are its states, and reachability is in polynomial time. On the definitions this is SO(TC) ⊆ SO(LFP).

theorem DescriptiveComplexity.PSPACE_subset_coEXPTIME : PSPACE ⊆ coEXPTIME

PSPACE ⊆ coEXPTIME, by the complement equality.

theorem DescriptiveComplexity.PTIME_subset_PSPACE : PTIME ⊆ PSPACE

PTIME ⊆ PSPACE, routed through NP – the polynomial-level inclusion the exponential ones are lifted from.

theorem DescriptiveComplexity.EXPTIME_subset_EXPSPACE : EXPTIME ⊆ EXPSPACE

EXPTIME ⊆ EXPSPACE, i.e., SO(LFP) ⊆ SO(PFP) – the second-order shadow of PTIME ⊆ PSPACE.

theorem DescriptiveComplexity.coEXPTIME_subset_EXPSPACE : coEXPTIME ⊆ EXPSPACE

coEXPTIME ⊆ EXPSPACE, by the complement equality.

theorem DescriptiveComplexity.EXPTIME_subset_NEXPTIME : EXPTIME ⊆ NEXPTIME

EXPTIME ⊆ NEXPTIME, the second-order shadow of PTIME ⊆ NP.

theorem DescriptiveComplexity.NEXPTIME_subset_EXPSPACE : NEXPTIME ⊆ EXPSPACE

NEXPTIME ⊆ EXPSPACE, the second-order shadow of NP ⊆ PSPACE.

theorem DescriptiveComplexity.NL_exp_subset_EXPTIME : NL.exp ⊆ EXPTIME

NL.exp ⊆ EXPTIME, the second-order shadow of NL ⊆ PTIME. Together with DescriptiveComplexity.PSPACE_subset_NL_exp it sandwiches NL.exp between PSPACE and EXPTIME.

The polynomial classes inside the exponential ones

All of these route through PSPACE ⊆ EXPTIME, which is the only inclusion of this development with content.

theorem DescriptiveComplexity.PTIME_subset_EXPTIME : PTIME ⊆ EXPTIME

theorem DescriptiveComplexity.NP_subset_NEXPTIME : NP ⊆ NEXPTIME

theorem DescriptiveComplexity.PSPACE_subset_EXPSPACE : PSPACE ⊆ EXPSPACE

theorem DescriptiveComplexity.PH_subset_EXPTIME : PH ⊆ EXPTIME

The whole polynomial hierarchy sits inside EXPTIME, through DescriptiveComplexity.PH_subset_PSPACE.