トップページ   実数とは何か?無限とは?   Σ1健全性による不完全性定理   クライゼルの注意   備忘録   不完全性定理のための傾向と対策

このページでは数式をたくさん使います。文章だけで説明してくれという人は こちらのページ をご覧ください。

目次

  1. 不完全性定理のすごく簡単な説明
  2. 不完全性定理に至る歴史
  3. 万能論理式
  4. リシャールのパラドクス
  5. パラドクスの原因
  6. 証明関数の不完全性その1
  7. 証明関数の不完全性その2
  8. ゲーデル文
  9. ゲーデル文の真理値
  10. モデル
  11. 完全な自然数論
  12. ゲーデル文は論理的帰結か?
  13. AIは知性を実現できるか?
  14. 超形式的体系
  15. 自己言及しない不完全性定理
  16. 真の算術と選択公理
  17. 正直者のパラドクス
  18. 第二不完全性定理
  19. あとがき
  20. 備忘録

不完全性定理のすごく簡単な説明

 ここでは、 ゲーデルの不完全性定理の証明を専門書で読んでみたけど分かった気がしない人向けに、 すごく簡単な説明を試みます。 そういう私も、実は不完全性定理をよく理解しているわけではありません。 しかし、とある入門書を参考に、以下で紹介する説明を考えて一応納得できました。 そこで、未来の自分が忘れてしまわないように書き留めておくことにしました。

 とは言うものの、 専門書で紹介されているような一般的応用の効く形で説明するのは難しいので、 始めは、一階述語論理による健全な自然数論の不完全性定理に的を絞ります。 あまり汎用的すぎると抽象度が高くなって難解になります。 そういう場合、具体的に対象を絞った方がわかりやすくなると思うからです。 その後、いろいろ拡張した話題を取り上げます。

 インターネット上には、 嘘つきのパラドクスなどを用いた日常言語による不完全性定理の解説が多数あります。 確かにそれでも分かった気になれるかもしれませんが、 私は何だか誤魔化されているような気がして、今一つ数学した気分になれません。 かと言って、バリバリに専門的な説明を展開されてもチンプンカンプンです。

 日常言語で誤魔化されたくはないけれど、専門的な説明も勘弁。 そんなニッチな要望に応えるために、このページは書かれました。 まあ、そのニッチは主に私なんですけどね。 私以外でも、不完全性定理にそのような思いを抱える人がいるなら、 このページを是非参考にしてみてください。 数式は見たくないけど、不完全性定理について知りたいという方は こちらのページ をご覧ください。

 このページは、 既に不完全性定理に関してそれなりに知っている人を対象としていますが、 一応、不完全性定理とは何なのかを説明しておきます。

 不完全性定理には第一不完全性定理と第二不完全性定理があります。 第一不完全性定理とは、ある条件を満たす自然数論は、 どんなに工夫してもその中に証明も反証もできない論理式が存在するというものです。 ある条件とは、 感覚的に説明すると「コンピュータで扱えて矛盾がない」と思えば大体合ってます。

 第二不完全性定理とは、第一不完全性定理の条件に加えて、 数学的帰納法が扱える自然数論では、 自分自身が無矛盾であることを証明することはできないというものです。 つまり、第一不完全性定理の証明も反証もできない論理式の例の1つが、 自分自身の無矛盾性を表す論理式ということです。

【不完全性定理に至る歴史】

 まず簡単に、不完全性定理がどのような経緯で登場したのか触れておきます。 不完全性定理登場前夜の19世紀に、 それまでの数学からそれ以後の数学へと、 その性格を一変させる大発明がカントールさんによってなされました。 集合論と呼ばれる数学分野の登場です。

 私は小学生のころに集合を習いましたが、 何のためにこんなことをするのか理解できませんでした。 いや、問題を解くことはできましたけどね。 しかし、実のところ集合論はあらゆる数学の基礎であり、 集合という概念のみで現代数学の全ての概念を説明できる画期的な理論だったのです。 集合を使ってありとあらゆる数学上の構造を作り出し説明できる。 数学者の喜びは大きなものでしたと竹内外史さんの「集合とはなにか」に書かれています。 このことを聖書になぞらえてカントールの楽園と呼ぶそうです。

 ところが、しばらくして集合論におかしなことが見つかり始めます。 例えば、全ての集合の集合 S を考えると、 S も集合なので S 自身が S の要素になります。つまり自分自身を含んでいます。 このような集合があちこちで矛盾を生じ始めたのです。 なら、自分自身を含まない集合だけ考えれば良いのではと思うかもしれません。 しかし、自分自身を含まない集合の集合 R を考えると、 R は自分自身を含むとしても含まないとしても矛盾してしまうのです。 これをラッセルのパラドクスと言います。

 集合論で数学の全てが説明できますから、 集合論の矛盾はそのまま数学の矛盾と考えられました。 そう、数学は深刻な危機に陥ってしまったのです。 数学者たちはカントールの楽園から出ていかねばならなくなりました。 まさしく失楽園というわけです。

 この危機的状況を打開するために、ヒルベルトさんがある計画を提案します。 曖昧だった集合論の公理系を整備して、形式的体系と呼ばれる体系を構築し、 以下の2つの目標を達成しようとしたのです。

 これをヒルベルト・プログラムと言います。

 多くの数学者たちが数学の危機を救おうと、 ヒルベルト・プログラムに取り組みました。 そしてその時、ゲーデルさんが不完全性定理を証明してしまったのです。 つまり、ある条件を満たす形式的体系は不完全であり無矛盾性は証明できないと。 ヒルベルト・プログラムは大きな痛手を負ってしまいました。

 その後、数学者たちは、非形式的な有限の立場やその拡張で、 数学の無矛盾性の証明にチャレンジしていくことになります。 そして現在、集合論の矛盾の原因などが理解されるようになり、 矛盾を回避する公理系なども整備されたことにより、 数学の危機はあまり心配されることはなくなったそうです。

【万能論理式】

 それでは本題に入りましょう。 はじめに、自然数論に関する全ての1変数論理式に番号を振ります。 例えば、論理式番号 \(1\) の論理式は \(x \gt 0\)、 論理式番号 \(2\) の論理式は \(x + 1 = 2\) という風に番号を振ります。 実際の番号の振り方は対応表の作り方によって変わるので、 ここではあくまで一例と思ってください。 後にリシャールのパラドクスという逆説を使って自然数論の不完全性を証明する際に、 この論理式番号が必要になります。

 ゲーデルさんがゲーデル数という概念を使って、 任意の記号列が文法的に正しい論理式かどうかを判定する原始帰納的述語を作ったので、 1変数論理式に番号を振ることが可能です。

 いろいろ専門用語が出てきたので1つ1つ説明しましょう。まず、 ゲーデル数とは、論理式や関数などあらゆる記号列をコード化したものです。 UTF-8 などの文字コードを想像してもらえば分かりやすいと思います。 論理式や関数などの記号列も、 文字コードで見れば極めて大きな1つの自然数と見なせます。それがゲーデル数です。 自然数論では自然数やその関数しか扱えませんので、 自然数論の中で記号列を操作して証明を行うためには、 記号列をこのゲーデル数に置き換えて考える必要があります。 ちょっとだけ注意点ですが、ゲーデル数と論理式番号は別物ですよ。 論理式番号は1変数論理式のみに振られた番号です。 ゲーデル数はあらゆる記号列に振られた番号です。

 次に、原始帰納的とは、計算に必要なステップ数の最大値を、 あらかじめ有限な数値として見積もることができることを言います。 つまり、必ず予定時間内に計算結果を確認できるということです。 無限ループに陥って、計算が停止しないというようなことはありません。 計算が必ず停止するというこの性質は、 不完全性と密接な関係にあるので気に留めておいてください。

 そして、述語とは、\(A(x)\) のような論理式で表され、 変数 \(x\) に具体的数を代入すると真か偽かが判定できる式のことです。 具体的数にゲーデル数を指定すると、 ゲーデル数に対応した記号列に対して何かの性質を判定できることになります。

 さて、話を論理式番号に戻しましょう。 1変数論理式に番号を振る仕組みは以下のようなものです。 まず、ゲーデル数を \(0\) から始めて \(0,1,2,3,\ldots\) とカウントアップします。 次にそれを、 文法的に正しい1変数論理式のゲーデル数かどうかを判定する述語で判定します。 何が文法的に正しいかは、自然数論の言語から決まります。 判定に合格したゲーデル数を集めることで、 全ての文法的に正しい1変数論理式のゲーデル数が得られます。 最後に、得られたゲーデル数を大きさ順に並べれば、 全ての1変数論理式に番号が振れます。判定に合格しない多くのゲーデル数は、 1変数論理式でないか文法的におかしい無意味な記号列のゲーデル数です。

 直感的には、これはコンパイラと思えば分かりやすいと思います。つまり、 書いたソースコードが文法的に正しい1変数論理式かコンパイルして確かめるわけです。 実行結果は実行してみないと分かりませんが、 文法的に正しいかチェックするだけなら原始帰納的にできると思ってください。

 続いて、万能論理式の話に入りましょう。論理式番号を \(m\) として、 \(m\) 番目の1変数論理式 \(f_m(y)\) と論理的に同値となる論理式を \(u(m,y)\) とします。これは、 あらゆる文法的に正しい自然数論の1変数論理式を表すことができる万能論理式です。 つまり、任意の論理式番号 \(m\) と 入力 \(n\) に対して以下の関係が成り立ちます。

