The polynomial hierarchy, defined by second-order alternation

The levels Σₖᵖ/Πₖᵖ of the polynomial hierarchy for k ≥ 1 – in particular NP = Σ₁ᵖ and coNP = Π₁ᵖ – are defined here as ComplexityClasses, via Fagin's (Fagin 1974) and Stockmeyer's (Stockmeyer 1976) theorems: membership is second-order definability with k alternating quantifier blocks (DescriptiveComplexity.SigmaSODefinable / DescriptiveComplexity.PiSODefinable), and the closure of membership under (ordered) FO reductions is provided by the pullback theorems of DescriptiveComplexity.SecondOrderPull and DescriptiveComplexity.SecondOrderOrdered.

Hardness is defined cofinally: P is hard when every problem of the class reduces (by an ordered FO reduction) to every relational problem that P itself reduces to. For a problem over a relational vocabulary this is equivalent to the usual “everything in the class reduces to P” (DescriptiveComplexity.cofinalHard_iff, with per-class specializations DescriptiveComplexity.hard_sigmaP_succ_iff, DescriptiveComplexity.hard_piP_succ_iff and DescriptiveComplexity.hard_PTIME_iff), and the formulation makes hardness travel forward along reductions even through non-relational vocabularies.

Level 0 is DescriptiveComplexity.PTIME, polynomial time, defined here as definability in the Horn fragment SO-Horn of existential second-order logic (Grädel 1992) – the same move as defining NP by Σ₁-definability, and equally a definition rather than an axiom: the library declares no axioms, every theorem depending on nothing beyond Lean's standard propext, Classical.choice and Quot.sound (check with #print axioms). The order-free characterization of PTIME is the Chandra–Harel/Gurevich problem and is not needed here: SO-Horn definability, like ordered FO reductions, is stated over ordered structures.

What level 0 does and does not give. It is a genuine class, closed under (ordered) FO reductions by the shape-preserving pullback of DescriptiveComplexity.SecondOrderHornPull, and Πₖᵖ is the complements of Σₖᵖ at every level (DescriptiveComplexity.mem_piP_iff) – at level 0 by definition, above it by the quantifier duality.

All four inclusions of level 0 into level 1 are proved – PTIME ⊆ NP, PTIME ⊆ coNP and their complements (DescriptiveComplexity.PTIME_subset_NP, DescriptiveComplexity.PTIME_subset_coNP, DescriptiveComplexity.coPTIME_subset_NP, DescriptiveComplexity.coPTIME_subset_coNP); they live downstream with HORN-SAT, since they go through the Horn discharge and, for the two crossing ones, through the certificate of Horn unsatisfiability of DescriptiveComplexity.Problems.HornSat.Unsat.

That the two zeroth levels coincide – PiP 0 = SigmaP 0, polynomial time closed under complement – is proved downstream, as DescriptiveComplexity.piP_zero_eq: it is Grädel's capture theorem at level 0, and its route is the logic-to-logic equivalence of SO-Horn with FO(LFP) (DescriptiveComplexity.lfpDefinable_iff_sigmaSOHornDefinable, in DescriptiveComplexity.FixedPointHorn), a full logic being closed under negation by construction; no machine model is involved.

The level inclusions above 0, the duality Πₖᵖ = co-Σₖᵖ and the class PH are all proved (DescriptiveComplexity.sigmaP_subset_sigmaP_succ, DescriptiveComplexity.mem_piP_iff…).

Congruence of definability in the problem

theorem DescriptiveComplexity.sigmaSODefinable_congr {L : FirstOrder.Language} {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) (k : ℕ) : SigmaSODefinable k P ↔ SigmaSODefinable k Q

Σₖ-definability only depends on the finite instances of a problem.

theorem DescriptiveComplexity.piSODefinable_congr {L : FirstOrder.Language} {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) (k : ℕ) : PiSODefinable k P ↔ PiSODefinable k Q

