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.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. Registered in the Lax archive as Lax134656.AbiteboulVianu.ifpDefinableFree_eq_pfpDefinableFree_iff_ptime_eq_pspace.