\[ u(m,n) \Leftrightarrow f_m(n) \]

 今のところ、万能論理式 \(u(x,y)\) が存在するかどうかはまだ分かりませんが、 とりあえず一旦存在すると仮定しましょう。

 ところで、このページでは \(x,y,z\) などは変数を表し、\(a,c,g,k,m,n\) などは定数を表すとします。 変数の値は具体的に定まっていませんが、定数は定まっていると考えます。 つまり、定数はその値を使って具体的に計算を実行することができます。そして、 変数のある論理式の変数全てに定数を代入した論理式を閉論理式と呼ぶことにします。 つまり、論理式 \(A(x,y)\) の \(x,y\) に \(m,n\) を代入した \(A(m,n)\) のような論理式が閉論理式です。 さらに、元から変数の無い論理式のことも閉論理式に含めます。 また、ここでは詳しく説明しませんが、 変数が全て量化子で束縛されている論理式も閉論理式です。

 変数のある論理式は変数が変数のままでは具体的な値が定まらず。 \(x = x\) のような例外を除いて真理値は定まりませんが、 閉論理式なら具体的な計算が実行可能なので必ず真理値が定まっていると考えられます。 以下の議論では真理値が定まっている論理式を主体的に扱います。

【リシャールのパラドクス】

 ここで、万能論理式 \(u(x,y)\) 自体が文法的に正しい自然数論の論理式だとします。 すると \(u(m,y)\) は \(m\) を適当に選べば、 あらゆる文法的に正しい自然数論の1変数論理式と論理的に同値とすることができるので、 次のような1変数論理式 \(\lnot u(y,y)\) とも論理的に同値となります(\(\lnot\) は否定を表す)。

\[ u(m,n) \Leftrightarrow \lnot u(n,n) \]

 しかし、 ここで入力 \(n\) を \(n = m\) となるように選ぶと以下のように矛盾します。

\[ u(m,m) \Leftrightarrow \lnot u(m,m) \]

 \(u(m,m)\) とその否定が論理的に同値になるわけです。 これがいわゆるリシャールのパラドクスです。 自然数論に万能論理式 \(u(x,y)\) が存在すると仮定すると、 このような矛盾が起こります。 つまり、万能論理式は存在しないということです。

【パラドクスの原因】

 パラドクスが起きた原因を探ってみましょう。 それには \(u(x,y)\) がどのように作られているかを分析してみます。 まず、\(x\) 番目の1変数論理式に \(y\) を代入した閉論理式のゲーデル数を返す関数を \(s(x,y)\) としましょう。 これを代入関数と呼ぶことにします。 代入関数は自然数論で原始帰納的に書けることをゲーデルさんが証明しています。

\[ s(x,y) = x~番目の1変数論理式に~y~を代入した閉論理式のゲーデル数 \]

 ここで、論理式 \(A(y)\) の論理式番号を \(a\) とし、\(n\) を任意の自然数、 \(A(n)\) のゲーデル数を \(|A(n)|\) で表すと、

\[ s(a,n)=|A(n)| \]

 と表せます。あとで使いますから憶えておいてくださいね。

 \(s(x,y)\) が自然数論で原始帰納的に書けることの証明は、 非常に面倒臭いものですが、プログラマなら、 これが簡単な構文解析で実現できることを直感的に理解できるでしょう。 また、\(x\) 個以上の文法的に正しい1変数論理式を得るまでに、 最大でも何桁のゲーデル数まで計算すればよいのか見積もれるので、 バグがなければ無限ループに陥るような処理でもありません。 つまり、原始帰納的に書けることはほぼ明らかです。

 感覚的に説明すると、\(s(x,y)\) は、 論理式番号 \(x\) と入力 \(y\) を指定して、 文法的に正しい閉論理式をリストアップする関数です。 例えば、実際に計算が実行できる計算可能な論理式などがリストアップされます。 ただし、必ずしも計算可能な論理式だけがリストアップされるわけではありません。 真理値を具体的に判定するアルゴリズムが無い論理式なども含まれます。 アルゴリズムとは有限回の計算で結果に到達する手続きのことです。 また、無限に長い論理式はリストアップされません。 無限に長い論理式は神様には計算可能かもしれませんが、 \(s(x,y)\) では取り扱いません。\(s(x,y)\) は原始帰納的だからです。 つまり、無限に長い論理式は文法的に正しいとは考えません。

 続いて、文法的に正しい閉論理式 \(f\) のゲーデル数 \(z=|f|\) を入力すると、 その真理値を \(1\) か \(0\) で返す関数を \(t(z)\) と仮定します。

