The defining sentence of the order on an expanded universe

DescriptiveComplexity.Exponential.Order orders the points of an expansion – tag first, then the assignment read as a binary number. This file writes that order down as a first-order sentence over the base vocabulary and two copies of the block, and proves it defines exactly that order (DescriptiveComplexity.SOBlock.realize_ordLtF).

Everything is first-order because a padded atom is a relation variable – of which there are finitely many, so the choice is a static disjunction – together with a tuple of base elements, which an ordinary quantifier can range over. The sentence says:

at some atom, the first copy is false and the second true, while the two copies agree at every strictly smaller atom

and “strictly smaller” splits into the two ways DescriptiveComplexity.SOBlock.atomIx_lt_iff allows: a strictly earlier relation variable – a static condition, so a finite conjunction – or the same variable at a lexicographically earlier tuple, which is DescriptiveComplexity.lexSelLtF.

The three quantifier blocks over Fin (blockArityBound B) are Formula.iExs and Formula.iAlls, so the free-variable bookkeeping is Sum.inr for the innermost tuple and Sum.inl ∘ Sum.inr for the one bound outside it.

An enumeration of the relation variables

noncomputable def DescriptiveComplexity.SOBlock.ivars (B : SOBlock) : List B.ι

The relation variables of a block, as a list: the finite disjunction and conjunction of the comparison sentence range over it.

Equations

• B.ivars = Finset.univ.toList

theorem DescriptiveComplexity.SOBlock.mem_ivars (B : SOBlock) (i : B.ι) : i ∈ B.ivars

The atom of one copy

noncomputable def DescriptiveComplexity.SOBlock.atomF (L : FirstOrder.Language) (B : SOBlock) (c : Fin 2) (i : B.ι) {γ : Type} (sel : Fin (blockArityBound B) → γ) : ((L.sum FirstOrder.Language.order).sum (B.replicate 2).lang).Formula γ

The atom “copy c of the block holds of the tuple selected by sel”: the relation variable i of that copy, applied to the first B.arity i of the selected variables.

Equations

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

theorem DescriptiveComplexity.SOBlock.realize_atomF {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] [LinearOrder A] (ρs : Fin 2 → B.Assignment A) (c : Fin 2) (i : B.ι) {γ : Type} (sel : Fin (blockArityBound B) → γ) (v : γ → A) : (atomF L B c i sel).Realize v ↔ B.atomSet (ρs c) (i, fun (k : Fin (blockArityBound B)) => v (sel k))

The atom says what it should: the copy's assignment, at the padded atom the selected variables name.

noncomputable def DescriptiveComplexity.SOBlock.ivarsBelow (B : SOBlock) (i : B.ι) : List B.ι

The relation variables strictly below i, in the arbitrary order on the block's index type. Factored out so that the order on B.ι – the one thing in the comparison sentence that is resolved statically – is confined to this definition and its characterization, and the sentence itself never has to be unfolded past them.

Equations

• B.ivarsBelow i = List.filter (fun (j : B.ι) => decide (j < i)) B.ivars

theorem DescriptiveComplexity.SOBlock.mem_ivarsBelow (B : SOBlock) (i j : B.ι) : j ∈ B.ivarsBelow i ↔ j < i

The comparison sentence

noncomputable def DescriptiveComplexity.SOBlock.ordLtF (L : FirstOrder.Language) (B : SOBlock) : ((L.sum FirstOrder.Language.order).sum (B.replicate 2).lang).Sentence

The defining sentence of the order on an expanded universe: at some padded atom the first copy is false and the second true, and the two copies agree at every strictly smaller atom – at every earlier relation variable (statically many), and at the same variable on every lexicographically earlier tuple.

Equations

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

Correctness

theorem DescriptiveComplexity.SOBlock.agree_below_iff (B : SOBlock) {A : Type} [LinearOrder A] (ρs : Fin 2 → B.Assignment A) (i : B.ι) (x : Fin (blockArityBound B) → A) : ((∀ j ∈ B.ivarsBelow i, ∀ (y : Fin (blockArityBound B) → A), B.atomSet (ρs 0) (j, y) ↔ B.atomSet (ρs 1) (j, y)) ∧ ∀ (y : Fin (blockArityBound B) → A), toLex y < toLex x → (B.atomSet (ρs 0) (i, y) ↔ B.atomSet (ρs 1) (i, y))) ↔ ∀ (q : B.AtomIx A), B.atomLt q (i, x) → (B.atomSet (ρs 0) q ↔ B.atomSet (ρs 1) q)

The two agreement conjuncts of the sentence say exactly “the copies agree strictly below the witnessed atom”, by DescriptiveComplexity.SOBlock.atomIx_lt_iff: an atom is below (i, x) either at a strictly earlier relation variable, or at i on a lexicographically earlier tuple.

theorem DescriptiveComplexity.SOBlock.realize_ordLtF {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ρs : Fin 2 → B.Assignment A) : A ⊨ ordLtF L B ↔ B.atomSet (ρs 0) < B.atomSet (ρs 1)

The comparison sentence is the order: it holds of two assignments exactly when the first is below the second in the binary-number order on their padded atoms.

From the strict order to ≤

An expansion defines its order by the symbol leSymb, so what DescriptiveComplexity.ExpExpansion.ordExtend needs is the reflexive comparison. Equality of assignments is definable in the same breath – the two copies hold of exactly the same padded atoms – and ≤ is the disjunction.

noncomputable def DescriptiveComplexity.SOBlock.eqAssignF (L : FirstOrder.Language) (B : SOBlock) : ((L.sum FirstOrder.Language.order).sum (B.replicate 2).lang).Sentence

The two copies of the block hold of exactly the same padded atoms.

Equations

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

theorem DescriptiveComplexity.SOBlock.realize_eqAssignF {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] [LinearOrder A] (ρs : Fin 2 → B.Assignment A) : A ⊨ eqAssignF L B ↔ B.atomSet (ρs 0) = B.atomSet (ρs 1)

noncomputable def DescriptiveComplexity.SOBlock.ordLeF (L : FirstOrder.Language) (B : SOBlock) : ((L.sum FirstOrder.Language.order).sum (B.replicate 2).lang).Sentence

The reflexive comparison of two assignments: strictly below, or equal.

Equations

• DescriptiveComplexity.SOBlock.ordLeF L B = DescriptiveComplexity.SOBlock.ordLtF L B ⊔ DescriptiveComplexity.SOBlock.eqAssignF L B

theorem DescriptiveComplexity.SOBlock.realize_ordLeF {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ρs : Fin 2 → B.Assignment A) : A ⊨ ordLeF L B ↔ B.atomSet (ρs 0) ≤ B.atomSet (ρs 1)