Ordered First-Ordered Structures #
This file defines ordered first-order languages and structures, as well as their theories.
Main Definitions #
FirstOrder.Language.order
is the language consisting of a single relation representing≤
.FirstOrder.Language.IsOrdered
points out a specific symbol in a language as representing≤
.FirstOrder.Language.OrderedStructure
indicates that the≤
symbol in an ordered language is interpreted as the actual relation≤
in a particular structure.FirstOrder.Language.linearOrderTheory
and similar define the theories of preorders, partial orders, and linear orders.FirstOrder.Language.dlo
defines the theory of dense linear orders without endpoints, a particularly useful example in model theory.FirstOrder.Language.orderStructure
is the structure on an ordered type, assigning the symbol representing≤
to the actual relation≤
.- Conversely,
FirstOrder.Language.LEOfStructure
,FirstOrder.Language.preorderOfModels
,FirstOrder.Language.partialOrderOfModels
, andFirstOrder.Language.linearOrderOfModels
are the orders induced by first-order structures modelling the relevant theory.
Main Results #
PartialOrder
s model the theory of partial orders,LinearOrder
s model the theory of linear orders, and dense linear orders without endpoints modelLanguage.dlo
.- Under
L.orderedStructure
assumptions, elements of anyL.HomClass M N
are monotone, and strictly monotone if injective. - Under
Language.order.orderedStructure
assumptions, anyOrderHomClass
has an instance ofL.HomClass M N
, whileM ↪o N
and anyOrderIsoClass
have an instance ofL.StrongHomClass M N
. FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo
shows that any countable nonempty model of the theory of linear orders is a Fraïssé limit of the class of finite models of the theory of linear orders.FirstOrder.Language.isFraisse_finite_linear_order
shows that the class of finite models of the theory of linear orders is Fraïssé.FirstOrder.Language.aleph0_categorical_dlo
shows that the theory of dense linear orders isℵ₀
-categorical, and thus complete.
The type of relations for the language of orders, consisting of a single binary relation le
.
Instances For
Equations
- FirstOrder.Language.instDecidableEqOrderRel = FirstOrder.Language.decEqorderRel✝
The relational language consisting of a single relation representing ≤
.
Equations
- FirstOrder.Language.order = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.orderRel }
Instances For
Equations
Equations
- ⋯ = ⋯
Equations
Equations
- FirstOrder.Language.order.instUniqueSymbols = { default := Sum.inr default, uniq := FirstOrder.Language.order.instUniqueSymbols.proof_1 }
A language is ordered if it has a symbol representing ≤
.
- leSymb : L.Relations 2
The relation symbol representing
≤
.
Instances
Equations
Joins two terms t₁, t₂
in a formula representing t₁ ≤ t₂
.
Equations
- t₁.le t₂ = FirstOrder.Language.leSymb.boundedFormula₂ t₁ t₂
Instances For
The language homomorphism sending the unique symbol ≤
of Language.order
to ≤
in an ordered
language.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The theory of preorders.
Equations
- L.preorderTheory = {FirstOrder.Language.leSymb.reflexive, FirstOrder.Language.leSymb.transitive}
Instances For
Equations
- ⋯ = ⋯
The theory of partial orders.
Instances For
Equations
- ⋯ = ⋯
The theory of linear orders.
Instances For
Equations
- ⋯ = ⋯
A sentence indicating that an order has no top element: $\forall x, \exists y, \neg y \le x$.
Equations
Instances For
A sentence indicating that an order has no bottom element: $\forall x, \exists y, \neg x \le y$.
Equations
Instances For
A sentence indicating that an order is dense: $\forall x, \forall y, x < y \to \exists z, x < z \wedge z < y$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The theory of dense linear orders without endpoints.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Any linearly-ordered type is naturally a structure in the language Language.order
.
This is not an instance, because sometimes the Language.order.Structure
is defined first.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A structure is ordered if its language has a ≤
symbol whose interpretation is ≤
.
- relMap_leSymb : ∀ (x : Fin 2 → M), FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb x ↔ x 0 ≤ x 1
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Any structure in an ordered language can be ordered correspondingly.
Equations
- L.leOfStructure M = { le := fun (a b : M) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b] }
Instances For
Equations
- ⋯ = ⋯
The order structure on an ordered language is decidable.
Equations
- L.decidableLEOfStructure M = h
Instances For
Any model of a theory of preorders is a preorder.
Equations
- L.preorderOfModels M = Preorder.mk ⋯ ⋯ ⋯
Instances For
Any model of a theory of partial orders is a partial order.
Equations
- L.partialOrderOfModels M = PartialOrder.mk ⋯
Instances For
Any model of a theory of linear orders is a linear order.
Equations
- L.linearOrderOfModels M = LinearOrder.mk ⋯ inferInstance decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
This is not an instance because it would form a loop with
FirstOrder.Language.order.instStrongHomClassOfOrderIsoClass
.
As both types are Prop
s, it would only cause a slowdown.
Equations
- ⋯ = ⋯
Any countable nonempty model of the theory of dense linear orders is a Fraïssé limit of the class of finite models of the theory of linear orders.
The class of finite models of the theory of linear orders is Fraïssé.
The theory of dense linear orders is ℵ₀
-categorical.
The theory of dense linear orders is ℵ₀
-complete.