def LO.FirstOrder.LT.le {L : Language} [Semiformula.Operator.Eq L] [Semiformula.Operator.LT L] : Semiformula.Operator L 2

Equations

• LO.FirstOrder.LT.le = op(=).or op(<)

theorem LO.FirstOrder.le_eq {L : Language} [Semiformula.Operator.Eq L] [Semiformula.Operator.LT L] {μ : Type u_1} {n : ℕ} (t₁ t₂ : Semiterm L μ n) : LT.le.operator ![t₁, t₂] = (“(!!t₁ = !!t₂ ∨ !!t₁ < !!t₂)”)

theorem LO.FirstOrder.Order.leIffEqOrLt {L : Language} [Semiformula.Operator.Eq L] [Semiformula.Operator.LT L] {T : Theory L} : T ⊢ (“∀¹ ∀¹ (!!(Semiterm.bvar 1) ≤ !!(Semiterm.bvar 0) ↔ (!!(Semiterm.bvar 1) = !!(Semiterm.bvar 0) ∨ !!(Semiterm.bvar 1) < !!(Semiterm.bvar 0)))”)

theorem LO.FirstOrder.Order.complete {L : Language} [Semiformula.Operator.Eq L] [Semiformula.Operator.LT L] {T : Theory L} [𝗘𝗤 L ⪯ T] (φ : Sentence L) (H : ∀ (M : Type (max u w)) [inst : Nonempty M] [inst_1 : LT M] [inst_2 : Structure L M] [Structure.Eq L M] [Structure.LT L M] [M↓[L] ⊧* T], M↓[L] ⊧ φ) : T ⊢ φ