初等関数演算

証明論（数理論理学の一分野）では、初等関数算術（EFA）は、初等算術や指数関数算術とも呼ばれ、^{[ 1 ]} 0、1  、 +、 ×、 ${\displaystyle x^{y}}$有界量化子を持つ論理式の帰納法とともに。

EFAは非常に弱い論理システムであり、その証明論的順序数は$\displaystyle \omega ^{3}}$しかし、それでもなお、一階算術の言語で表現できる通常の数学の多くを証明できるようである。

EFAは一階述語論理（等号を含む）の体系である。その言語には以下が含まれる。

• 2つの定数${\displaystyle 0}$、${\displaystyle 1}$、
• 3つの二項演算${\displaystyle +}$、${\displaystyle \times }$、${\displaystyle {\textrm {exp}}}$、 と$\displaystyle {\textrm {exp}}(x,y)}$通常、次のように書かれる${\displaystyle x^{y}}$、
• 二項関係記号${\displaystyle <}$（これは他の演算を用いて記述できるため、必ずしも必要ではなく、省略されることもありますが、有界量化子を定義する際には便利です。）

有界量化子は、次の形式のものである。${\displaystyle \forall (x<y)}$そして${\displaystyle \exists (x<y)}$これらは略語です$\displaystyle \forall x(x<y)\rightarrow \ldots }$そして${\displaystyle \exists x(x<y)\land \ldots }$通常の方法で。

EFAの公理は

• ロビンソン算術の公理は${\displaystyle 0}$、${\displaystyle 1}$、${\displaystyle +}$、${\displaystyle \times }$、${\displaystyle <}$
• べき乗の公理：${\displaystyle x^{0}=1}$、${\displaystyle x^{y+1}=x^{y}\times x}$。
• すべての量化子が有界である（ただし、自由変数を含む場合もある）論理式の帰納法。

ハーヴェイ・フリードマンの壮大な予想は、フェルマーの最終定理のような多くの数学的定理が、EFAのような非常に弱いシステムでも証明できることを示唆している。

フリードマン（1999）によるこの予想の原文は以下のとおりです。

「 『数学年報』に掲載された定理のうち、その記述が有限な数学的対象のみを含むもの（すなわち、論理学者が算術命題と呼ぶもの）はすべてEFAで証明できる。EFAは、0、1、+、×、 expに関する通常の量化子フリー公理と、その言語におけるすべての量化子が有界であるすべての論理式に対する帰納法体系に基づいた、ペアノ算術の弱い断片である。」    

EFAでは真であるが証明できない人工的な算術命題を構築することは容易であるが、フリードマン予想の要点は、数学においてそのような命題の自然な例が稀であるように見えることである。自然な例としては、論理学における無矛盾性命題、セメレディの正則性補題などのラムゼイ理論に関連するいくつかの命題、およびグラフ小定理などが挙げられる。

EFAと同様の特性を持つ、関連する計算複雑性クラスがいくつか存在する。

• ロビンソン算術と、有界量化子を持つすべての式に対する帰納法、そしてべき乗はどこでも定義される関数であるというおおよその公理を組み合わせることで、言語から二項関数記号expを省略することができる。これはEFAに似ており、証明論的な強さは同じだが、扱いがより煩雑になる。
• 2階算術の弱い断片があり、${\displaystyle {\mathsf {RCA}}_{0}^{*}}$そして${\displaystyle {\mathsf {WKL}}_{0}^{*}}$EFAよりも保守的な$\displaystyle \Pi _{2}^{0}}$文（つまり任意の文）$\displaystyle \Pi _{2}^{0}}$証明された文${\displaystyle {\mathsf {RCA}}_{0}^{*}}$または${\displaystyle {\mathsf {WKL}}_{0}^{*}}$すでにEFAによって証明されている。）^{[ 2 ]}特に、これらは一貫性ステートメントに対して保守的である。これらの断片は、逆数学で研究されることがある（Simpson 2009 ）。
• 初等再帰算術( ERA ) は、再帰が限定された和と積に限定された原始再帰算術(PRA)のサブシステムです。$\displaystyle \Pi _{2}^{0}}$EFA と同様に、文は、EFA が ∀x∃y P ( x , y ) を証明するとき、P は量化子フリーであるという意味で、ERA は、TがERA で定義可能な項である開式P ( x , T ( x )) を証明する。PRA と同様に、ERA は、置換と帰納の規則とすべての基本再帰関数の定義式のみを使用して、完全に論理フリーな方法で定義できる。ただし、PRA とは異なり、基本再帰関数は有限個の基底関数の合成と射影による閉包によって特徴付けられるため、有限個の定義式のみが必要となる。

• 初等関数– 数学関数の一種 
• グレゴルチク階層– 計算可能性理論における関数 
• 逆算数学― 数理論理学の一分野 
• 順序分析– 証明論で用いられる数学的手法 
• タルスキーの高校代数問題– 数学の問題 

• Avigad、Jeremy (2003)、「整数論と初等算術」、Philosophia Mathematica、シリーズ III、11 (3): 257–284、doi : 10.1093/philmat/11.3.257、ISSN 0031-8019、MR 2006194  
• フリードマン、ハーヴェイ（1999年4月16日）、「壮大な予想」、FOMメーリングリスト、2019年11月29日にオリジナルからアーカイブ済み
• シンプソン、スティーブン・G. (2009)、「2階算術のサブシステム」、論理学の展望（第2 版）、ケンブリッジ大学出版局、ISBN 978-0-521-88439-6MR 1723993​