初等関数算術

数理論理学の分枝である証明論において、初等関数算術（英: elementary function arithmetic）または指数関数算術（EFA）は算術の体系のひとつであり、関数記号 $0,1,+,\times ,x^{y}$ の初等的な性質と、有界論理式に対する帰納法の公理図式からなる。同じことであるが、有界算術のひとつである $I\Delta _{0}$ に指数関数を追加して得られる体系といってもよい。そのためEFAは $I\Delta _{0}(\exp )$ とも呼ばれる。

EFAは非常に弱い論理体系であり、その証明論的順序数は $\omega ^{3}$ である。しかしながら一階算術の言語で書かれた通常の数学で現れる多くの命題を証明できる。例えば $I\Delta _{0}$ では素数の無限性を証明できるか否かは不明であるが、EFAは指数関数を備えているので、階乗を利用した通常の証明をEFA上で形式化できる。

定義

EFAは（等号付き）一階述語論理の上の理論である。言語は次のものからなる：

2つの定数記号 $0,1$
3つの二項関数記号 $+,\times ,\exp$ ここで $exp(x,y)$ は $x^{y}$ と書かれる
1つの二項述語記号 $<$ （これは必ずしも必要はない。この述語記号は定義により導入できる。ただし有界量化の定義に便利である。）

有界量化子あるいは限定量化子は $\forall x<y$ と $\exists x<y$ の形をしたもので、これらは $\forall x(x<y\to \cdots )$ および $\exists x(x<y\wedge \cdots )$ の省略形である。全ての量化子が有界であるような論理式のことを有界論理式、限定論理式あるいは $\Delta _{0}$ 論理式という。

EFAの公理は次のものからなる：

ロビンソン算術の公理すべて（ $0,1,+,\times ,<$ に関するもの）
指数関数の公理: $x^{0}=1,x^{y+1}=x^{y}\times x$
有界論理式に対する帰納法の公理図式

フリードマンの壮大な予想

ハービー・フリードマンの壮大な予想（grand conjecture）は多くの数学の定理、例えばフェルマーの最終定理が、EFAなどの非常に弱い体系において証明可能であることを含意する。

Friedman (1999)にあるように本来の予想の主張は次のようである：

"Annals of Mathematicsにおいて出版されており、有限的な数学的対象だけを扱うような（すなわちロジシャンのいうところの算術的言明）、いかなる定理もEFAにおいて証明可能である。EFAはペアノ算術の弱い断片であり、

0,1,+,\times ,\exp

に関する基本的な量化子のない公理と、全ての量化子が有界である論理式に対する帰納法の公理図式からなる。"

標準モデルで真であるがEFAで証明不能であるような、人工的な数学的言明が簡単に構成できる。フリードマンの予想のポイントはそのような自然な例は稀であるということである。幾つかの自然な例としてはロジックにおける無矛盾性を示す文や、ラムゼイ理論に関連する幾つかの命題、例えばSzemerédiの補題やグラフマイナー定理、素集合データ構造に対するタージャンのアルゴリズムなどが含まれる。