Supporting results for pointwise provable equality.

Preperations for arithmetic

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

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

An interpretation of zero, one, addition, multiplication and strict order.

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

@[instance_reducible]

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

Equations

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

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

The numeral construction in FFL.ORingStructure.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ArithmeticTheory : Type

The Arithmetic Theory construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ArithmeticTheory = PointwiseComposition.FFL.FirstOrder.Theory ℒₒᵣ

@[reducible, inline]

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

The Arithmetic Semiterm construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ArithmeticSemiterm ξ n = PointwiseComposition.FFL.FirstOrder.Semiterm ℒₒᵣ ξ n

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ArithmeticTerm (ξ : Type u_1) : Type u_1

The Arithmetic Term construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ArithmeticTerm ξ = PointwiseComposition.FFL.FirstOrder.Term ℒₒᵣ ξ

@[reducible, inline]

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

The Arithmetic Semiformula construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ArithmeticSemiformula ξ n = PointwiseComposition.FFL.FirstOrder.Semiformula ℒₒᵣ ξ n

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ArithmeticFormula (ξ : Type u_1) : Type u_1

The Arithmetic Formula construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ArithmeticFormula ξ = PointwiseComposition.FFL.FirstOrder.Formula ℒₒᵣ ξ

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ArithmeticSemisentence (n : ℕ) : Type

The Arithmetic Semisentence construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ArithmeticSemisentence n = PointwiseComposition.FFL.FirstOrder.Semisentence ℒₒᵣ n

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ArithmeticSentence : Type

The Arithmetic Sentence construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ArithmeticSentence = PointwiseComposition.FFL.FirstOrder.Sentence ℒₒᵣ

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ArithmeticSemiproposition (n : ℕ) : Type

The Arithmetic Semiproposition construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ArithmeticSemiproposition n = PointwiseComposition.FFL.FirstOrder.Semiproposition ℒₒᵣ n

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ArithmeticProposition : Type

The Arithmetic Proposition construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ArithmeticProposition = PointwiseComposition.FFL.FirstOrder.Proposition ℒₒᵣ

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

The to String ORing construction in FFL.FirstOrder.Semiterm.

Equations

• One or more equations did not get rendered due to their size.
• (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar x_1).toStringORing = "x_{" ++ toString (n - 1 - ↑x_1) ++ "}"
• (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar x_1).toStringORing = "a_{" ++ toString x_1 ++ "}"
• (PointwiseComposition.FFL.FirstOrder.Semiterm.func PointwiseComposition.FFL.FirstOrder.Language.ORing.Func.zero a).toStringORing = "0"
• (PointwiseComposition.FFL.FirstOrder.Semiterm.func PointwiseComposition.FFL.FirstOrder.Language.ORing.Func.one a).toStringORing = "1"

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• PointwiseComposition.FFL.FirstOrder.instToStringArithmeticSemiterm = { toString := PointwiseComposition.FFL.FirstOrder.Semiterm.toStringORing }

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

The to String ORing construction in FFL.FirstOrder.Semiformula.

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• PointwiseComposition.FFL.FirstOrder.instToStringArithmeticSemiformula = { toString := PointwiseComposition.FFL.FirstOrder.Semiformula.toStringORing }

@[instance_reducible]

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

Equations

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

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

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

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Tarski.Structure.ORing (L : Language) [L.ORing] (M : Type w) [ORingStructure M] [Structure L M] extends PointwiseComposition.FFL.FirstOrder.Tarski.Structure.Zero L M, PointwiseComposition.FFL.FirstOrder.Tarski.Structure.One L M, PointwiseComposition.FFL.FirstOrder.Tarski.Structure.Add L M, PointwiseComposition.FFL.FirstOrder.Tarski.Structure.Mul L M, PointwiseComposition.FFL.FirstOrder.Tarski.Structure.Eq L M, PointwiseComposition.FFL.FirstOrder.Tarski.Structure.LT L M : Prop

Data and laws for ORing in FFL.FirstOrder.Tarski.Structure.

• 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 PointwiseComposition.FFL.FirstOrder.Tarski.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 PointwiseComposition.FFL.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

The ball LTSucc construction in FFL.FirstOrder.Semiformula.

Equations

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

def PointwiseComposition.FFL.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

The bexs LTSucc construction in FFL.FirstOrder.Semiformula.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_ballLTSucc {L : Language} [L.LT] [L.Zero] [L.One] [L.Add] {M : Type u_1} {s : Tarski.Structure L M} [LT M] [One M] [Add M] [Tarski.Structure.LT L M] [Tarski.Structure.One L M] [Tarski.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 PointwiseComposition.FFL.FirstOrder.Semiformula.eval_bexsLTSucc {L : Language} [L.LT] [L.Zero] [L.One] [L.Add] {M : Type u_1} {s : Tarski.Structure L M} [LT M] [One M] [Add M] [Tarski.Structure.LT L M] [Tarski.Structure.One L M] [Tarski.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 PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∀_<⁺_,_» : Lean.ParserDescr

The «first order formula∀ <⁺ , » construction in FFL.FirstOrder.BinderNotation.

Equations

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

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

The «first order formula∃ <⁺ , » construction in FFL.FirstOrder.BinderNotation.

Equations

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