The game on finite linear orders

Ehrenfeucht's theorem (Ehrenfeucht 1961; Ebbinghaus–Flum 1995, ch. 2): two finite linear orders with at least 2 ^ n elements each are n-round equivalent (DescriptiveComplexity.efEquiv_linearOrder), whatever their sizes. First-order logic can therefore count the elements of an ordered set no further than exponentially in its quantifier rank – and, since the bound depends on the sentence only, not at all in the limit.

This is the order-invariant half of the inexpressibility of DescriptiveComplexity.EVEN, and the reason it is a real theorem rather than the observation that a bare set carries no information: here the structure carries all the information about the position of every point, and the duplicator still wins.

The strategy

A position is read through the ranks of its points (DescriptiveComplexity.orank, the number of strict predecessors, shared with the order-walk machinery) and two sentinels, -1 below everything and the cardinality above everything (DescriptiveComplexity.extRank); the duplicator's invariant (DescriptiveComplexity.OrdInv) is then one equation per pair of points: their distances agree up to truncation at 2 ^ n (DescriptiveComplexity.truncAt). The sentinels are what makes it one equation: the distance to the ends of the order is the distance to a point like any other.

Everything the invariant is used for is arithmetic and lives in DescriptiveComplexity.Games.Distance, in particular the answer to a move (DescriptiveComplexity.exists_answer), where the budget halves. What is left here is the translation between the game and the arithmetic: a position is legal exactly when the ranks are in the same order, and a round is one application of the answer lemma.

The invariant

noncomputable def DescriptiveComplexity.extRank {A : Type} [LinearOrder A] {j : ℕ} (a : Fin j → A) : Fin j ⊕ Bool → ℤ

The ranks of a position, extended by two sentinels: -1, below every element, and the cardinality, above every element. The distances to the two ends of the order thereby become distances between points, so that the whole invariant is one equation.

Equations

• DescriptiveComplexity.extRank a (Sum.inl i) = ↑(DescriptiveComplexity.orank (a i))
• DescriptiveComplexity.extRank a (Sum.inr false) = -1
• DescriptiveComplexity.extRank a (Sum.inr true) = ↑(Nat.card A)

def DescriptiveComplexity.OrdInv {A B : Type} [LinearOrder A] [LinearOrder B] {j : ℕ} (n : ℕ) (a : Fin j → A) (b : Fin j → B) : Prop

The duplicator's invariant on two finite linear orders: any two points of the position – sentinels included – are at the same distance on both sides, up to truncation at 2 ^ n.

Equations

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

theorem DescriptiveComplexity.OrdInv.symm {A B : Type} [LinearOrder A] [LinearOrder B] {j n : ℕ} {a : Fin j → A} {b : Fin j → B} (h : OrdInv n a b) : OrdInv n b a

The invariant is symmetric.

theorem DescriptiveComplexity.OrdInv.mono {A B : Type} [LinearOrder A] [LinearOrder B] {j n : ℕ} {a : Fin j → A} {b : Fin j → B} {m : ℕ} (hmn : m ≤ n) (h : OrdInv n a b) : OrdInv m a b

The invariant weakens as the budget is spent.

One round

theorem DescriptiveComplexity.extRank_snoc_lift {A : Type} [LinearOrder A] {j : ℕ} (a : Fin j → A) (c : A) (i : Fin j ⊕ Bool) : extRank (Fin.snoc a c) (Sum.map Fin.castSucc id i) = extRank a i

The extended tuple of a position lengthened by one point, at an old coordinate.

theorem DescriptiveComplexity.extRank_snoc_last {A : Type} [LinearOrder A] {j : ℕ} (a : Fin j → A) (c : A) : extRank (Fin.snoc a c) (Sum.inl (Fin.last j)) = ↑(orank c)

The extended tuple of a position lengthened by one point, at the new coordinate.

theorem DescriptiveComplexity.extIndex_cases {j : ℕ} (i : Fin (j + 1) ⊕ Bool) : (∃ (i₀ : Fin j ⊕ Bool), i = Sum.map Fin.castSucc id i₀) ∨ i = Sum.inl (Fin.last j)

An extended coordinate of a lengthened position is either an old one or the new one.

theorem DescriptiveComplexity.ordInv_default {A B : Type} [LinearOrder A] [LinearOrder B] (n : ℕ) (hA : 2 ^ n ≤ Nat.card A) (hB : 2 ^ n ≤ Nat.card B) : OrdInv n default default

The empty position satisfies the invariant as soon as both orders have at least 2 ^ n elements: the only distance to check is the one between the two sentinels, and it is beyond the truncation on both sides.

theorem DescriptiveComplexity.exists_ordInv_snoc {A B : Type} [LinearOrder A] [LinearOrder B] {j n : ℕ} {a : Fin j → A} {b : Fin j → B} [Finite A] [Finite B] (h : OrdInv (n + 1) a b) (c : A) : ∃ (d : B), OrdInv n (Fin.snoc a c) (Fin.snoc b d)

One round of the game: whatever point the spoiler adds on the left, the duplicator has an answer on the right keeping the invariant, at the cost of one unit of budget. The answer is computed in the integers (DescriptiveComplexity.exists_answer) and comes back into the structure because it lands strictly between the two sentinels.

The game

theorem DescriptiveComplexity.partialIso_of_ordInv {A B : Type} [LinearOrder A] [LinearOrder B] {j n : ℕ} {a : Fin j → A} {b : Fin j → B} [Finite A] [Finite B] [FirstOrder.Language.empty.Structure A] [FirstOrder.Language.empty.Structure B] (h : OrdInv n a b) : PartialIso (FirstOrder.Language.empty.sum FirstOrder.Language.order) a b

A position satisfying the invariant is legal: the equalities between coordinates and the order between them are read off the ranks, which the invariant preserves.

theorem DescriptiveComplexity.efStage_of_ordInv {A B : Type} [LinearOrder A] [LinearOrder B] [Finite A] [Finite B] [FirstOrder.Language.empty.Structure A] [FirstOrder.Language.empty.Structure B] (n : ℕ) {j : ℕ} (a : Fin j → A) (b : Fin j → B) : OrdInv n a b → efStage (FirstOrder.Language.empty.sum FirstOrder.Language.order) n a b

The duplicator survives on a line: a position satisfying the invariant with budget n survives n rounds.

Ehrenfeucht's theorem

theorem DescriptiveComplexity.efEquiv_linearOrder {A B : Type} [FirstOrder.Language.empty.Structure A] [FirstOrder.Language.empty.Structure B] [LinearOrder A] [LinearOrder B] [Finite A] [Finite B] (n : ℕ) (hA : 2 ^ n ≤ Nat.card A) (hB : 2 ^ n ≤ Nat.card B) : EFEquiv (FirstOrder.Language.empty.sum FirstOrder.Language.order) A B n

Ehrenfeucht's theorem: two finite linear orders with at least 2 ^ n elements each are n-round equivalent, however far apart their sizes. By the methodology lemma (DescriptiveComplexity.realize_sentence_of_efEquiv) a sentence of quantifier rank n over the ordered vocabulary cannot separate them: first-order logic counts the elements of an ordered set only up to 2 ^ n.