Elementary Functional Arithmetic

Elementary Functional Arithmetic, or EFA, is a weak theory of arithmetic created by removing induction from Peano Arithmetic. Because it lacks induction, axioms defining exponentiation must be added.

• $\forall x(x^{\prime }\ne 0)$ ($0$ is the first number)

• $\forall x,y(x^{\prime }=y^{\prime }\to x=y)$ (the successor function is one-to-one)

• $\forall x(x+0=x)$ ($0$ is the additive identity)

• $\forall x,y(x+y^{\prime }={(x+y)}^{\prime })$ (addition is the repeated application of the successor function)

• $\forall x(x\cdot 0=0)$

• $\forall x,y(x\cdot (y^{\prime })=x\cdot y+x$ (multiplication is repeated addition)

• ($0$ is the smallest number)

• $\forall x(x^0=1)$

• $\forall x(x^{y^{\prime }}=x^y\cdot x)$