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 onetoone)

•
$\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)$
Title  Elementary Functional Arithmetic 

Canonical name  ElementaryFunctionalArithmetic 
Date of creation  20130322 12:56:39 
Last modified on  20130322 12:56:39 
Owner  Henry (455) 
Last modified by  Henry (455) 
Numerical id  5 
Author  Henry (455) 
Entry type  Definition 
Classification  msc 03F30 
Synonym  EFA 
Related topic  PeanoArithmetic 