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<y^{\prime}\leftrightarrow x<y\vee x=y)$
•

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

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

Title	Elementary Functional Arithmetic
Canonical name	ElementaryFunctionalArithmetic
Date of creation	2013-03-22 12:56:39
Last modified on	2013-03-22 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