Closure of second-order definability under ordered FO reductions

If P ≤ᶠᵒ[≤] Q and Q is Σₖ₊₁- (resp. Πₖ₊₁-) definable, then so is P (DescriptiveComplexity.SigmaSODefinable.of_orderedReduction, DescriptiveComplexity.PiSODefinable.of_orderedReduction).

Pulling the defining sentence back through the interpretation (DescriptiveComplexity.SecondOrderPull) yields a sentence over the ordered expansion L.sum Language.order – correct for every linear order on the input, by order-invariance of the reduction. The order is then eliminated by re-quantifying it inside the first second-order block:

• the first block is extended with one binary relation variable, the order (DescriptiveComplexity.SOBlock.withOrder);
• the sentence is transported along the language morphism DescriptiveComplexity.orderElimLHom mapping the order symbol to the new variable;
• it is guarded by the first-order sentence DescriptiveComplexity.linearGuard stating that the variable is a linear order – as a conjunct if the block is existential (Σₖ₊₁), as a premise if it is universal (Πₖ₊₁).

Correctness of the guard uses DescriptiveComplexity.linearOrderOfGuard to promote a guarded relation variable to an actual LinearOrder instance, and the order-invariance clause of OrderedFOReduction.correct to connect different choices of the order. This requires at least one second-order block to piggyback on, whence the level k + 1.

Adding an order variable to a block

def DescriptiveComplexity.SOBlock.withOrder (B : SOBlock) : SOBlock

The block B extended with one extra binary relation variable, used to re-quantify the order of an ordered reduction.

Equations

• B.withOrder = { ι := Unit ⊕ B.ι, ιFinite := ⋯, arity := Sum.elim (fun (x : Unit) => 2) B.arity }

def DescriptiveComplexity.SOBlock.orderSym (B : SOBlock) : B.withOrder.lang.Relations 2

The order variable of the extended block.

Equations

• B.orderSym = ⟨Sum.inl (), ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.ordVarSym (L : FirstOrder.Language) (B : SOBlock) : (L.sum B.withOrder.lang).Relations 2

The order variable, as a relation symbol of the expanded language.

Equations

• DescriptiveComplexity.ordVarSym L B = Sum.inr B.orderSym

def DescriptiveComplexity.SOBlock.restPart {A : Type} (B : SOBlock) (ρ : B.withOrder.Assignment A) : B.Assignment A

The assignment of the original block variables underlying an assignment of the extended block.

Equations

• B.restPart ρ i = ρ (Sum.inr i)

def DescriptiveComplexity.SOBlock.joinOrder {A : Type} (B : SOBlock) (R : (Fin 2 → A) → Prop) (ρ : B.Assignment A) : B.withOrder.Assignment A

The assignment of the extended block determined by a binary relation (for the order variable) and an assignment of the original block.

Equations

• B.joinOrder R ρ (Sum.inl val) = R
• B.joinOrder R ρ (Sum.inr i) = ρ i

The linear-order guard

noncomputable def DescriptiveComplexity.linearGuard (L : FirstOrder.Language) (B : SOBlock) : (L.sum B.withOrder.lang).Sentence

The guard sentence: the order variable is (reflexive, transitive, antisymmetric and total, i.e.) a linear order.

Equations

• DescriptiveComplexity.linearGuard L B = DescriptiveComplexity.reflS✝ L B ⊓ (DescriptiveComplexity.transS✝ L B ⊓ (DescriptiveComplexity.antisymmS✝ L B ⊓ DescriptiveComplexity.totalS✝ L B))

theorem DescriptiveComplexity.realize_linearGuard {A : Type} (L : FirstOrder.Language) (B : SOBlock) (instA : L.Structure A) (ρ : B.withOrder.Assignment A) : A ⊨ linearGuard L B ↔ (∀ (a : A), ρ (Sum.inl ()) ![a, a]) ∧ (∀ (a b c : A), ρ (Sum.inl ()) ![a, b] → ρ (Sum.inl ()) ![b, c] → ρ (Sum.inl ()) ![a, c]) ∧ (∀ (a b : A), ρ (Sum.inl ()) ![a, b] → ρ (Sum.inl ()) ![b, a] → a = b) ∧ ∀ (a b : A), ρ (Sum.inl ()) ![a, b] ∨ ρ (Sum.inl ()) ![b, a]

Realization of the guard: the four linear-order axioms for the relation assigned to the order variable.

Promoting a guarded order variable to a linear order

@[instance_reducible]

