初等関数算術

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

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

定義

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

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

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

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

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

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

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

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

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

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

関連する体系

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

EFAと同じ証明論的な強さを持ち、 Π 2 0 {\displaystyle \Pi _{2}^{0}} 保存的な、二階算術の弱い断片が幾つか存在する。それらはRCA*
0 とWKL*
0と呼ばれる。これらは逆数学においてしばしば研究される(Simpson 2009)。

初等帰納的算術（英: elementary recursive arithmetic、ERA）は原始帰納的算術（PRA）の部分体系であり、再帰を限定和と限定積に制限したものである。これもEFAと同じ Π 2 0 {\displaystyle \Pi _{2}^{0}} 文を持つ。その意味するところは、EFAで ∀ x ∃ y P ( x , y ) {\displaystyle \forall x\exists yP(x,y)} （ P ( x , y ) {\displaystyle P(x,y)} は量化子を持たない）が証明可能であるときに限り、ERAで項 T {\displaystyle T} が定義できて P ( x , T ( x ) ) {\displaystyle P(x,T(x))} が証明可能である、ということである。

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

関連項目

参考文献

  • Avigad, Jeremy (2003), “Number theory and elementary arithmetic”, Philosophia Mathematica. Philosophy of Mathematics, its Learning, and its Application. Series III 11 (3): 257–284, doi:10.1093/philmat/11.3.257, ISSN 0031-8019, MR2006194 
  • Friedman, Harvey (1999), grand conjectures, http://cs.nyu.edu/pipermail/fom/1999-April/003014.html 
  • Simpson, Stephen G. (2009), Subsystems of second order arithmetic, Perspectives in Logic (2nd ed.), Cambridge University Press, ISBN 978-0-521-88439-6, MR1723993, http://www.math.psu.edu/simpson/sosoa/