Ordered structures from the order of a type, and non-well-founded models

Mathlib's FirstOrder.Language.orderStructure makes a type with ≤ a structure in the language of orders, but it is not an instance, and neither it nor a structure in an expanded language L.sum Language.order is known to be an OrderedStructure. This file supplies both instances. Thus, after installing orderStructure M and an L-structure on M, for example FirstOrder.Ring.compatibleRingOfRing M for the language of rings, the expanded structure on M interprets ≤ as the order of M, and results stated for ordered structures apply to it.

It also shows that well-foundedness is not first-order: every first-order theory of an infinite linear order has a countable model that is not well-ordered. An infinite linear order contains a strictly monotone or strictly antitone sequence, so in an ultraproduct over a nonprincipal ultrafilter on ℕ its shifted copies form a strictly decreasing sequence, and by Łoś's theorem the ultraproduct is still a model. A countable elementary substructure containing this sequence, given by the downward Löwenheim–Skolem theorem, is the required model. Consequently, for an infinite countable well-order M, no first-order theory has, among countable structures, exactly the copies of M as its models.

Main results

• TauCeti.exists_countable_model_not_wellFoundedLT: every first-order theory of an infinite linear order has a countable model that is a linear order but not a well-order.
• TauCeti.not_exists_theory_model_iff_nonempty_orderIso: for an infinite countable well-order M, no first-order theory has as countable models exactly the orders isomorphic to M.

instance FirstOrder.Language.orderedStructure_orderStructure (M : Type u_2) [LE M] : Language.order.OrderedStructure M

The order structure of a type interprets the order symbol ≤ as the order of the type.

instance FirstOrder.Language.orderedStructure_sum {L : Language} {M : Type u_1} [L.Structure M] [LE M] [Language.order.Structure M] [Language.order.OrderedStructure M] : (L.sum Language.order).OrderedStructure M

Expanding a language by the order symbol preserves the interpretation of ≤.

theorem TauCeti.exists_countable_model_not_wellFoundedLT (T : FirstOrder.Language.order.Theory) (M : Type w) [FirstOrder.Language.order.Structure M] [LinearOrder M] [FirstOrder.Language.order.OrderedStructure M] [Infinite M] [M ⊨ T] : ∃ (N : Type w) (x : FirstOrder.Language.order.Structure N) (x_1 : LinearOrder N) (_ : FirstOrder.Language.order.OrderedStructure N), Countable N ∧ N ⊨ T ∧ ¬WellFoundedLT N

Well-foundedness is not first-order. Every first-order theory in the language of orders that holds in an infinite linear order has a countable model that is a linear order, in the same universe, but not a well-order.

theorem TauCeti.not_exists_theory_model_iff_nonempty_orderIso (M : Type w) [LinearOrder M] [WellFoundedLT M] [Infinite M] [Countable M] : ¬∃ (T : FirstOrder.Language.order.Theory), ∀ (N : Type w) [inst : FirstOrder.Language.order.Structure N] [inst_1 : LE N] [FirstOrder.Language.order.OrderedStructure N] [Countable N], N ⊨ T ↔ Nonempty (M ≃o N)

Infinite well-orders are not first-order axiomatizable among countable structures. For an infinite countable well-order M, no first-order theory in the language of orders has as its countable models, in the universe of M, exactly the orders isomorphic to M. Contrast TauCeti.exists_sentenceω_realize_iff_nonempty_orderIso in TauCeti.ModelTheory.Scott.WellOrder, which gives a single Lω₁ω sentence with this property.