nLab elementary function arithmetic

Idea

Elementary function arithmetic (EFA), also known as $I\Delta_0 + \exp$, is a first-order theory of natural numbers, one of the weakest fragments of arithmetic strong enough to do nontrivial mathematics. It is strictly weaker than Peano arithmetic.

Regarding the strength of EFA, Harvey Friedman has put forth the following “grand conjecture”:

“Every theorem published in the Annals of Mathematics whose statement involves only finitary mathematical objects (i.e., what logicians call an arithmetical statement) can be proved in EFA. EFA is the weak fragment of Peano Arithmetic based on the usual quantifier-free axioms for 0, 1, +, ×, exp, together with the scheme of induction for all formulas in the language all of whose quantifiers are bounded.”

Here “bounded quantifier” refers to a quantifier of shape $\forall_{m \lt n}$; more formally, if a variable $n$ does not occur in a formula $\phi$, then $\forall_{m \lt n} \phi(m)$ means $\forall_m (m \lt n) \Rightarrow \phi(m)$.

Definition

The language of EFA is one-sorted with

• Two constants $0, 1$

• Three binary function symbols $+, \cdot, \exp$ (where $\exp(x, y)$ is usually written $x^y$).

The axioms of EFA are

• Those of Robinson arithmetic (where $s$ is translated as $1 + (-)$, i.e., as $+(1, -)$);

• Exponentiation axioms, viz. $x^0 = 1$ and $x^y \cdot x = x^{y+1}$;

• The induction axiom for formulas all of whose quantifiers are bounded.

Example

For example, in order to prove in EFA that addition is commutative, one can prove $(\forall a)(\forall b)(a \leq b \vee b \leq a)$ on the one hand, and, on the other hand, prove by induction over a $\Delta_0$ formula that $(\forall a)(\forall b \leq a)(a+b=b+a)$ holds.

Related concepts

• Peano arithmetic

• second-order arithmetic

References

• Wikipedia, Elementary function arithmetic.

“Grand conjectures” by Harvey Friedman may be found here:

• Post from Harvey Friedman to FOM, April 16, 1999. (web)

A MathOverflow discussion on Friedman’s grand conjecture about EFA may be found here,

• Charles, Status of Harvey Friedman’s grand conjecture?, http://mathoverflow.net/questions/39452 (version: 2011-03-24), (link)