Theory of orders

This file formalizes the basic theories of orders -- the theory of partial order PO and the theory of linear (total) order LO.

Design note

We always use less-equal ⪯ and less-than ≺ for orders, and do not define greater-equal ⪰ or greater-than ≻. When naming theorems, we may use ge or gt when it is actually le or lt (e.g. LO.lt_or_ge is the lt_or_le in Mathlib).

class FirstOrder.Language.Order (L : Language) : Type

Language with two binary formulas that represent less-equal ⪯ and less-than ≺.

• leDef : L.Formula 2
• ltDef : L.Formula 2

def FirstOrder.Language.Order.le {n : ℕ} {L : Language} [L.Order] (t₁ t₂ : L.Term n) : L.Formula n

Equations

• t₁ ⪯ t₂ = FirstOrder.Language.Order.leDef[[t₁, t₂]ᵥ]ₚ

def FirstOrder.Language.Order.«term_⪯_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.Order.subst_le {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} {m✝ : ℕ} {σ : L.Subst n m✝} : (t₁ ⪯ t₂)[σ]ₚ = t₁[σ]ₜ ⪯ t₂[σ]ₜ

def FirstOrder.Language.Order.lt {n : ℕ} {L : Language} [L.Order] (t₁ t₂ : L.Term n) : L.Formula n

Equations

• t₁ ≺ t₂ = FirstOrder.Language.Order.ltDef[[t₁, t₂]ᵥ]ₚ

def FirstOrder.Language.Order.«term_≺_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.Order.subst_lt {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} {m✝ : ℕ} {σ : L.Subst n m✝} : (t₁ ≺ t₂)[σ]ₚ = t₁[σ]ₜ ≺ t₂[σ]ₜ

def FirstOrder.Language.Order.bdall {n : ℕ} {L : Language} [L.Order] (t : L.Term n) (p : L.Formula (n + 1)) : L.Formula n

Bounded forall.

Equations

• ∀[≺ t] p = ∀' (#0 ≺ t[FirstOrder.Language.Subst.shift 1]ₜ ⇒ p)

