Ehrenfeucht–Fraïssé games on finite linear orders

Finite linear orders are structures in Mathlib's language of orders FirstOrder.Language.order, whose only symbol is the binary relation ≤, interpreted by the order of the type (Language.order.OrderedStructure). Duplicator wins the n-round Ehrenfeucht–Fraïssé game on two finite linear orders exactly when they have the same number of elements or both have at least 2 ^ n - 1 elements (duplicatorWins_iff_card). By the Ehrenfeucht–Fraïssé theorem, a sentence of quantifier rank n therefore has the same truth value in all finite linear orders with at least 2 ^ n - 1 elements (realize_iff_of_two_pow_le_card), and the bound cannot be lowered (exists_sentence_of_card_ne). In particular, EVEN is not first-order definable on finite linear orders, even when only orders above a size threshold are considered (not_exists_sentence_realize_iff_even).

Libkin states the sufficient condition with the threshold 2 ^ n for both orders; the sharp form proved here, with threshold 2 ^ n - 1 and its converse, is the characterization of n-equivalence of finite linear orders in Kolaitis's survey [Kol07]. Duplicator's strategy keeps every gap between consecutive pebbles (and the two virtual endpoints) either equal in both orders or at least 2 ^ r in both, r being the number of rounds left; Spoiler wins from any other position by splitting the longer of two different gaps.

Use in ordered descriptive complexity

Ordered descriptive complexity in this library follows Immerman: structures on Fin n carry the numeric vocabulary ≤, BIT, 0, 1, max (CslibFrontier.Logics.FirstOrder.Ordered.Basic). The results here concern the pure order vocabulary FO(≤). The constants 0, 1, max are FO(≤)-definable, but BIT is not: EVEN is defined in FO(≤, BIT) by the least significant bit of max, so the nondefinability of EVEN shows that BIT adds expressive power over ≤. To apply these results to a query on ordered structures, state it for Mathlib's Language.order (for example on Fin n with orderStructure), and use realize_iff_of_two_pow_le_card to show that no sentence has the required truth values on two large orders. The game itself (CslibFrontier.Logics.FirstOrder.EhrenfeuchtFraisse.Basic) is for relational vocabularies; numeric constants must first be replaced by their defining formulas.

Main results

• Cslib.Logic.FO.FiniteLinearOrder.duplicatorWins_iff_card: Duplicator wins the n-round game on two finite linear orders iff they have equal size or both have size at least 2 ^ n - 1.
• Cslib.Logic.FO.FiniteLinearOrder.realize_iff_of_two_pow_le_card: no sentence of quantifier rank at most n distinguishes two finite linear orders of size at least 2 ^ n - 1.
• Cslib.Logic.FO.FiniteLinearOrder.exists_sentence_of_card_ne: the bound is sharp.
• Cslib.Logic.FO.FiniteLinearOrder.not_exists_sentence_realize_iff_even: EVEN is not first-order definable on finite linear orders.

References

• P. G. Kolaitis, On the expressive power of logics on finite models, Chapter 2 of Finite Model Theory and Its Applications (the sharp characterization of n-equivalent finite linear orders).
• L. Libkin, Elements of Finite Model Theory, Chapter 3: Theorem 3.6 (linear orders of size at least 2 ^ n are indistinguishable in n rounds) and Corollary 3.12 (EVEN is not definable over orders).

Gaps

Coordinates

Positions

Extending a position

The game on linear orders

theorem Cslib.Logic.FO.FiniteLinearOrder.duplicatorWins_iff_card {M : Type u_1} {N : Type u_2} [LinearOrder M] [LinearOrder N] [FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M] [FirstOrder.Language.order.Structure N] [FirstOrder.Language.order.OrderedStructure N] [Finite M] [Finite N] {n : ℕ} {a : Fin 0 → M} {b : Fin 0 → N} : DuplicatorWins FirstOrder.Language.order n a b ↔ Nat.card M = Nat.card N ∨ 2 ^ n ≤ Nat.card M + 1 ∧ 2 ^ n ≤ Nat.card N + 1

Ehrenfeucht–Fraïssé games on finite linear orders [Kol07]. Duplicator wins the n-round game on two finite linear orders exactly when they have the same size or both have at least 2 ^ n - 1 elements.

theorem Cslib.Logic.FO.FiniteLinearOrder.realize_iff_of_two_pow_le_card {M : Type u_1} {N : Type u_2} [LinearOrder M] [LinearOrder N] [FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M] [FirstOrder.Language.order.Structure N] [FirstOrder.Language.order.OrderedStructure N] [Finite M] [Finite N] {n : ℕ} (hM : 2 ^ n ≤ Nat.card M + 1) (hN : 2 ^ n ≤ Nat.card N + 1) {φ : FirstOrder.Language.order.Sentence} (hφ : quantifierRank φ ≤ n) : M ⊨ φ ↔ N ⊨ φ

No first-order sentence of quantifier rank at most n distinguishes two finite linear orders with at least 2 ^ n - 1 elements each.

theorem Cslib.Logic.FO.FiniteLinearOrder.exists_sentence_of_card_ne {M : Type u_1} {N : Type u_2} [LinearOrder M] [LinearOrder N] [FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M] [FirstOrder.Language.order.Structure N] [FirstOrder.Language.order.OrderedStructure N] [Finite M] [Finite N] {n : ℕ} (hne : Nat.card M ≠ Nat.card N) (h : Nat.card M + 1 < 2 ^ n ∨ Nat.card N + 1 < 2 ^ n) : ∃ (φ : FirstOrder.Language.order.Sentence), quantifierRank φ ≤ n ∧ M ⊨ φ ∧ ¬N ⊨ φ

The bound is sharp: two finite linear orders of different sizes, one of them with fewer than 2 ^ n - 1 elements, are distinguished by a sentence of quantifier rank at most n.

theorem Cslib.Logic.FO.FiniteLinearOrder.not_exists_sentence_realize_iff_even (t : ℕ) : ¬∃ (φ : FirstOrder.Language.order.Sentence), ∀ (M : Type) [inst : LinearOrder M] [Finite M] [inst_2 : FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M], t ≤ Nat.card M → (M ⊨ φ ↔ Even (Nat.card M))

EVEN is not first-order definable on finite linear orders [Lib04]: for every size threshold t, no sentence in the language of orders holds in exactly those finite linear orders with at least t elements that have an even number of elements.