The Abiteboul–Vianu theorem

The inflationary and partial fixed-point logics have the same expressive power on unordered finite structures exactly when PTIME = PSPACE (Abiteboul–Vianu 1991; proved here along the purely logical route of Dawar–Lindell–Weinstein 1995, also that of Ebbinghaus–Flum 1995, ch. 7): DescriptiveComplexity.ifpDefinableFree_eq_pfpDefinableFree_iff_ptime_eq_pspace. The two classes PTIME and PSPACE are the library's logically defined ones; the machine-model reading is supplied beside them by DescriptiveComplexity.dtmAccept_PTIME_complete and DescriptiveComplexity.dtmAcceptSpace_PSPACE_complete.

Right to left, from the coincidence of the classes: a PSPACE problem is FO(≤, PFP) definable (DescriptiveComplexity.pfpDefinable_iff_mem_PSPACE), its order relativization is order-free FO(PFP) definable (DescriptiveComplexity.FixedPointOrderTransfer), hence by hypothesis order-free FO(IFP) definable, so the problem is FO(≤, IFP) definable and in PTIME (DescriptiveComplexity.ifpDefinable_iff_mem_PTIME).

Left to right, through the invariant structure (DescriptiveComplexity.Invariant) – the invariant and its inflationary-definable order of Dawar–Lindell–Weinstein 1995, in place of the original's relational machine: an order-free FO(PFP) definition has a k-variable budget, so its stages are ≡ᵏ-invariant and its whole computation runs on the invariant structure Iᵏ A (DescriptiveComplexity.StepDef.pfpHolds_invStepDef) – a problem over the invariant vocabulary, order-free FO(PFP) definable by construction, hence in PSPACE, hence by the hypothesis in PTIME, hence FO(≤, IFP) definable. On Iᵏ A the order is not given but computed: the canonical order on ≡ᵏ-classes is one inflationary induction (DescriptiveComplexity.Invariant.OrderDef), and the ordered induction delivered by the capture pulls back along the quotient map to an order-free induction over A reading that computed order (DescriptiveComplexity.StepDef.ifpHolds_backStepDef), the two glued into a single induction by stratification (DescriptiveComplexity.StepDef.ifpHolds_stratify). The theorem is stated for the IFP-versus-PFP form, as in Abiteboul and Vianu's original; Gurevich–Shelah (order-free LFP = IFP) is deliberately not involved.

theorem DescriptiveComplexity.SigmaSOHornDefinable.sotcDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : SigmaSOHornDefinable P) : SOTCDefinable P

The easy inclusion between the two logically defined classes: PTIME ⊆ PSPACE, read on membership witnesses – an SO-Horn definition is an FO(LFP) one, hence FO(≤, IFP), hence FO(≤, PFP), hence SO(TC).

theorem DescriptiveComplexity.ptime_eq_pspace_of_ifpDefinableFree_eq_pfpDefinableFree (h : ∀ {L : FirstOrder.Language} [inst : L.IsRelational] (P : DecisionProblem L), IFPDefinableFree P ↔ PFPDefinableFree P) : PTIME = PSPACE

Abiteboul–Vianu, right to left: if the order-free inflationary and partial fixed-point logics have the same expressive power, then PTIME = PSPACE. A PSPACE problem is FO(≤, PFP) definable; its ordered relativization is order-free FO(PFP) definable, hence – by the hypothesis – order-free FO(IFP) definable, so the problem itself is FO(≤, IFP) definable and lands in PTIME.

theorem DescriptiveComplexity.ifpDefinableFree_of_pfpDefinableFree_of_ptime_eq_pspace (hPP : PTIME = PSPACE) {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : PFPDefinableFree P) : IFPDefinableFree P

Abiteboul–Vianu, left to right: if PTIME = PSPACE, an order-free FO(PFP) definable problem is order-free FO(IFP) definable. The whole computation factors through the invariant structure Iᵏ A; there – ordered by the canonical, itself inflationary-definable order on ≡ᵏ-classes – the hypothesis turns the PSPACE computation into a PTIME one, delivered as an ordered inflationary induction, which pulls back along the quotient map and is glued to the order's own induction by stratification.

theorem DescriptiveComplexity.ifpDefinableFree_eq_pfpDefinableFree_iff_ptime_eq_pspace : (∀ {L : FirstOrder.Language} [inst : L.IsRelational] (P : DecisionProblem L), IFPDefinableFree P ↔ PFPDefinableFree P) ↔ PTIME = PSPACE

The Abiteboul–Vianu theorem. The inflationary and partial fixed-point logics have the same expressive power on unordered finite structures exactly when polynomial time and polynomial space coincide.