The classes are closed under FO(LFP) reductions

Membership in PTIME, in NP and in coNP travels backward along an FO(LFP) reduction (DescriptiveComplexity.mem_PTIME_of_lfpReduction, DescriptiveComplexity.mem_NP_of_lfpReduction, DescriptiveComplexity.mem_coNP_of_lfpReduction), exactly as it does along a first-order one. This is what makes ≤ˡᶠᵖ a usable reduction notion for these classes rather than a definition with no theorems: without it, “P reduces to a problem of the class” would say nothing about P.

The three proofs are different, and the difference is the point.

• PTIME is closed because the logic is: the reduction's induction and the membership's induction stratify into one (DescriptiveComplexity.StepDef.stratify), after the latter is pulled back through the interpretation. Nothing is guessed.
• NP is closed because an induction can be eliminated from a Σ₁ definition (DescriptiveComplexity.sigmaSODefinable_of_ifpExpand), the quantifier block that replaces it merging with the one already there.
• coNP is closed by complementation – a reduction complements (DescriptiveComplexity.LFPReduction.compl) – which is cheaper than redoing the argument with a universal block.

Above the first level nothing is claimed here. The same argument would put an extra existential block innermost in a Σₖ prefix, which merges with the innermost block only when that block is existential; the even levels would need the dual elimination, through DescriptiveComplexity.PTIME_subset_coNP, and the vocabulary bookkeeping of a block inserted in the middle of a prefix. PSPACE is open here for a sharper reason: FO(PFP) has no stratification theorem, the partial iteration not being monotone.

Hardness

DescriptiveComplexity.CofinalHardLFP is hardness stated with ≤ˡᶠᵖ in place of ≤ʳᶠᵒ[≤], and DescriptiveComplexity.CofinalHard.toLFP says that a hard problem in the library's sense is hard in this weaker one – the expected implication, since a first-order reduction is an FO(LFP) reduction. Note the direction: hardness under a larger class of reductions is a weaker statement, so every completeness theorem of the catalog implies its polynomial-time-reduction reading, and none of them is superseded by it.

The definable domain is inhabited, as a sentence

noncomputable def DescriptiveComplexity.RelFOInterpretation.domNonemptyS {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} (I : RelFOInterpretation L₁ L₂ Tag dim) : L₁.Sentence

“Some tagged tuple is in the domain”, as a first-order sentence of the source vocabulary: the disjunction over the (finitely many) tags of the existential closure of the domain formula.

Equations

• I.domNonemptyS = FirstOrder.Language.Formula.iSup fun (t : Tag) => FirstOrder.Language.Formula.iExs (Fin dim) (FirstOrder.Language.Formula.relabel Sum.inr (I.domFormula t))

theorem DescriptiveComplexity.RelFOInterpretation.realize_domNonemptyS {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} (I : RelFOInterpretation L₁ L₂ Tag dim) (A : Type) [L₁.Structure A] : A ⊨ I.domNonemptyS ↔ Nonempty (I.MapRel A)

Polynomial time

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

FO(≤, IFP) definability is closed under FO(LFP) reductions: the reduction's induction and the definition's induction stratify into one, the latter pulled back through the (order-extended) interpretation.

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

PTIME is closed under FO(LFP) reductions: a problem reducing to a polynomial-time problem by a polynomial-time reduction is polynomial time.

NP, and coNP by complementation

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

Σ₁-definability is closed under FO(LFP) reductions. The membership sentence is pulled back through the interpretation, over the base structure expanded by the reduction's induction (DescriptiveComplexity.sorealize_pullRelSO); the induction is then eliminated from the pulled definition (DescriptiveComplexity.sigmaSODefinable_of_ifpExpand), and the order the reduction uses is re-quantified inside the block (DescriptiveComplexity.sigmaSODefinable_of_orderPull).

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

NP is closed under FO(LFP) reductions: a problem reducing to an NP problem by a polynomial-time reduction is in NP.

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

