The polynomial hierarchy

This file defines the polynomial hierarchy via certificate quantifiers, following the quantified-formula definition (Arora–Barak Definition 5.4, stated over the library's pair codec): polyExistsLang p L holds of x when some witness w of length at most p.eval |x| puts the encoded pair pair x w in L, and polyForallLang p L requires this of every such witness. Lifting these to class operators gives the levels SigmaP 0 = P, SigmaP (n + 1) = polyExistsClass (PiP n), PiP n = complClass (SigmaP n), and their union PH.

The level inclusions SigmaP n ⊆ SigmaP (n + 1) and PiP n ⊆ PiP (n + 1) need one computational fact: decoding the first component of a canonical pair is polynomial-time computable (pairFst_mem_FP, from Complexitylib.Classes.P.Pairing), so every result in this file is unconditional.

Main definitions

• polyExistsLang, polyForallLang — witness quantifiers on languages
• polyExistsClass, polyForallClass — the induced operators on classes
• SigmaP, PiP, PH — the hierarchy levels and their union

Main results

• compl_polyExistsLang / compl_polyForallLang — quantifier duality
• complClass_polyExistsClass / complClass_polyForallClass — class duality
• SigmaP_zero, PiP_zero, SigmaP_succ, PiP_succ — recursion laws
• pairFst_mem_FP — the pair decoder is polynomial-time
• P_subset_polyExistsClass_P / P_subset_polyForallClass_P — base inclusions
• SigmaP_subset_SigmaP_succ / PiP_subset_PiP_succ — level inclusions
• SigmaP_subset_PH, P_subset_PH

TODO

• Relate SigmaP 1 to the NTM-based NP through the witness characterization interface in Complexitylib.Classes.NP.Witness.

Witness quantifiers on languages

def Complexity.polyExistsLang (p : Polynomial ℕ) (L : Language) : Language

The language of inputs x admitting a witness w of length at most p.eval |x| such that the encoded pair pair x w lies in L.

Equations

• Complexity.polyExistsLang p L = {x : List Bool | ∃ (w : List Bool), w.length ≤ Polynomial.eval x.length p ∧ Complexity.pair x w ∈ L}

def Complexity.polyForallLang (p : Polynomial ℕ) (L : Language) : Language

The language of inputs x such that every witness w of length at most p.eval |x| puts the encoded pair pair x w in L.

Equations

• Complexity.polyForallLang p L = {x : List Bool | ∀ (w : List Bool), w.length ≤ Polynomial.eval x.length p → Complexity.pair x w ∈ L}

@[simp]

theorem Complexity.mem_polyExistsLang {p : Polynomial ℕ} {L : Language} {x : List Bool} : x ∈ polyExistsLang p L ↔ ∃ (w : List Bool), w.length ≤ Polynomial.eval x.length p ∧ pair x w ∈ L

Membership in polyExistsLang unfolds to a bounded existential.

@[simp]

theorem Complexity.mem_polyForallLang {p : Polynomial ℕ} {L : Language} {x : List Bool} : x ∈ polyForallLang p L ↔ ∀ (w : List Bool), w.length ≤ Polynomial.eval x.length p → pair x w ∈ L

Membership in polyForallLang unfolds to a bounded universal.

theorem Complexity.compl_polyExistsLang (p : Polynomial ℕ) (L : Language) : (polyExistsLang p L)ᶜ = polyForallLang p Lᶜ

Complementing a bounded existential yields a bounded universal over the complement: some-witness failure is all-witness exclusion.

theorem Complexity.compl_polyForallLang (p : Polynomial ℕ) (L : Language) : (polyForallLang p L)ᶜ = polyExistsLang p Lᶜ

Complementing a bounded universal yields a bounded existential over the complement.

Quantifier operators on classes

def Complexity.polyExistsClass (C : Set Language) : Set Language

The class of languages expressible as a polynomially-bounded existential over some language of C.

Equations

• Complexity.polyExistsClass C = {L : Complexity.Language | ∃ (p : Polynomial ℕ), ∃ L' ∈ C, L = Complexity.polyExistsLang p L'}

def Complexity.polyForallClass (C : Set Language) : Set Language

The class of languages expressible as a polynomially-bounded universal over some language of C.

Equations

• Complexity.polyForallClass C = {L : Complexity.Language | ∃ (p : Polynomial ℕ), ∃ L' ∈ C, L = Complexity.polyForallLang p L'}

theorem Complexity.polyExistsClass_mono {C D : Set Language} (h : C ⊆ D) : polyExistsClass C ⊆ polyExistsClass D

polyExistsClass is monotone in the base class.

theorem Complexity.polyForallClass_mono {C D : Set Language} (h : C ⊆ D) : polyForallClass C ⊆ polyForallClass D

polyForallClass is monotone in the base class.

theorem Complexity.complClass_polyExistsClass (C : Set Language) : complClass (polyExistsClass C) = polyForallClass (complClass C)

Class-level quantifier duality: the complement class of a bounded existential class is the bounded universal class over the complement class.

theorem Complexity.complClass_polyForallClass (C : Set Language) : complClass (polyForallClass C) = polyExistsClass (complClass C)

Class-level quantifier duality: the complement class of a bounded universal class is the bounded existential class over the complement class.

Base inclusions

theorem Complexity.P_subset_polyExistsClass_P : P ⊆ polyExistsClass P

Every language of P is a bounded existential over P: take the zero witness bound, so the only witness is [], and decide pair x [] by decoding the first component and running the original decider.

theorem Complexity.P_subset_polyForallClass_P : P ⊆ polyForallClass P

Every language of P is a bounded universal over P: with the zero witness bound the only witness is [], decided as in P_subset_polyExistsClass_P.

The hierarchy

def Complexity.SigmaP : ℕ → Set Language

The Σ levels of the polynomial hierarchy: SigmaP 0 = P and SigmaP (n + 1) is a bounded existential over the complement class of SigmaP n (that is, over PiP n).

Equations

• Complexity.SigmaP 0 = Complexity.P
• Complexity.SigmaP n.succ = Complexity.polyExistsClass (Complexity.complClass (Complexity.SigmaP n))

def Complexity.PiP (n : ℕ) : Set Language

The Π levels of the polynomial hierarchy: PiP n is the complement class of SigmaP n.

Equations

• Complexity.PiP n = Complexity.complClass (Complexity.SigmaP n)

def Complexity.PH : Set Language

The polynomial hierarchy: the union of all Σ levels.

Equations

• Complexity.PH = ⋃ (n : ℕ), Complexity.SigmaP n

@[simp]

theorem Complexity.SigmaP_zero : SigmaP 0 = P

The zeroth Σ level is P.

@[simp]

theorem Complexity.complClass_SigmaP (n : ℕ) : complClass (SigmaP n) = PiP n

The complement class of a Σ level is the corresponding Π level.

@[simp]

theorem Complexity.complClass_PiP (n : ℕ) : complClass (PiP n) = SigmaP n

The complement class of a Π level is the corresponding Σ level.

@[simp]

theorem Complexity.PiP_zero : PiP 0 = P

The zeroth Π level is P, since P is closed under complement.

theorem Complexity.SigmaP_succ (n : ℕ) : SigmaP (n + 1) = polyExistsClass (PiP n)

Recursion law for Σ levels: SigmaP (n + 1) is a bounded existential over PiP n.

theorem Complexity.PiP_succ (n : ℕ) : PiP (n + 1) = polyForallClass (SigmaP n)

Recursion law for Π levels: PiP (n + 1) is a bounded universal over SigmaP n.

theorem Complexity.SigmaP_one : SigmaP 1 = polyExistsClass P

The first Σ level is the bounded existential closure of P — the certificate form of NP.

theorem Complexity.PiP_one : PiP 1 = polyForallClass P

The first Π level is the bounded universal closure of P — the certificate form of coNP.

Level inclusions

theorem Complexity.SigmaP_subset_SigmaP_succ (n : ℕ) : SigmaP n ⊆ SigmaP (n + 1)

Each Σ level is contained in the next.

theorem Complexity.PiP_subset_PiP_succ (n : ℕ) : PiP n ⊆ PiP (n + 1)

Each Π level is contained in the next.

PH

theorem Complexity.mem_PH_iff {L : Language} : L ∈ PH ↔ ∃ (n : ℕ), L ∈ SigmaP n

Membership in PH is membership in some Σ level.

theorem Complexity.SigmaP_subset_PH (n : ℕ) : SigmaP n ⊆ PH

Every Σ level is contained in the hierarchy.

theorem Complexity.P_subset_PH : P ⊆ PH

P is contained in the polynomial hierarchy.