class LO.ORingStruc (α : Type u_1) extends Zero , One , Add , Mul , LT : Type u_1

instance LO.instORingStrucOfZeroOfOneOfAddOfMulOfLT {α : Type u_1} [Zero α] [One α] [Add α] [Mul α] [LT α] : LO.ORingStruc α

Equations

• LO.instORingStrucOfZeroOfOneOfAddOfMulOfLT = LO.ORingStruc.mk

def LO.ORingStruc.numeral {α : Type u_1} [LO.ORingStruc α] : ℕ → α

Equations

• LO.ORingStruc.numeral 0 = 0
• LO.ORingStruc.numeral 1 = 1
• LO.ORingStruc.numeral n.succ.succ = LO.ORingStruc.numeral (n + 1) + 1

@[simp]

theorem LO.ORingStruc.zero_eq_zero {α : Type u_1} [LO.ORingStruc α] : LO.ORingStruc.numeral 0 = 0

@[simp]

theorem LO.ORingStruc.one_eq_one {α : Type u_1} [LO.ORingStruc α] : LO.ORingStruc.numeral 1 = 1

@[simp]

theorem LO.Nat.numeral_eq (n : ℕ) : LO.ORingStruc.numeral n = n

def LO.FirstOrder.Language.oringEmb {L : LO.FirstOrder.Language} [L.ORing] : ℒₒᵣ.Hom L

Equations

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

@[simp]

theorem LO.FirstOrder.Language.oringEmb_zero {L : LO.FirstOrder.Language} [L.ORing] : LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.Zero.zero = LO.FirstOrder.Language.Zero.zero

@[simp]

theorem LO.FirstOrder.Language.oringEmb_one {L : LO.FirstOrder.Language} [L.ORing] : LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.One.one = LO.FirstOrder.Language.One.one

@[simp]

theorem LO.FirstOrder.Language.oringEmb_add {L : LO.FirstOrder.Language} [L.ORing] : LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.Add.add = LO.FirstOrder.Language.Add.add

@[simp]

theorem LO.FirstOrder.Language.oringEmb_mul {L : LO.FirstOrder.Language} [L.ORing] : LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.Mul.mul = LO.FirstOrder.Language.Mul.mul

@[simp]

theorem LO.FirstOrder.Language.oringEmb_eq {L : LO.FirstOrder.Language} [L.ORing] : LO.FirstOrder.Language.oringEmb.rel op(=) = op(=)

@[simp]

theorem LO.FirstOrder.Language.oringEmb_lt {L : LO.FirstOrder.Language} [L.ORing] : LO.FirstOrder.Language.oringEmb.rel op(<) = op(<)

instance LO.FirstOrder.Semiterm.instCoeORing {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_2} {n : ℕ} : Coe (LO.FirstOrder.Semiterm ℒₒᵣ ξ n) (LO.FirstOrder.Semiterm L ξ n)

Equations

• LO.FirstOrder.Semiterm.instCoeORing = { coe := LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb }

@[simp]

theorem LO.FirstOrder.Semiterm.oringEmb_zero {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (LO.FirstOrder.Semiterm.Operator.const op(0)) = LO.FirstOrder.Semiterm.Operator.const op(0)

@[simp]

theorem LO.FirstOrder.Semiterm.oringEmb_one {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (LO.FirstOrder.Semiterm.Operator.const op(1)) = LO.FirstOrder.Semiterm.Operator.const op(1)

@[simp]

theorem LO.FirstOrder.Semiterm.oringEmb_add {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} (v : Fin 2 → LO.FirstOrder.Semiterm ℒₒᵣ ξ n) : LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (op(+).operator v) = (‘(!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) + !!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1)))’)

@[simp]

theorem LO.FirstOrder.Semiterm.oringEmb_mul {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} (v : Fin 2 → LO.FirstOrder.Semiterm ℒₒᵣ ξ n) : LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (op(*).operator v) = ‘(!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) * !!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1)))’

@[simp]

theorem LO.FirstOrder.Semiterm.oringEmb_numeral {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} (z : ℕ) : LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ z)) = LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral L z)

instance LO.FirstOrder.Semiformula.instCoeORing {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_2} {n : ℕ} : Coe (LO.FirstOrder.Semiformula ℒₒᵣ ξ n) (LO.FirstOrder.Semiformula L ξ n)

Equations

