Theory $\mathsf{I}{\Sigma }_0$

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$.

instance exponential_definable [M ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Relation (Exponential : M → M → Prop)

• LO.Arith.exponential_definable

lemma exponential_zero_one [M ⊧ₘ* 𝐈𝚺₀] :
    Exponential 0 1

• LO.Arith.Exponential.exponential_zero_one

lemma exponential_succ_mul_two [M ⊧ₘ* 𝐈𝚺₀] {x y : M} :
    Exponential (x + 1) (2 * y) ↔ Exponential x y

• LO.Arith.Exponential.exponential_succ_mul_two

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