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

Equations

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

theorem FFL.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 FFL.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 FFL.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 : Tarski.Structure L M] [Tarski.Structure.Eq L M] [Tarski.Structure.LT L M] [M↓[L] ⊧* T], M↓[L] ⊧ φ) : T ⊢ φ