Basic

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

Imported declaration from the Incompleteness formalization.

• zero : α
• one : α
• add : α → α → α
• mul : α → α → α
• lt : α → α → Prop

@[implicit_reducible]

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

Equations

• LO.instORingStrucOfZeroOfOneOfAddOfMulOfLT = { toZero := inst✝⁴, toOne := inst✝³, toAdd := inst✝², toMul := inst✝¹, toLT := inst✝ }

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

Imported declaration from the Incompleteness formalization.

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} [ORingStruc α] : numeral 0 = 0

@[simp]

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

instance LO.FirstOrder.Semiterm.instCoeORing {L : Language} [L.ORing] {ξ : Type u_2} {n : ℕ} : Coe (Semiterm ℒₒᵣ ξ n) (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 : Language} [L.ORing] {ξ : Type u_1} {n : ℕ} : lMap Language.oringEmb ↑op(0) = ↑op(0)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Semiformula.instCoeTheoryORing {L : Language} [L.ORing] : Coe (Theory ℒₒᵣ) (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 : Language} [L.ORing] {ξ : Type u_1} {n : ℕ} (v : Fin 2 → Semiterm ℒₒᵣ ξ n) : (lMap Language.oringEmb) (op(=).operator v) = (“!!(Semiterm.lMap Language.oringEmb (v 0)) = !!(Semiterm.lMap Language.oringEmb (v 1))”)

@[simp]

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

• zero : Semiterm.Operator.val op(0) ![] = 0
• one : Semiterm.Operator.val op(1) ![] = 1
• add (a b : M) : op(+).val ![a, b] = a + b
• mul (a b : M) : op(*).val ![a, b] = a * b
• eq (a b : M) : op(=).val ![a, b] ↔ a = b
• lt (a b : M) : op(<).val ![a, b] ↔ a < b

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

• sound {σ : Sentence L} : F σ → T ⊢! ↑σ → ℕ ⊧ₘ₀ σ

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

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

@[implicit_reducible]

instance LO.FirstOrder.Arith.instGoedelNumberORingOfEncodable {α : Type u_1} [Encodable α] : 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 : α) : Semiterm.Operator.GoedelNumber.goedelNumber a = Semiterm.Operator.encode ℒₒᵣ a

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

• refl {L : Language} [L.Eq] : 𝐄𝐐' (“!!(Semiterm.fvar 0) = !!(Semiterm.fvar 0)”)
• replace {L : Language} [L.Eq] (φ : SyntacticSemiformula L 1) : 𝐄𝐐' (“∀' ∀' (!!(Semiterm.bvar 1) = !!(Semiterm.bvar 0) → !(φ/[Semiterm.bvar 1] ==> φ/[Semiterm.bvar 0]))”)

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

Imported declaration from the Incompleteness formalization.

Equations

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

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