Documentation

DescriptiveComplexity.Games.LinearOrder

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 #

source
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
Instances For
    Dependency graph

    One round #

    The game #

    Ehrenfeucht's theorem #

    source
    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. Registered in the Lax archive as Lax945089.GamesOnLinearOrders.efEquiv_linearOrder.

    Dependency graph