Elementary function arithmetic

In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic, is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, x y {\displaystyle x^{y}} , together with induction for formulas with bounded quantifiers. EFA is a very weak logical system, whose proof-theoretic ordinal is ω 3 {\displaystyle \omega ^{3}} , but still seems able to prove much of ordinary mathematics that can be stated in the language of first-order arithmetic.

Source: Wikipedia — Elementary function arithmetic (CC BY-SA 4.0)