関連する体系
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2020/05/20 10:10 UTC 版)
ロビンソン算術に有界論理式に対する帰納法の公理を追加し、さらに指数関数の全域性を示す論理式を公理に追加することによって、二項関数記号 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とは異なり、初等帰納的算術は有限個の基底関数と射影の関数合成による閉包として特徴付けることができ、したがって有限個の定義式だけを必要とする。
※この「関連する体系」の解説は、「初等関数算術」の解説の一部です。
「関連する体系」を含む「初等関数算術」の記事については、「初等関数算術」の概要を参照ください。
- 関連する体系のページへのリンク