coNP is closed under FO(LFP) reductions, by complementation: the same interpretation reduces the complements.

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

Π₁-definability is closed under FO(LFP) reductions – the same statement as DescriptiveComplexity.mem_coNP_of_lfpReduction, at the level of the logic.

Membership under relativized first-order reductions

The same three classes are closed under the relativized first-order reductions ≤ʳᶠᵒ[≤] – the notion all of this library's hardness travels along. Only the hardness half of that closure was available before (DescriptiveComplexity.ComplexityClass.hard_of_relOrderedReduction); the membership half is these three theorems, and they are corollaries of the pullback of DescriptiveComplexity.SecondOrderRelPull and of DescriptiveComplexity.IFPDefinable.of_relOrderedReduction. (What is still missing is the corresponding field of DescriptiveComplexity.ComplexityClass, which every class literal of the library would have to supply.)

theorem DescriptiveComplexity.mem_PTIME_of_relOrderedReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : RelOrderedFOReduction P Q) (h : PTIME.Mem Q) : PTIME.Mem P

PTIME is closed under relativized ordered reductions.

theorem DescriptiveComplexity.mem_NP_of_relOrderedReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : RelOrderedFOReduction P Q) (h : NP.Mem Q) : NP.Mem P

NP is closed under relativized ordered reductions.

theorem DescriptiveComplexity.mem_coNP_of_relOrderedReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : RelOrderedFOReduction P Q) (h : coNP.Mem Q) : coNP.Mem P

coNP is closed under relativized ordered reductions.

Hardness under FO(LFP) reductions

def DescriptiveComplexity.CofinalHardLFP {L : FirstOrder.Language} [L.IsRelational] (Mem : {L₀ : FirstOrder.Language} → [inst : L₀.IsRelational] → DecisionProblem L₀ → Prop) (P : DecisionProblem L) : Prop

Hardness for a collection of problems under FO(LFP) reductions, stated cofinally as DescriptiveComplexity.CofinalHard is: every problem of the collection FO(LFP)-reduces to every problem that P FO(LFP)-reduces to.

Hardness under a wider class of reductions is a weaker statement, so this is implied by the library's own hardness (DescriptiveComplexity.CofinalHard.toLFP) and does not replace it.

Equations

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

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

Over a relational vocabulary, hardness under FO(LFP) reductions is the usual notion: every problem of the collection reduces to P itself.

theorem DescriptiveComplexity.CofinalHardLFP.of_lfpReduction {L : FirstOrder.Language} [L.IsRelational] {Mem : {L₀ : FirstOrder.Language} → [inst : L₀.IsRelational] → DecisionProblem L₀ → Prop} {L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : LFPReduction P Q) (hP : CofinalHardLFP (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => Mem) P) : CofinalHardLFP (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => Mem) Q

Hardness travels forward along FO(LFP) reductions.

theorem DescriptiveComplexity.CofinalHard.toLFP {L : FirstOrder.Language} [L.IsRelational] {Mem : {L₀ : FirstOrder.Language} → [inst : L₀.IsRelational] → DecisionProblem L₀ → Prop} {P : DecisionProblem L} (h : CofinalHard (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => Mem) P) : CofinalHardLFP (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => Mem) P

A problem hard for a collection under first-order reductions is hard for it under FO(LFP) reductions: every first-order reduction is an FO(LFP) reduction.

theorem DescriptiveComplexity.ComplexityClass.hard_lfp_of_hard {L : FirstOrder.Language} [L.IsRelational] {C : ComplexityClass} {P : DecisionProblem L} (hC : ∀ {L' : FirstOrder.Language} [inst : L'.IsRelational] (R : DecisionProblem L'), C.Hard R ↔ CofinalHard (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => C.Mem) R) (h : C.Hard P) : CofinalHardLFP (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => C.Mem) P

A 𝒞-hard problem of a class of this library is hard under FO(LFP) reductions. Reading a completeness theorem of the catalog with polynomial-time reductions in place of first-order ones is this corollary.