Elementary function arithmetic

This article includes a list of references, related reading, or external links, but its sources remain unclear because it lacks inline citations. Please help improve this article by introducing more precise citations. (November 2017) (Learn how and when to remove this message)

In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic,^[1] is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, ${\displaystyle x^{y}}$, together with induction for formulas with bounded quantifiers.

EFA is a very weak logical system, whose proof theoretic ordinal is ${\displaystyle \omega ^{3}}$, but still seems able to prove much of ordinary mathematics that can be stated in the language of first-order arithmetic.