def FirstOrder.Language.Order.«term∀[≺_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.Order.subst_bdall {n : ℕ} {L : Language} [L.Order] {t : L.Term n} {p : L.Formula (n + 1)} {m✝ : ℕ} {σ : L.Subst n m✝} : (∀[≺ t] p)[σ]ₚ = ∀[≺ t[σ]ₜ] p[⇑ₛσ]ₚ

def FirstOrder.Language.Order.bdex {n : ℕ} {L : Language} [L.Order] (t : L.Term n) (p : L.Formula (n + 1)) : L.Formula n

Bounded exists.

Equations

• ∃[≺ t] p = ∃' (#0 ≺ t[FirstOrder.Language.Subst.shift 1]ₜ ⩑ p)

def FirstOrder.Language.Order.«term∃[≺_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.Order.subst_bdex {n : ℕ} {L : Language} [L.Order] {t : L.Term n} {p : L.Formula (n + 1)} {m✝ : ℕ} {σ : L.Subst n m✝} : (∃[≺ t] p)[σ]ₚ = ∃[≺ t[σ]ₜ] p[⇑ₛσ]ₚ

theorem FirstOrder.Language.Order.iff_congr_le {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} {Γ : L.FormulaSet n} {t₁' t₂' : L.Term n} : Γ ⊢ t₁ ≐ t₁' ⇒ t₂ ≐ t₂' ⇒ t₁ ⪯ t₂ ⇔ t₁' ⪯ t₂'

theorem FirstOrder.Language.Order.iff_congr_lt {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} {Γ : L.FormulaSet n} {t₁' t₂' : L.Term n} : Γ ⊢ t₁ ≐ t₁' ⇒ t₂ ≐ t₂' ⇒ t₁ ≺ t₂ ⇔ t₁' ≺ t₂'

theorem FirstOrder.Language.Order.iff_congr_bdall {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} {Γ : L.FormulaSet n} {p : L.Formula (n + 1)} : Γ ⊢ t₁ ≐ t₂ ⇒ ∀[≺ t₁] p ⇔ ∀[≺ t₂] p

theorem FirstOrder.Language.Order.iff_congr_bdex {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} {Γ : L.FormulaSet n} {p : L.Formula (n + 1)} : Γ ⊢ t₁ ≐ t₂ ⇒ ∃[≺ t₁] p ⇔ ∃[≺ t₂] p

theorem FirstOrder.Language.Order.neg_bdall_iff {n : ℕ} {L : Language} [L.Order] {t : L.Term n} {Γ : L.FormulaSet n} {p : L.Formula (n + 1)} : Γ ⊢ ~ ∀[≺ t] p ⇔ ∃[≺ t] (~ p)

theorem FirstOrder.Language.Order.neg_bdex_iff {n : ℕ} {L : Language} [L.Order] {t : L.Term n} {Γ : L.FormulaSet n} {p : L.Formula (n + 1)} : Γ ⊢ ~ ∃[≺ t] p ⇔ ∀[≺ t] (~ p)

def FirstOrder.Language.order : Language

The language of order, with only two binary relations, ⪯ and ≺.

Equations

• FirstOrder.Language.order = { Func := fun (x : ℕ) => Empty, Rel := FirstOrder.Language.order.Rel✝ }

instance FirstOrder.Language.order.instOrder : order.Order

Equations

• FirstOrder.Language.order.instOrder = { leDef := FirstOrder.Language.order.Rel.le✝ ⬝ʳ [#0, #1]ᵥ, ltDef := FirstOrder.Language.order.Rel.lt✝ ⬝ʳ [#0, #1]ᵥ }

instance FirstOrder.Language.order.instRepr : order.Repr

Equations

• One or more equations did not get rendered due to their size.

inductive FirstOrder.Language.Theory.PO {L : Language} [L.Order] : L.Theory

Theory of partial order.

• ax_le_refl {L : Language} [L.Order] : PO (∀' (#0 ⪯ #0))
• ax_le_antisymm {L : Language} [L.Order] : PO (∀' ∀' (#1 ⪯ #0 ⇒ #0 ⪯ #1 ⇒ #1 ≐ #0))
• ax_le_trans {L : Language} [L.Order] : PO (∀' ∀' ∀' (#2 ⪯ #1 ⇒ #1 ⪯ #0 ⇒ #2 ⪯ #0))
• ax_lt_iff_le_not_ge {L : Language} [L.Order] : PO (∀' ∀' (#1 ≺ #0 ⇔ #1 ⪯ #0 ⩑ ~ #0 ⪯ #1))

theorem FirstOrder.Language.Theory.PO.le_refl {n : ℕ} {L : Language} [L.Order] {t : L.Term n} : ↑ᵀ^[n] PO ⊢ t ⪯ t

theorem FirstOrder.Language.Theory.PO.le_antisymm {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ⪯ t₂ ⇒ t₂ ⪯ t₁ ⇒ t₁ ≐ t₂

theorem FirstOrder.Language.Theory.PO.le_trans {n : ℕ} {L : Language} [L.Order] {t₁ t₂ t₃ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ⪯ t₂ ⇒ t₂ ⪯ t₃ ⇒ t₁ ⪯ t₃

theorem FirstOrder.Language.Theory.PO.lt_iff_le_not_ge {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ≺ t₂ ⇔ t₁ ⪯ t₂ ⩑ ~ t₂ ⪯ t₁

theorem FirstOrder.Language.Theory.PO.le_trans' {n : ℕ} {L : Language} [L.Order] {t₁ t₂ t₃ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₂ ⪯ t₃ ⇒ t₁ ⪯ t₂ ⇒ t₁ ⪯ t₃

theorem FirstOrder.Language.Theory.PO.le_of_lt {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ≺ t₂ ⇒ t₁ ⪯ t₂

theorem FirstOrder.Language.Theory.PO.not_ge_of_lt {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ≺ t₂ ⇒ ~ t₂ ⪯ t₁

theorem FirstOrder.Language.Theory.PO.not_gt_of_le {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ⪯ t₂ ⇒ ~ t₂ ≺ t₁

theorem FirstOrder.Language.Theory.PO.lt_iff_le_and_ne {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ≺ t₂ ⇔ t₁ ⪯ t₂ ⩑ ~ t₁ ≐ t₂

theorem FirstOrder.Language.Theory.PO.ne_of_lt {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ≺ t₂ ⇒ ~ t₁ ≐ t₂

theorem FirstOrder.Language.Theory.PO.le_iff_lt_or_eq {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ⪯ t₂ ⇔ t₁ ≺ t₂ ⩒ t₁ ≐ t₂

theorem FirstOrder.Language.Theory.PO.lt_irrefl {n : ℕ} {L : Language} [L.Order] {t : L.Term n} : ↑ᵀ^[n] PO ⊢ ~ t ≺ t

theorem FirstOrder.Language.Theory.PO.lt_of_lt_of_le {n : ℕ} {L : Language} [L.Order] {t₁ t₂ t₃ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ≺ t₂ ⇒ t₂ ⪯ t₃ ⇒ t₁ ≺ t₃

theorem FirstOrder.Language.Theory.PO.lt_of_le_of_lt {n : ℕ} {L : Language} [L.Order] {t₁ t₂ t₃ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ⪯ t₂ ⇒ t₂ ≺ t₃ ⇒ t₁ ≺ t₃

theorem FirstOrder.Language.Theory.PO.lt_of_lt_of_le' {n : ℕ} {L : Language} [L.Order] {t₁ t₂ t₃ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₂ ≺ t₃ ⇒ t₁ ⪯ t₂ ⇒ t₁ ≺ t₃

theorem FirstOrder.Language.Theory.PO.lt_of_le_of_lt' {n : ℕ} {L : Language} [L.Order] {t₁ t₂ t₃ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₂ ⪯ t₃ ⇒ t₁ ≺ t₂ ⇒ t₁ ≺ t₃

theorem FirstOrder.Language.Theory.PO.lt_asymm {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ≺ t₂ ⇒ ~ t₂ ≺ t₁

theorem FirstOrder.Language.Theory.PO.lt_trans {n : ℕ} {L : Language} [L.Order] {t₁ t₂ t₃ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₁ ≺ t₂ ⇒ t₂ ≺ t₃ ⇒ t₁ ≺ t₃

theorem FirstOrder.Language.Theory.PO.lt_trans' {n : ℕ} {L : Language} [L.Order] {t₁ t₂ t₃ : L.Term n} : ↑ᵀ^[n] PO ⊢ t₂ ≺ t₃ ⇒ t₁ ≺ t₂ ⇒ t₁ ≺ t₃

inductive FirstOrder.Language.Theory.LO {L : Language} [L.Order] : L.Theory

Theory of linear order.

• ax_po {L : Language} [L.Order] {p : L.Sentence} : p ∈ PO → LO p
• ax_le_total {L : Language} [L.Order] : LO (∀' ∀' (#1 ⪯ #0 ⩒ #0 ⪯ #1))

instance FirstOrder.Language.Theory.LO.instSubtheoryPO {L : Language} [L.Order] : PO ⊆ᵀ LO

instance FirstOrder.Language.Theory.LO.instSubtheoryPO_1 {L : Language} [L.Order] {T : L.Theory} [h : LO ⊆ᵀ T] : PO ⊆ᵀ T

theorem FirstOrder.Language.Theory.LO.le_total {n : ℕ} {L : Language} [L.Order] (t₁ t₂ : L.Term n) : ↑ᵀ^[n] LO ⊢ t₁ ⪯ t₂ ⩒ t₂ ⪯ t₁

theorem FirstOrder.Language.Theory.LO.neg_le_iff {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] LO ⊢ ~ t₁ ⪯ t₂ ⇔ t₂ ≺ t₁

theorem FirstOrder.Language.Theory.LO.neg_lt_iff {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] LO ⊢ ~ t₁ ≺ t₂ ⇔ t₂ ⪯ t₁

theorem FirstOrder.Language.Theory.LO.le_or_gt {n : ℕ} {L : Language} [L.Order] (t₁ t₂ : L.Term n) : ↑ᵀ^[n] LO ⊢ t₁ ⪯ t₂ ⩒ t₂ ≺ t₁

theorem FirstOrder.Language.Theory.LO.lt_or_ge {n : ℕ} {L : Language} [L.Order] (t₁ t₂ : L.Term n) : ↑ᵀ^[n] LO ⊢ t₁ ≺ t₂ ⩒ t₂ ⪯ t₁

theorem FirstOrder.Language.Theory.LO.lt_trichotomy {n : ℕ} {L : Language} [L.Order] (t₁ t₂ : L.Term n) : ↑ᵀ^[n] LO ⊢ t₁ ≺ t₂ ⩒ t₁ ≐ t₂ ⩒ t₂ ≺ t₁

theorem FirstOrder.Language.Theory.LO.ne_iff_lt_or_gt {n : ℕ} {L : Language} [L.Order] {t₁ t₂ : L.Term n} : ↑ᵀ^[n] LO ⊢ ~ t₁ ≐ t₂ ⇔ t₁ ≺ t₂ ⩒ t₂ ≺ t₁