Πₖ-definability only depends on the finite instances of a problem.

def DescriptiveComplexity.OrderedFOReduction.congrSource {L L' : FirstOrder.Language} [L'.IsRelational] {P P' : DecisionProblem L} {S : DecisionProblem L'} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ P'.Holds A) (g : OrderedFOReduction P S) : OrderedFOReduction P' S

An ordered FO reduction can be transported along an agreement of the source problems on finite structures.

Equations

• DescriptiveComplexity.OrderedFOReduction.congrSource h g = { Tag := g.Tag, tagFinite := ⋯, tagNonempty := ⋯, dim := g.dim, toInterpretation := g.toInterpretation, correct := ⋯ }

Cofinal hardness

def DescriptiveComplexity.CofinalHard {L : FirstOrder.Language} (Mem : {L₀ : FirstOrder.Language} → DecisionProblem L₀ → Prop) (P : DecisionProblem L) : Prop

Hardness for a collection of problems, cofinally: every problem of the collection reduces to every relational problem that P reduces to. For P over a relational vocabulary this is the usual notion (see DescriptiveComplexity.hard_sigmaP_succ_iff); this formulation is closed under reductions out of arbitrary vocabularies.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.CofinalHard.of_foReduction {Mem : {L₀ : FirstOrder.Language} → DecisionProblem L₀ → Prop} {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : FOReduction P Q) (hP : CofinalHard (fun {L₀ : FirstOrder.Language} => Mem) P) : CofinalHard (fun {L₀ : FirstOrder.Language} => Mem) Q

theorem DescriptiveComplexity.CofinalHard.of_orderedReduction {Mem : {L₀ : FirstOrder.Language} → DecisionProblem L₀ → Prop} {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : OrderedFOReduction P Q) (hP : CofinalHard (fun {L₀ : FirstOrder.Language} => Mem) P) : CofinalHard (fun {L₀ : FirstOrder.Language} => Mem) Q

theorem DescriptiveComplexity.CofinalHard.of_relOrderedReduction {Mem : {L₀ : FirstOrder.Language} → DecisionProblem L₀ → Prop} {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : RelOrderedFOReduction P Q) (hP : CofinalHard (fun {L₀ : FirstOrder.Language} => Mem) P) : CofinalHard (fun {L₀ : FirstOrder.Language} => Mem) Q

theorem DescriptiveComplexity.CofinalHard.congr {Mem : {L₀ : FirstOrder.Language} → DecisionProblem L₀ → Prop} {L₁ : FirstOrder.Language} {P P' : DecisionProblem L₁} (h : ∀ (A : Type) [inst : L₁.Structure A] [Finite A], P.Holds A ↔ P'.Holds A) (hP : CofinalHard (fun {L₀ : FirstOrder.Language} => Mem) P) : CofinalHard (fun {L₀ : FirstOrder.Language} => Mem) P'

theorem DescriptiveComplexity.cofinalHard_iff {L : FirstOrder.Language} [L.IsRelational] (Mem : {L₀ : FirstOrder.Language} → DecisionProblem L₀ → Prop) (P : DecisionProblem L) : CofinalHard (fun {L₀ : FirstOrder.Language} => Mem) P ↔ ∀ {L'' : FirstOrder.Language} (Q : DecisionProblem L''), Mem Q → Nonempty (RelOrderedFOReduction Q P)

Over a relational vocabulary, cofinal hardness is the usual notion: every problem of the collection reduces to P itself. This holds whatever the collection is – the proof only uses reflexivity and transitivity of reductions – so the specializations to the individual classes below (DescriptiveComplexity.hard_sigmaP_succ_iff, DescriptiveComplexity.hard_piP_succ_iff, DescriptiveComplexity.hard_PTIME_iff) are corollaries by definitional unfolding.

The left-to-right direction is what a user of a hardness result needs, to extract an actual reduction; it is where relationality of P is used, to instantiate the cofinal quantifier at P itself.

