初等関数算術

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

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

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

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

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

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

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

"Annals of Mathematicsにおいて出版されており、有限的な数学的対象だけを扱うような（すなわちロジシャンのいうところの算術的言明）、いかなる定理もEFAにおいて証明可能である。EFAはペアノ算術の弱い断片であり、${\displaystyle 0,1,+,\times ,\exp }$ に関する基本的な量化子のない公理と、全ての量化子が有界である論理式に対する帰納法の公理図式からなる。"

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