初等関数算術
数理論理学の分枝である証明論において、初等関数算術（）または指数関数算術（EFA）は算術の体系のひとつであり、関数記号 formula_1 の初等的な性質と、有界論理式に対する帰納法の公理図式からなる。同じことであるが、有界算術のひとつである formula_2 に指数関数を追加して得られる体系といってもよい。そのためEFAは formula_3 とも呼ばれる。
EFAは非常に弱い論理体系であり、その証明論的順序数は formula_4 である。しかしながら一階算術の言語で書かれた通常の数学で現れる多くの命題を証明できる。例えば formula_2 では素数の無限性を証明できるか否かは不明であるが、EFAは指数関数を備えているので、階乗を利用した通常の証明をEFA上で形式化できる。