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 LO.ISigma0.exponential_definable
    [M ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Relation (Exponential : M → M → Prop)

• LO.ISigma0.exponential_definable

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

• LO.ISigma0.Exponential.exponential_zero_one

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

• LO.ISigma0.Exponential.exponential_succ_mul_two

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