noncomputable def DescriptiveComplexity.linearOrderOfGuard {A : Type} (r : (Fin 2 → A) → Prop) (hrefl : ∀ (a : A), r ![a, a]) (htrans : ∀ (a b c : A), r ![a, b] → r ![b, c] → r ![a, c]) (hantisymm : ∀ (a b : A), r ![a, b] → r ![b, a] → a = b) (htotal : ∀ (a b : A), r ![a, b] ∨ r ![b, a]) : LinearOrder A

A binary relation variable satisfying the guard axioms determines a linear order (decidability by choice).

Equations

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

Eliminating the order symbol

def DescriptiveComplexity.orderElimLHom (L : FirstOrder.Language) (B : SOBlock) : (L.sum FirstOrder.Language.order).sum B.lang →ᴸ L.sum B.withOrder.lang

The language morphism eliminating the order symbol of the ordered expansion in favor of the order variable of the extended block.

Equations

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

theorem DescriptiveComplexity.orderElimLHom_isExpansionOn (L : FirstOrder.Language) (B : SOBlock) (A : Type) (instA : L.Structure A) (lo : LinearOrder A) (ρ : B.withOrder.Assignment A) (hord : ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ w 0 ≤ w 1) : (orderElimLHom L B).IsExpansionOn A

When the order variable is assigned (a relation equivalent to) the linear order of the structure, the extended structure is an expansion along orderElimLHom of the ordered structure extended by the underlying assignment.

Order elimination, as a statement about sentences

The two theorems below are the order-elimination construction on its own, separated from the reduction that usually produces the sentence: a problem defined – over the ordered expansion, so with the order visible to the sentence – by a Σₖ₊₁ sentence for some linear order, or by a Πₖ₊₁ sentence for every linear order, is definable at that level over the bare vocabulary. The closure theorems of the next section are the case where the sentence comes from pulling a definition back through an ordered reduction, where order-invariance makes "for some" and "for every" agree.

Stated this way the construction also applies where no single order-invariant problem is in sight – to each half of a DescriptiveComplexity.DPDefinable definition separately, say, whose two halves are not individually order-invariant.

theorem DescriptiveComplexity.sigmaSODefinable_of_orderPull {L₁ : FirstOrder.Language} {P : DecisionProblem L₁} {k : ℕ} (Cs : List SOBlock) (hk : Cs.length = k + 1) (χ : (soLang (L₁.sum FirstOrder.Language.order) Cs).Sentence) (h : ∀ (A : Type) [inst : L₁.Structure A] [Finite A] [Nonempty A], P.Holds A ↔ ∃ (lo : LinearOrder A), SORealize (L₁.sum FirstOrder.Language.order) A Cs χ true) : SigmaSODefinable (k + 1) P

Order elimination, existentially: a problem defined by a Σₖ₊₁ sentence over the ordered expansion, correct for some linear order on each instance, is Σₖ₊₁-definable. The order is re-quantified inside the first block, guarded by a conjunct stating that it is a linear order.

theorem DescriptiveComplexity.piSODefinable_of_orderPull {L₁ : FirstOrder.Language} {P : DecisionProblem L₁} {k : ℕ} (Cs : List SOBlock) (hk : Cs.length = k + 1) (χ : (soLang (L₁.sum FirstOrder.Language.order) Cs).Sentence) (h : ∀ (A : Type) [inst : L₁.Structure A] [Finite A] [Nonempty A], P.Holds A ↔ ∀ (lo : LinearOrder A), SORealize (L₁.sum FirstOrder.Language.order) A Cs χ false) : PiSODefinable (k + 1) P

Order elimination, universally: a problem defined by a Πₖ₊₁ sentence over the ordered expansion, correct for every linear order on each instance, is Πₖ₊₁-definable. The order is re-quantified inside the first block, guarded as the premise of an implication.

Closure of the definability levels under ordered FO reductions

theorem DescriptiveComplexity.SigmaSODefinable.of_orderedReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : OrderedFOReduction P Q) (h : SigmaSODefinable (k + 1) Q) : SigmaSODefinable (k + 1) P

Σₖ₊₁-definability is closed under ordered FO reductions: the order is re-quantified existentially inside the first block, guarded by a conjunct stating that it is a linear order. Order-invariance of the reduction is what lets DescriptiveComplexity.sigmaSODefinable_of_orderPull be applied: the pulled-back sentence is correct not merely for some order but for every one.

theorem DescriptiveComplexity.PiSODefinable.of_orderedReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {k : ℕ} (f : OrderedFOReduction P Q) (h : PiSODefinable (k + 1) Q) : PiSODefinable (k + 1) P

Πₖ₊₁-definability is closed under ordered FO reductions: the order is re-quantified universally inside the first block, guarded as the premise of an implication.