定義可能性、証明、計算可能性の相互関係
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/06/24 05:44 UTC 版)
「再帰理論」の記事における「定義可能性、証明、計算可能性の相互関係」の解説
自然数の集合のチューリング次数と、一階述語論理を用いてその集合を定義する（算術的階層から見た）困難さの間には、密接な関係がある。そのような関係性を正確に示す一例がポストの定理である。より弱い関係性として、例えばクルト・ゲーデルが不完全性定理の証明の中で示した例がある。ゲーデルの証明は、実効的な一階理論の論理的結果の集合は帰納的可算集合を成すこと、そしてもしその理論が十分強いならこの集合は計算不可能になることを示している。同様に、タルスキの定義不可能性定理(en)は定義可能性と計算可能性の両方の言葉で解釈することができる。 再帰理論は二階算術（自然数と自然数の集合に関する形式的理論）とも関係している。特定の集合が計算可能だったり相対的に計算可能だったりする場合、それらの集合は二階算術の中の弱い体系内で定義できることがよくある。逆数学の研究プログラムは、よく知られた数学的定理に内在する計算不可能性を測る尺度としてこれらの体系を用いる。Simpson (1999) は二階算術と逆数学に関する様々な話題を取り上げている。 証明論の分野の研究対象には、二階算術とペアノ算術の他にも、ペアノ算術よりも弱い自然数に関する形式的体系などがある。これらの弱い体系の強さを分類する一つの方法として、それらの体系の中で「どの計算可能関数が全域関数であると証明できるか」による特徴付けがある (Fairtlough and Wainer (1998)を参照されたい)。例えば、原始帰納的算術において全域関数であることが証明可能な計算可能関数は原始帰納的なものに限られるが、ペアノ算術ではアッカーマン関数のような原始帰納的でない関数が全域関数であることを証明できる。とはいえペアノ算術でも全ての計算可能関数が全域関数と証明できる訳ではない。そのような関数としてはグッドスタインの定理から得られる例がある。
※この「定義可能性、証明、計算可能性の相互関係」の解説は、「再帰理論」の解説の一部です。
「定義可能性、証明、計算可能性の相互関係」を含む「再帰理論」の記事については、「再帰理論」の概要を参照ください。
- 定義可能性、証明、計算可能性の相互関係のページへのリンク
