# 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}\neq 0)$ ($0$ is the first number)

• $\forall x,y(x^{\prime}=y^{\prime}\rightarrow 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)

• $\forall x(\neg(x<0))$ ($0$ is the smallest number)

• $\forall x,y(x

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

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

Title Elementary Functional Arithmetic ElementaryFunctionalArithmetic 2013-03-22 12:56:39 2013-03-22 12:56:39 Henry (455) Henry (455) 5 Henry (455) Definition msc 03F30 EFA PeanoArithmetic