初等関数算術のソースを表示

[[数理論理学]]の一分野である[[証明論]]において、'''初等関数算術'''（{{lang-en-short|elementary function arithmetic}}）または'''指数関数算術'''（'''EFA'''）は[[自然数論|算術]]の体系のひとつであり、関数記号 <math>0,1,+,\times,x^y</math> の初等的な性質と、[[有界論理式]]に対する[[数学的帰納法|帰納法]]の[[公理図式]]からなる。同じことであるが、[[有界算術]]のひとつである <math>I\Delta_0</math> に指数関数を追加して得られる体系といってもよい。そのためEFAは <math>I\Delta_0(\exp)</math> とも呼ばれる。

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

==定義==
EFAは（等号付き）一階述語論理の上の理論である。言語は次のものからなる：
*2つの定数記号 <math>0,1</math>
*3つの二項関数記号 <math>+,\times,\exp</math> ここで <math>exp(x,y)</math> は <math>x^y</math> と書かれる
*1つの二項述語記号 <math> < </math> （これは必ずしも必要はない。この述語記号は定義により導入できる。ただし有界量化の定義に便利である。）

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

EFAの公理は次のものからなる：
*[[ロビンソン算術]]の公理すべて（<math>0,1,+,\times,<</math> に関するもの）
*指数関数の公理: <math>x^0 = 1, x^{y+1} = x^y \times x</math>
*有界論理式に対する帰納法の公理図式

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

{{harvtxt|Friedman|1999}}にあるように本来の予想の主張は次のようである：

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

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

==関連する体系==

ロビンソン算術に有界論理式に対する帰納法の公理を追加し、さらに指数関数の全域性を示す論理式を公理に追加することによって、二項関数記号 <math>\exp</math> を落とすことができる。これはEFAと類似の体系で、同じ証明論的な強さを持つが、そこでの作業はより面倒なことになる。
二項関数記号 <math>\exp</math> を忘却することができる。

EFAと同じ証明論的な強さを持ち、<math>\Pi^0_2</math> 保存的な、二階算術の弱い断片が幾つか存在する。それらはRCA{{su|p=*|b=0}} とWKL{{su|p=*|b=0}}と呼ばれる。これらは[[逆数学]]においてしばしば研究される{{harv|Simpson|2009}}。

'''初等帰納的算術'''（{{lang-en-short|elementary recursive arithmetic}}、ERA）は[[原始帰納的算術]]（PRA）の部分体系であり、再帰を[[ELEMENTARY#定義と例|限定和と限定積]]に制限したものである。これもEFAと同じ <math>\Pi^0_2</math> 文を持つ。その意味するところは、EFAで <math>\forall x\exists y P(x,y)</math>（<math>P(x,y)</math> は量化子を持たない）が証明可能であるときに限り、ERAで項 <math>T</math> が定義できて <math>P(x,T(x))</math> が証明可能である、ということである。

PRAと同様、ERAは論理を用いることなく、代入、帰納法、初等帰納的関数の定義式とによって定義できる。しかしながら、PRAとは異なり、初等帰納的算術は有限個の基底関数と射影の関数合成による閉包として特徴付けることができ、したがって有限個の定義式だけを必要とする。

== 関連項目 ==

*[[ELEMENTARY]] 関係する計算複雑性クラス
*[[グジェゴルチク階層]]
*[[逆数学]]
*[[タルスキの高校代数問題]]

==参考文献==
*{{Citation | last1=Avigad | first1=Jeremy | title=Number theory and elementary arithmetic | doi=10.1093/philmat/11.3.257 | mr=2006194 | year=2003 | journal=Philosophia Mathematica. Philosophy of Mathematics, its Learning, and its Application. Series III | issn=0031-8019 | volume=11 | issue=3 | pages=257–284}}
*{{citation |first=Harvey |last=Friedman |title=grand conjectures |year=1999 |url=http://cs.nyu.edu/pipermail/fom/1999-April/003014.html}}
*{{Citation | last1=Simpson | first1=Stephen G. | title=Subsystems of second order arithmetic | url=http://www.math.psu.edu/simpson/sosoa/ | publisher=[[Cambridge University Press]] | edition=2nd | series=Perspectives in Logic | isbn=978-0-521-88439-6 | mr=1723993 | year=2009}}

{{デフォルトソート:しよとうかんすうさんしゆつ}}
[[Category:証明論]]
[[Category:算術の形式理論]]
[[Category:数理論理学]]
[[Category:数学に関する記事]]