Order relativization: moving the order between the instance and the vocabulary

The ordered fixed-point definability notions (DescriptiveComplexity.IFPDefinable, DescriptiveComplexity.PFPDefinable) quantify over every linear order on the universe of an L-structure; the order-free notions over the ordered expansion L.sum Language.order instead see the order as one more relation of the instance. This file proves the two readings interchangeable, the bookkeeping the unordered Abiteboul–Vianu theorem (DescriptiveComplexity.AbiteboulVianu) threads its right-to-left direction through:

• DescriptiveComplexity.DecisionProblem.withOrder – the problem «the order symbol is a linear order, and P holds on the L-reduct», over L.sum Language.order;
• DescriptiveComplexity.ifpDefinable_iff_ifpDefinableFree_withOrder and DescriptiveComplexity.pfpDefinable_iff_pfpDefinableFree_withOrder – P is FO(≤, IFP) (resp. FO(≤, PFP)) definable exactly when P.withOrder is order-free FO(IFP) (resp. FO(PFP)) definable.

Left to right, the induction is reused as is and its output is guarded by the first-order sentence «the order symbol is a linear order» (DescriptiveComplexity.leLinearS, via DescriptiveComplexity.StepDef.guardOut); on an instance whose order symbol does satisfy the guard, the promoted order (DescriptiveComplexity.LeLinearOn.linearOrder) rebuilds the ordered instance, identical to the given one through the identity isomorphism (DescriptiveComplexity.relMapIffEquiv). Right to left is immediate: an ordered L-structure is an instance of the expansion whose order symbol is a linear order (DescriptiveComplexity.sumOrderStructure).

Identity isomorphisms between structures with the same relations

def DescriptiveComplexity.relMapIffEquiv {L : FirstOrder.Language} [L.IsRelational] {A : Type} (inst inst' : L.Structure A) (h : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → A), FirstOrder.Language.Structure.RelMap r x ↔ FirstOrder.Language.Structure.RelMap r x) : L.Equiv A A

Two structures over a relational vocabulary interpreting every relation symbol equivalently are isomorphic through the identity map.

Equations

• DescriptiveComplexity.relMapIffEquiv inst inst' h = { toEquiv := Equiv.refl A, map_fun' := ⋯, map_rel' := ⋯ }

def DescriptiveComplexity.reductSumInlEquiv {L L' : FirstOrder.Language} {A B : Type} [instA : (L.sum L').Structure A] [instB : (L.sum L').Structure B] (e : (L.sum L').Equiv A B) : L.Equiv A B

An isomorphism over an expanded vocabulary is an isomorphism of the reducts.

Equations

• DescriptiveComplexity.reductSumInlEquiv e = { toEquiv := e.toEquiv, map_fun' := ⋯, map_rel' := ⋯ }

«The order symbol is a linear order»

def DescriptiveComplexity.LeLinearOn (L : FirstOrder.Language) (A : Type) [(L.sum FirstOrder.Language.order).Structure A] : Prop

The interpretation of the order symbol of the ordered expansion is a linear order: reflexive, transitive, antisymmetric and total. This is the guard under which a structure over L.sum Language.order is an ordered L-structure.

Equations

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

def DescriptiveComplexity.leLinearS (L : FirstOrder.Language) : (L.sum FirstOrder.Language.order).Sentence

The guard sentence «the order symbol is a linear order», over the ordered expansion.

Equations

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

theorem DescriptiveComplexity.realize_leLinearS (L : FirstOrder.Language) (A : Type) [(L.sum FirstOrder.Language.order).Structure A] : A ⊨ leLinearS L ↔ LeLinearOn L A

Realization of the guard sentence: the order symbol is a linear order.

@[instance_reducible]

noncomputable def DescriptiveComplexity.LeLinearOn.linearOrder {L : FirstOrder.Language} {A : Type} [(L.sum FirstOrder.Language.order).Structure A] (h : LeLinearOn L A) : LinearOrder A

Promoting a linear order symbol to a linear order on the universe (decidability by choice).

Equations

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