The complement of a class

noncomputable def DescriptiveComplexity.ComplexityClass.compl (C : ComplexityClass) : ComplexityClass

The complement of a complexity class: the problems whose complement belongs to it – the “co-” operator. Closure under reductions is inherited, since a reduction complements (DescriptiveComplexity.FOReduction.compl).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DescriptiveComplexity.ComplexityClass.mem_compl (C : ComplexityClass) {L : FirstOrder.Language} (P : DecisionProblem L) : C.compl.Mem P ↔ C.Mem Pᶜ

The levels of the hierarchy

noncomputable def DescriptiveComplexity.sigmaLevel (k : ℕ) : ComplexityClass

The class Σₖ₊₁ᵖ, defined by second-order definability with k + 1 alternating blocks starting existentially.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.piLevel (k : ℕ) : ComplexityClass

The class Πₖ₊₁ᵖ, defined by second-order definability with k + 1 alternating blocks starting universally.

Equations

• One or more equations did not get rendered due to their size.

Polynomial time, by the Horn fragment

noncomputable def DescriptiveComplexity.PTIME : ComplexityClass

The class PTIME: the problems definable in the Horn fragment SO-Horn of existential second-order logic (Grädel 1992), which captures polynomial time on ordered structures. It is a bona fide DescriptiveComplexity.ComplexityClass because SO-Horn definability is closed under (ordered) first-order reductions – the Horn shape survives the pullback, see DescriptiveComplexity.SecondOrderHornPull.

This is level 0 of the hierarchy below (DescriptiveComplexity.SigmaP, DescriptiveComplexity.PiP), and it has a complete problem, HORN-SAT (DescriptiveComplexity.HORNSAT_PTIME_complete). That the class is closed under complement – PiP 0 = SigmaP 0 – is DescriptiveComplexity.piP_zero_eq, through the equivalence with FO(LFP).

Equations

• One or more equations did not get rendered due to their size.

The hierarchy

noncomputable def DescriptiveComplexity.SigmaP : ℕ → ComplexityClass

The Σₖᵖ levels of the polynomial hierarchy: polynomial time at level 0 (DescriptiveComplexity.PTIME, defined by the Horn fragment SO-Horn), second-order definability with k alternations above.

Equations

• DescriptiveComplexity.SigmaP 0 = DescriptiveComplexity.PTIME
• DescriptiveComplexity.SigmaP k.succ = DescriptiveComplexity.sigmaLevel k

noncomputable def DescriptiveComplexity.PiP : ℕ → ComplexityClass

The Πₖᵖ levels of the polynomial hierarchy; level 0 is co-polynomial time, the complements of the SO-Horn definable problems. That this coincides with DescriptiveComplexity.PTIME is the closure of polynomial time under complement, DescriptiveComplexity.piP_zero_eq – see the module docstring.

Equations

• DescriptiveComplexity.PiP 0 = DescriptiveComplexity.PTIME.compl
• DescriptiveComplexity.PiP k.succ = DescriptiveComplexity.piLevel k

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.NP : ComplexityClass

