初等関数算術

数理論理学の分枝である証明論において、初等関数算術（）または指数関数算術（EFA）は算術の体系のひとつであり、関数記号 formula_1 の初等的な性質と、有界論理式に対する帰納法の公理図式からなる。同じことであるが、有界算術のひとつである formula_2 に指数関数を追加して得られる体系といってもよい。そのためEFAは formula_3 とも呼ばれる。
EFAは非常に弱い論理体系であり、その証明論的順序数は formula_4 である。しかしながら一階算術の言語で書かれた通常の数学で現れる多くの命題を証明できる。例えば formula_2 では素数の無限性を証明できるか否かは不明であるが、EFAは指数関数を備えているので、階乗を利用した通常の証明をEFA上で形式化できる。
定義.
EFAは（等号付き）一階述語論理の上の理論である。言語は次のものからなる：
有界量化子あるいは限定量化子は formula_11 と formula_12 の形をしたもので、これらは formula_13 および formula_14 の省略形である。全ての量化子が有界であるような論理式のことを有界論理式、限定論理式あるいは formula_15 論理式という。
EFAの公理は次のものからなる：
フリードマンの壮大な予想.
ハービー・フリードマンの壮大な予想（grand conjecture）は多くの数学の定理、例えばフェルマーの最終定理が、EFAなどの非常に弱い体系において証明可能であることを含意する。
にあるように本来の予想の主張は次のようである：
標準モデルで真であるがEFAで証明不能であるような、人工的な数学的言明が簡単に構成できる。フリードマンの予想のポイントはそのような自然な例は稀であるということである。幾つかの自然な例としてはロジックにおける無矛盾性を示す文や、ラムゼイ理論に関連する幾つかの命題、例えばSzemerédiの補題やグラフマイナー定理、素集合データ構造に対するタージャンのアルゴリズムなどが含まれる。
関連する体系.
ロビンソン算術に有界論理式に対する帰納法の公理を追加し、さらに指数関数の全域性を示す論理式を公理に追加することによって、二項関数記号 formula_19 を落とすことができる。これはEFAと類似の体系で、同じ証明論的な強さを持つが、そこでの作業はより面倒なことになる。
二項関数記号 formula_19 を忘却することができる。
EFAと同じ証明論的な強さを持ち、formula_21 保存的な、二階算術の弱い断片が幾つか存在する。それらはRCA とWKLと呼ばれる。これらは逆数学においてしばしば研究される。
初等帰納的算術（、ERA）は原始帰納的算術（PRA）の部分体系であり、再帰を限定和と限定積に制限したものである。これもEFAと同じ formula_21 文を持つ。その意味するところは、EFAで formula_23（formula_24 は量化子を持たない）が証明可能であるときに限り、ERAで項 formula_25 が定義できて formula_26 が証明可能である、ということである。
PRAと同様、ERAは論理を用いることなく、代入、帰納法、初等帰納的関数の定義式とによって定義できる。しかしながら、PRAとは異なり、初等帰納的算術は有限個の基底関数と射影の関数合成による閉包として特徴付けることができ、したがって有限個の定義式だけを必要とする。