Extending an expansion with its own order

DescriptiveComplexity.ExpExpansion.ordExtend adds the order symbol to the expanded vocabulary, defined by the sentence of DescriptiveComplexity.Exponential.OrdFormula, and DescriptiveComplexity.ExpExpansion.ordExtendLEquiv says the result is exactly the original expansion carrying DescriptiveComplexity.ExpExpansion.mapLinearOrder.

This is the analogue, one level up, of DescriptiveComplexity.FOInterpretation.ordExtend and its ordExtendLEquiv, and it plays the same role: an interpretation whose formulas mention the order of the structure they read can only be composed with an expansion once that expansion defines its order. It is the prerequisite of the outer composition that is about the order rather than about quantifiers.

The tag comparison is static, exactly as in DescriptiveComplexity.lexLeF: two points with different tags are ordered by their tags alone, so the defining sentence at such a pair is ⊤ or ⊥, and only the equal-tag case emits a real comparison.

The defining sentence of the order

noncomputable def DescriptiveComplexity.ExpExpansion.ordSentence {L : FirstOrder.Language} (X : ExpExpansion L) (t₁ t₂ : X.Tag) : ((L.sum FirstOrder.Language.order).sum (X.B.replicate 2).lang).Sentence

The defining sentence of the order at a pair of tags: the tags are compared statically, and at equal tags the assignments are compared as binary numbers.

Equations

• X.ordSentence t₁ t₂ = if t₁ = t₂ then DescriptiveComplexity.SOBlock.ordLeF L X.B else if t₁ < t₂ then ⊤ else ⊥

theorem DescriptiveComplexity.ExpExpansion.realize_ordSentence {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (t₁ t₂ : X.Tag) (ρs : Fin 2 → X.B.Assignment A) : A ⊨ X.ordSentence t₁ t₂ ↔ (t₁, ρs 0) ≤ (t₂, ρs 1)

The defining sentence is the order on points.

The extended expansion

noncomputable def DescriptiveComplexity.ExpExpansion.ordExtend {L : FirstOrder.Language} {X : ExpExpansion L} : ExpExpansion L

The expansion extended with its own order: the tags, the block and the domain are unchanged, the expanded vocabulary gains the order symbol, and that symbol is defined by DescriptiveComplexity.ExpExpansion.ordSentence.

Equations

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

@[instance_reducible]

noncomputable def DescriptiveComplexity.ExpExpansion.ordExtendStructure {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [L.Structure A] [LinearOrder A] : (X.E.sum FirstOrder.Language.order).Structure (ordExtend.Map A)

The expanded structure of the order extension, at the vocabulary written as a sum – equal to the extension's own by definition, but not syntactically, so instance search has to be handed it.

Equations

• X.ordExtendStructure A = DescriptiveComplexity.ExpExpansion.ordExtend.mapStructure A

noncomputable def DescriptiveComplexity.ExpExpansion.ordExtendLEquiv {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (X.E.sum FirstOrder.Language.order).Equiv (ordExtend.Map A) (X.Map A)

The extension produces exactly the original expanded structure equipped with its order: the identity map is an isomorphism over the order-expanded vocabulary.

Equations

• X.ordExtendLEquiv A = { toEquiv := Equiv.refl (DescriptiveComplexity.ExpExpansion.ordExtend.Map A), map_fun' := ⋯, map_rel' := ⋯ }