ゲーデルの不完全性定理は、数理論理学の 2 つの有名な定理であり、クルト ゲーデルによって 1931 年に論文Über format unentscheidbare Sätze der Principia Mathematica und verwandter Systeme ( Principia Mathematicaおよび関連システムの形式的決定不可能性について) で実証されました。
導入
大まかに言うと、最初の定理は、算術を行うのに十分な理論は、実証不可能であり、その否定も実証不可能なステートメントが必然的に存在するという意味で、必然的に不完全であると述べています。つまり、次のようなステートメントが存在します。この理論の枠内では決して何も言えないことを私たちは知っています。検討した理論に関する同じ種類の仮説の下で、第 2 の定理は、理論の一貫性を表現するステートメントが存在すること、つまり、すべてを証明することはできず、したがって何かを証明することはできないという事実が存在し、このステートメントは次のような形で証明することはできないことを確認します。理論そのもの。定理の仮定により、集合論など、数学のすべてを形式化すると主張する理論は影響を受けます。したがって、数学的言説には普遍的な真理値があるという考えを放棄すべきでしょうか?純粋に数学の内部的な手段だけではそれに到達することはできないように見えるのですが、それが首尾一貫しているかどうかをどのような根拠で知ることができるのでしょうか?ゲーデルの定理は答えを与えませんが、単純すぎる定理を除外することはできます。この記事の残りの部分で示すように、これら 2 つの制限 (真実がアクセスできない発言、言説の一貫性) は相対的なものにすぎないことにすでに注意する必要があります。
これらの定理、特に当時の数学者、特にデイヴィッド・ヒルベルトとその生徒たちが抱いていた専門分野の概念に対する定理の影響は、非常に予想外でした。最初にこれらの定理とその意味を理解した数学者はほとんどいませんでした。その中には、ジョン・フォン・ノイマンも数えなければなりません。彼は、1930 年に第一不完全性定理に関するゲーデルの最初のプレゼンテーションに出席した後、第二定理 (ゲーデルはすでに知っていた) である帰結について言及する手紙を彼に送りました。 David Hilbert の緊密な協力者である Paul Bernays も、これらの定理が後者の概念に及ぼす影響をすぐに理解し、Grundlagen der Mathematik (Hilbert との共同署名) という著作の中で第 2 の定理[ 1 ]の最初の詳細な実証を行いました。 。最後に、ゲーデルは 1930 年代に数回米国を訪問し、彼の研究はアロンゾ チャーチとその生徒であるスティーブン コール クリーンとジョン バークレー ロッサーに広く受け入れられ、計算可能性の理論の誕生に重要な役割を果たしました。
1900 年にパリでヒルベルトが提示した有名な問題リストの 2 番目は、算術の一貫性を証明する問題でした。問題全体は、ヒルベルトによって回避されていませんが、そのような証明のために私たちがどのような手段を自分自身に与えるかを知ることです。第 2 不完全性定理は、算術そのものよりも (ある意味で明確に) 「強力」でなければならない理論が必要であることを示しています。ヒルベルトの 2 番目の問題に対する答えは、一般に否定的であると考えられています。しかし、1936 年にゲルハルト ゲンツェンは、もちろんゲーデルの第 2 定理と互換性のある方法で、算術の一貫性を証明しました。この証明は非常に興味深いものですが、一貫性の証明としてのその重要性には疑問が残ります (ゲンツェンとヒルベルトのプログラムに関する記事を参照)。
- ゲーデルが自身の定理を実証するに至った歴史的背景と、当時のこれらの定理の影響をよりよく理解するには、ヒルベルトのプログラムに関する記事を参照してください。
この記事の残りの部分は、ゲーデルの記事の内容に正確に従おうとするものではありません。その後、いくつかの点が明らかになりました。まだ少しカジュアルなプレゼンテーションから始めます。定理の証明のスケッチとその記述の詳細は、記事の最後に記載されています。
2 つの定理の説明
第一不完全性定理は、次のような、まだある程度近似的な方法で述べることができます (専門用語は次の段落で説明されています)。
- 一貫性があり、「算術の形式化」が可能な、再帰的に公理化可能な理論では、この理論では証明も反駁もできない算術ステートメントを構築できます。
このような言明は、この理論では決定できないと言われています。理論に依存しないとも言います。
まだ 1931 年の論文の中で、ゲーデルは第 2 不完全性定理を推論しています。
- T が同様の仮定を満たす一貫した理論である場合、理論Tで表現できるTの一貫性はTでは実証できません。
これら 2 つの定理はペアノ算術で証明されており、したがってこの定理よりも強力な理論、特に集合論やプリンキピア数学などの数学の発見を目的とした理論でも証明されています。
定理の適用条件
アイデアを確立するために、問題の理論は、今述べたもの (ペアノ算術、集合論) と同様に、たとえ不完全性の定理が依然として有効であるとしても、同じ条件下では、たとえば直観主義的な論理[ 2 ]またはより高次の論理に移行することによって。
- 再帰的に公理化可能な理論とは、理論の言語のステートメント間の公理を純粋に機械的な方法で認識できるような方法で理論が公理化できることを意味します。これは明らかに、通常の数学のすべてまたは一部を形式化するために使用される理論に当てはまります。
- 理論が公理から矛盾を証明できない場合、その理論は首尾一貫しています。一貫性がある、矛盾がないとも言います。最初の不完全性定理について、ゲーデルは一貫性について少し強力な仮定を立てました。第 2 の定理については、いずれの場合でも、単純なコヒーレンス仮説で十分です。この定理は、コヒーレンス ステートメントの非実証性を示すだけです。 1936 年に JB Rosser は、一貫性の単純な仮説に基づいて最初の不完全性定理の証明を行いました。したがって、厳密に言えば、この記事の冒頭で示した第一不完全性定理の記述は、ゲーデルの記述とまったく同じではありません。これはゲーデル・ロッサーの定理と呼ばれることが多いです。
- 理論により、一方では、少なくとも通常の演算で (ゼロと後続関数によって与えられる) 整数を (特定する必要があるという意味で) 定義できれば、算術演算を形式化することが可能になります。足し算と掛け算、そして一方で、整数に関する特定の数の記述は理論で証明可能です。ペアノ算術はそのような理論であり、両方の不完全性定理の仮定を満たします。実際、前者については、はるかに弱い算術理論で十分です (再帰性は本質的に役に立ちません)。 2 番目の場合、最小限の再発が必要です。
算術を形式化するには、(ゼロと後続に加えて) 加算と乗算で十分であることは注目に値します。これは、ヒルベルトの 10 番目の問題 (Matiyasevich の定理を参照) の解決に向けたまさに最初のステップです。加算だけでは十分ではありません。プレスブルガー算術は、ペアノ算術を加算の言語 (ゼロとその後継に加えて) に限定することによって得られる理論です。
第一不完全性定理の直接的な結果
理論Tが有用な仮説を満たす場合、2 つの理論のそれぞれが得られるようなステートメントが存在すると言うことで、最初の不完全性定理を再定式化できます。1 つはこのステートメントを公理としてTに追加することによって、もう 1 つは次の否定を追加することによって得られます。この声明は一貫しています。それを実証してみましょう。
ステートメントGが与えられた場合、その否定をnot Gで表しましょう。理論T + non-G (公理non-G を追加した理論T ) が一貫している場合にのみ、ステートメントG がTで証明できないことは簡単に示されます。実際、 GがTで実証可能な場合、 G ではない T +は明らかに矛盾しています。逆に、 G ではなく T + が矛盾しているとします。これは、理論Tでは、 G ではないことから矛盾を推測できることを意味します。 G はTの結果であると推測します (これは不合理な推論です)。
したがって、これは、ステートメントG が一貫した理論Tでは決定不可能であると言うのと、2 つの理論T + 非 GおよびT + Gが一貫していると言うのと同じです。これら 2 つの理論のそれぞれにおいて、ステートメントG は明らかに決定不可能ではないため、決定不可能なステートメントの概念は本質的に特定の理論に対して相対的なものであることがわかります。
したがって、 G が第一不完全性定理によってTに対して与えられた決定不可能なステートメントである場合、この定理を再度適用することによって、理論T + Gで決定不可能な (したがって理論Tでも決定不可能な) 新しいステートメントが得られます。
実際、不完全性定理が理論Tに適用される場合、再帰的に公理可能である限り、この理論のすべての一貫した拡張に適用されます。そのような理論を完成させる効果的な方法はありません。
また、どのような理論が関与していても、ゲーデルは得られたステートメントが算術的であること、つまり、それが算術言語で表現できることを示したことにも注目すべきです。これは、明示的に書くのは面倒ですが、論理的には非常に単純な算術記述です (ある意味、この記事の最後で説明します)。たとえば、ツェルメロ・フランケル集合理論に適用されるゲーデルの定理によって算術ステートメントを取得しますが、このステートメントでは決定不可能になります。
第 2 不完全性定理の直接的な結果
第 2 不完全性定理のステートメントを理解し、対偶を使用して再定式化すると役立つ場合があります。
- T が「十分な算術」の形式化を可能にする再帰的公理可能理論であり、 T がそれが首尾一貫していることを表すステートメントを証明する場合、 T は矛盾しています。
一方、第 2 不完全性定理自体から推測できるように、一貫性がないことを表現するステートメントを実証する理論は、矛盾しない可能性が非常に高いです。
証明してみましょう。理論TにおけるTの一貫性を表すステートメントを coh Tと呼びましょう。最初の定理に関する前の段落と同じように、 Tに関する有用な仮説の下で、理論Tが一貫性がある場合、理論T’=T + non coh Tは依然として一貫性のある。 「 Tが矛盾している」とは、 Tに矛盾の証拠があることを意味することを思い出してください。 Tの証明はT’の証明でもあり、追加の公理があるだけです。したがって、ゲーデルの定理の仮説を満たすTのような理論では、非 coh T が結果として非 coh T’を持つことを示すのは簡単です (ただし、 coh Tとcoh Tは表現されたステートメントであることを忘れないでください)これらの理論の言葉で言えば、証明が真に完全であるためには、この表現の詳細に踏み込んでこの含意を示す必要があるでしょう）。したがって、我々は、第 2完全性定理と、この定理の仮説を満たす一貫した理論Tの存在から、たとえばペアノ算術を考えますが、非 coh T’を証明する一貫した理論T’の存在を推定しました。一貫性がないことを表明する声明。幸いなことに、そのような理論は病理学的であり、通常の数学理論の中でそれらに遭遇したことはありません。この結果は直観に衝撃を与えるかもしれませんが、有用な仮説を満たす一貫した理論には、その一貫性の否定を示す拡張があると言うことで、第 2 不完全性定理を再定式化できることを理解することが重要です。
逆に、すべてのステートメントが証明可能である一貫性のない理論では、明らかに、それが一貫性があることを表現するステートメントが実証されます。
これらのさまざまな発言から、第 2 不完全性定理は、それが適用される理論の一貫性、たとえばペアノ算術の一貫性を損なうものではないことがわかります。後者について彼が言っているのは、それは論理的により強力な理論でのみ証明できるということだけです。
第 2 不完全性定理の単純だがかなり驚くべき応用のもう 1 つの例は、レーブの定理です。これは、有用な仮説を満たす理論Tにおいて、このステートメントが理論的に証明可能であるという仮説に基づいてステートメントをTで証明すると述べています。発言を証明することになります。つまり、この仮説は役に立たないということです。
真実と実証可能性
数学的論理以外ではほとんど知られていないものの、ゲーデルの定理を理解するのに役立つ、真理の概念を紹介します。真理は数学的な概念であり、非常に直感的ですが、実証可能性が形式化される理論ほど単純な理論では形式化されないことがわかります。最小限の集合論が必要ですが、実証可能性は算術で満足されます。私たちが使用する真理の概念は数学的に定義されます (ただし、研究されている理論よりも強力な理論で定義されます)。使用される語彙は直感に対応しており、概念は非常に便利です。しかし、この概念を使用するために、この概念に過剰な価値を認める必要はありません。たとえば、ゲーデルは、N で真であることが示されるステートメントを効果的に構築します。これは、「最初の理論よりも強力な理論でそれを証明する方法を知っている」と解釈できます。
ゲーデルの定理は、算術を十分に形式化できる理論に関連しています。簡単にするために、この段落では算術理論、つまり整数についてのみ言及する理論に限定します。
算術標準モデルの真実
実証可能性は理論、公理系との関係で定義されますが、真理はモデル、数学的構造、つまり法則と関係を備えたセットとの関係で定義されます。理論ではステートメントが決定不可能である場合、モデルではステートメントは真か偽であり、他の選択肢はありません。続いて、算術の標準モデルにおける真理、つまり「誰もが知っている」整数(N [ 3 ]と表記します) に焦点を当てます。非常に直感的な構造なので、これらの詳細は不必要に見えるかもしれません。しかし正確には、ゲーデルの不完全性定理は、奇妙にも整数に似た数学的構造の存在を示しています。たとえば、それらは漸化式を含むペアノ算術のすべての公理を検証しますが、「 Nにおける誤った記述を検証する」ため、これらは通常の整数ではありません。実際、 G がTの決定不可能な式である場合、 Tに対するペアノ算術を考えてみましょう。前のセクションで、理論T + GとT + 非 Gが一貫していることを見ました。これは、ゲーデルの完全性定理によれば、これらの理論にはそれぞれモデルがあることを意味します。これら 2 つのモデルは同じステートメントを満たしていません。つまり、同一であることはできません。したがって、そのうちの少なくとも 1 つは標準モデルではありません。ゲーデルの定理を証明すると、標準モデルにおける 2 つの定理のどちらが正しいかがわかります (理論Tが一貫していることがわかります)。ペアノの算術理論でそれを証明する方法を知らずに、モデルNでステートメントが真であることを知っているという事実は、単に、それをより強力な算術理論で証明する方法を知っていることを意味しますが、それは必ずしも知りませんでした。説明するために。
ゲーデルが 1929 年に完全性定理を実証して以来、ゲーデルが定理を実証した時点では、真理の概念は、たとえゲーデルが知っていたとしても、実際には形式化されていませんでした。現在使用されている定義はAlfred Tarski によるもので、1956 年に発行された記事に記載されています。
Nで真理を定義しましょう。この言語には、唯一の定数記号として0 があり、唯一の関数記号としてs (1 を加算する後続関数)、+ および × があり、等号に加えて唯一の関係記号として不等号記号 ≤ があります。
標準モデルは単純に定義されます。モデルの基本セットの唯一の要素は通常の整数であり、すべてs … s 0の形式の言語用語で記述されます ( sは後続関数「add 1」の符号です) “)、つまり、整数の原始的な概念に対応するよく知られた単項表記です。この言語の用語は本質的に、いくつかの変数と正の整数係数を持つ多項式、つまり論理記号を持たない多項式の等式または不等式の基本的なステートメントである原子式です。モデルを定義するには、閉じた原子式、つまり変数、true と false を使用せずに記述する必要があります。
このようにして記した整数 (変数なし!) に関する多項式の等式と不等式のNの真理を簡単に定義できます。また、それを機械的に行うこともできます。つまり、アトミックなステートメント (等式と閉じた多項式の不等式) の真理は次のようになります。アルゴリズム的な意味で決定可能です。関係するアルゴリズムは基本的に 1 進数の加算と乗算であり、概念的には小学校で教えられる 10 進数のアルゴリズムよりも単純です (ただし、使用するのはおそらくより面倒です)。
そこからモデルを定義したため、このモデル内の式の真理性の帰納による定義が得られます。正式な定義には立ち入らずに、いくつかの特定のケースを観察してみましょう。まず第一に、量指定子のない閉じた式の真実は依然として決定可能です。それを等式と不等式 (≠ と ≤) の多項式の論理積と論理和に還元することができます。量指定子の話に移ります。P とQ が1 つの変数をもつ多項式である ∃x( P (x)=Q(x))のようなステートメントは、 P(n)=Q ( n) 。このような整数が存在する場合、マシンは整数を昇順に 1 つずつ試すことで、その整数を見つけることができることに注意してください。しかし、そのような整数が存在しない場合、マシンは停止しません。このような式の検証がアルゴリズムによって決定可能であるという証拠はありません (実際にはそうではありません)。
全称量指定子の場合、状況は「さらに悪い」です。各整数nについて、等式P(n) =Q(n) が真である場合、 ∀ x(P(x)=Q(x))のようなステートメントは真となります。 : これは明確に定義されていますが、その定義に従うと、無限の検証が必要になります。真実と実証可能性の違いがはっきりとわかります。証明は必然的に有限であり、さらに形式的証明を機械的に認識できなければなりません。このような普遍的なステートメントを証明するには、通常、再帰を行います。簡単に言うと、帰納法による証明は、無限の検証を表す有限の方法です。漸化式は、整数ごとに 1 つずつ、無限の証明を構築するために「展開」できます。ただし、再発により、これらの証明には一定の均一性が導入されます[ 4 ] 。この方法ですべての普遍的記述のNにおける真実を捉えることができるという証拠はなく、ゲーデルの定理はこれが当てはまらないことを正確に示しています。ゲーデルのステートメントは、 Nでは真ですが実証不可能ですが、まさに普遍的なステートメントであり、これを∀ x H(x)と呼びます。ペアノ算術の場合を考えてみましょう。このステートメントを正確に定義すると、各整数nについて、 H(n) がペアノ算術で証明可能であることがわかります。しかし、 ∀ x H(x) [ 5 ]を証明することはできません。
N 個の特定のクラスのステートメント、たとえば量指定子のないステートメントの真偽を決定する機械的手段がある場合、特に、この非形式的な意味で、これらのステートメント、またはその否定の証明が得られることに注意してください。この概念は、この証明が導き出された理論に必ずしも注意を払う必要はありません。上で説明したケースでは、これらの証明は、ゲーデルの定理を証明できる理論に効果的に導き出されます。
真実と不完全さ
モデル内の真のステートメントからステートメントを証明する場合、得られるステートメントはこのモデル内で真であり、モデル内のステートメント (閉じた式) は真か偽のいずれかであることを思い出してください。したがって、 Nにおける真のステートメントの理論は演繹によって閉じられ、完全になります。第一不完全性定理からすぐに次のことが導き出されます。
- Nにおける真のステートメントの理論は再帰的に公理化できません。
したがって、真実は演繹によって閉じられる
- T が「十分な算術」を形式化できる再帰的公理可能理論であり、その公理のすべてが N で真である場合、 Tでは証明できないステートメントG true が N で存在します。
これは不完全性定理ですが、ゲーデルの最初の不完全性定理よりも弱いですが、適用される理論が少なく、仮説が大幅に強力であるためです。さらに、第 2 不完全性定理を導出するために、これを算術で直接形式化することはできません[ 6 ] 。したがって、これはタルスキーの定理(1933 年) から推定されており、ゲーデルの定理よりも実証するのが簡単です。証明不可能なステートメントGはNにおいて真であり、理論はNにおいてのみ真のステートメントを証明するため、このステートメントの否定も証明可能ではありません。さらに、理論Tにはモデルがあるため、一貫性があります。
ただし、ゲーデルによって実証されたものと真に同等の主張をこの形式で与えることは可能です。確かに、定理のステートメントで、上記のステートメントGの論理的な複雑さを指定できます。したがって、理論のすべての公理、したがって最終的にはそのすべての定理がNにおいて真であると仮定するのではなく、論理的複雑さのすべての定理が成り立つという結果をもたらす理論の公理に関する仮説で満足することができます。 Gの否定のうち、 Nでは真になります。これはまさに、ゲーデルの一貫性仮説 (後の脚注で説明) に当てはまります。このような主張は、記事の残りの部分の対角化の段落の最後に記載されています。
不完全なシステムと決定不能なステートメントの例
不完全な理論が存在するのは日常茶飯事です。群、環、物体の理論など、多くの理論は完全ではありません。たとえば、群または物体には 2 つの要素または 3 つの要素があると一次的に言えます。算術の場合は異なります。公理を使用して自然数のすべての特性を把握したいと考えています。数学の発見を目的とした理論、プリンキピア・マテマティカまたは公理集合論の場合、まだすべての公理が発見されていないことが予想されます。しかし、ゲーデルの定理は、(理論が再帰的に公理可能である限り) 常に決定不可能なステートメントが残ると述べています。
すでに述べたプレスバーガー算術、特定の特性の代数的に閉じた体の理論、閉じた実体の理論、それに関連する初等幾何学など、興味深い完全な理論もあります。
ペアノ算術における決定不可能なステートメント
ゲーデルの定理を算術に適用すると、理論の一貫性に関わるため、非常に興味深い意味を持つ記述が得られます。ただし、これらのステートメントは選択したコーディングによって異なります。明示的に書くのは面倒です。
パリスとハリントンは 1977 年に、 Nで真となる有限ラムジー定理の強化はペアノ算術では証明できないことを示しました。これは、言語コーディングを使用しない、算術における決定不可能なステートメントの最初の例です。それ以来、私たちは他の人たちを発見してきました。グッドスタインの定理はそのようなステートメントです。その証明は特に単純です (序数が分かっている場合) が、可算序数 ε 0までの帰納法を使用します。カービーとパリスは 1982 年に、ペアノ算術ではこの定理を証明できないことを証明しました。
発見されたこの種のステートメントは、組み合わせ論の結果です。彼らの証明は必ずしも非常に複雑ではなく、実際、証明の技術的な複雑さとそれをペアノ算術で形式化できる可能性との間に関連性があると考える理由はありません。
集合論における決定不可能なステートメント
集合論では、ゲーデルの定理によって提供されるもの以外にも、異なる性質を持つ可能性のある決定不可能なステートメントがあります。したがって、ゲーデル、次にポール・コーエンの研究によると、選択公理と連続体の仮説は、ZF では、Zermelo と Fraenkel の集合論では決定不可能なステートメントであり、2 番目の公理もZFCでは決定不可能です (ZF に次の公理を加えたものです)。選択）。しかし一方で、これらは算術ステートメントではありません。一方、選択公理またはその否定を ZF に追加することによって得られる理論は、ZF に対して等一貫性があります。つまり、一方の一貫性が他方の一貫性につながり、その逆も同様です。連続体仮説も同様です。これは、まさに第 2 不完全性定理に従って、ZF の一貫性を表すステートメントには当てはまりません。第一不完全性定理の通常の証明によって得られる 2 つのステートメントのうちの 1 つについても同様です (これは一貫性ステートメントに相当します)。
集合論T+Aで、集合 (理論の対象) が集合論Tのモデル、つまりTの一貫性であることを示すことができるとすぐに、第 2 不完全性定理によって次のように推定されます。 、 Tが矛盾しない場合、 A はTで証明できません。したがって、「大きな」基数の存在を肯定する特定の公理が ZFC では実証できないことを示します。
不完全性定理と計算可能性
計算可能性の概念は、不完全性定理に関してさまざまな方法で介入します。仮説を定義するためにそれを使用しました。これは、第一不完全性定理の証明に関与します (ゲーデルは原始再帰関数を使用します)。最後に、算術の不完全性と決定不可能性は関連しています。
アルゴリズムの決定不能性
理論のアルゴリズムによる決定可能性、ステートメントが定理であるかどうかをテストするための機械的方法の存在、およびこの理論の完全性の間には密接な関係があります。再帰的に公理可能で完全な理論は決定可能です。したがって、有用な仮説を満たす理論が決定できないことを示すことで、第一不完全性定理を証明できます。この結果、つまり最初の不完全性定理の仮定を満たす理論のアルゴリズムによる決定不可能性は、ゲーデルが最初の不完全性定理のために開発した手法を使用して、1936 年にチューリングとチャーチによって独立して証明されました (決定問題を参照)。決定不可能性の結果、つまり負の結果については、計算可能性を形式化し、この形式化が正しいと確信する必要があります。この確信は数学的根拠のみに基づくものではありません。 1931 年、ゲーデルは、ジャック エルブランドが彼に宛てた手紙の中で説明され、現在ではチューリング完全と呼ばれる計算モデル、一般的な再帰関数を知っていました。ゲーデルは、1934 年にそれを彼自身が明確にして暴露しました。彼がすべての計算可能な関数をこの方法で記述したとき。クリーン、チャーチ、チューリングの研究に続いて、後の 2 人は 1936 年に独立してチャーチの理論を述べました: 計算可能な関数は一般的な再帰関数です。
確率が決定できないステートメントの制限されたクラスを与えることで、より正確に行うことができます。上記の「真実と証明可能性」の段落で展開された議論を取り上げると、たとえば、量指定子のない (変数のない) ステートメントのクラス自体が決定可能であることがわかります。
ゲーデルによって開発された議論を使用して、ステートメント Σ 1の確率が決定不可能であることを示します。 Σ 1 の式の定義 (以下に説明) について詳しく説明するまでもなく、これはヒルベルトの 10 番目の問題、つまり方程式ディオファンティーンを解くための決定アルゴリズムの存在に対する否定的な解決策からそれほど遠くないと思われます。しかし、マーティン・デイビス、ヒラリー・パットナム、ジュリア・ロビンソン、そして最終的にユーリ・マティアセビッチを含む数人の数学者の継続的な努力と、数十年の歳月を経て、1970 年にそこに到達しました (マチアセビッチの定理を参照)。
マティアセヴィッチの定理からゲーデルの第一定理を完全に演繹することができます。決定不可能性を証明するのがはるかに簡単な結果で十分であるため、これは人為的に見えるかもしれません。しかし、特に単純な形式の決定不可能なステートメントを推定することはできます。実際、マティアセヴィッチの定理は、実存的に数量化された多項式等式として記述されたステートメント (閉じた式) の真実性は決定できないと言っているのと同じです。金 ：
- 私たちはそのようなステートメントを機械的に認識できるため、その否定も認識できます。
- このような真のステートメントはすべて再帰的に列挙可能であるため、Matiassevitch の定理によれば、そのような偽のステートメントはすべて再帰的に列挙可能ではありません。
- 再帰的公理化可能な理論の定理のセットは再帰的に列挙可能です (再帰的公理化可能な理論を参照)。したがって、すべての定理は存在量化された多項式等式の否定として記述されます。
- ゲーデルが最初の不完全性定理に対して行った一貫性の仮説は、存在的かつ偽の定量化された平等性が実証できないという直接的な結果をもたらします。
そこから、存在的な量化された多項式の等式性の否定として、またはより単純に普遍的に量化された多項式の不等式として記述される、実証できない真の記述が存在することが推測されます。
不完全性の第一定理の部分的な証明
ゲーデルによる最初の不完全定理の証明には、基本的に 2 つの要素が使用されます。
- 整数の言語とそれを操作できるようにする関数によるコーディング、いわゆる構文の算術化。
- 構文の算術化を使用して、嘘つきのパラドックスに似たステートメントを明らかにする対角線の議論:ゲーデルのステートメントは、コーディングを介して、検討されている理論におけるそれ自体の証明不可能性を肯定するステートメントと同等です。
しかし、ゲーデルの発言は逆説的ではありません。 N が偽であれば証明されるため、 Nは真です。ただし、このステートメントは論理的に複雑であり、コード算術でnの真理を導き出すことができる一貫した理論で証明できるため、十分に単純です ( nが理論のモデルであると仮定する必要はありません)。したがって、 nにも当てはまります。したがって、ステートメントの定義により、それは証明できません。
ゲーデルのステートメントの否定も証明されていないことを示すには、ゲーデルが行ったようなより強力な一貫性仮説が必要です。 Rosser は、単に一貫性を使用できるようにステートメントを巧みに変更しました。ゲーデルの証明に関して、議論は次のとおりです。つまり、ステートメントは真であり、その否定は偽です。 n が理論のモデルであると仮定した場合、それを実証するにはそれだけで十分でしょう。しかし、ゲーデルは、はるかに弱い仮説で十分であるにもかかわらず、十分に弱い論理的複雑さのステートメントを構築しました。それは本質的に、そのような誤ったステートメントは実証可能ではないと言う問題であり、構文的な方法でそれを表現することができます。
上で概略的に示した証拠は、「対角化」の段落でより正確に再開されます。
構文演算
現時点では、コンピューター サイエンスを少しでも知っている人であれば、理論の記述を数値で表現できることを容易に想像できます。ただし、これらのコーディングも理論的には操作する必要があります。問題は言語の制限にあります。つまり、基本的に加算と乗算を関数記号として使用する一次理論です。これは、確率が理論上の式で表現できることを示すためにゲーデルが解決した困難です。
残りは少し技術的なものになります。最初の読み物では、 nがtのモデルであると仮定して引数を簡素化することができます。その場合、ステートメントの論理的な複雑さに注意を払う必要はありません。 β機能と再発の表現の部分は有用なままです。また、概念と、ほぼ上記で想起または書かれた結果を指定します。
コード
自分でコーディングを書くのは楽しいかもしれません。したがって、文献には多くの多様性があります。コーディングの選択自体は重要ではありません。おそらく、理論的にはより簡単に「処理」する人もいます。式とデモンストレーションは、文字、文字、スペース、句読点、およびこれらの句の完成した結果と見なすことができるため、それらを数字でコーディングできます。全体の完成した結果をコーディングできる他の手段（Gödelは、数字を一次因子に分解する出展者を使用します）。また、カップルのコーディング（以下を参照）を使用して、結果、木、したがって有用な構文構造を表現し、完成させます…
式σ0
より重要な問題は、コンピュータープログラムに相当するこれらの構造を操作する機能を備えていることです。一定の機能、加算、乗算の構成、つまりポジティブ全体の係数を持つ多項式に満足できないことは明らかです。式による有用な機能を表します。コードにも非常に役立つ例を見てみましょう。 n × nとnの間のカントールの双方向きはよく知られており、完全に計算可能です。たとえば、 2番目のコンポーネントを栽培することにより、対角線全体（定数合計）によって斜めのカップルをリストします。
この関数は、分割が2であるため、言語の用語で表されることはなくなりましたが、式で表されます（同等の関係には「≡」を使用します）。
- z =
次に、デコード機能、つまり逆トルクトルクなどに進みましょう。量子が必要です：
- x = π1 （z）するまみz 2z =（x+y）（x+y+1）+2y; y = π2 （z） ≡x≤z2z=（x+y）（x+y+1）+2y
したがって、私たちは関数を表し、より正確に彼のグラフ（下線付きの式）は、算術の言語の式によって形成されました。上記の式は非常に具体的です。1つ目は多項式の平等です。3つの自由変数を閉じた言語条件で置き換えると（ S…S0 ）、決定可能になります。次の2つは、境界のある量子を使用しています。 “∃x≤za” a “aなどのxがxが最小または等しいxがあります」。繰り返しますが、2つの自由変数を整数に置き換えた場合、この式は決定可能になります。限られた実存的な定量化を検証するには、端末を探すのに十分であり、見つけたか、声明が検証されているか、それを見つけられませんでしたそうではありません。実存的な定量化が制限されていない場合、これはもはや（アサーションの第2部の場合）そうではありません。境界のある普遍的な定量化を追加することにより、この減速性プロパティを維持できます。「∀x≤pa」（「p、p、a」）のすべてのxの場合は “）に記載されています。通常のブールコネクタを使用した多項式等式から構築された式、および境界のある定量のみが式σ0と呼ばれます。式σ0の否定はσ0であることに注意してください。
私たちは簡単に自分自身を納得させます。閉じた式σ0のnの真実が拒否されることを、真実と実証可能性の段落に議論が与えられます。それらが真か偽かを知る機械的な手段があります。 Gödelの最初の不完全性定理（Gödel-Rosserにはもう少しかかり、2番目の再発）、理論の最小条件、再帰的に公理化可能であることに加えて、Coellenceの仮説を示すことは、すべての式を実証することです。 n 、したがって、 σ0とコヒーレンスの否定による安定性によって、偽らないことを示す。これは、「十分な算術化」によって聞いたことです。これは理論の公理に関する仮説であることに注意してください。たとえば、 nが決定する式σ0のセットは、非常に再帰的に公理化可能な理論の公理システムとして選択できます（明らかに単純化できます）。特に、次のことを示すことができます。
- Peanoの算術では、閉じた式σ0はn Siで真であり、実証可能な場合のみです。
ピアノの算術の再発の公理を実際に使用せずに実証されている結果（これらのステートメントには実際には普遍的な定量がないため、自然です）。
式σ1
式σ0で表される機能を操作するのに満足するのは非常に便利です。真実と実証可能性は混乱し、これらの式は決定されるため、式σ0で表される関数は計算可能です。しかし、「 プログラミング言語」は十分に豊かではありません。式σ1を導入する必要があります。これは、式σ0の頭に実存的な量子を配置することによって得られる式です。一般に、式σ1の否定は式σ1と同等ではありません。次のプロパティがあります。
- nですべての式σ0が真であることを証明する理論では、 nで式σ1が証明可能です。
実際、式σ1 “∃x a x”はnで真です。特定の整数では、「s … s0」を書くことができること、式「s … s0」が真であるか、この式はσ0です。 。
コヒーレントな算術理論があり、 σ0で何が起こっているかに反して、閉じたσ1の誤式を示すものがあります。そのような算術理論は、自分の矛盾を表明する声明を示す人々など、非常に病理学的であることに注意する必要があります（記事の開始を参照）。不完全性の最初の定理に役立つ追加の一貫性の仮説は、 σ共同と呼ばれます。理論は閉じた式σ1falsを示していないと想定することです。特定の式を実証できないため、矛盾はそうではありません。少なくとも単純な一貫性と同じくらい強いコヒーレンスの仮説です。それは本当に強いです：式σ1 [ 7 ]によって理論の一貫性の否定を表現することができます。
決定的な関数、表現可能な関数
nのサブセットe 、またはより一般的なサブセット