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). Registered in the Lax archive as Lax535992.PTIMEEqCoPTIME.PTIME_eq_coPTIME.

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. Registered in the Lax archive as Lax480241.ExponentialComplements.mem_EXPTIME_compl_iff.

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. Registered in the Lax archive as Lax480241.ExponentialComplements.mem_EXPSPACE_compl_iff.

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). Registered in the Lax archive as Lax480241.ExponentialInclusions.PSPACE_subset_EXPTIME.

theorem DescriptiveComplexity.PTIME_subset_PSPACE : PTIME ⊆ PSPACE

PTIME ⊆ PSPACE, routed through NP – the polynomial-level inclusion the exponential ones are lifted from. Registered in the Lax archive as Lax134656.HierarchyInPSPACE.PTIME_subset_PSPACE.

theorem DescriptiveComplexity.EXPTIME_subset_EXPSPACE : EXPTIME ⊆ EXPSPACE

EXPTIME ⊆ EXPSPACE, i.e., SO(LFP) ⊆ SO(PFP) – the second-order shadow of PTIME ⊆ PSPACE. Registered in the Lax archive as Lax480241.ExponentialInclusions.EXPTIME_subset_EXPSPACE.

theorem DescriptiveComplexity.EXPTIME_subset_NEXPTIME : EXPTIME ⊆ NEXPTIME

EXPTIME ⊆ NEXPTIME, the second-order shadow of PTIME ⊆ NP. Registered in the Lax archive as Lax480241.ExponentialInclusions.EXPTIME_subset_NEXPTIME.

theorem DescriptiveComplexity.NEXPTIME_subset_EXPSPACE : NEXPTIME ⊆ EXPSPACE

NEXPTIME ⊆ EXPSPACE, the second-order shadow of NP ⊆ PSPACE. Registered in the Lax archive as Lax480241.ExponentialInclusions.NEXPTIME_subset_EXPSPACE.

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. Registered in the Lax archive as Lax480241.ExponentialInclusions.NL_exp_subset_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

PTIME ⊆ EXPTIME. Registered in the Lax archive as Lax480241.ExponentialInclusions.PTIME_subset_EXPTIME.

theorem DescriptiveComplexity.NP_subset_NEXPTIME : NP ⊆ NEXPTIME

NP ⊆ NEXPTIME. Registered in the Lax archive as Lax480241.ExponentialInclusions.NP_subset_NEXPTIME.

theorem DescriptiveComplexity.PSPACE_subset_EXPSPACE : PSPACE ⊆ EXPSPACE

PSPACE ⊆ EXPSPACE. Registered in the Lax archive as Lax480241.ExponentialInclusions.PSPACE_subset_EXPSPACE.

theorem DescriptiveComplexity.PH_subset_EXPTIME : PH ⊆ EXPTIME

The whole polynomial hierarchy sits inside EXPTIME, through DescriptiveComplexity.PH_subset_PSPACE. Registered in the Lax archive as Lax480241.ExponentialInclusions.PH_subset_EXPTIME.