メタ数学の時代とは？ わかりやすく解説

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/04/24 15:46 UTC 版)

「論理学の歴史」の記事における「メタ数学の時代」の解説

ゲーデルとタルスキの名前が1930年代、メタ数学-数学的手法を用いてメタ理論、つまり他の数学的理論に関する数学的理論、を作り出す数学-の発展において決定的な時代を支配した。メタ数学に対する初期の研究はヒルベルト・プログラムによって駆り立てられた。ヒルベルト・プログラムは、有限個の公理で全ての数学を基礎づけることで数学の基礎付けにおいて進行中の危機を解決しようとするもので、「有限主義」的な手法によって数学に無矛盾性を与え、全ての数学的言明の真偽を判断する手続きを提供する。メタ数学の研究が頂点に達したのは、一階述語論理による任意の文は論理的に妥当であるときに、そしてそのときのみ-すなわち、その文がその言語におけるいかなる構造においても真であるとき-導出可能である。これはゲーデルの完全性定理として知られる。その後、彼は二つの重要な定理を証明しており、ヒルベルト・プログラムはその元々の形では達成不可能であることがそれによって示された。二つのうちの一つ目は、アルゴリズムやコンピュータ・プログラムのような効果的方法によってその定理を並べ挙げることができるような無矛盾な公理系で自然数に関する全ての事実を与えられるようなものはないという定理である。そのような全ての系に対して、真であるがその系から証明できない自然数に関する命題が常に存在する。二つ目は、そうした系が自然数に関する基本的な事実を証明できるならば、その系は自身の無矛盾性を証明できないというものである。この二つの結果はゲーデルの不完全性定理、あるいは単に「ゲーデルの定理」と呼ばれる。後に、ゲーデルは選択公理および連続体仮説がツェルメロ-フレンケル集合論と無矛盾であることの証明の一環として集合論的構成可能性の概念を発達させた。 証明論においては、ゲルハルト・ゲンツェンが自然演繹とシークエント計算という概念を発達させた。自然演繹とは論理的推論を、それが実践の中で「自然に」起き、直観論理に最も容易に適用できるものであるように造形しようとする試みであり、シークエント計算は任意の形式的体系において論理的証明の導出を定式化するために構築される。ゲンツェンの著作以降、自然演繹とシークエント計算は証明論、数学的論理学、計算機科学といった分野に広く適用されてきた。また、ゲンツェンは正規化定理とカット除去定理を証明したが、これは論理的証明を正規の形式に還元するのに使われるもので直観論理及び古典論理に呈してなされた。 ウカシェヴィチの弟子アルフレト・タルスキは真理と論理的帰結の定義、論理的充足という意味論的概念によって最もよく知られている。1933年に、彼は(ポーランド語で)『形式言語における真理の概念』を発表し、その中で自身の真理の意味論を提案した: 「雪は白い」のような文は雪が白いときに、そしてそのときにのみ真である。タルスキの理論はメタ言語、つまり言明を真にするもの、と対象言語、つまり真であると主張される文を包含するもの、とを区別して、対象言語の語句と解釈の要素との間に一致(Tスキーマ)を与えた。真理を説明するという困難な課題に対するタルスキのアプローチは論理学と哲学に、特にモデル理論の発展に永続的に影響を与えている。タルスキは演繹系の方法論や完全性、決定可能性、無矛盾性、構造といった重要な諸原理に関する重要な研究も行っている。Anita Fefermanによれば、タルスキは「20世紀の論理学の相貌を一変させた。」 アロンゾ・チャーチとアラン・チューリングは計算可能性の形式的なモデルを提議し、1936年および1937年にそれぞれ独自にヒルベルトの「決定問題」を否定的に解決した。「決定問題」とは、任意の形式的・数学的言明が与えられたときにその言明の真偽をアルゴリズム的に決定できる手順を探求するものである。チャーチとチューリングはそのような手順が存在しないことを証明した; チューリングの論文ではアルゴリズム的な解決が存在しない数学的問題の重要な例として停止性問題が挙げられている。 チャーチの計算のシステムは発展してラムダ計算となり、一方チューリングマシンは多目的計算装置の標準的なモデルとなった。他にも数多くの計算モデルが提起されたが、それらは皆チャーチやチューリングが提案したものと同等の能力を持っていた。この結果から、人間が実行できる任意の確定的アルゴリズムはチューリングマシンも実行できるというチャーチ＝チューリングのテーゼが導かれた。チャーチは補足的な決定不可能の結果を証明し、ペアノ計算も一階述語論理も決定不可能であることを示した。その後、1940年代にエミール・ポストとスティーヴン・コール・クリーネが計算可能性理論の射程を拡張し、チューリング次数の概念を導入した。 20世紀最初の十年の成果は分析哲学や哲学的論理学に、特に1950年以降の様相論理、時相論理、義務論理、適切さの論理といった分野に影響を及ぼした。

※この「メタ数学の時代」の解説は、「論理学の歴史」の解説の一部です。
「メタ数学の時代」を含む「論理学の歴史」の記事については、「論理学の歴史」の概要を参照ください。