theorem DescriptiveComplexity.LeLinearOn.equiv {L : FirstOrder.Language} {A B : Type} [(L.sum FirstOrder.Language.order).Structure A] [(L.sum FirstOrder.Language.order).Structure B] (e : (L.sum FirstOrder.Language.order).Equiv A B) (h : LeLinearOn L A) : LeLinearOn L B

The guard transports along an isomorphism over the ordered expansion.

The problem, moved to the ordered expansion

def DescriptiveComplexity.DecisionProblem.withOrder {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : DecisionProblem (L.sum FirstOrder.Language.order)

«The order symbol is a linear order, and P holds on the L-reduct»: the problem P, moved to the ordered expansion of its vocabulary with the order now part of the instance. The order-relativized problem through which definability quantified over all linear orders (DescriptiveComplexity.IFPDefinable, DescriptiveComplexity.PFPDefinable) is compared with order-free definability over the expansion.

Equations

• P.withOrder = { Holds := fun (A : Type) (x : (L.sum FirstOrder.Language.order).Structure A) => DescriptiveComplexity.LeLinearOn L A ∧ P.Holds A, iso_invariant := ⋯ }

Guarding the output of an induction

def DescriptiveComplexity.StepDef.guardOut {L' : FirstOrder.Language} (d : StepDef L') (χ : L'.Sentence) : StepDef L'

Guard the output of a simultaneous induction by a sentence over the base vocabulary: same block, same step formulas, the output conjoined with the guard.

Equations

• d.guardOut χ = { B := d.B, step := d.step, out := FirstOrder.Language.LHom.sumInl.onSentence χ ⊓ d.out }

theorem DescriptiveComplexity.StepDef.ifpHolds_guardOut {L' : FirstOrder.Language} (d : StepDef L') (χ : L'.Sentence) (A : Type) [L'.Structure A] : (d.guardOut χ).IFPHolds A ↔ A ⊨ χ ∧ d.IFPHolds A

The inflationary value of the guarded induction: the guard holds and the original value does.

theorem DescriptiveComplexity.StepDef.pfpHolds_guardOut {L' : FirstOrder.Language} (d : StepDef L') (χ : L'.Sentence) (A : Type) [L'.Structure A] : (d.guardOut χ).PFPHolds A ↔ A ⊨ χ ∧ d.PFPHolds A

The partial value of the guarded induction: the guard holds and the original value does.

The transfer

theorem DescriptiveComplexity.ifpDefinable_iff_ifpDefinableFree_withOrder {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : IFPDefinable P ↔ IFPDefinableFree P.withOrder

Order relativization, inflationary case: P is FO(≤, IFP) definable exactly when its ordered relativization (DescriptiveComplexity.DecisionProblem.withOrder) is order-free FO(IFP) definable.

theorem DescriptiveComplexity.pfpDefinable_iff_pfpDefinableFree_withOrder {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : PFPDefinable P ↔ PFPDefinableFree P.withOrder

Order relativization, partial case: P is FO(≤, PFP) definable exactly when its ordered relativization (DescriptiveComplexity.DecisionProblem.withOrder) is order-free FO(PFP) definable.

Order-free definability implies ordered definability

noncomputable def DescriptiveComplexity.StepDef.liftOrder {L : FirstOrder.Language} (d : StepDef L) : StepDef (L.sum FirstOrder.Language.order)

A simultaneous induction over the base vocabulary, read over the ordered expansion: the formulas ignore the order symbol.

Equations

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

theorem DescriptiveComplexity.StepDef.ifpHolds_liftOrder {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] [LinearOrder A] : d.liftOrder.IFPHolds A ↔ d.IFPHolds A

The inflationary value of the lifted induction is the original one.

theorem DescriptiveComplexity.StepDef.pfpHolds_liftOrder {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] [LinearOrder A] : d.liftOrder.PFPHolds A ↔ d.PFPHolds A

The partial value of the lifted induction is the original one.

theorem DescriptiveComplexity.IFPDefinableFree.ifpDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : IFPDefinableFree P) : IFPDefinable P

Order-free FO(IFP) definability implies ordered definability: the induction ignores the order.

theorem DescriptiveComplexity.PFPDefinableFree.pfpDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : PFPDefinableFree P) : PFPDefinable P

Order-free FO(PFP) definability implies ordered definability: the induction ignores the order.