The whole polynomial hierarchy is closed under FO(LFP) reductions

DescriptiveComplexity.FixedPointReductionClosure closes PTIME, NP and coNP under ≤ˡᶠᵖ. This file does the same at every level (DescriptiveComplexity.mem_sigmaP_of_lfpReduction, DescriptiveComplexity.mem_piP_of_lfpReduction) and for PH itself (DescriptiveComplexity.mem_PH_of_lfpReduction), and – a reduction of one notion being a reduction of the wider ones – for ≤ᵗᶜ and ≤ᵈᵗᶜ too.

Only one ingredient is new, and it is the one that was missing at level 1: DescriptiveComplexity.exists_expand_sorealize removes the reduction's induction from a definition with a prefix of any length. Everything else is the argument of the first level verbatim – pull the definition back through the interpretation (DescriptiveComplexity.sorealize_pullRelSO), guard it with the domain's inhabitedness, and re-quantify the order inside the first block (DescriptiveComplexity.sigmaSODefinable_of_orderPull).

The universal levels come by complementation, as coNP did: a reduction complements (DescriptiveComplexity.LFPReduction.compl), and Πₖ definability is Σₖ definability of the complement (DescriptiveComplexity.piSODefinable_iff_compl). Nothing here needs the Π-polarity of the expansion theorem – though it has it, which is what would be needed to close the levels without complementing.

The levels

theorem DescriptiveComplexity.SigmaSODefinable.of_lfpReduction_succ {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : LFPReduction P Q) (h : SigmaSODefinable (k + 1) Q) : SigmaSODefinable (k + 1) P

Σₖ₊₁-definability is closed under FO(LFP) reductions, at every level: the membership sentence is pulled back through the interpretation, the induction is eliminated from under the whole quantifier prefix (DescriptiveComplexity.exists_expand_sorealize), and the order the reduction uses is re-quantified inside the first block.

theorem DescriptiveComplexity.PiSODefinable.of_lfpReduction_succ {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : LFPReduction P Q) (h : PiSODefinable (k + 1) Q) : PiSODefinable (k + 1) P

Πₖ₊₁-definability is closed under FO(LFP) reductions, by complementation.

The classes

theorem DescriptiveComplexity.mem_sigmaP_of_lfpReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : LFPReduction P Q) (h : (SigmaP k).Mem Q) : (SigmaP k).Mem P

Every level Σₖᵖ is closed under FO(LFP) reductions.

theorem DescriptiveComplexity.mem_piP_of_lfpReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : LFPReduction P Q) (h : (PiP k).Mem Q) : (PiP k).Mem P

Every level Πₖᵖ is closed under FO(LFP) reductions.

theorem DescriptiveComplexity.mem_PH_of_lfpReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : LFPReduction P Q) (h : PH.Mem Q) : PH.Mem P

The polynomial hierarchy is closed under FO(LFP) reductions.

The same, at the reduction notions below

theorem DescriptiveComplexity.mem_sigmaP_of_tcReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : TCReduction P Q) (h : (SigmaP k).Mem Q) : (SigmaP k).Mem P

Every level Σₖᵖ is closed under FO(TC) reductions.

theorem DescriptiveComplexity.mem_piP_of_tcReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : TCReduction P Q) (h : (PiP k).Mem Q) : (PiP k).Mem P

Every level Πₖᵖ is closed under FO(TC) reductions.

theorem DescriptiveComplexity.mem_PH_of_tcReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : TCReduction P Q) (h : PH.Mem Q) : PH.Mem P

The polynomial hierarchy is closed under FO(TC) reductions.

theorem DescriptiveComplexity.mem_sigmaP_of_dtcReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : DTCReduction P Q) (h : (SigmaP k).Mem Q) : (SigmaP k).Mem P

Every level Σₖᵖ is closed under FO(DTC) reductions.

theorem DescriptiveComplexity.mem_piP_of_dtcReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : DTCReduction P Q) (h : (PiP k).Mem Q) : (PiP k).Mem P

Every level Πₖᵖ is closed under FO(DTC) reductions.

theorem DescriptiveComplexity.mem_PH_of_dtcReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : DTCReduction P Q) (h : PH.Mem Q) : PH.Mem P

The polynomial hierarchy is closed under FO(DTC) reductions.