NP is Σ₁ᵖ: by definition, the existential-second-order definable problems (Fagin's theorem).

Equations

• DescriptiveComplexity.NP = DescriptiveComplexity.SigmaP 1

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.coNP : ComplexityClass

coNP is Π₁ᵖ: the universal-second-order definable problems.

Equations

• DescriptiveComplexity.coNP = DescriptiveComplexity.PiP 1

theorem DescriptiveComplexity.mem_piP_iff (k : ℕ) {L : FirstOrder.Language} (P : DecisionProblem L) : (PiP k).Mem P ↔ (SigmaP k).Mem Pᶜ

Πₖᵖ consists of the complements of the Σₖᵖ problems, at every level: by definition at level 0, and by the quantifier duality DescriptiveComplexity.piSODefinable_iff_compl above from level 1 on.

(That moreover PiP 0 = SigmaP 0 – polynomial time closed under complement – is DescriptiveComplexity.piP_zero_eq: complementing a Horn program needs its least model computed inside the fragment, which is what the translation from FO(LFP) provides.)

theorem DescriptiveComplexity.sigmaP_subset_sigmaP_succ (k : ℕ) : SigmaP (k + 1) ⊆ SigmaP (k + 2)

Σₖ₊₁ᵖ ⊆ Σₖ₊₂ᵖ, by padding. (The level-0 inclusions are proved downstream with HORN-SAT, which their proofs go through: DescriptiveComplexity.PTIME_subset_NP and friends. Uniform monotonicity, j ≤ k → Σⱼᵖ ⊆ Σₖᵖ, therefore also lives there: DescriptiveComplexity.sigmaP_mono.)

theorem DescriptiveComplexity.sigmaP_subset_piP_succ (k : ℕ) : SigmaP (k + 1) ⊆ PiP (k + 2)

Σₖ₊₁ᵖ ⊆ Πₖ₊₂ᵖ.

theorem DescriptiveComplexity.piP_subset_sigmaP_succ (k : ℕ) : PiP (k + 1) ⊆ SigmaP (k + 2)

Πₖ₊₁ᵖ ⊆ Σₖ₊₂ᵖ.

theorem DescriptiveComplexity.piP_subset_piP_succ (k : ℕ) : PiP (k + 1) ⊆ PiP (k + 2)

Πₖ₊₁ᵖ ⊆ Πₖ₊₂ᵖ.

noncomputable def DescriptiveComplexity.PH : ComplexityClass

The polynomial hierarchy: union of all the levels. A problem is PH-hard if it is hard for every level.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.sigmaP_subset_PH (k : ℕ) : SigmaP k ⊆ PH

theorem DescriptiveComplexity.piP_subset_PH (k : ℕ) : PiP (k + 1) ⊆ PH

Πₖ₊₁ᵖ ⊆ PH. (At level 0 this is DescriptiveComplexity.piP_zero_subset_PH, which needs PTIME ⊆ NP and so lives downstream, with HORN-SAT.)

theorem DescriptiveComplexity.compl_mem_coNP_iff {L : FirstOrder.Language} (P : DecisionProblem L) : coNP.Mem Pᶜ ↔ NP.Mem P

A problem's complement is in coNP iff the problem is in NP.

Hardness over relational vocabularies

theorem DescriptiveComplexity.hard_sigmaP_succ_iff {L : FirstOrder.Language} [L.IsRelational] (k : ℕ) (P : DecisionProblem L) : (SigmaP (k + 1)).Hard P ↔ ∀ {L'' : FirstOrder.Language} (Q : DecisionProblem L''), SigmaSODefinable (k + 1) Q → Nonempty (RelOrderedFOReduction Q P)

Over a relational vocabulary, cofinal Σₖ₊₁ᵖ-hardness is the usual notion: every Σₖ₊₁-definable problem reduces to P.

theorem DescriptiveComplexity.hard_piP_succ_iff {L : FirstOrder.Language} [L.IsRelational] (k : ℕ) (P : DecisionProblem L) : (PiP (k + 1)).Hard P ↔ ∀ {L'' : FirstOrder.Language} (Q : DecisionProblem L''), PiSODefinable (k + 1) Q → Nonempty (RelOrderedFOReduction Q P)

Over a relational vocabulary, cofinal Πₖ₊₁ᵖ-hardness is the usual notion: every Πₖ₊₁-definable problem reduces to P.

theorem DescriptiveComplexity.hard_PTIME_iff {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : PTIME.Hard P ↔ ∀ {L'' : FirstOrder.Language} (Q : DecisionProblem L''), SigmaSOHornDefinable Q → Nonempty (RelOrderedFOReduction Q P)

Over a relational vocabulary, cofinal PTIME-hardness is the usual notion: every SO-Horn definable problem reduces to P.