• LO.FirstOrder.Semiformula.instCoeORing = { coe := ⇑(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) }

instance LO.FirstOrder.Semiformula.instCoeTheoryORing {L : LO.FirstOrder.Language} [L.ORing] : Coe (LO.FirstOrder.Theory ℒₒᵣ) (LO.FirstOrder.Theory L)

Equations

• LO.FirstOrder.Semiformula.instCoeTheoryORing = { coe := fun (x : LO.FirstOrder.Theory ℒₒᵣ) => ⇑(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) '' x }

@[simp]

theorem LO.FirstOrder.Semiformula.oringEmb_eq {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} (v : Fin 2 → LO.FirstOrder.Semiterm ℒₒᵣ ξ n) : (LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) (op(=).operator v) = (“!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) = !!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1))”)

@[simp]

theorem LO.FirstOrder.Semiformula.oringEmb_lt {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} (v : Fin 2 → LO.FirstOrder.Semiterm ℒₒᵣ ξ n) : (LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) (op(<).operator v) = (“!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) < !!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1))”)

@[reducible, inline]

abbrev LO.FirstOrder.Polynomial (n : ℕ) : Type

Equations

• LO.FirstOrder.Polynomial n = LO.FirstOrder.Semiterm ℒₒᵣ Empty n

class LO.FirstOrder.Structure.ORing (L : LO.FirstOrder.Language) [L.ORing] (M : Type w) [LO.ORingStruc M] [LO.FirstOrder.Structure L M] extends LO.FirstOrder.Structure.Zero , LO.FirstOrder.Structure.One , LO.FirstOrder.Structure.Add , LO.FirstOrder.Structure.Mul , LO.FirstOrder.Structure.Eq , LO.FirstOrder.Structure.LT : Type

@[simp]

theorem LO.FirstOrder.Structure.numeral_eq_numeral {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.Zero L] [LO.FirstOrder.Semiterm.Operator.One L] [LO.FirstOrder.Semiterm.Operator.Add L] {M : Type u} [LO.ORingStruc M] [LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Zero L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] (z : ℕ) : LO.FirstOrder.Semiterm.Operator.val (LO.FirstOrder.Semiterm.Operator.numeral L z) ![] = LO.ORingStruc.numeral z

def LO.FirstOrder.Semiformula.ballLTSucc {L : LO.FirstOrder.Language} [L.LT] [L.Zero] [L.One] [L.Add] {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.ballLTSucc t p = LO.FirstOrder.Semiformula.ballLT (‘(!!t + 1)’) p

def LO.FirstOrder.Semiformula.bexLTSucc {L : LO.FirstOrder.Language} [L.LT] [L.Zero] [L.One] [L.Add] {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.bexLTSucc t p = LO.FirstOrder.Semiformula.bexLT (‘(!!t + 1)’) p

theorem LO.FirstOrder.Semiformula.eval_ballLTSucc {n : ℕ} {L : LO.FirstOrder.Language} [L.LT] [L.Zero] [L.One] [L.Add] {ξ : Type u_1} {M : Type u_2} {s : LO.FirstOrder.Structure L M} [LT M] [One M] [Add M] [LO.FirstOrder.Structure.LT L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] {t : LO.FirstOrder.Semiterm L ξ n} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} {e : Fin n → M} {ε : ξ → M} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.ballLTSucc t p) ↔ ∀ x < LO.FirstOrder.Semiterm.val s e ε t + 1, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p

theorem LO.FirstOrder.Semiformula.eval_bexLTSucc {n : ℕ} {L : LO.FirstOrder.Language} [L.LT] [L.Zero] [L.One] [L.Add] {ξ : Type u_1} {M : Type u_2} {s : LO.FirstOrder.Structure L M} [LT M] [One M] [Add M] [LO.FirstOrder.Structure.LT L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] {t : LO.FirstOrder.Semiterm L ξ n} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} {e : Fin n → M} {ε : ξ → M} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.bexLTSucc t p) ↔ ∃ x < LO.FirstOrder.Semiterm.val s e ε t + 1, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p

def LO.FirstOrder.BinderNotation.«first_order_formula∀_<⁺_,_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.BinderNotation.«first_order_formula∃_<⁺_,_» : Lean.ParserDescr

Equations

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

