Preperations for arithmetic

• NOTE: To avoid the duplicate definitions of Structure ℒₒᵣ for models, we basically use ORingStructure, and generated standardStructure instead of Structure ℒₒᵣ itself.

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

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

abbrev LO.FirstOrder.ArithmeticTheory : Type

Equations

• LO.FirstOrder.ArithmeticTheory = LO.FirstOrder.Theory ℒₒᵣ

@[reducible, inline]

abbrev LO.FirstOrder.ArithmeticSemiterm (ξ : Type u_1) (n : ℕ) : Type u_1

Equations

• LO.FirstOrder.ArithmeticSemiterm ξ n = LO.FirstOrder.Semiterm ℒₒᵣ ξ n

@[reducible, inline]

abbrev LO.FirstOrder.ArithmeticTerm (ξ : Type u_1) : Type u_1

Equations

• LO.FirstOrder.ArithmeticTerm ξ = LO.FirstOrder.Term ℒₒᵣ ξ

@[reducible, inline]

abbrev LO.FirstOrder.ArithmeticSemiformula (ξ : Type u_1) (n : ℕ) : Type u_1

Equations

• LO.FirstOrder.ArithmeticSemiformula ξ n = LO.FirstOrder.Semiformula ℒₒᵣ ξ n

@[reducible, inline]

abbrev LO.FirstOrder.ArithmeticFormula (ξ : Type u_1) : Type u_1

Equations

• LO.FirstOrder.ArithmeticFormula ξ = LO.FirstOrder.Formula ℒₒᵣ ξ

@[reducible, inline]

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

Equations

• LO.FirstOrder.ArithmeticSemisentence n = LO.FirstOrder.Semisentence ℒₒᵣ n

@[reducible, inline]

abbrev LO.FirstOrder.ArithmeticSentence : Type

Equations

• LO.FirstOrder.ArithmeticSentence = LO.FirstOrder.Sentence ℒₒᵣ

@[reducible, inline]

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

Equations

• LO.FirstOrder.ArithmeticSemiproposition n = LO.FirstOrder.Semiproposition ℒₒᵣ n

@[reducible, inline]

abbrev LO.FirstOrder.ArithmeticProposition : Type

Equations

• LO.FirstOrder.ArithmeticProposition = LO.FirstOrder.Proposition ℒₒᵣ

def LO.FirstOrder.Semiterm.toStringORing {ξ : Type u_1} [ToString ξ] {n : ℕ} : ArithmeticSemiterm ξ n → String

Equations

• (LO.FirstOrder.Semiterm.bvar x_1).toStringORing = "x_{" ++ toString (n - 1 - ↑x_1) ++ "}"
• (LO.FirstOrder.Semiterm.fvar x_1).toStringORing = "a_{" ++ toString x_1 ++ "}"
• (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.zero a).toStringORing = "0"
• (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.one a).toStringORing = "1"
• (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.add v).toStringORing = "(" ++ (v 0).toStringORing ++ " + " ++ (v 1).toStringORing ++ ")"
• (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.mul v).toStringORing = "(" ++ (v 0).toStringORing ++ " \\cdot " ++ (v 1).toStringORing ++ ")"

@[implicit_reducible]

instance LO.FirstOrder.instReprArithmeticSemiterm {ξ : Type u_1} [ToString ξ] {n : ℕ} : Repr (ArithmeticSemiterm ξ n)

Equations

• LO.FirstOrder.instReprArithmeticSemiterm = { reprPrec := fun (t : LO.FirstOrder.ArithmeticSemiterm ξ n) (x : ℕ) => Std.Format.text (LO.FirstOrder.Semiterm.toStringORing t) }

@[implicit_reducible]

instance LO.FirstOrder.instToStringArithmeticSemiterm {ξ : Type u_1} [ToString ξ] {n : ℕ} : ToString (ArithmeticSemiterm ξ n)

Equations

• LO.FirstOrder.instToStringArithmeticSemiterm = { toString := LO.FirstOrder.Semiterm.toStringORing }

