Back-and-forth for discrete linear orders without endpoints

A discrete linear order without endpoints is a linear order in which every element has an immediate successor and an immediate predecessor and there is no least or greatest element; in Mathlib terms, a linear order with SuccOrder, PredOrder, NoMaxOrder and NoMinOrder. The integers ℤ are the basic example, and so is ℤ ⊕ₗ ℤ, two copies of ℤ one after the other.

Any two nonempty discrete linear orders without endpoints are back-and-forth equivalent at every finite level, hence elementarily equivalent. The proof is the classical Ehrenfeucht–Fraïssé argument: at level k it suffices that the entries of two tuples compare in the same way after shifting each of them by at most 4 ^ k successor steps. A new element within 4 ^ (k - 1) steps of an old entry is answered at the same offset from the matching entry, and an element far from every old entry is answered by an element far from every matching entry, in the same gap.

These orders are not all isomorphic, even among countable ones: ℤ and ℤ ⊕ₗ ℤ are countable, elementarily equivalent and not isomorphic, since every bounded interval of ℤ is finite while the interval between the two copies of 0 in ℤ ⊕ₗ ℤ is infinite. By Karp's theorem for countable structures they are therefore not even L_{ω₁ω}-equivalent: elementary equivalence is strictly weaker than infinitary equivalence.

The same pair shows that winning Ehrenfeucht–Fraïssé strategies for every finite length, chosen separately, need not assemble into one coherent strategy for the infinite game: Duplicator wins every finite game between ℤ and ℤ ⊕ₗ ℤ, but has no coherent infinite strategy, since such a strategy would make them potentially isomorphic.

Main results

• TauCeti.sameAtomicType_order_iff: in the language of orders, two tuples have the same atomic type exactly when they have the same equalities and order relations between their entries.
• TauCeti.bfEquiv_omega0_of_succOrder_of_predOrder: nonempty discrete linear orders without endpoints are back-and-forth equivalent at level ω.
• TauCeti.elementarilyEquivalent_of_succOrder_of_predOrder: nonempty discrete linear orders without endpoints are elementarily equivalent.
• TauCeti.nonempty_efStrategy_family_of_succOrder_of_predOrder: Duplicator wins every finite Ehrenfeucht–Fraïssé game between nonempty discrete linear orders without endpoints.
• TauCeti.isEmpty_equiv_int_sumLex_int, TauCeti.elementarilyEquivalent_int_sumLex_int and TauCeti.not_infEquivAt_nat_int_sumLex_int: ℤ and ℤ ⊕ₗ ℤ are elementarily equivalent but neither isomorphic nor L_{ω₁ω}-equivalent.
• TauCeti.not_potentialIso_int_sumLex_int and TauCeti.isEmpty_coherentEFStrategy_int_sumLex_int: ℤ and ℤ ⊕ₗ ℤ are not potentially isomorphic, so Duplicator has no coherent strategy for the infinite Ehrenfeucht–Fraïssé game between them.

References

• Andrzej Ehrenfeucht, An application of games to the completeness problem for formalized theories, Fundamenta Mathematicae 49, 1961.
• Wilfrid Hodges, Model Theory, Cambridge University Press, 1993, Section 3.3.
• David Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016.

