Ordered First-Ordered Structures #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines ordered first-order languages and structures, as well as their theories.
Main Definitions #
first_order.language.orderis the language consisting of a single relation representing≤.first_order.language.order_Structureis the structure on an ordered type, assigning the symbol representing≤to the actual relation≤.first_order.language.is_orderedpoints out a specific symbol in a language as representing≤.first_order.language.ordered_structureindicates that the≤symbol in an ordered language is interpreted as the actual relation≤in a particular structure.first_order.language.linear_order_theoryand similar define the theories of preorders, partial orders, and linear orders.first_order.language.DLOdefines the theory of dense linear orders without endpoints, a particularly useful example in model theory.
Main Results #
partial_orders model the theory of partial orders,linear_orders model the theory of linear orders, and dense linear orders without endpoints modelTheory.DLO.
@[protected]
The language consisting of a single relation representing ≤.
Instances for first_order.language.order
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[class]
- le_symb : L.relations 2
A language is ordered if it has a symbol representing ≤.
Instances of this typeclass
Instances of other typeclasses for first_order.language.is_ordered
- first_order.language.is_ordered.has_sizeof_inst
def
first_order.language.term.le
{L : first_order.language}
{α : Type w}
{n : ℕ}
[L.is_ordered]
(t₁ t₂ : L.term (α ⊕ fin n)) :
L.bounded_formula α n
Joins two terms t₁, t₂ in a formula representing t₁ ≤ t₂.
Equations
- t₁.le t₂ = first_order.language.is_ordered.le_symb.bounded_formula₂ t₁ t₂
def
first_order.language.term.lt
{L : first_order.language}
{α : Type w}
{n : ℕ}
[L.is_ordered]
(t₁ t₂ : L.term (α ⊕ fin n)) :
L.bounded_formula α n
Joins two terms t₁, t₂ in a formula representing t₁ < t₂.
The language homomorphism sending the unique symbol ≤ of language.order to ≤ in an ordered
language.
Equations
Instances for first_order.language.order_Lhom
@[protected, instance]
Equations
@[protected, instance]
The theory of preorders.
Equations
Instances for first_order.language.preorder_theory
The theory of partial orders.
Equations
Instances for first_order.language.partial_order_theory
The theory of linear orders.
Equations
Instances for first_order.language.linear_order_theory
def
first_order.language.no_top_order_sentence
(L : first_order.language)
[L.is_ordered] :
L.sentence
A sentence indicating that an order has no top element: $\forall x, \exists y, \neg y \le x$.
Equations
- L.no_top_order_sentence = (((first_order.language.term.var ∘ sum.inr) 1).le ((first_order.language.term.var ∘ sum.inr) 0)).not.ex.all
def
first_order.language.no_bot_order_sentence
(L : first_order.language)
[L.is_ordered] :
L.sentence
A sentence indicating that an order has no bottom element: $\forall x, \exists y, \neg x \le y$.
Equations
- L.no_bot_order_sentence = (((first_order.language.term.var ∘ sum.inr) 0).le ((first_order.language.term.var ∘ sum.inr) 1)).not.ex.all
def
first_order.language.densely_ordered_sentence
(L : first_order.language)
[L.is_ordered] :
L.sentence
A sentence indicating that an order is dense: $\forall x, \forall y, x < y \to \exists z, x < z \wedge z < y$.
Equations
- L.densely_ordered_sentence = ((((first_order.language.term.var ∘ sum.inr) 0).lt ((first_order.language.term.var ∘ sum.inr) 1)).imp (((first_order.language.term.var ∘ sum.inr) 0).lt ((first_order.language.term.var ∘ sum.inr) 2) ⊓ ((first_order.language.term.var ∘ sum.inr) 2).lt ((first_order.language.term.var ∘ sum.inr) 1)).ex).all.all
The theory of dense linear orders without endpoints.
Equations
Instances for first_order.language.DLO
@[reducible]
def
first_order.language.ordered_structure
(L : first_order.language)
(M : Type w')
[L.is_ordered]
[has_le M]
[L.Structure M] :
Prop
A structure is ordered if its language has a ≤ symbol whose interpretation is
@[simp]
theorem
first_order.language.ordered_structure_iff
{L : first_order.language}
{M : Type w'}
[L.is_ordered]
[has_le M]
[L.Structure M] :
L.ordered_structure M ↔ L.order_Lhom.is_expansion_on M
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem
first_order.language.rel_map_le_symb
{L : first_order.language}
{M : Type w'}
[L.is_ordered]
[L.Structure M]
[has_le M]
[L.ordered_structure M]
{a b : M} :
@[simp]
theorem
first_order.language.term.realize_le
{L : first_order.language}
{α : Type w}
{M : Type w'}
{n : ℕ}
[L.is_ordered]
[L.Structure M]
[has_le M]
[L.ordered_structure M]
{t₁ t₂ : L.term (α ⊕ fin n)}
{v : α → M}
{xs : fin n → M} :
(t₁.le t₂).realize v xs ↔ first_order.language.term.realize (sum.elim v xs) t₁ ≤ first_order.language.term.realize (sum.elim v xs) t₂
@[simp]
theorem
first_order.language.term.realize_lt
{L : first_order.language}
{α : Type w}
{M : Type w'}
{n : ℕ}
[L.is_ordered]
[L.Structure M]
[preorder M]
[L.ordered_structure M]
{t₁ t₂ : L.term (α ⊕ fin n)}
{v : α → M}
{xs : fin n → M} :
(t₁.lt t₂).realize v xs ↔ first_order.language.term.realize (sum.elim v xs) t₁ < first_order.language.term.realize (sum.elim v xs) t₂
@[simp]
@[simp]
@[simp]
theorem
first_order.language.realize_densely_ordered
{M : Type w'}
[preorder M]
[h : densely_ordered M] :
@[protected, instance]
def
first_order.language.model_DLO
{M : Type w'}
[linear_order M]
[densely_ordered M]
[no_top_order M]
[no_bot_order M] :