Abiteboul–Vianu, the ordered case

On ordered structures, the inflationary and partial fixed-point logics have the same expressive power exactly when polynomial time and polynomial space coincide (Abiteboul–Vianu 1989) – a corollary of the two capture theorems, FO(≤, IFP) = PTIME (DescriptiveComplexity.ifpDefinable_iff_mem_PTIME) and FO(≤, PFP) = PSPACE (DescriptiveComplexity.pfpDefinable_iff_mem_PSPACE), and mathematically content-free once they are in place: each side of the equivalence is rewritten through its capture.

The theorem proper – the same statement for the order-free logics DescriptiveComplexity.IFPDefinableFree and DescriptiveComplexity.PFPDefinableFree, where no capture is available and the equivalence with P = PSPACE is the celebrated content – is DescriptiveComplexity.AbiteboulVianu, built on the ≡ᵏ-invariant layer of DescriptiveComplexity.Invariant. This file is the ordered milestone on that route, and the natural stopping point of the capture half.

theorem DescriptiveComplexity.ifpDefinable_eq_pfpDefinable_iff_ptime_eq_pspace : (∀ {L : FirstOrder.Language} [inst : L.IsRelational] (P : DecisionProblem L), IFPDefinable P ↔ PFPDefinable P) ↔ PTIME = PSPACE

Abiteboul–Vianu, ordered case: the inflationary and partial fixed-point logics agree on ordered structures exactly when PTIME = PSPACE. A corollary of the two capture theorems; see the module docstring for what it does not say (the unordered statement).