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₂)”)

noncomputable def 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)))”)

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.Order.provOf {L : Language} [Semiformula.Operator.Eq L] [Semiformula.Operator.LT L] {T : Theory L} [𝐄𝐐 ≼ T] (φ : SyntacticFormula L) (H : ∀ (M : Type (max u w)) [inst : Nonempty M] [inst_1 : LT M] [inst_2 : Structure L M] [inst_3 : Structure.Eq L M] [inst_4 : Structure.LT L M] [inst_5 : M ⊧ₘ* T], M ⊧ₘ φ) : T ⊨ φ