def LO.FirstOrder.Semiformula.toStringORing {ξ : Type u_1} [ToString ξ] {n : ℕ} : ArithmeticSemiformula ξ n → String

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Semiformula.verum.toStringORing = "\\top"
• LO.FirstOrder.Semiformula.falsum.toStringORing = "\\bot"
• (LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.ORing.Rel.eq v).toStringORing = (v 0).toStringORing ++ " = " ++ (v 1).toStringORing
• (LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.ORing.Rel.lt v).toStringORing = (v 0).toStringORing ++ " < " ++ (v 1).toStringORing
• (LO.FirstOrder.Semiformula.nrel LO.FirstOrder.Language.ORing.Rel.eq v).toStringORing = (v 0).toStringORing ++ " \\not = " ++ (v 1).toStringORing
• (LO.FirstOrder.Semiformula.nrel LO.FirstOrder.Language.ORing.Rel.lt v).toStringORing = (v 0).toStringORing ++ " \\not < " ++ (v 1).toStringORing
• (LO.FirstOrder.Semiformula.and φ ψ).toStringORing = "[" ++ LO.FirstOrder.Semiformula.toStringORing φ ++ "]" ++ " \\land " ++ "[" ++ LO.FirstOrder.Semiformula.toStringORing ψ ++ "]"
• (LO.FirstOrder.Semiformula.or φ ψ).toStringORing = "[" ++ LO.FirstOrder.Semiformula.toStringORing φ ++ "]" ++ " \\lor " ++ "[" ++ LO.FirstOrder.Semiformula.toStringORing ψ ++ "]"
• (LO.FirstOrder.Semiformula.all φ).toStringORing = "(\\forall x_{" ++ toString x✝ ++ "}) " ++ "[" ++ LO.FirstOrder.Semiformula.toStringORing φ ++ "]"
• (LO.FirstOrder.Semiformula.exs φ).toStringORing = "(\\exists x_{" ++ toString x✝ ++ "}) " ++ "[" ++ LO.FirstOrder.Semiformula.toStringORing φ ++ "]"

@[implicit_reducible]

instance LO.FirstOrder.instReprArithmeticSemiformula {ξ : Type u_1} [ToString ξ] {n : ℕ} : Repr (ArithmeticSemiformula ξ n)

Equations

• LO.FirstOrder.instReprArithmeticSemiformula = { reprPrec := fun (φ : LO.FirstOrder.ArithmeticSemiformula ξ n) (x : ℕ) => Std.Format.text (LO.FirstOrder.Semiformula.toStringORing φ) }

@[implicit_reducible]

instance LO.FirstOrder.instToStringArithmeticSemiformula {ξ : Type u_1} [ToString ξ] {n : ℕ} : ToString (ArithmeticSemiformula ξ n)

Equations

• LO.FirstOrder.instToStringArithmeticSemiformula = { toString := LO.FirstOrder.Semiformula.toStringORing }

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.instGödelNumberORing {α : Type u_1} [Encodable α] : Semiterm.Operator.GödelNumber ℒₒᵣ α

Equations

• LO.FirstOrder.Arithmetic.instGödelNumberORing = LO.FirstOrder.Semiterm.Operator.GödelNumber.ofEncodable

theorem LO.FirstOrder.Arithmetic.gödelNumber_def {α : Type u_1} [Encodable α] (a : α) : Semiterm.Operator.GödelNumber.gödelNumber a = Semiterm.Operator.encode ℒₒᵣ a

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

theorem LO.FirstOrder.Arithmetic.gödelNumber'_eq_coe_encode {α : Type u_2} [Encodable α] {ξ : Type u_1} {n : ℕ} (a : α) : ⌜a⌝ = ↑(Encodable.encode a)

@[simp]

theorem LO.FirstOrder.Arithmetic.encode_encode_eq {α : Type u_1} [Encodable α] (a : α) : Semiterm.Operator.GödelNumber.gödelNumber (Encodable.encode a) = Semiterm.Operator.GödelNumber.gödelNumber a

@[simp]

theorem LO.FirstOrder.Arithmetic.rew_gödelNumber' {α : Type u_3} [Encodable α] {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} (ω : Rew ℒₒᵣ ξ₁ n₁ ξ₂ n₂) (a : α) : ω ⌜a⌝ = ⌜a⌝

Semantics of arithmetic

class LO.FirstOrder.Structure.ORing (L : Language) [L.ORing] (M : Type w) [ORingStructure 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

• zero : Semiterm.Operator.val ![] op(0) = 0
• one : Semiterm.Operator.val ![] op(1) = 1
• add (a b : M) : Semiterm.Operator.val ![a, b] op(+) = a + b
• mul (a b : M) : Semiterm.Operator.val ![a, b] op(*) = a * b
• eq (a b : M) : Semiformula.Operator.val ![a, b] op(=) ↔ a = b
• lt (a b : M) : Semiformula.Operator.val ![a, b] op(<) ↔ 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} [ORingStructure 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) = ORingStructure.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

Equations

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

def LO.FirstOrder.Semiformula.bexsLTSucc {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

Equations

• LO.FirstOrder.Semiformula.bexsLTSucc t φ = LO.FirstOrder.Semiformula.bexsLT (‘(!!t + 1)’) φ

theorem LO.FirstOrder.Semiformula.eval_ballLTSucc {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] {ξ : Type u_2} {n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ n} {fv : Fin n → M} {bv : ξ → M} : (Eval fv bv) (ballLTSucc t φ) ↔ ∀ x < Semiterm.val fv bv t + 1, (Eval (x :> fv) bv) φ

theorem LO.FirstOrder.Semiformula.eval_bexsLTSucc {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] {ξ : Type u_2} {n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ n} {fv : Fin n → M} {bv : ξ → M} : (Eval fv bv) (bexsLTSucc t φ) ↔ ∃ x < Semiterm.val fv bv t + 1, (Eval (x :> fv) bv) φ

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.