Formalized Formal Logic

2.1. ISigma0🔗

2.1.1. Exponential

The graph of exponential \mathrm{Exp}(x, y) is definable by \Sigma_0-fomrula, and its inductive properties are proved in \mathsf{I}\Sigma_0.

🔗theorem
LO.ISigma0.exponential_definable.{u_1} {V : Type u_1} [LO.ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₀] : 𝚺₀-Relation LO.ISigma0.Exponential
LO.ISigma0.exponential_definable.{u_1}
  {V : Type u_1} [LO.ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₀] :
  𝚺₀-Relation LO.ISigma0.Exponential

The graph of the exponential function can be defined by the $\Delta_0$-formula.

🔗theorem
LO.ISigma0.Exponential.exponential_zero_one.{u_1} {V : Type u_1}
  [LO.ORingStruc V] [V ⊧ₘ* 𝗜𝚺₀] : LO.ISigma0.Exponential 0 1
LO.ISigma0.Exponential.exponential_zero_one.{u_1}
  {V : Type u_1} [LO.ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₀] : LO.ISigma0.Exponential 0 1
🔗theorem
LO.ISigma0.Exponential.exponential_succ_mul_two.{u_1} {V : Type u_1}
  [LO.ORingStruc V] [V ⊧ₘ* 𝗜𝚺₀] {x y : V} :
  LO.ISigma0.Exponential (x + 1) (2 * y) ↔ LO.ISigma0.Exponential x y
LO.ISigma0.Exponential.exponential_succ_mul_two.{u_1}
  {V : Type u_1} [LO.ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₀] {x y : V} :
  LO.ISigma0.Exponential (x + 1) (2 * y) ↔
    LO.ISigma0.Exponential x y

Other basic functions, such as \log x, |x| are defined by using exponential.