Closure of ∃SO[new] definability under ordered FO reductions

If P ≤ᶠᵒ[≤] Q and Q is ∃SO[new]-definable, then so is P (DescriptiveComplexity.SigmaSONewDefinable.of_orderedReduction). With the pullback of DescriptiveComplexity.SecondOrderNewPull this is the second closure property a complexity class needs, and RE becomes one (DescriptiveComplexity.RecursivelyEnumerable).

The shape is the one of DescriptiveComplexity.SecondOrderOrdered: pulling the definition back through the interpretation yields a sentence over the ordered expansion – correct for every linear order on the instance, by order-invariance of the reduction – and the order is then re-quantified inside the second-order block, guarded by a sentence saying that the variable is a linear order.

What value invention changes. The order variable now ranges over the extended universe A ⊕ Fin n, where it cannot be a linear order at all: the order symbol of the extended structure relates original elements only (invented values are related to nothing, by DescriptiveComplexity.extBase), so the guard must be relativized: DescriptiveComplexity.extLinearGuard states that the variable relates original elements only, and is reflexive and total on them. That is exactly enough to recover a LinearOrder on the instance (DescriptiveComplexity.linearOrderOfGuard) and to know that the variable is the order of the extended structure (DescriptiveComplexity.extLeRel), which is what the language morphism DescriptiveComplexity.extOrderElim needs to be an expansion.

The order of the instance, seen in the extended universe

def DescriptiveComplexity.extLeRel (A : Type) [LE A] (n : ℕ) : (Fin 2 → A ⊕ Fin n) → Prop

The order of the instance, as a relation on the extended universe: it relates two original elements when their values are ordered, and relates nothing else.

Equations

• DescriptiveComplexity.extLeRel A n w = ∃ (y : Fin 2 → A), (∀ (i : Fin 2), w i = Sum.inl (y i)) ∧ y 0 ≤ y 1

theorem DescriptiveComplexity.extLeRel_isOld {A : Type} [LE A] {n : ℕ} {w : Fin 2 → A ⊕ Fin n} (h : extLeRel A n w) : IsOld (w 0) ∧ IsOld (w 1)

@[simp]

theorem DescriptiveComplexity.extLeRel_inl {A : Type} [LE A] {n : ℕ} (a b : A) : extLeRel A n ![Sum.inl a, Sum.inl b] ↔ a ≤ b

theorem DescriptiveComplexity.relMap_ext_le {A : Type} [LE A] {n : ℕ} (L : FirstOrder.Language) [L.Structure A] [Nonempty A] (w : Fin 2 → A ⊕ Fin n) : FirstOrder.Language.Structure.RelMap (Sum.inl (Sum.inr FirstOrder.Language.leSymb)) w ↔ extLeRel A n w

Eliminating the order symbol

@[reducible, inline]

abbrev DescriptiveComplexity.extOldSym (L : FirstOrder.Language) (C : SOBlock) : ((newLang L).sum C.withOrder.lang).Relations 1

The marker old, as a symbol of the vocabulary the eliminated sentence lives in.

Equations

• DescriptiveComplexity.extOldSym L C = Sum.inl (Sum.inr FirstOrder.Language.oldSym)

def DescriptiveComplexity.extOrderElim (L : FirstOrder.Language) (C : SOBlock) : (newLang (L.sum FirstOrder.Language.order)).sum C.lang →ᴸ (newLang L).sum C.withOrder.lang

The language morphism eliminating the order symbol of the extended ordered vocabulary in favour of the order variable of the extended block.

Equations

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

theorem DescriptiveComplexity.extOrderElim_isExpansionOn {L : FirstOrder.Language} {C : SOBlock} {A : Type} [L.Structure A] [Nonempty A] {n : ℕ} [lo : LinearOrder A] (ρ : C.withOrder.Assignment (A ⊕ Fin n)) (ρ' : C.Assignment (A ⊕ Fin n)) (hrest : C.restPart ρ = ρ') (hord : ∀ (w : Fin 2 → A ⊕ Fin n), ρ (Sum.inl ()) w ↔ extLeRel A n w) : (extOrderElim L C).IsExpansionOn (A ⊕ Fin n)

When the order variable is assigned the order of the instance, read in the extended universe, the extended structure over the bare vocabulary is an expansion along DescriptiveComplexity.extOrderElim of the extended structure over the ordered one.

The relativized linear-order guard

noncomputable def DescriptiveComplexity.extLinearGuard (L : FirstOrder.Language) (C : SOBlock) : ((newLang L).sum C.withOrder.lang).Sentence

The relativized guard: the order variable relates original elements only, and is a linear order on them. Relativization is forced by value invention: the order symbol of an extended structure relates original elements only, so an unrelativized guard would be unsatisfiable as soon as something is invented.

Equations

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

theorem DescriptiveComplexity.realize_extLinearGuard {L : FirstOrder.Language} {C : SOBlock} (A : Type) [L.Structure A] [Nonempty A] (n : ℕ) (ρ : C.withOrder.Assignment (A ⊕ Fin n)) : (A ⊕ Fin n) ⊨ extLinearGuard L C ↔ (∀ (x y : A ⊕ Fin n), ρ (Sum.inl ()) ![x, y] → IsOld x ∧ IsOld y) ∧ (∀ (x : A ⊕ Fin n), IsOld x → ρ (Sum.inl ()) ![x, x]) ∧ (∀ (x y z : A ⊕ Fin n), ρ (Sum.inl ()) ![x, y] → ρ (Sum.inl ()) ![y, z] → ρ (Sum.inl ()) ![x, z]) ∧ (∀ (x y : A ⊕ Fin n), ρ (Sum.inl ()) ![x, y] → ρ (Sum.inl ()) ![y, x] → x = y) ∧ ∀ (x y : A ⊕ Fin n), IsOld x → IsOld y → ρ (Sum.inl ()) ![x, y] ∨ ρ (Sum.inl ()) ![y, x]

Order elimination for ∃SO[new]

theorem DescriptiveComplexity.sigmaSONewDefinable_of_orderPull {L : FirstOrder.Language} {P : DecisionProblem L} (C : SOBlock) (ψ : (soLang (newLang (L.sum FirstOrder.Language.order)) [C]).Sentence) (h : ∀ (A : Type) [inst : L.Structure A] [Finite A] [inst_2 : Nonempty A], P.Holds A ↔ ∃ (lo : LinearOrder A) (n : ℕ), SORealize (newLang (L.sum FirstOrder.Language.order)) (A ⊕ Fin n) [C] ψ true) : SigmaSONewDefinable P

Order elimination for ∃SO[new]: a problem defined by an ∃SO[new] sentence over the ordered expansion – correct for some linear order on each instance – is ∃SO[new]-definable. The order becomes one more relation variable of the block, guarded by DescriptiveComplexity.extLinearGuard.

Closure under ordered FO reductions

theorem DescriptiveComplexity.SigmaSONewDefinable.of_orderedReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : OrderedFOReduction P Q) (h : SigmaSONewDefinable Q) : SigmaSONewDefinable P

∃SO[new]-definability is closed under ordered FO reductions: pull the definition back through the interpretation over the ordered expansion, then re-quantify the order inside the block, guarded by the relativized linear-order guard.