class LO.FirstOrder.Arith.SoundOn {L : LO.FirstOrder.Language} [LO.FirstOrder.Structure L ℕ] (T : LO.FirstOrder.Theory L) (F : LO.FirstOrder.SyntacticFormula L → Prop) : Type

• sound : ∀ {p : LO.FirstOrder.SyntacticFormula L}, F p → T ⊢! p → ℕ ⊧ₘ p

theorem LO.FirstOrder.Arith.SoundOn.sound {L : LO.FirstOrder.Language} [LO.FirstOrder.Structure L ℕ] {T : LO.FirstOrder.Theory L} {F : LO.FirstOrder.SyntacticFormula L → Prop} [self : LO.FirstOrder.Arith.SoundOn T F] {p : LO.FirstOrder.SyntacticFormula L} : F p → T ⊢! p → ℕ ⊧ₘ p

theorem LO.FirstOrder.Arith.consistent_of_sound {L : LO.FirstOrder.Language} [LO.FirstOrder.Structure L ℕ] (T : LO.FirstOrder.Theory L) (F : Set (LO.FirstOrder.SyntacticFormula L)) [LO.FirstOrder.Arith.SoundOn T F] (hF : ⊥ ∈ F) : LO.System.Consistent T

theorem LO.FirstOrder.Arith.consequence_of {L : LO.FirstOrder.Language} [L.ORing] (T : LO.FirstOrder.Theory L) [𝐄𝐐 ≼ T] (p : LO.FirstOrder.SyntacticFormula L) (H : ∀ (M : Type (max u w)) [inst : LO.ORingStruc M] [inst_1 : LO.FirstOrder.Structure L M] [inst_2 : LO.FirstOrder.Structure.ORing L M] [inst_3 : M ⊧ₘ* T], M ⊧ₘ p) : T ⊨ p

instance LO.FirstOrder.Arith.instGoedelNumberORingOfEncodable {α : Type u_1} [Encodable α] : LO.FirstOrder.Semiterm.Operator.GoedelNumber ℒₒᵣ α

Equations

• LO.FirstOrder.Arith.instGoedelNumberORingOfEncodable = LO.FirstOrder.Semiterm.Operator.GoedelNumber.ofEncodable

theorem LO.FirstOrder.Arith.goedelNumber_def {α : Type u_1} [Encodable α] (a : α) : LO.FirstOrder.Semiterm.Operator.GoedelNumber.goedelNumber a = LO.FirstOrder.Semiterm.Operator.encode ℒₒᵣ a

theorem LO.FirstOrder.Arith.goedelNumber'_def {ξ : Type u_1} {n : ℕ} {α : Type u_2} [Encodable α] (a : α) : ⌜a⌝ = LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.encode ℒₒᵣ a)

@[simp]

theorem LO.FirstOrder.Arith.encode_encode_eq {α : Type u_1} [Encodable α] (a : α) : LO.FirstOrder.Semiterm.Operator.GoedelNumber.goedelNumber (Encodable.encode a) = LO.FirstOrder.Semiterm.Operator.GoedelNumber.goedelNumber a

inductive LO.FirstOrder.Theory.EQ' {L : LO.FirstOrder.Language} [L.Eq] : LO.FirstOrder.Theory L

• refl: ∀ {L : LO.FirstOrder.Language} [inst : L.Eq], 𝐄𝐐' (“!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 0)”)
• replace: ∀ {L : LO.FirstOrder.Language} [inst : L.Eq] (p : LO.FirstOrder.SyntacticSemiformula L 1), 𝐄𝐐' (“∀' ∀' (!!(LO.FirstOrder.Semiterm.bvar 1) = !!(LO.FirstOrder.Semiterm.bvar 0) → !((LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 1]).hom p ➝ (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom p))”)

def LO.FirstOrder.Theory.«term𝐄𝐐'» : Lean.ParserDescr

Equations

• LO.FirstOrder.Theory.«term𝐄𝐐'» = Lean.ParserDescr.node `LO.FirstOrder.Theory.term𝐄𝐐' 1024 (Lean.ParserDescr.symbol "𝐄𝐐'")

noncomputable instance LO.FirstOrder.Theory.EQ'.subTheoryOfEQ {L : LO.FirstOrder.Language} [L.Eq] : 𝐄𝐐' ≼ 𝐄𝐐

Equations

• LO.FirstOrder.Theory.EQ'.subTheoryOfEQ = LO.System.Subtheory.ofAxm! ⋯