\[ t(z) = \left\{ \begin{array}{cl} 1 & (~ゲーデル数が~z~の閉論理式が真~) \\ 0 & (~ゲーデル数が~z~の閉論理式が偽~) \end{array} \right. \]

 すると、\(F\) を文法的に正しい全ての閉論理式の集合とする時、 以下の関係が成り立ちます。後で使いますから憶えておいてくださいね。

\[ \forall f\in F(~f\Leftrightarrow t(|f|)=1~)\hspace{3em}\tag{式★} \]

 \(\forall f\in F(...)\) という式は、 集合 \(F\) に属する全ての \(f\) に対して \(...\) が成り立つという意味です。

 この \(s(x,y)\) と \(t(z)\) を使うと、 万能論理式 \(u(x,y)\) は以下のように書けます。

\[ u(x,y) \stackrel{\mathrm{def}}{=} t(s(x,y))=1 \]

 「\(\stackrel{\mathrm{def}}{=}\)」は左辺を右辺で定義するの意味です。 先のコンパイラの例え話で言うと、\(s(x,y)\) が返すゲーデル数(実行ファイル)を \(t(z)\) という処理系で実行すると解釈できます。

 \(s(x,y)\) は、 ゲーデルさんが自然数論で原始帰納的に書けることを証明しているので、 何か間違いがあるとは思えません。 すると、問題があるのは \(t(z)\) と言うことになります。 つまり、\(F\) に属する任意の閉論理式のゲーデル数を与えると、 その真理値を \(1\) あるいは \(0\) と判定するアルゴリズムのある \(t(z)\) は存在しないということです。 これをタルスキの定理と言うんだそうです。もし、そのような \(t(z)\) が存在すると、 \(t(z)=1\) は当然文法的に正しい自然数の論理式になるので、 \(u(x,y)\) が文法的に正しい自然数論の論理式で書けることになり、 リシャールのパラドクスが起こります。

 ただし、アルゴリズムの無い \(t(z)\) は存在します。 しかし、リシャールのパラドクスは起こりません。 矛盾を導く具体的なアルゴリズムが無いか、 \(t(z)=1\) が無限に長い論理式になって自然数論では書けないからです。

【証明関数の不完全性その1】

 さて、ここからいよいよ不完全性の話です。 以下の説明では、証明可能なこと自身を証明するというようなメタな議論をしますので、 証明される証明のことを形式的証明と呼び、メタな証明と区別します。 そして、「形式的に証明される」のように表現することとします。 ただし、文脈から明らかな時は、形式的という言葉は省略することとします。

 専門書では、ここで数項だの表現定理だのを用いて自然数論を形式化しますが、 はっきり言ってわけが分からないので、本ページではアバウトに行きます。 感覚的には形式化とは、 論理式をゲーデル数で表して数値計算することで証明を行うことです。 また、表現定理というのは、 我々が普段使っている自然数論で計算可能な関数や述語は、 形式化された自然数論の中にも存在することを言います。

 それでは、証明関数から定義しましょう。 ゲーデル数が \(z\) であるような \(F\) に属する閉論理式が、 形式的に証明可能な時に \(1\)、証明不能な時に \(0\) を返す関数を証明関数と言い \(p(z)\) で表します。 「証明可能」と「真」という概念は似ていますが別物であることに注意してください。 \(p(z)\) は以下のように定義されます。

\[ p(z) = \left\{ \begin{array}{cl} 1 & (~ゲーデル数が~z~の閉論理式は形式的に証明可能~) \\ 0 & (~ゲーデル数が~z~の閉論理式は形式的に証明不能~) \end{array} \right. \]

 ただし、ここでは証明関数は計算可能であるとします。 おおざっぱに言えば結果を計算するプログラムが存在するということです。 プログラムが存在しないような証明関数を考えると、 以下の議論は成り立ちませんので注意してください。 理由については こちら に書いてあります。

 証明関数の具体的実装の1つは、 ゲーデル数のカウントアップを使ってあり得る形式的証明の全てを生成して、 ゲーデル数が \(z\) の閉論理式の証明になっていないかチェックするというものです。 形式的証明も記号列で表されますからゲーデル数で表すことができます。 よって、形式的証明が存在するならカウントアップでいずれは到達します。 したがって、この実装では形式的証明が存在するなら必ず証明できます。 問題が難しいから証明できないということはありません。 逆に、形式的証明が存在しない場合は計算が終了しません。

 次に、証明関数を用いて形式的完全性を定義しましょう。 自然数論のような理論が形式的に完全であるとは、 \(F\) に属する任意の閉論理式 \(f\) に対して、少なくとも \(p(|f|)\) あるいは \(p(|\lnot f|)\) が必ず \(1\) を返すことを言います。 \(F\) に属する閉論理式は、 少なくとも形式的に証明あるいは反証できるということです。 つまり、以下の条件を満たすとき形式的に完全であると言います。

\[ \forall f\in F(~p(|f|)=1 \lor p(|\lnot f|)=1~) \]

 また、証明関数 \(p(z)\) は、 \(p(|f|) = 1\) のとき閉論理式 \(f\) は真となり、 \(p(|\lnot f|) = 1\) のとき閉論理式 \(f\) は偽となるという条件も満たしていないと意味がありません。 つまり、「証明可能なら真」「反証可能なら偽」ということです。 これを健全性と言います。 証明可能な論理式の真理値が偽だったら、そんな証明に意味はありませんよね? 健全性は証明関数が証明関数であるためには譲れない条件です。 ここは重要ですから憶えておいてくださいね。

\[ 閉論理式~f~の真理値 = \left\{ \begin{array}{cl} 真 & (~p(|f|)=1~) \\ 偽 & (~p(|\lnot f|)=1~) \end{array} \right.\hspace{3em}\tag{式※} \]

 ここで、もし自然数論が形式的に完全かつ健全だとすると、 証明不能と反証可能が同値になります。 なぜなら、形式的に完全だと少なくとも証明あるいは反証できます。 証明も反証もできないということはありません。 また、健全だと証明できれば真であり反証できれば偽なので、 証明可能と反証可能が同時に成立することはありません。したがって、 集合 \(F\) が証明可能と反証可能でオーバーラップ無しにきれに2分割されます。 さらに、証明可能か証明不能かのどちらかなのですから、 証明不能と反証可能が同値になります。つまり、以下の関係が成り立ちます。

\[ \forall f\in F(~p(|f|)=0\Leftrightarrow p(|\lnot f|)=1~) \]

 詳しい証明はその2で行います。

 そして、証明不能と反証可能が同値になると、\(p(z)\) は以下の関係を満たし、

\[ \forall f\in F(~f\Leftrightarrow p(|f|)=1~) \]

 先の \(t(z)\) そのものとなり((式★)参照)、 万能論理式 \(p(s(x,y))=1\) が作れることになります。 すなわち、\(F\) に属する任意の閉論理式 \(f\) に対して、 \(p(|f|)\) が \(1\) か \(0\) か決定するアルゴリズムが有ることになります。 つまり、健全性を仮定してあるので、任意の \(f\) に対して真理値を決定するアルゴリズムが有ることになりパラドクスが起こります。 よって、健全性を維持したままパラドクスを回避するには、 完全性をあきらめる必要があります。したがって、\(p(z)\) は \(F\) に属する全ての閉論理式を証明あるいは反証することはできません。 言い換えると、特定の \(z\) に対してアルゴリズムが有りません。

 まとめると、健全性が成り立ち、\(s(x,y)\) が存在するような数学的理論で、 リシャールのパラドクスを回避したければ、その理論は不完全になるということです。 つまり、その理論に形式的完全性の条件を満足する \(p(z)\) は存在しません。 自然数論では \(s(x,y)\) が原始帰納的に書けますので、 自然数論は、\(p(z)\) が健全で計算可能なら不完全ということになります。 これで自然数論の不完全性が証明できました。

 ところで、 アルゴリズムと計算可能という言葉の使い方が気になった人もいるかもしれません。 自然数論は不完全で \(p(z)\) は特定の \(z\) に対してアルゴリズムが無いのに、 \(p(z)\) を計算可能と言ってもいいのかと。 私もこの言葉の使い方は気持ち悪いんですが、 計算理論では、このような部分的にアルゴリズムが無い、 つまり、有限回の計算で結果にたどり着かないことがある関数も、 全体としてプログラムで記述できる場合は計算可能とみなします。

【証明関数の不完全性のその2】

 次の話に移りますが、専門書で説明されている不完全性定理では、 上記、「健全性が成り立ち」の部分が「無矛盾で」と書かれていると思います。 健全性は無矛盾性を含むより強い性質なので、健全なら形式的に無矛盾です。 本ページでは説明のしやすさのため、より強い健全性を仮定しています。 ちなみに、形式的に矛盾するとは \(p(|f|)=1\) かつ \(p(|\lnot f|)=1\) となる \(f\) が存在することです。

 簡単に健全であれば形式的に無矛盾であることを説明しておきます。 「証明可能なら真」ですから、 証明可能な閉論理式の集合は真である閉論理式の集合の部分集合です。 また、「反証可能なら偽」ですから、 反証可能な閉論理式の集合は偽である閉論理式の集合の部分集合です。 真である集合と偽である集合は共通部分を持ちませんから、 証明可能な集合と反証可能な集合も共通部分を持ちません。 つまり、\(p(|f|)=1\) かつ \(p(|\lnot f|)=1\) となる \(f\) は存在しません。

 さて、健全なら無矛盾であることが示されたので、 説明を先送りしていたところを説明します。 上記では、形式的に完全かつ健全なら証明不能と反証可能が同値になると書きましが、 その詳しい証明を示しましょう。 まず、健全なら無矛盾なので以下の式が成り立ちます。

\[ \lnot(\exists f\in F(~p(|f|)=1 \land p(|\lnot f|)=1~)) \]

 \(\exists f\in F(...)\) という式は、 集合 \(F\) に属するどれかの \(f\) に対して \(...\) が成り立つという意味です。

 これは、ド・モルガンの法則より以下の式と同値です。

\[ \forall f\in F(~p(|f|)=0 \lor p(|\lnot f|)=0~) \]

 さらに、形式的に完全なら形式的完全性の条件より、以下の式が成り立ちます。

\[ \forall f\in F(~p(|f|)=1 \lor p(|\lnot f|)=1~) \]

 \(\lnot A \lor B\) は \(A \Rightarrow B\) と \(A \lor \lnot B\) は \(A \Leftarrow B\) と同値でなので、 これらは、

\[ \begin{eqnarray} \forall f\in F(~p(|f|)=0 & \Leftarrow & p(|\lnot f|)=1~) \\ \forall f\in F(~p(|f|)=0 & \Rightarrow & p(|\lnot f|)=1~) \end{eqnarray} \]

 という関係になります。よって、以下のように両辺が同値ということになります。

\[ \forall f\in F(~p(|f|)=0 \Leftrightarrow p(|\lnot f|)=1~) \\ \]

 最後に、証明関数 \(p(z)\) に関して注意すべき点が1つあります。 \(p(z)\) の値を計算するとき、計算が永遠に終わらない場合があるのです。 つまり、\(p(z)\) は原始帰納的ではありません。 そして、計算が終わらないときは \(p(z)=0\) であると考えます。何故ならば、 計算が終了しないのなら証明も終了しないからです。 証明が終了しないのなら証明不能です。つまり、値は \(0\) でなくてはなりません。 しかし、実際には \(0\) であることを確認することはできません。 終了しないのですから。

 この点は結構重要で、もし1日コンピュータで \(p(z)\) を動かせば必ず終了するのだとするとすごいことが起こります。 例えば、数学上の未解決な問題を1つ持ってきて \(A\) という論理式で表すとします。 すると、\(p(z)\) に \(|A|\) および \(|\lnot A|\) を入力すれば、 それが肯定的に解決されるのか否定的に解決されるのか、 もしくは証明も反証もできない類の問題なのか1日あれば判明することになります。 これでは数学者は全員失業ですね。

 実際には、太陽が赤色巨星になるまで \(p(z)\) を動かし続けても結果が \(1\) か \(0\) か分からないかもしれません。 このページではいとも簡単に \(p(z)=0\) のように計算が終了したかのように書いてますが、 ある意味これは神の視点と言えるでしょう。

【ゲーデル文】

 今までの説明で、不完全性は証明されましたが、 まだ具体的に形式的証明も反証もできない閉論理式は構成していません。 ここでは、実際に証明も反証もできない閉論理式がどんなものか確認してみましょう。 以下では、対象となる理論は健全であると仮定します。

 まず、以下のような1変数論理式 \(G(y)\) を定義します。 ただし、\(p(z)\) は計算可能な証明関数であり自然数論で書けるとします。

\[ G(y) \stackrel{\mathrm{def}}{=} \lnot(p(s(y,y))=1) \]

 \(G(y)\) は自然数論の1変数論理式なので、論理式番号が対応しています。 仮にその論理式番号を \(g\) とすると、\(G(g)\) が目的の閉論理式になります。 この \(G(g)\) のことをゲーデル文と呼びます。

 本当に証明も反証もできないか確認してみましょう。 まず、\(G(g)\) が形式的に証明可能と仮定してみます。 すると、以下のようになります。

\[ \begin{eqnarray} p(|G(g)|)=1 &\Rightarrow & G(g) ~~\cdots 証明可能なら真(式※)より\\ &\Leftrightarrow& \lnot(p(s(g,g))=1) \\ &\Leftrightarrow& \lnot(p(|G(g)|)=1)~~\cdots s(g,g)=|G(g)|~より \end{eqnarray} \]

 証明可能、つまり \(p(|G(g)|)=1\) と仮定したのに、\(\lnot(p(|G(g)|)=1)\) が導かれ矛盾します。

 今度は、\(G(g)\) が形式的に反証可能と仮定してみましょう。 すると、以下のようになります。

\[ \begin{eqnarray} p(|\lnot G(g)|)=1 &\Rightarrow & \lnot G(g) ~~\cdots 反証可能なら偽(式※)より\\ &\Leftrightarrow& p(s(g,g))=1 \\ &\Leftrightarrow& p(|G(g)|)=1 \end{eqnarray} \]

 反証可能、つまり、\(p(|\lnot G(g)|)=1\) と仮定したのに、 \(p(|G(g)|)=1\) が導かれ、形式的に矛盾します。 健全なら形式的に無矛盾のはずなので、これも矛盾です。 証明可能と仮定しても反証可能と仮定しても矛盾するため、 \(G(g)\) は証明も反証もできません。 すなわち、\(p(|G(g)|)=0\) かつ \(p(|\lnot G(g)|)=0\) です。 これを第一不完全性定理と言います。

 少し補足しておきますと、ここでは形式的矛盾とメタな矛盾の両方が出てきました。 メタな矛盾は我々が普段使っている論理の矛盾ですから、 あり得るはずがないと強く信じられています。ゆえに、背理法が意味を持ちます。 一方で、形式的に矛盾する形式的理論はあり得ます。 ただ、そのような理論では、どんな間違った定理でも証明できるので、 あまり役には立ちません。上記の証明では、健全と仮定した理論が、 つまり形式的に無矛盾なはずの理論が形式的に矛盾するという結論を導いたので、 メタな証明においても矛盾なわけです。

【ゲーデル文の真理値】

 その理論が健全なら、 ゲーデル文は形式的に証明も反証もできないことが分かりました。 では、ゲーデル文の真理値はどうなっているのでしょうか?

 とある入門書によると、 ゲーデル文もゲーデル文の否定も自然数論と矛盾しないそうです。 ただし、その理論が健全なら、 標準的な解釈の下でゲーデル文は真になるそうです。そのため、 不完全性定理は「正しいのに証明できない閉論理式がある」と説明されるようです。 このざっくりとした説明が結構曲者なんです。 ちょっと確認してみましょう。

 ゲーデル文は、その理論が健全なら形式的に証明も反証もできませんでした。 つまり、健全なら \(p(|G(g)|)=0\) かつ \(p(|\lnot G(g)|)=0\) です。 よって、健全なら \(p(|G(g)|)=0\) は真です。そこからたどると、

\[ \begin{eqnarray} p(|G(g)|)=0 &\Leftrightarrow& \lnot(p(|G(g)|)=1) \\ &\Leftrightarrow& \lnot(p(s(g,g))=1) \\ &\Leftrightarrow& G(g) \end{eqnarray} \]

 のようになります。つまり、\(G(g)\Leftrightarrow p(|G(g)|)=0\) であり、 その理論が健全ならゲーデル文は真だと分かります。

 ちょっと待った! その理論が健全ならゲーデル文は証明も反証もできないはず。 しかしここでは、ゲーデル文が真であることが証明されてるじゃないか! と言いたくなるでしょう。はい、確かにゲーデル文が証明されてしまってますが、 この証明は証明関数 \(p(z)\) の扱う証明の対象外なんです。 不完全性定理を、どんな方法を使っても証明できない閉論理式があると誤解している人もいるかもしれませんが、実はそうではないのです。 自然数論からはみ出してよいのなら、 つまり形式的証明でないのならゲーデル文も証明できます。

 そのカラクリを説明しましょう。 上記の証明は、\(G(y)\) の論理式番号 \(g\) を使っています。 \(g\) はもう少し正確に書けば、以下のような

\[ g = l(G) \]

 論理式 \(G\) を自然数の論理式番号 \(g\) へ対応させる関数 \(l(G)\) です。 しかし、自然数論の中には自然数を自然数に対応させる関数しか含まれていません。 つまり、\(l(G)\) のような関数は自然数論の中には存在しません。 上記の証明は自然数論の体系外にはみ出しているのです。 \(G(g)\) のゲーデル数 \(|G(g)|\) なども自然数論の関数ではないですね。

 もちろん、\(g\) や \(|G(g)|\) が論理式と対応しているなどと考えず、 単に何らかの自然数であるとみなせば、

\[ G(m) \Leftrightarrow p(n)=0\ \]

 という関係を満たす自然数 \(m\) と \(n\) があるということは自然数論の中の話です。

 また、健全なら \(p(|G(g)|)=0\) という関係は標準モデル(標準的解釈)で成立しています。 標準モデルなので、 論理式番号やゲーデル数の中身を解釈すれば、その意味を考えることができて、 「健全なら \(G(g)\) は形式的に証明できない」というものになります。 しかし、\(G(g)\Leftrightarrow p(|G(g)|)=0\) なので、 これは同時に標準モデルで、 健全なら \(G(g)\) が成立していることの証明にもなっています。 形式的にという言葉と標準モデルでという言葉の違いを見落とすと、 何だか矛盾しているように見えます。

 標準モデルとは何ぞやという人もいると思いますが、 モデルについては後で詳しく説明します。とりあえず簡単に説明すると、 論理式の意味はそれを解釈する世界に応じて複数の意味があり、 標準モデルというのは、我々が普段用いている自然数論の解釈を用いる世界です。

 実のところ、\(p(z)\) が扱う証明は形式的証明です。 形式的証明は全てのモデルに共通の公理のみを用いて証明されねばならず、 標準モデル以外でも成立しないといけません。 しかし、健全なとき \(G(g)\) は標準モデル以外では成立している保証はありません。 なので、上記の証明があっても、 「健全なら \(G(g)\) が形式的に証明できる」となることはありません。 つまり、標準モデルで、健全なら \(p(|G(g)|)=1\) となることはありません。

 何かだまされたような気もするでしょうが、きっとだまされてます。 私の言うことなど信じてはダメですよ(と、嘘つきのパラドクス風に言ってみる)。

【モデル】

 ゲーデル文は真と仮定しても偽と仮定しても、 自然数論と矛盾しないそうですが、 これは、以下のようなアナロジーを考えると納得できると思います。

\[ 平行線は無限遠点で交わるのか交わらないのか? \]

 平行線とは何かという問いは、 非ユークリッド幾何まで考えると実は難しい問題なんだそうですが、 ここではまず、一定の距離 \(d\ne 0\) を保った2本の直線と考えてみましょう。 するとこれは、無限遠点まで平行線を伸ばしても交わらないと考えられます。 普通の人の素朴な直感ではこの解釈になるのではないでしょうか?

 次に以下のように考えてみましょう。 3つの異なる点 A,B,C を取り、線分 AB,AC を考えます。 線分 AB,AC は点 A で交わっています。 ここで、点 A を線分 BC と垂直方向の無限遠点まで引き伸ばします。 すると、線分 AB,AC は平行線になるはずです。 この解釈ですと、平行線は無限遠点で交わると考えられます。

 数学的言葉を使うと、平行線が無限遠点で交わるモデルも、 交わらないモデルも考えられるということです。 ゲーデル文の真偽も、ちょうどこの無限遠点での平行線の話と同様だと言えます。 厳密には、ユークリッド空間に無限遠点という点は存在しないので、 これは分かりやすく説明するためのオレオレ幾何の話と思ってください。

 ゲーデル文が無限遠点と考えられるのは、それなりの根拠があります。 証明関数 \(p(z)\) にとってゲーデル文は無限に遠い論理式と見なせるからです。 ここで、証明関数の実装について再度説明しておきましょう。 証明関数の実装は、数式を使ってコンパイラやインタプリタを実装することに相当し、 非常に面倒臭いものです。証明関数の仕組みをちょっとだけ説明すると、 ありうる形式的証明のゲーデル数をしらみつぶしにカウントアップして、 \(z\) に対応する閉論理式の証明になっているかチェックするというものです。 ですから、証明も反証もできない閉論理式とは、 無限の彼方まで証明を探しても見つからない点と見なせます。

 さて、様々なモデルを考えると、ゲーデル文の真偽は定まっていないというのなら、 ゲーデル文かゲーデル文の否定を公理として自然数論に付け加えてやれば、 完全な理論が得られるのではないでしょうか?残念ながら、 そうして得られた新しい理論でも新しいゲーデル文(正確にはロッサー文)が作れます。 なら、それも公理に付け加えてといくら繰り返しても、 新しいゲーデル文は尽きることがありません。結局、自然数論を含むような理論は、 ゲーデル文を有限な方法で次々と加えるというやり方で拡大する限り、 全て不完全ということになります。 正確には、ゲーデル文の否定を公理系に追加すると\(\Sigma_1\)健全性が破れるので、 このお話はゲーデル文ではなくロッサー文と呼ばれるその親戚に関して成り立ちます。

【完全な自然数論】

 不完全性定理から、通常の自然数論を有限な方法で拡大した理論は全て不完全です。 すると、完全な自然数論というものは存在しないのでしょうか? いえ、実は通常の自然数論でなければ完全な自然数論もあり得ます。 そのような完全な自然数論は、真の算術(TA)と呼ばれています。

 真の算術は、自然数論の標準モデルで真となる閉論理式全てからなる理論です。 つまり、標準モデルで正しい閉論理式の全てを公理にしてしまった理論です。 ですから当然、全ての閉論理式が形式的に証明あるいは反証可能ということになります。 公理の中にリストアップされているかをチェックすればいいだけですから。

 ここで、真の算術が不完全性定理の対象から外れる理由を見ていきましょう。 真の算術は形式的に完全ですから、 任意の閉論理式のゲーデル数 \(z\) に対して、 その閉論理式が形式的に証明可能なら証明関数 \(p(z)\) が 1 を返し、 反証可能なら 0 を返します。 真の算術の公理は全ての正しい閉論理式の集まりですから、 証明される閉論理式は全て真であり、反証される閉論理式は全て偽です。 すなわち、\(p(z) = t(z)\) とおけば、\(p(z)\) は真の算術の証明関数になります。 真の算術の場合、\(t(z)=1\) は無限に長い論理式となって自然数論では書けません。 したがって、\(p(z)=1\) は自然数論では書けなくなります。 言い換えると \(p(z)\) はプログラムで書けなくなります。 ゲーデル文は \(p(z)=1\) を使って作りましたから、真の算術では、 ゲーデル文が自然数論では書けないことになります。 つまり、真の算術の中にはゲーデル文が存在しないというわけです。

 なんだ、完全な自然数論もあるんじゃないか。なら、それを使えばいいじゃない。 と思うかもしれませんが、それには大きな困難が立ちはだかります。 証明関数 \(p(z)\) が計算可能であることを、 その理論が再帰的に公理化可能と言います。 しかし、真の算術の場合、 \(p(z)=1\) は無限に長い論理式となって \(p(z)\) が計算可能となりません。 つまり、真の算術は再帰的に公理化可能ではありません。 何か神ががった力で計算することが可能なのかもしれませんが、 普通のやり方では、真の算術は人間には取り扱い不能ということです。

【ゲーデル文は論理的帰結か?】

 ゲーデル文は、様々な自然数論のモデルを考えると、 真にも偽にもなるはずなんですが、上記では標準モデルにおいて、 健全ならゲーデル文の真理値が真だと証明しました。 本当にゲーデル文が恒真式ではないのか心配ですよね。確認してみましょう。 ちなみに恒真式とは、全てのモデルで真になる閉論理式のことです。 恒偽式というものもあって、全てのモデルで偽になる閉論理式のことです。

 なお、ここでは論理的帰結のことを恒真式、その反対を恒偽式と書いています。 正しい用語ではありませんが、他に適切で短い表現を思いつかなかったので、 このページに限った表現ということでご理解ください。 専門書を読むときは、ここでの表現は忘れてくださいね。

 ゲーデルさんは不完全性定理で有名ですが、それ以外にも、 まぎらわしい名前の定理を証明しています。完全性定理と言います。 完全性定理によると、 一階述語論理による自然数論の恒真式は必ず形式的に証明できます。 もちろん、自然数論の恒真式なら自然数論を用いて必ず証明できると言う意味です。 また、その逆に、証明できれば必ず恒真式です。 さらに、論理的には同じことですが、恒偽式なら必ず形式的に反証でき、 反証できれば必ず恒偽式です。

 まず、ゲーデル文は恒真式だと仮定してみましょう。 すると、以下のようになります。

\[ \begin{eqnarray} G(g)~は恒真式 &\Leftrightarrow& p(|G(g)|)=1 ~~\cdots 恒真式なら形式的に証明できる \\ \end{eqnarray} \]

 一方、恒真式は真なので、ゲーデル文はその定義より以下のようになります。

\[ \begin{eqnarray} G(g) &\Leftrightarrow& \lnot(p(s(g,g))=1) \\ &\Leftrightarrow& \lnot(p(|G(g)|)=1) ~~\cdots s(g,g)=|G(g)|~より \end{eqnarray} \]

 \(p(|G(g)|)=1\) かつ \(\lnot(p(|G(g)|)=1)\) となり矛盾します。 以上のことよりゲーデル文は恒真式ではありません。

 次に、ゲーデル文は恒偽式だと仮定してみましょう。 すると、以下のようになります。

\[ \begin{eqnarray} G(g)~は恒偽式 &\Leftrightarrow& p(|\lnot G(g)|)=1 ~~\cdots 恒偽式なら形式的に反証できる \end{eqnarray} \]

 一方、恒偽式は偽なので、ゲーデル文はその定義より以下のようになります。

\[ \begin{eqnarray} \lnot G(g) &\Leftrightarrow& p(s(g,g))=1 \\ &\Leftrightarrow& p(|G(g)|)=1 \end{eqnarray} \]

 \(p(|\lnot G(g)|)=1\) かつ \(p(|G(g)|)=1\) となり形式的に矛盾します。 健全なら形式的に無矛盾のはずなので、これは矛盾です。 以上のことよりゲーデル文は恒偽式でもありません。 つまりゲーデル文は、モデルにより真にも偽にもなります。

 これは、不完全性定理のもう一つの証明と見ることもできます。 恒真式でないものは証明できず(証明できれば必ず恒真式の対偶)、 恒偽式でないものは反証もできないからです(反証できれば必ず恒偽式の対偶)。

 ただ、この証明、 自分の乗っている土台の正しさを土台に乗ったまま証明するようなもので、 そもそも土台が間違ってたら台無しという状態なんだそうです。 不完全性定理を証明するような時は、 有限の立場という制限された立場で証明しないといけないそうで、 完全性定理などは贅沢すぎる道具なんだそうです。 なので、ここでの証明は、あくまで検算と思ってください。

 しかし、こうして見ると、ゲーデルの不完全性定理って、 モデルによって真にも偽にもなる閉論理式なんて、 全てのモデルに共通の性質を定めた公理からは形式的に証明できるはずがないじゃない。 と言ってるだけなんですね。

【AIは知性を実現できるか?】

 不完全性定理によって形式的に証明できない命題がゲーデル文ですが、 機械はゲーデル文が真であることを証明できないが、 人間はゲーデル文が真であることを知っているので、人間と機械は同じではない。 よって、人間のような AI は作ることはできないという話があるそうです。 ただし、対象となる理論は健全と仮定します。

 これには色々と反論があるようですが、私も個人的には、 これは構文論と意味論を意図的に混同しているのではないかと思ってます。 対象となる理論が健全と仮定した場合、 機械がゲーデル文を証明できないというのは構文論での話です。 一方で、人間がゲーデル文を真だと知っているというのは意味論での話です。 機械には構文論しか許さないのに、 人間は意味論も使っていいというのは不公平ですよね。しかし、 構文論の世界が意味論も含めた人間の知性の世界とどう違うのかという話題は、 興味深い話題だと思いますので少し考えてみましょう。

 まず簡単に、ゲーデル文の意味論について解説しておきます。ゲーデル文は、 標準モデルにおいて、この命題は形式的に証明できないという意味の命題です。 そして事実、不完全性定理によってゲーデル文は形式的に証明できないのですから、 標準モデルにおけるゲーデル文の真理値は真です。 命題の意味を知っている人間には自明なことですよね。 ただし、対象となる理論は健全と仮定しました。

 さて次に、構文論と意味論の関係について考察してみます。 ここに、不完全性定理の証明が書かれた本が一冊あったとします。 果たして、この本は知性を実現したものと言えるでしょうか? もし、この世界に知的存在が一人もいなかったとしたら、 この本は不完全性定理の証明が書かれた本と言えるでしょうか? 実際には、紙とインクの集まりでしかないのではないでしょうか。 何を哲学的なことを言い出すのかと思うかもしれませんが、 これは、構文論の世界である形式的体系の本質に関わる問題です。 形式的体系は、意味論的な視点を一切排除してしまうと、 内容の良くわからない自然数の計算ということになってしまいます。

 不完全性定理の証明が書かれた本が、 不完全性定理の証明が書かれた本であるためには、 それを読んで意味を解釈する知的存在がいなければなりません。 それと同じで、形式的体系が何かを証明していたとしても、 それを解釈する知的存在がいなければ、単なる自然数の計算に過ぎないのです。 人間と機械が違うと主張する人が出てくるのも、たぶん、 ここが遠因になっているのでしょう。 この手の議論で機械と言えばチューリングマシンですが、 数理論理学や計算可能性理論でチューリングマシンについて書かれた古典的な書籍では、 チューリングマシンは比較的簡単なプログラムに従って動く、 正に機械的な機械として描かれていると思います。 実際には、プログラムはいくらでも高度化複雑化できるのですが、印象としては、 機械自体が意味を考えるという風には感じられないのではないでしょうか?

 少し脱線すると、 この話題は量子力学の観測の話と何となく似ているようにも思います。箱の中の猫は、 人間が観測するまでは半分死んでいて半分生きているというあれです。 形式的体系も、人間が解釈しなければ意味は定まっていないというところが似ています。

 さらに脱線すると、このページの筆者である私が人間である保証はなく、 実は何等かの自然数の計算から、 日本語っぽい記号列を打ち出しているだけの機械である可能性もあるわけです。 そこに意味を感じるのは、最終的には読者の主観の話ということになります。

 さて、私は AI の専門家ではありませんので、ここから先は私の空想になります。 専門家から見れば的外れなことを言っているかもしれませんのでご注意ください。 知性において、人間と機械は違うという主張は、 現状ではそれほど外れた主張ではないでしょう。 確かに、まだ機械は形式的体系の意味を理解するレベルには到達していないと思います。 しかし、AI の研究は着々と進んでいますので、 ひょっとすると私が生きている間に形式的体系の意味を理解する AI が登場するかもしれないと思ってます。 AI に証明とは何かをいろんな角度で質問してみたり、 それこそゲーデル文の真理値について聞いてみたりして、 人間と同じように答えられたら意味を理解しているとしていいと思います。 つまり、あなたが納得できたら意味を理解しているとしていいと思います。 もちろん、カンニングペーパーを用意しておくのは無しとして。 そうなれば、不完全性定理の証明も機械によって理解され、 機械の世界に閉じた形で知性が実現できるようになるのではないでしょうか。

 まあ、AI には正しいと理解できるのに、 人間の方が理解できないなんてこともあるんでしょうね。 その場合はどうしましょう(^^; この文章は2020年7月に書かれました。願わくば、 この文章がすぐに時代遅れとなることを期待します。

【超形式的体系】

 ここでは少し上級者向けの話をします。 使う記号も上級者なら既に知っているとみなして説明はしません。 分からないという人は読み飛ばしてください。

 人間のようなAIを作ることは可能であると主張する人たちの中に、その理由は、 形式的体系と人間の証明能力が同じであるからと説明する人たちがいます。 私もたぶんそうだろうと思うのですが、その説明が不十分というか、 端的に言って間違っていることがあります。 某有名大学の数理論理学の先生ですら、素人向けの解説書で、 その不十分な説明をしているので、 その説を信じている人は相当数に上ると思われます。 私のような数学の素人の指摘の方が間違っている可能性も大有りですが、 ここではそのことについて述べます。

 人間のようなAIは作れないと主張する人たちは、 人間はゲーデル文を真だと知っているが、 形式的体系はゲーデル文を真だと証明できないので、 人間と形式的体系は同じではないと指摘することがあります。

 これに対して、 人間のようなAIを作ることができるという人たちの一部はこう反論します。 人間が知っているのはゲーデル文が真であることではなく、 無矛盾ならばゲーデル文が真であることである。 そして、無矛盾ならばゲーデル文が真であることなら形式的にも証明できる。 すなわち、\(T\vdash Con(T)\rightarrow G\) であると。 ここで \(Con(T)\) は標準モデルで理論 \(T\) の無矛盾性を表す論理式で、 \(G\) はゲーデル文です。

 しかし、この説明では不十分です。 無矛盾ならゲーデル文は真であることを論理式で表すと \(\mathbb{N}\vDash Con(T)\rightarrow G\) となります。 このとき、\(Con(T)\) が真なら \(G\) も真であると結論できますが、 \(T\vdash Con(T)\rightarrow G\) で無理やり同様のことをやろうとするとこうなります。 \(Con(T)\) が証明できるならば \(G\) も証明できると結論できる。 あれ?\(G\) はゲーデル文だから証明できないはず。 それ以前に、第二不完全性定理で \(Con(T)\) は証明できないので、 \(Con(T)\) を証明できるという仮定を置くと矛盾してしまいます。

 つまり、多くの場合 \(T\vdash\) と \(\mathbb{N}\vDash\) は似たようなことを表しているのですが、 常に似たようなことを表しているわけではないのです。 \(T\vdash\) と \(\mathbb{N}\vDash\) は完全な相似形ではありません。 人間が知っているのは \(\mathbb{N}\vDash Con(T)\rightarrow G\) の方であり、 \(T\vdash Con(T)\rightarrow G\) だとしても \(\mathbb{N}\vDash Con(T)\rightarrow G\) と等価と考えることはできないのです。 \(\mathbb{N}\vDash 1+2=3\) と \(T\vdash 1+2=3\) なら等価と言えるでしょうけど。

 すると、こう反論されるかもしれません。 いやいや、確かに一般の形式的体系ではそうかもしれないが、 こういう場合は健全性を仮定してある。だから形式的に証明できれば十分なのだと。

 そのとおり、健全性が保証されていれば、 \(T\vdash Con(T)\rightarrow G\) ならば \(\mathbb{N}\vDash Con(T)\rightarrow G\) となります。すなわち、無矛盾ならばゲーデル文が真であることに言及できます。

 しかし、これで全て解決とはいきません。健全性を知っているのは誰でしょうか? 形式的体系が知っているのでしょうか。もしそうなら、 健全性を証明するためにはモデル理論の知識が必要なので、 形式的体系は集合論やモデル理論の公理を含んでいなければならないはずです。 しかし、入門書で紹介されるような健全性が成り立つ代表的な形式的体系である Q や PA には、そのような公理は含まれていません。 つまり、通常の形式的体系は健全性を知らないのです。結局、 健全性を知っているのは不完全性定理の証明を読んでいる人間ということになります。 ゲーデル文の真偽に言及するには、普通は人間の手を借りているということになります。 したがって、Q や PA は人間と同じではありません。

 ここまで読んだ人は、 私のことを人間のようなAIは作れない論者と思ったかもしれません。 いいえ、私は人間のようなAIは作れるんじゃないかと思っています。 私が指摘したのは、少なくとも Q や PA は人間と同じではないということです。 より大きな形式的体系を使って、集合論やモデル理論の公理を取り込み、 \(T\vdash\) や \(\mathbb{N}\vDash\) といった記号を取り扱える形式的体系があれば、 つまり、形式的体系をさらにもう一段形式化した超形式的体系があれば、 健全性を扱えるようになり、ゲーデル文の真偽も形式的に示せるのではないでしょうか。 私のような半可通にはそれを示す能力はありませんけれど。

 ひょっとすると、そのような形式的体系は既にあって、専門家に言わせれば、 君の言うようなことは既に証明済みだよということかもしれません。 先の数理論理学の先生もそれを知っていて、素人に説明するようなことではないから、 大筋だけ説明したんだよということかもしれません。 そうだとすると、それを読んだ私のような半可通は誤解するよなぁ。

【余談】

 ところで、超形式的体系とその外側の意味論にまたがる定理とかは、 超形式的体系では証明できないので、超々形式的体系が必要になります。 さらにその上に超々々形式的体系があってと無限に続きそうな予感がします。 機械は、どこかで形式的体系を固定しないとだめだろうと思いますが、 人間なら形式化の階段をどこまでも登っていけるのでしょうか。 そうだとすると人間と機械は違うのかもしれません。

 でも、人間も実際には限界があるんじゃないですかね。 自然数にしたっていくらでも数えられるといいますけれど、 実際には人間に数えられる自然数の大きさには限界がありますしね。

【自己言及しない不完全性定理】

 第一不完全性定理は、 「この論理式は証明できない」という意味の論理式を構成することで証明されました。 つまり、嘘つきのパラドクスと同様に自己言及している怪しい論理式を用います。 そのため、第一不完全性定理の本質は自己言及であるかのように感じてしまいます。 あるいは対角線論法がその本質であるかのように感じるかもしれません。 しかし、第一不完全性定理は自己言及や対角線論法抜きでも証明できます。 ちょっとやってみましょう。

 前提として、ちょっとズルをして、超準モデルの性質を証明に使います。 我々が普段使っている自然数のモデルを標準モデルと言いますが、 標準モデルには無限大の数は含まれていません。 一方、超準モデルの自然数は無限大の数を含みます。 超準モデルのこの性質が以下の証明では重要な役割を果たします。 超準モデルが存在することは深く考えずに認めてしまってください。 理論が健全なら無矛盾であり、無矛盾なら完全性定理よりモデルを持ちます。 そうしたモデルの中に標準モデルや超準モデルが存在します。

 もう1つ、\(\Sigma_1\)健全性を仮定します。 \(\Sigma_1\)健全性はただの健全性より強さを弱めた健全性です。 \(A(x)\) を原始帰納的述語とするとき、 \(\exists x~A(x)\) の形の論理式を\(\Sigma_1\)論理式と言います。ここで、 \(\exists x~...\) という式は \(...\) を満たす \(x\) が存在するという意味です。 \(\exists x~A(x)\) が形式的に証明できるならば、標準モデルで \(\exists x~A(x)\) が成り立つとき、つまり証明できれば標準モデルで真のとき、 その理論 \(T\) は\(\Sigma_1\)健全であると言います。

 それでは証明を始めましょう。まず対象とする理論 \(T\) は、 自然数論を含む再帰的に公理化可能な\(\Sigma_1\)健全な理論で、 可算超準モデルを持つとします。 次に、以下のような原始帰納的関数 \(\mathrm{std}(x)\) を定義します。

\[ \mathrm{std}(x) = \left\{ \begin{array}{cl} 1 & (~x = 0~または~\mathrm{std}(x - 1)=1~) \\ 0 & (~上記でない~) \end{array} \right. \]

 これは標準モデルにおける実装です。 端的に言うと、\(x\) が有限な数なら有限時間で \(1\) を返し、 そうでないなら計算が終了しない関数です。

 さらに超準モデルにおける実装もあります。 \(\mathrm{std}(x)\) の超準モデルにおける代表的な実装は、 \(x\) が有限の数であるとき、 すなわち標準モデルの自然数であるとき有限時間で \(1\) を返し、 \(x\) が無限大の数であるとき、 すなわち超準モデルの自然数であるとき有限時間で \(0\) を返すというものです。 超準モデルでは、それ以外にもいろいろな実装があり得ます。 そして、形式的証明では想定する公理に合わせて最大公約数的実装を選びます。 今回は\(\Sigma_1\)健全なので標準モデルの実装を選びます。

 この関数を用いると、\(\exists x(\mathrm{std}(x)=0)\) がゲーデル文(正確にはその否定)になっています。 実際、\(\Sigma_1\)健全性より、 \(\exists x(\mathrm{std}(x)=0)\) が形式的に証明できるならば、 標準モデルで \(\exists x(\mathrm{std}(x)=0)\) が成り立たないといけません。 しかし、\(x\) がどんな標準モデルの自然数だとしてもこの式は成り立ちません。 標準モデルには無限大の数は含まれていないからです。 したがって、\(\exists x(\mathrm{std}(x)=0)\) は形式的に証明できません。

 一方、\(\exists x(\mathrm{std}(x)=0)\) の否定は \(\forall x(\mathrm{std}(x)=1)\) です。ここで、 \(\forall x~...\) という式は全ての \(x\) で \(...\) を満たすという意味です。 もし、\(\forall x(\mathrm{std}(x)=1)\) が形式的に証明できるならば一階述語論理の推論規則より、 \(n\) を任意定数として \(\mathrm{std}(n)=1\) が全てのモデルで成り立たないといけません。 これは標準モデルでは成り立ちますが、様々な超準モデルを考えると成り立ちません。 \(\mathrm{std}(x)\) が上記の超準モデルにおける代表的な実装の場合、 \(\mathrm{std}(n)=0\) となる \(n\) が存在します。 つまり、無限大の数が存在します。 よって、\(\forall x(\mathrm{std}(x)=1)\) も形式的に証明できません。 ただし、\(\forall x(\mathrm{std}(x)=1)\) かそれと等価な公理を含まない仮定しました。

 以上のことより、\(\exists x(\mathrm{std}(x)=0)\) は、 形式的に証明も反証もできません。これで不完全性が証明できました。 通常の不完全性定理から考えると、 こんな簡単な論理式がゲーデル文になるのは驚きですね。 正確には、ゲーデル文は標準モデルで真でないといけないので、 \(\forall x(\mathrm{std}(x)=1)\) の方がゲーデル文です。 また、\(\forall x(\mathrm{std}(x)=1)\) かそれと等価な公理を含まないという条件が必要なので、 本当の意味での不完全性定理ではありません。 まあ、この条件はペアノ算術なら満たしているでしょうが。

 この証明が意味することは何でしょうか?これは、\(\exists x(\mathrm{std}(x)=0)\) や \(\forall x(\mathrm{std}(x)=1)\) かそれと等価な公理を設定しない限り、 無限大の存在は自然数論からは証明も反証もできないということです。 集合論では、無限集合の存在を保証するために無限公理というものを仮定しますが、 自然数論でも無限大の存在は公理で保証するか否定するようなことをしないと、 存在するともしないとも言えないということです。

 集合論の無限公理は他の公理からは独立しています。 選択公理が他の公理から独立であると聞いたことのある人もいると思いますが、 上記の証明で、そのような公理の独立の証明の雰囲気を感じられると思います。

 もう一点指摘しておきましょう。上記の証明で不完全性が証明できたのは、 我々が、標準モデルには無限大の数は存在せず、 超準モデルには無限大の数が存在するということを知っているからです。 つまり、非形式的体系では形式的体系外の知識が使えるため、 不完全性定理が証明できているわけです。

 それにしても、非形式的に無限大が存在する存在しないという知識を用いることで、 形式的に無限大の存在が証明も反証もできないことが導かれるのは何とも逆説的ですね。 非形式的体系と形式的体系が、これほど鮮やかなコントラストを見せるとは、 人間の持つ論理という認識能力の不思議さを感じます。

 ところで、実のところ可算超準モデルが存在することは不完全性から導かれるので、 上記の証明は本当は話が逆です。しかし、話が逆だとしても \(\forall x(\mathrm{std}(x)=1)\) がゲーデル文になることは変わりません。

 さて、上記の証明では\(\Sigma_1\)健全性を仮定しました。 しかし、この制限は以下のように考えると緩和でき、 無矛盾性にまで弱められると私は考えています。 今、対象となる理論 \(T\) は、 自然数論を含み再帰的に公理化可能で無矛盾な理論であるとします。 ただし、\(\Sigma_1\)健全性は成り立たないとします。

 \(\Sigma_1\)健全性が成り立たないので、 理論 \(T\) は無限大の存在を保証する公理を持つことができます。 ここで、公理で存在を保証された無限大を表す記号を \(c\) とし、 \(x\) が標準モデルの数と \(c\) との四則演算の繰り返しで \(0\) から到達可能な場合に \(1\) を返し、 到達可能でない場合に \(0\) を返す関数を \(\mathrm{pol}(c,x)\) とすると、 \(\exists x(\mathrm{pol}(c,x)=0)\) が証明も反証もできない閉論理式になっていると思います。

 ただし、 \(\forall x(\mathrm{pol}(c,x)=1)\) かそれと等価な公理は無いとします。 また、四則演算と言っても、 減算と除算は自然数の公理を破らないように工夫して制限します。 \(\mathrm{pol}(c,x)\) は \(\Sigma_1\)健全の時の \(\mathrm{std}(x)\) のように簡単には表せませんが、 \(c\) の有理係数多項式を順次生成するアルゴリズムで実現できるはずです。 このとき、生成される多項式の最大次数の係数の符号は正とします。

 つまり、\(\mathrm{pol}(c,x)\) を特性関数として決まる集合をモデルにすると、 それが\(\Sigma_1\)健全の時の標準モデルと同じような役割を果たします。 そして、標準モデルの数と \(c\) との四則演算の繰り返しで \(0\) から到達可能でない、 より高位の無限大を持つより高位の超準モデルが存在しているため、 \(\exists x(\mathrm{pol}(c,x)=0)\) がゲーデル文(正確にはその否定)となり、 不完全性が成り立つことになると思われます。

【真の算術と選択公理】

 こちらのセクションでは、 完全な自然数論として真の算術があることを紹介しました。 真の算術は標準モデルで正しい閉論理式を全て公理にした理論です。 真の算術を作るには、ゲーデル数を \(z=0,1,2,3,\cdots\) とカウントアップし、 それを \(t(z)=1\) で判定して真になったものを大きさ順に並べれば OK です。 ただし、\(z\) が閉論理式のゲーデル数でない場合は \(t(z)=0\) とするとします。 列挙されたゲーデル数に対応する閉論理式が真の算術の公理になります。 判定に合格した順に番号を振れば、真の算術の公理の集合と自然数の集合 \(\mathbb{N}\) との間に1対1対応があることになります。

 しかし、\(t(z)\) は自然数論を使っては書けませんでした。 何か超越的な方法を用いないと定義できず、 具体的に構成することはできないということです。 具体的に構成することができないものが存在していると言えるのでしょうか? つまり、 本当に真の算術の公理を1番目、2番目、3番目と列挙することが可能なのでしょうか? もっと言うと、 真の算術の公理の集合と \(\mathbb{N}\) との間に1対1対応はあるのでしょうか? そう、こういう時はあの有名な選択公理の出番ですね。

 まず、 真の算術の公理の集合とその公理のゲーデル数の集合を同一視して TA と書きます。 すると TA は \(\mathbb{N}\) の部分集合になっていますから、 TA の濃度は可算無限以下であることは確かです。 また、標準モデルで正しい閉論理式は、\(0=0,1=1,2=2,3=3,\cdots\) のように無数にありますから、TA は有限集合ではありません。 ここで選択公理を仮定すると、最も小さい無限集合の濃度は可算無限になりますので、 TA の濃度は可算無限以上可算無限以下となり、結局、可算無限ということになります。 つまり、TA と \(\mathbb{N}\) との間に1対1対応があるということです。

 したがって、具体的に構成することはできませんが、選択公理を使うと、 真の算術の公理を1番目、2番目、3番目と列挙することができるということになります。 つまり、真の算術の存在は選択公理を仮定すれば保証できることになります。

 具体的に構成できないのに存在はしていると言われても納得しがたいですよね。 そこで、以下のように考えてみてはどうでしょうか? コイントスを使って自然数の数列を生成することを考えます。 つまり、コイントスを繰り返して、 \(n+1\) 回目に表が出れば数列に \(n\) が含まれるとします。 コイントスを無限に繰り返せば、\(\mathbb{N}\) の部分集合が生成できます。 コイントスが真の乱数なら、典型的なケースにおいて、 数列の \(m\) 番目にどの自然数 \(n\) が対応するのかを決定するアルゴリズムはありません。つまりこの数列は、 乱数を含まない純粋な自然数論を使って具体的に構成する方法はありません。 一方で真の乱数なら、 コイントスの全ての可能性の中に TA を生成する場合があるはずです。 コイントスで表が出た回数 \(m\) を数えておけば、 この数列に番号を振ることが可能です。 したがって、TA と \(\mathbb{N}\) との間には1対1対応があると考えられます。

【正直者のパラドクス】

 ここでは、嘘つきのパラドクスと対をなす、もう一つのパラドクスを紹介します。 嘘つきのパラドクスは有名ですよね。「私は嘘つきです」 という文は真と考えても偽と考えても矛盾するため真とも偽とも言えません。 このパラドクスの原因は否定的自己言及にあると言われています。 しかし、実際には否定的でない自己言及も病的な文となることがあります。 それが正直者のパラドクスです。

 正直者のパラドクスは「私は正直者です」という文の真理値を考えると起こります。 この言葉を発した者が事実正直者であれば、 この文は正しいことになり何の矛盾もありません。 しかし、この言葉を発した者が嘘つきだと仮定しても、 嘘つきが正直に自分を嘘つきだと言うはずがありませんので、 嘘つきが自分のことを正直者と嘘をつくことに何の矛盾もありません。 つまり、この文は真と解釈しても偽と解釈しても矛盾せず、 嘘つきのパラドクス同様に真とも偽とも言えないわけです。

【第二不完全性定理】

 ここでは、私が独自に解釈した第二不完全性定理をズバリ説明します。 それは、ペアノ算術の拡大理論の最も基本的な証明関数 \(p(x)\) を用いた無矛盾性を表す論理式 \(p(|1=0|)=0\) は、 その理論が無矛盾ならペアノ算術では形式的に証明できないというものになります。 つまり、対象となる理論で矛盾(\(1=0\))が証明できないという論理式は、 その理論が無矛盾なら正しいが、 そのことはペアノ算術では形式的に証明することはできないということです。

 ペアノ算術とは何ぞやという人は適当にググってください。 ごく簡単に説明すると、数学的帰納法が使える最も基本的な自然数論のことです。

 それでは説明を始めましょう。まず、証明関数の定義から確認します。 証明関数は、ゲーデル数が \(x\) の閉論理式の形式的証明のゲーデル数は \(y\) であるという原始帰納的述語 \(P(x,y)\) を用いて以下のように定義できます。 \(P(x,y)\) を証明述語と言います。

\[ p(x) = \left\{ \begin{array}{cl} 1 & (~\exists y~P(x,y)~) \\ 0 & (~\forall y~\lnot P(x,y)~) \end{array} \right. \]

 つまり、\(P(x,y)\) が最も基本的な証明述語のとき、 ゲーデル数が \(x\) の閉論理式が形式的に証明可能であるなら \(p(x)=1\) であり、有限な \(y\) で計算終了します。 しかし、形式的に証明不能ならば \(p(x)=0\) であり、 \(y\) の取り得る範囲は全ての自然数ということになります。

 注意しなければいけないのは、 \(P(x,y)\) が最も基本的な証明述語ではない場合です。 ロッサーさんが定義した証明述語を用いた場合、 ゲーデル数が \(x\) の閉論理式が反証できるときは、 有限な \(y\) で証明不能と判定できるショートカットがあります。 これは、証明関数に以下の仮の無矛盾性が組み込まれていることに相当します。

\[ p(\mathrm{neg}(x))=1 \Rightarrow p(x)=0 \]

 ただし、\(\mathrm{neg}(|f|)=|\lnot f|\) とします。 そのため、クライゼルの注意 と呼ばれる現象が起きて、\(p(|1=0|)=0\) が形式的に証明可能になることがあります。 無矛盾性が組み込まれているのですから、無矛盾性が証明可能なのは半ば当然ですね。

 しかし、クライゼルの注意は本当の無矛盾性の証明として適切とは言えません。 そこでまず、最も基本的な \(p(x)\) は、 クライゼルの注意のような現象を起こす証明関数にならないことを確認します。

 クライゼルの注意を起こすような証明関数には、 仮の無矛盾性をショートカットとして組み込む必要があります。 しかし、ショートカットを組み込んだ場合、 \(p(x)\) を構成する証明述語 \(P(x,y)\) が、 より基本的な証明述語に分解できることになります。 本来の機能である証明可能かどうかの判定以外に、 反証可能かどうかを判定できないといけないからです。 これは \(p(x)\) が最も基本的であることに反します。 よって、最も基本的な \(p(x)\) にはショートカットは存在せず、 クライゼルの注意のような現象は起きません。 ただし、最も基本的な \(p(x)\) が一意に定まるとは限りません。

 次に、最も基本的な証明関数による論理式 \(p(|1=0|)=0\) は、 ペアノ算術では形式的に証明できないことを確認します。

 \(p(|1=0|)=0\) を証明述語を使って表せば \(\forall y~\lnot P(|1=0|,y)\) となります。 \(1=0\) は矛盾なので、対象となる理論が無矛盾なら形式的に証明できません。 そして、ショートカットは組み込まれていないので、 \(\forall y~\lnot P(|1=0|,y)\) は全ての可能な形式的証明のゲーデル数 \(y\) を調べて、 \(1=0\) の証明になっていないことを確認することになります。 したがって、対象となる理論の定理の集合全体に言及することになります。

 一方、ペアノ算術の定理の集合を定める段階では、 ペアノ算術の拡大理論の定理の集合全体(すなわちペアノ算術の定理の集合全体を含む)に言及する論理式はまだ意味が確定していません。 ペアノ算術の定理の集合が完成した後でなければ、 定理の集合全体に言及することはできないからです。 そのため、\(p(|1=0|)=0\) をペアノ算術の定理の集合の要素にはできません。 つまり、ペアノ算術の定理の中に \(p(|1=0|)=0\) は存在しません。

 まとめると、 \(p(x)\) がペアノ算術の無矛盾な拡大理論の最も基本的な証明関数であるとき、 その理論の無矛盾性を表す論理式 \(p(|1=0|)=0\) は、 ペアノ算術で形式的に証明することはできません。

 これで第二不完全性定理が証明できました。 ただし、本来の第二不完全性定理とは異なり、 自分の無矛盾性を表すように見える論理式が、 自分自身で形式的に証明できないことを証明してはいません。 ペアノ算術の無矛盾な拡大理論の無矛盾性は、 ペアノ算術では形式的に証明できないことを証明しています。

 私は、こちらの方が第二不完全性定理として適切ではないかと考えています。 なぜなら、\(p(|1=0|)=0\) という論理式が無矛盾性を表すのは、 標準モデルで解釈した場合だからです。ペアノ算術は標準モデルを持つので、 \(p(|1=0|)=0\) の意味を標準モデルで解釈することができます。

 この話について、もう少し詳しい説明を読みたい方は、 備忘録 をご覧ください。

 以下は補足です。\(p(|1=1|)=1\) のような論理式は、 ペアノ算術で形式的に証明できます。 この論理式は証明述語を使って表せば \(\exists y~P(|1=1|,y)\) となります。\(1=1\) は正しい\(\Sigma_1\)論理式なので、 有限な証明のゲーデル数 \(y\) で計算が終了します。 よって、ペアノ算術の定理の集合全体には言及しません。 そのため、ペアノ算術の定理の集合が完成する前に意味が確定します。 つまり、\(p(|1=1|)=1\) をペアノ算術の定理とすることができます。

 また、\(p(|1=0|)=0\) はペアノ算術で形式的に反証することもできません。 なぜなら、形式的に反証できると\(\Sigma_1\)健全性により \(p(|1=0|)=1\) という論理式が標準モデルで真となり、 対象となる理論が形式的に無矛盾であること、 すなわち、標準モデルで \(p(|1=0|)=0\) が真であることに反するからです。 つまり、\(p(|1=0|)=0\) はペアノ算術のゲーデル文になっています。

 もう1つ重要な事実を指摘しておきます。 無矛盾性の仮定より、\(p(|1=0|)=0\) は標準モデルで真です。 もし、ペアノ算術で \(p(|1=0|)=0\) が有限時間で計算できるなら、 \(p(|1=0|)=0\) が形式的に証明できることになります。 しかし、実際には形式的に証明できませんでした。そのため、 ペアノ算術では \(p(|1=0|)=0\) は有限時間で計算できないことが分かります。 この事実は、備忘録で使います。

 注意すべき点は、無矛盾性の仮定より、標準モデルでは \(p(|1=0|)=0\) であることを有限時間で「知る」ことができる点です。 これは、無矛盾性の仮定が非形式的な知識であるということです。

【あとがき】

 さて皆さん、不完全性定理のすごく簡単な説明はお楽しみいただけましたか? 不完全性定理が分かった気になれなかった人に、 少しでも分かった気になってもらえたのなら、私の企みは成功と言えます。 成功してるといいなぁ(^^;

 ここでは、私が不完全性定理を勉強してみて感じたことを書こうと思います。

 まず、ある程度第一不完全性定理を理解して思ったのは、 知の革命とか理性の限界とか言うのはちょっと大げさすぎると言うことです。 第一不完全性定理は、 ゲーデルさんのような天才でなければ思いつかない超難問というより、 証明するとはどういうことかを丁寧に整理していけば、 いずれは誰かがたどり着く必然的な内容のように思えるからです。

 言っていることは、 ある公理系 \(T\) にはそれを解釈するモデルが複数あることがあり、 ある種の論理式はモデルを指定しないと真偽が定まらないということです。 つまり、モデルによって真になったり偽になったりする論理式は、 全てのモデルに共通の性質を定めた公理からは証明できるはずがない。 むしろ証明できたらおかしいというだけなんですね。

 私は情報工学科卒なので、数学科のカリキュラムは知りませんが、 多分、第一不完全性定理は、 数学科では最初の方で習う初等的な定理なのではないでしょうか?

 ひょっとしたら、ゲーデルさんが証明した時代においては、 一級の数学者たちも、証明とは何かを整理しきれておらず、 知の革命だったのかもしれません。 現代日本に住んでいると民主主義なんて当たり前と思えますが、 絶対王政を打倒した当時の西洋の人々には、正に精神的にも革命だったように。 ただ、そういう歴史的文脈から外れて、 知の革命とか理性の限界と語るのは、やはり大げさすぎるという印象です。

 また、第二不完全性定理の数学は数学自身の無矛盾性を証明できないという宣伝も、 言葉を補わないと誤解を招くと思います。 実際には、ある種の条件を満たす理論や証明関数において、 形式的に証明できないということであって、 形式的でない有限の立場やその拡張で証明できないとされたわけではありません。 事実、不完全性定理の後に、 ゲンツェンさんが有限の立場を拡張して、自然数論の無矛盾性を証明しています。

 一方で、数学自身で数学の無矛盾性が証明できたとしても、 それは「私は嘘は申しません」という人を信用できるかと言うことであって、 不完全性定理を持ち出すまでもなく、常識としてそんな主張は無意味です。 まさに正直者のパラドクスになっています。 数学の無矛盾性の保証は、あくまで現実への有益な応用を通じて保証されるもので、 他者からの評判で判断するしかないわけです。 そうだとすると、不完全性定理で無矛盾性の証明ができないとされたことは、 数学にとって特に打撃というわけではないでしょう。 実際、数学は有益な応用を多数持つわけですから。 また、有限の立場とは、信用できると評判の定まった立場とも言えるかもしれません。

 問題として残るのは、現実への応用を持たない、 数学のための数学みたいな分野の無矛盾性をどう保証するかなのでしょうね。

 何やら偉そうに知った風なことを書いてしまいましたが、 私の感想が真実を言い当てているかどうかは、 皆さんが不完全性定理を理解することでご判断ください。 このページがそのきっかけになれば幸いです。


備忘録


トップページ   実数とは何か?無限とは?   Σ1健全性による不完全性定理   クライゼルの注意   備忘録   不完全性定理のための傾向と対策