Documentation

Complexity.Computability.Complexity.Classes.BooleanHierarchy.PH

The Boolean hierarchy inside the polynomial hierarchy #

The intersection of matching existential and universal PH levels is closed under Boolean operations. At level two it contains NP, hence every finite difference over NP. This gives BooleanHierarchy ⊆ SigmaP 2 ∩ PiP 2, in particular for DP and coDP, using the existing exact-length alternating verifiers Arora and Barak, Chapter 5. It is a containment, not a collapse of either hierarchy; Kadin's collapse theorem is not used.

Main results #

References #

source
theorem Cslib.Complexity.compl_mem_SigmaP_inter_PiP {α : Type} {enc : α ↪ List Bool} {A : Set α} {k : ℕ} (hA : A ∈ SigmaP k enc ∩ PiP k enc) :
Aᶜ ∈ SigmaP k enc ∩ PiP k enc

Matching existential and universal PH levels are jointly closed under complement.

source
theorem Cslib.Complexity.diff_mem_SigmaP_inter_PiP {α : Type} {enc : α ↪ List Bool} {A B : Set α} {k : ℕ} (hA : A ∈ SigmaP k enc ∩ PiP k enc) (hB : B ∈ SigmaP k enc ∩ PiP k enc) :
A \ B ∈ SigmaP k enc ∩ PiP k enc

Taking a difference preserves membership in both matching PH levels.

source
theorem Cslib.Complexity.BooleanHierarchy_subset_SigmaP_two_inter_PiP_two {α : Type} {enc : α ↪ List Bool} :
BooleanHierarchy enc ⊆ SigmaP 2 enc ∩ PiP 2 enc

Every finite Boolean combination of NP languages belongs to both second PH levels.

source
theorem Cslib.Complexity.DP_subset_SigmaP_two_inter_PiP_two {α : Type} {enc : α ↪ List Bool} :
DP enc ⊆ SigmaP 2 enc ∩ PiP 2 enc

NP minus NP is in both second PH levels.

source
theorem Cslib.Complexity.coDP_subset_SigmaP_two_inter_PiP_two {α : Type} {enc : α ↪ List Bool} :
coDP enc ⊆ SigmaP 2 enc ∩ PiP 2 enc

The complement difference class is in both second PH levels.