theorem TauCeti.sameAtomicType_order_iff {M : Type w} {N : Type w'} [LE M] [LE N] [FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M] [FirstOrder.Language.order.Structure N] [FirstOrder.Language.order.OrderedStructure N] {n : ℕ} (a : Fin n → M) (b : Fin n → N) : SameAtomicType a b ↔ (∀ (i j : Fin n), a i = a j ↔ b i = b j) ∧ ∀ (i j : Fin n), a i ≤ a j ↔ b i ≤ b j

In the language of orders, two tuples have the same atomic type exactly when they have the same equalities and the same order relations between their entries.

theorem TauCeti.bfEquiv_omega0_of_succOrder_of_predOrder (M : Type w) (N : Type w') [LinearOrder M] [SuccOrder M] [LinearOrder N] [SuccOrder N] [NoMaxOrder M] [NoMaxOrder N] [PredOrder N] [NoMinOrder N] [PredOrder M] [NoMinOrder M] [FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M] [FirstOrder.Language.order.Structure N] [FirstOrder.Language.order.OrderedStructure N] [Nonempty M] [Nonempty N] : BFEquiv Ordinal.omega0 0 Fin.elim0 Fin.elim0

Discrete linear orders without endpoints are back-and-forth equivalent at level ω. In any two nonempty linear orders with successors and predecessors and without endpoints, the empty tuples are back-and-forth equivalent at every finite level.

theorem TauCeti.elementarilyEquivalent_of_succOrder_of_predOrder (M : Type w) (N : Type w') [LinearOrder M] [SuccOrder M] [LinearOrder N] [SuccOrder N] [NoMaxOrder M] [NoMaxOrder N] [PredOrder N] [NoMinOrder N] [PredOrder M] [NoMinOrder M] [FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M] [FirstOrder.Language.order.Structure N] [FirstOrder.Language.order.OrderedStructure N] [Nonempty M] [Nonempty N] : FirstOrder.Language.order.ElementarilyEquivalent M N

Discrete linear orders without endpoints are elementarily equivalent. Any two nonempty linear orders with successors and predecessors and without endpoints satisfy the same first-order sentences in the language of orders.

theorem TauCeti.nonempty_efStrategy_family_of_succOrder_of_predOrder (M : Type w) (N : Type w') [LinearOrder M] [SuccOrder M] [LinearOrder N] [SuccOrder N] [NoMaxOrder M] [NoMaxOrder N] [PredOrder N] [NoMinOrder N] [PredOrder M] [NoMinOrder M] [FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M] [FirstOrder.Language.order.Structure N] [FirstOrder.Language.order.OrderedStructure N] [Nonempty M] [Nonempty N] : Nonempty ((k : ℕ) → EFStrategy FirstOrder.Language.order k Fin.elim0 Fin.elim0)

Duplicator wins every finite Ehrenfeucht–Fraïssé game between discrete linear orders without endpoints. In any two nonempty linear orders with successors and predecessors and without endpoints, Duplicator has a winning strategy from the empty position for each finite number of rounds. The strategies for different lengths are not required to be compatible.

theorem TauCeti.isEmpty_equiv_int_sumLex_int : IsEmpty (FirstOrder.Language.order.Equiv ℤ (ℤ ⊕ₗ ℤ))

ℤ and ℤ ⊕ₗ ℤ are not isomorphic as orders: the interval between the two copies of 0 in ℤ ⊕ₗ ℤ is infinite, while every bounded interval of ℤ is finite.

theorem TauCeti.elementarilyEquivalent_int_sumLex_int : FirstOrder.Language.order.ElementarilyEquivalent ℤ (ℤ ⊕ₗ ℤ)

ℤ and ℤ ⊕ₗ ℤ satisfy the same first-order sentences in the language of orders.

theorem TauCeti.not_infEquivAt_nat_int_sumLex_int : ¬InfEquivAt ℕ ℤ (ℤ ⊕ₗ ℤ)

Elementary equivalence is strictly weaker than infinitary equivalence. The countable orders ℤ and ℤ ⊕ₗ ℤ are elementarily equivalent (elementarilyEquivalent_int_sumLex_int), but some L_{ω₁ω} sentence distinguishes them. A fortiori they are not L_{∞ω}-equivalent, since TauCeti.InfEquivW.infEquivAt turns L_{∞ω}-equivalence into agreement at ℕ.

theorem TauCeti.not_potentialIso_int_sumLex_int : ¬PotentialIso ℤ (ℤ ⊕ₗ ℤ)

ℤ and ℤ ⊕ₗ ℤ are not potentially isomorphic as orders, although they are back-and-forth equivalent at level ω (bfEquiv_omega0_of_succOrder_of_predOrder).

theorem TauCeti.isEmpty_coherentEFStrategy_int_sumLex_int : IsEmpty (CoherentEFStrategy FirstOrder.Language.order Fin.elim0 Fin.elim0)

Finite strategies do not assemble into a coherent infinite strategy. Duplicator has no coherent winning strategy for the infinite Ehrenfeucht–Fraïssé game between ℤ and ℤ ⊕ₗ ℤ, although by nonempty_efStrategy_family_of_succOrder_of_predOrder Duplicator wins the game of every finite length. Thus level-ω back-and-forth equivalence, which says exactly that a winning strategy exists for each finite length separately, does not give a coherent strategy.