In
proof theory, a branch of
mathematical logic,
elementary function arithmetic, also called
EFA,
elementary arithmetic and
exponential function arithmetic, is the system of arithmetic with the usual elementary properties of 0, 1, +, ×,
xy, together with
induction for formulas with bounded quantifiers.