初等関数算術

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