Scott analysis of dense linear orders

Dense linear orders without endpoints, the models of Mathlib's first-order theory Language.order.dlo, are the basic example of back-and-forth: by Cantor's argument (Mathlib's dlo_isExtensionPair) every finite order-preserving partial map extends to any new point. In the language of back-and-forth equivalence this gives, for structures of every cardinality:

• between two nonempty dense linear orders without endpoints, tuples are back-and-forth equivalent at every level exactly when they have the same order type, and the two orders are potentially isomorphic;
• every dense linear order without endpoints, including the empty one, has internal Scott rank one;
• the Scott sentence of a countable nonempty dense linear order without endpoints, such as ℚ, is satisfied exactly by the nonempty models of Language.order.dlo, in every cardinality.

For countable structures potential isomorphism is isomorphism (TauCeti.countable_potentialIso_iff_iso), so the first item refines Cantor's ℵ₀-categoricity (Mathlib's aleph0_categorical_dlo). For uncountable orders it is strictly weaker, even in a single cardinality: the lexicographic product ω₁ ×ₗ ℚ of ω₁ copies of ℚ and its order dual are nonempty dense linear orders without endpoints of cardinality ℵ₁, hence potentially isomorphic and L∞ω-equivalent, but they are not isomorphic, because the first has cofinality ℵ₁ and the second has cofinality ℵ₀.

Main results

• TauCeti.dlo_isExtensionPair_self: the self-extension property, with no nonemptiness assumption.
• TauCeti.bfEquiv_iff_sameAtomicType_of_dlo and TauCeti.potentialIso_of_dlo.
• TauCeti.internalScottRank_eq_one_of_dlo.
• TauCeti.realize_scottSentence_iff_of_dlo.
• TauCeti.isEmpty_equiv_orderDual_toType_omega_one_lex_rat and TauCeti.exists_dlo_aleph_one_potentialIso_isEmpty_equiv: two dense linear orders without endpoints of cardinality ℵ₁ that are potentially isomorphic but not isomorphic.

References

• Georg Cantor, Beiträge zur Begründung der transfiniten Mengenlehre, 1895.
• Dana Scott, Logic with denumerably long formulas and finite strings of quantifiers, 1965.
• Carol Karp, Finite-quantifier equivalence, in The Theory of Models, 1965.

theorem TauCeti.dlo_isExtensionPair_self (M : Type w) [FirstOrder.Language.order.Structure M] [M ⊨ FirstOrder.Language.order.dlo] : FirstOrder.Language.order.IsExtensionPair M M

A dense linear order without endpoints has the self-extension property. Unlike Mathlib's dlo_isExtensionPair, no nonemptiness is assumed: for an empty order it holds vacuously.

@[simp]

theorem TauCeti.internalScottRank_eq_one_of_dlo (M : Type w) [FirstOrder.Language.order.Structure M] [M ⊨ FirstOrder.Language.order.dlo] : internalScottRank M = 1

Every dense linear order without endpoints, of any cardinality and including the empty one, has internal Scott rank one.

theorem TauCeti.bfEquiv_iff_sameAtomicType_of_dlo (M : Type w) [FirstOrder.Language.order.Structure M] [M ⊨ FirstOrder.Language.order.dlo] [Nonempty M] (N : Type w') [FirstOrder.Language.order.Structure N] [N ⊨ FirstOrder.Language.order.dlo] [Nonempty N] {α : Ordinal.{o}} {n : ℕ} {a : Fin n → M} {b : Fin n → N} : BFEquiv α n a b ↔ SameAtomicType a b

Between nonempty dense linear orders without endpoints, tuples are back-and-forth equivalent at any level exactly when they have the same order type.

theorem TauCeti.potentialIso_of_dlo (M : Type w) [FirstOrder.Language.order.Structure M] [M ⊨ FirstOrder.Language.order.dlo] [Nonempty M] (N : Type w') [FirstOrder.Language.order.Structure N] [N ⊨ FirstOrder.Language.order.dlo] [Nonempty N] : PotentialIso M N

Any two nonempty dense linear orders without endpoints are potentially isomorphic, whatever their cardinalities.

theorem TauCeti.realize_scottSentence_iff_of_dlo (M : Type w) [FirstOrder.Language.order.Structure M] [M ⊨ FirstOrder.Language.order.dlo] [Nonempty M] [Countable M] (N : Type w') [FirstOrder.Language.order.Structure N] : FirstOrder.Language.SentenceInf.Realize (scottSentence M) N ↔ Nonempty N ∧ N ⊨ FirstOrder.Language.order.dlo

The Scott sentence of a countable nonempty dense linear order without endpoints holds in a structure of any cardinality exactly when that structure is a nonempty dense linear order without endpoints.

theorem TauCeti.isEmpty_equiv_orderDual_toType_omega_one_lex_rat : IsEmpty (FirstOrder.Language.order.Equiv (Lex ((Ordinal.omega 1).ToType × ℚ)) (Lex ((Ordinal.omega 1).ToType × ℚ))ᵒᵈ)

The lexicographic product ω₁ ×ₗ ℚ is not isomorphic, as a structure in the language of orders, to its order dual: it has cofinality ℵ₁, while its order dual has cofinality ℵ₀.

theorem TauCeti.exists_dlo_aleph_one_potentialIso_isEmpty_equiv : ∃ (M : Type w) (N : Type w) (x : FirstOrder.Language.order.Structure M) (x_1 : FirstOrder.Language.order.Structure N), M ⊨ FirstOrder.Language.order.dlo ∧ N ⊨ FirstOrder.Language.order.dlo ∧ Cardinal.mk M = Cardinal.aleph 1 ∧ Cardinal.mk N = Cardinal.aleph 1 ∧ PotentialIso M N ∧ InfEquivW M N ∧ IsEmpty (FirstOrder.Language.order.Equiv M N)

Potential isomorphism, and hence L∞ω-equivalence, does not imply isomorphism for uncountable structures of the same cardinality: in every universe there are two dense linear orders without endpoints of cardinality ℵ₁ that are potentially isomorphic, and so L∞ω-equivalent (TauCeti.InfEquivW), but not isomorphic. The witnesses are ω₁ ×ₗ ℚ and its order dual.