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 #

source

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

Instances For

Dependency graph

The atom of one copy #

source

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.

Instances For

Dependency graph

source

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

Instances For

Dependency graph

The comparison sentence #

source

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.

Instances For

Dependency graph

Correctness #

source

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.

Dependency graph

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.

source