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é.
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
- ⋯ = ⋯
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
- ⋯ = ⋯
Equations
- L.instDecidableRelLeOfRelMapLeSymbVecConsVecEmpty M = h
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é.