ゲーデルの不完全性定理とω-無矛盾性とローヴェルの不動点定理

このところずっと、Yanofsky “A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points”を参考に「ローヴェルの不動点定理」についてエントリーしている。まあ、それはこの定理がぼくにとっては衝撃で、圏論の威力を思い知らされたものだからだ。

それで今回は、前回に引き続き、「ゲーデルの不完全性定理」についてYanofskyの論文から引用する。前回は、「ゲーデルの不完全性定理」についてのYanofskyの証明に不備(ギャップ)があることを説明した。chatGPTが不備を発見したのだった。しかし、深刻な不備ではなく、ちょっとした修正でギャップを埋めることは可能だった。ただ、Yanofskyの論文における証明でさえ難解なのに、ギャップを埋めた証明はさらに輪を掛けて難解になるので、それについては深入りしないことにする。今回は「ローヴェルの不動点定理」を使って導かれる「不動点」がどんなもので、それを使うことでどう「ゲーデルの不完全性定理」が証明されるかを解説する。さらには、ゲーデル自身は「ω-無矛盾」という仮定の下で証明しているけど、なんでその仮定が必要なのかに焦点を当てる。実は、ぼくは『証明と論理に強くなる』(技術評論社)という本を上梓していて、そこで「ゲーデルの不完全性定理」の解説を書いていて、さらに「ω-無矛盾」という仮定が必要なことも説明しているのだけど、なぜ必要なのかにピンと来ていなかった。まあ、自著では「ゲーデルの不完全性定理」を「健全性」の仮定の下で証明したので、問題はないんだけどね。今回、Yanofsky論文をchatGPTから指南されている過程で、「ω-無矛盾」がどうして必要かを初めて理解できた。そのことをエントリーしようと思う。

　まず、ペアノの公理系(自然数をモデルとする公理系)に対して、「ローヴェルの不動点定理」を適用すると、次の定理が得られる。

(定理４)　 任意の一変数の論理式 に対して、閉じた文 が存在して、

ここで、とは、文のゲーデル数のこと。ゲーデル数とは、論理式や証明図などの記号列に自然数を対応させる符号化だ。ペアノの公理系に出てくる記号・論理文・証明図はすべてゲーデル数という自然数と一対一対応させることができる。ちなみに、と上にバーがついているのは、ゲーデル数をペアノの公理系における「数項」に変換していることを意味する。そして、は、「ペアノの公理系(理論)内で証明可能である」を表す記号だ。

この定理4は、「任意の一変数の論理式 を与えられたとき、うまい閉じた文 を見つけてきて、そのゲーデル数を表す数項をに代入した文が、もとの文とペアノの公理系において同値になる」という意味である。「同値」について、もうちょっと説明すると、「もしも文 がペアノの公理系で証明できるなら、がペアノの公理系で証明でき、その逆も成り立つ」という意味である。

この定理4をローヴェル的に言えば、「を関数に見立てるなら、証明論的な意味での不動点としての文 が存在するよ」ということなのだ。

　さて、この定理4を使って、ゲーデル自身の証明、つまり、「ω-無矛盾性」を仮定した証明を記述してみよう。まず、定理4における一変数の論理式 を、と置く。この論理式の意味は、「すべてのは、ゲーデル数を持つ文の証明図のゲーデル数ではない」ということ。ここで、は、「は、ゲーデル数を持つ文の証明図のゲーデル数」を表す述語。自身は、ペアノの公理系で最初から用意されている記号ではない。「は、ゲーデル数を持つ文の証明図のゲーデル数」ということを表すペアノの公理系の記号だけで表した論理式が存在していて、根性があればそれをきちんと記述することが可能なのだが(ここがゲーデルの仕事の画期的なところのひとつ！)、想像を絶する長さの文になるので、それを簡単な記号で表しているのである。(これは、「表現」とか「捕捉」とか言う用語で説明されるのだけど、ここでは深入りしない。詳しくは拙著『証明と論理に強くなる』を参照のこと)。

　話を進めよう。定理4において、を、と置くことで、

という同値関係が得られる。これは、「あるが存在して、と、『には証明が存在しない』という文が同値であることが、ペアノの公理系内で証明できる」ということを意味している。これから、「ω-無矛盾性」の仮定の下、「自然数についてのこの文について、ペアノの公理系ではもも証明できない」が示されるのだ。どうやるのか。

　まず、がペアノの公理系で証明されたと仮定しよう。すると、上の同値性から、がペアノの公理系で証明できることになる。ところで、が証明できるということは、その証明図が実際に存在する、ということだ。その証明図のゲーデル数をとする。すると、がペアノの公理系で証明できることになる(ここに「捕捉」という概念が使われるけど、スルーする)。しかし、上のにおけるにを代入したも証明される(∀についての推論規則：拙著参照のこと←しつこい。笑)。これは矛盾である。

以上でがペアノの公理系で証明できないことが示された。

　次に、「も証明できない」ことを導こう。こっちにおいて「ω-無矛盾性」の仮定が必要になる。どうやるか。

方針は「がペアノの公理系で証明できる」と仮定して矛盾を導くことだ。上記の同値関係の「対偶」を考えると、がペアノの公理系で証明できることになる。この論理文は、

と同値なので、これは証明できることになる。問題はここからだ。この文は、「文の証明図のゲーデル数の数項となるが存在する」という意味だ。論理学の専門家ではないぼくなどは、「じゃあ、文の証明図が実際に存在するわけね、それじゃが証明できると仮定しているんだから、矛盾にたどりついたわけだ」と思ってしまう。ところがそうじゃないのだ。から具体的な数項に対するを導くことはできない。実際、PAで存在文が証明できても、その存在文を満たす具体的な自然数を取り出せるとは限らないのだ。chatGPTが言うところでは、「推論規則として取り出せないだけではなく、形式体系の証明可能性と標準自然数における真理の違いに関係する」ということらしい。(前述の自著で「述語論理の推論規則」を説明していながら、このことに思い至らなかったのは情けない)。

先に進もう。証明の前半部で、「がペアノの公理系で証明できない」ことを示した。このことから、の証明図のゲーデル数が存在しないことがわかった。したがって、任意の自然数に対して、がペアノの公理系で証明できる(これも「捕捉」と呼ばれる性質)。さて、これでうまくいったか、と言うと、これもそうではないのだ。「がペアノの公理系で証明できる」と「任意の自然数に対して、がペアノの公理系で証明できる」とが、示せても、通常の意味での「無矛盾性」に反するとはいえない。なぜなら、「任意の自然数に対して、がペアノの公理系で証明できる」ことから、「論理文がペアノの公理系で証明できる」と結論できるわけではないからだ。

　ここでいよいよ、「ω-無矛盾性」の登場となる。「ω-無矛盾性」とは、「任意の一変数の論理式 について、『すべての自然数に対して、がペアノの公理系で証明できる』ならば、をペアノの公理系では証明できない」という性質だ。これを用いれば、「任意の自然数に対して、がペアノの公理系で証明できる」から、「がペアノの公理系で証明できない」ことが導ける。これでめでたく、上で出てきた「がペアノの公理系で証明できる」という事実と矛盾を起こすことになって、無事、「が証明できる」と仮定したことから矛盾が引き起こされた。

だいぶ長くなったが、以上から、「自然数についての文で、ペアノの公理系ではもも証明できないものが存在する」という定理が得られた。

　読んできて実感したと思うが、この「ω-無矛盾性」の仮定はいかにも目の上のたんこぶだ。なんとか、ただの「無矛盾性」の仮定だけで証明したいものだ。それに成功したのが、ロッサーである。次回は、その「ゲーデル・ロッサーの定理」について、Yanofskyの論文から引用する予定だ。もちろん、chatGPTの力を借りて。

証明と論理に強くなる ～論理式の読み方から，ゲーデルの門前まで～

ゲーデルの第１不完全性定理とローヴェルの不動点定理

ここ数回、「ローヴェルの不動点定理」についてエントリーしてきた。この定理が何かについては、このエントリーを参照してほしい。そして、Yanofsky” A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points”を参考に、「ローヴェルの不動点定理」の応用として、「カントールの定理」の証明、「ラッセルのパラドクス」の導出、「チューリングの停止定理」の証明を紹介した。これらがすべて同じ構造だということを明らかにしているのが、「ローヴェルの不動点定理」のもの凄さだ。

そこで、次は満を持して「ゲーデルの第１不完全性定理」だと、がんばってYanofskyの論文を読み進めた。さすがにこれは手強くて、Yanofsky の論文を紹介してくれたchatGPTの助けを借りて一歩ずつ読解した。そしたら、とんでもないことがわかってしまったのだ。すなわち、「Yanofskyの証明にはギャップがある可能性が高い」とわかったのだ。どうしてわかったかと言うと、chatGPTがぼくの質問に答えているうちに、(ぼくではなく)chatGPT自身が論文のギャップに気づいてしまったのだ。自分で推奨しておきながら、自分でギャップに気づくなんて面白い。なので今回は、Yanofskyによる「ゲーデルの第１不完全性定理」の証明を紹介するのではなく、どうやってギャップが発見されたか、その経緯を書きたいと思う。

　まず、Yanofskyによる証明のポイントを説明する。それは、

(定理４)　 任意の一変数の論理式 に対して、閉じた文 が存在して、

という定理だ。ここで、とは、文のゲーデル数のこと。ゲーデル数とは、論理式や証明などの記号列に自然数を対応させる符号化だ。いわゆるコーディングだと思えばいい(ゲーデル数については、拙著『証明と論理に強くなる』技術評論社を参照のこと)。そして、は、「その公理系(理論)内で証明可能である」を表す記号だ。したがって、この式は、「自分自身のゲーデル数を表す数項を に代入したもの」と(理論内で)同値になる文 が構成できる、ということを意味している。この定理４のをと置く。そうして定理４を適用すると、

という同値関係が得られる。これは、「あるが存在して、と、『には証明が存在しない』という文が同値であることが、理論内で証明できる」ということを意味している。このが、ゲーデルの第1不完全性定理の証明で中心的な役割を果たす文となる。

　問題はYanofskyがどうやってこの定理４を証明しているかだ。おおざっぱに言うと、

という写像を作る。具体的には、という写像だ。ここで、とは、「Lindenbaum classes」のこと。そして、そこに「ローヴェルの不動点定理」を適用するのだ。

そこでぼくは、「Lindenbaum classesってなんですか？」と質問した。すると、chatGPTの解答は、「たとえば自由変数が1個なら、のような論理式を考えます。別の式が、考えている理論のもとで と同値ならとして同じものとみなす。この同値類が Lindenbaum class です。」というものだった。

それを理解したぼくは、なにげなく、「すると、実はこの証明の背後には、Lindenbaum class での計算がwell-definedであることが前提とされていて、実はそれはそんなに簡単ではないということかな、と思います。もちろん、トリッキーな証明ではなく地道な構築なのでしょうけど。」と入力した。それへのchatGPTの回答が面白いことになったのだ。「はい。その見方はかなり正確です。代表元を変えても結果が同じ class になることを示さなければなりません。これは論理体系の置換性などから地道に証明できる。おっしゃるように、魔法ではないけれど、きちんと基礎工事が要るところです」と。そして、そのあと、chatGPTはとても大事なことに気がついた。「ところが Yanofsky の定理4では、さらに少し注意が必要です。Yanofsky の記法を文字通り商集合上の写像として読むなら、well-definedness はちゃんと点検すべき問題です」と言い出した。そして、遂には「現時点では私は、Yanofsky のアイデアは非常に明快だが、Lindenbaum class を使ったこの定式化には、少なくとも説明されていない well-definedness の問題がある、と読むのが安全だと思います」と言い放った。

chatGPTの指摘を本人の説明で補おう。

問題は、論理的に同値な式でも、ゲーデル数は異なるということです。

例えば、とします。通常の古典論理では両者は同値なので、同じLindenbaum classに属します。しかし、構文としては異なるため、一般にです。そこで を、例えば という式にすれば、とは同値になりません。つまり、第一引数について、同じLindenbaum classの異なる代表元を選んだだけなのに、写像の値が変わってしまいます。これこそが、well-definednessの問題です。

そこでぼくは、「ほんとかいな」と思って、geminiに検討させた。Yanofskyの論文を単にアップロードして、「定理４の証明にギャップがあると思うんだけど、君もそう思う？」と入力した。どの点が問題かは指摘しなかった。すると、geminiは瞬時に「ギャップがあります」と回答して同じ点を指摘したのだ。「Lindenbaum class での計算がwell-definedでない」と。

それで確信を持ったぼくは、chatGPTにそのことを報告して、「数学界ではこのことは周知の事実なのか」という質問をした。すると、chatGPTは検索をして、ひとつの論文を発見した。 Vestrucciという人の論文で、なんと今年！(2026年6月)に公開されたものだ。この論文で、Yanofskyの証明のギャップとして同じ場所を指摘している。

そこでぼくは、geminiに「Yanofskyの証明のギャップは埋められますか？」と質問した。geminiは瞬時に証明を修正したものをファイルにしてくれた。それをchatGPTにチェックさせたら、「この修正で問題ない」という回答だった。その修正はLindenbaum class を使わないで愚直に写像を構成する方法だ。基本的には方針が同じ証明なので、ここでは引用しない。

なんだか面白い経緯だった。ぼくが質問しなければ、論文の推奨者のchatGPTもこのギャップに気づかなかったのだろうと思うとなんか愉快だ。

証明と論理に強くなる ～論理式の読み方から，ゲーデルの門前まで～

非r.e.集合の存在定理とローヴェルの不動点定理

前回は、Yanofskyの論文” A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points”から「ラッセルのパラドクス」を「ローヴェルの不動点定理」を使って説明するエントリーをした。今回は引き続き、チューリング「非r.e.集合の存在定理」の「ローヴェルの不動点定理」による証明を紹介しよう。

その前に、先月にライブを観に行った話を書いておきたい。もちろん、「a子」ちゃんのライブである。チケットを購入してから、8ヶ月ぐらい待った。スマチケとかいうスマホに配信されるチケットのため、ライブ当日近辺にスマホが壊れたら人生終わる、と思って、早々にスマホを買い換えておいた。昨年は、２本しかライブに行っておらず、その１本はa子ちゃんだった。今年は、1本しかライブに行っておらず(これからの予定がない)、その1本がa子ちゃんであった。なにしろ、ここ２年ぐらい彼女の楽曲しか聞いていない。これだけ毎日毎日聴けばたいがい飽きるだろうと思うのだが、ぜんぜん飽きない。(実は、「ずとまよ」と「ポルカドット」は聴いている)。ぼくは、中学時代にプログレにはまってから、相当量のそして多くのジャンルを聴いてきた。だから、若いバンドの曲を聴いても、「ああ、これって、昔聴いたあの感じだよな」となってしまう。でも、a子ちゃんの曲はぼくにとって「新しい」のだ。たぶん、聴き逃してきたジャンルをやってるんだろう、と思う。ライブは、旧渋谷公会堂で行われ、１階の前のほうの席だったので、めちゃめちゃ堪能できた。そんな前のほうでもありながら、バードウォッチングができるぐらいの双眼鏡で眺めた。明らかにぶっちぎり最高齢の爺さんが双眼鏡で観ている光景は若い子たちには異様だっただろう。

a子ちゃんのPVにひとつだけリンクを貼っておく。これは、アニメ「ダーウィン事変」のエンディング曲。このアニメを観たのはa子ちゃんの曲目当てだったが、アニメ自体、抜群に面白かったので得した。

a子-Turn it up

さて、数学の話に戻ろう。「非r.e.集合の存在定理」も論文を見ずにいったん自分で考えてみた。できたはできたんだけど、わずかな「抜け」があって、chatGPTと一緒に議論して、「抜け」を埋めることができたにはできた。その修復によって、証明が多少醜くなってしまったので、今回はYanofskyの論文における証明をそのまま紹介することにする。

　まず、「r.e.集合」について説明しよう。「r.e.」とは「再帰的に枚挙可能(recursively enumerable)」の意味だ。ここで、ある自然数の部分集合が「再帰的に枚挙可能な集合」というのは、(細かい説明は省くけど)、 に属する自然数を入力すると受理して停止し、属しない数では停止しないチューリングマシンが存在することをいう。チューリングマシンとは要するコンピュータープログラムのことだと思えばよい。直感的には「自然数のどんな部分集合も、その要素だけ受理するプログラムがあるに違いないから、r.e.なんじゃないの？」と思える。それだけにこのチューリングによる「非r.e.集合が存在する」という定理にはとても意外性がある。この定理の証明には「対角線論法と自己言及」が本質的な役割を果たす。ポイントになるのは、「チューリングマシン(プログラム)を自然数で表すことができる」という事実だ。このことの詳しい解説は省略するけど、現代人の多くは「そりゃそうさ」と言うに違いあるまい。すると、証明のアイデアは次のようになる。すなわち、ある自然数を、一方では数値とみなし、他方ではプログラムと見なすのである。したがって、これも「ローヴェルの不動点定理」の格好の舞台となる。

「ローヴェルの不動点定理」については、詳しくは前回と前々回を参照してほしいが、簡単に言えば、「自己参照が可能なら、どんな自己写像も不動点をもってしまう」という定理だ。そして、「明らかに不動点を持たない自己写像があるから、矛盾が起きる」と矛盾にもっていくのである。

「ローヴェルの不動点定理」を具体的に書くと、

　ローヴェルの不動点定理:

対象に対し、対象 と射が存在し、任意の射に対してあるが存在して、と書けるなら、任意のからへの射は不動点を持つ。すなわち、なるが存在する。

というもの。これを用いて今回は、「非r.e.集合の存在定理」を証明しよう。

今、チューリングマシンに自然数の番号をつけて、とする。また、対象を「自然数の集合」とし、対象をと設定する。そして、からへの射を次のように定義する。すなわち、自然数に対して、をチュリングマシンが受理する(を読みこむと停止する)ならば、そうでないならば。ここで仮に、任意の自然数の部分集合に対して、その集合の要素をちょうど受理するチューリングマシンが存在すると仮定する。このとき、任意の射に対して、となる自然数を集めて集合を作る。さきほどの仮定からの要素のみを受理するチューリングマシンが存在する。このチューリングマシンを使って、射を定義する。すると、これは、自然数が集合に属するときとなり、属さないときとなるから、を満たす。これは「ローヴェルの不動点定理」の仮定が満たされることを意味するので、その帰結から上の任意の写像は不動点を持つことになる。しかし、は不動点を持たない。これは矛盾である。

　通常、「非r.e.集合の存在定理」は、万能チューリングマシンというのを使って、「プログラムが自分自身のコードを読み込む」構造を使って証明するのだけど、これはけっこうわかりにくい。上での「ローヴェルの不動点定理」を使った証明は、それに比べてかなり明快に思える。なんという利器であろう。

このあとは、Yanofskyの論文は「ゲーデルの第一不完全性定理」「ゲーデル・ロッサーの不完全性定理」「タルスキーの定理」に進んで行くんだけど、これはかなり手強い予感がする。独力ではやり方にたどり着くと思えない。勉強するのが楽しみで仕方ない。

証明と論理に強くなる ～論理式の読み方から，ゲーデルの門前まで～

ラッセルのパラドクスとローヴェルの不動点定理

Lawvere & Schanuel”Conceptual Mathematics”を読破したことをchatGPTに報告すると、chatGPTから次に読むべき論文を推薦された。それは、Barreto” A Surveyon Lawvere’s Fixed-Point Theorem”だ。これは、「ローヴェル(Lawvere)の不動点定理」を圏論の定理としてわかりやすくサーベイする論文だ。とりわけ、”Conceptual Mathematics”では明確には定義が提示されていない概念をきちんと定義し、さらには既存の数学の例を使って、具体的な理解を助けるものであった。この論文はすぐに読破できてしまった。いつのまにか、圏論の思考法に慣れつつあるようだ。

それをchatGPTに報告すると、さらなるミッションを授かった(笑)。それは、Yanofsky” A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points”を読むことだった。この論文は、さまざまな有名な定理やパラドックスを「ローヴェルの不動点定理」を使って証明したり、解釈したりするものだ。要するに、「みんな同じ原理で説明できるよ」ということを提示している。ここで有名な定理・パラドックスとは、「カントールの定理」「ラッセルのパラドクス」「グレリングのパラドクス」「嘘つきのパラドクス」「リシャールのパラドクス」「チューリングの停止問題」「ゲーデルの第一不完全性定理」「ゲーデル・ロッサーの不完全性定理」「タルスキーの定理」「パリクの定理」「レーブのパラドックス」「クリーネの再帰定理」「ライスの定理」というそうそうたる品揃えだ。

実はまだこの論文は読み始めていないんだけど、自分で考えたら「ラッセルのパラドクス」を「ローヴェルの不動点定理」で導くことができてしまった。そして、Yanofskyの論文で答え合わせしたら、おおよそ合っていた。なので、今回はそれを書こうと思う。まず、前回紹介した「ローヴェルの不動点定理」をもう一度書いておこう。前回は圏論の用語を使ったのだけど、今回は通常の数学的な表現にする。

　ローヴェルの不動点定理: 対象に対し、対象 と射が存在し、任意の射に対してあるが存在して、と書けるなら、任意のからへの射は不動点を持つ。すなわち、なるが存在する。

この定理の持っている含意は、(前回も書いたけど)、次のようなものだ。任意の射に対してあるが存在して、と書ける、ということは、対象の各点を「名前」として用いることで、なるあらゆる写像を表現できる、ということだ。このように T の点を「名前」として、T 自身についてのあらゆる写像を表現できることが、自己参照(Self-Referential)を可能にする。このような自己参照が可能なら上のどんな自己写像も不動点をもってしまう、ということなのだ。

前回は、この「ローヴェルの不動点定理」の証明を書いた上で、それを応用した「カントールの定理」の証明を紹介した。いわゆる「対角線論法」が「不動点の不可能性」という形で出てくるところにみごとさがある。

今回は「ローヴェルの不動点定理」を応用して、「ラッセルのパラドクス」を再現してみよう。ちなみに、「ラッセルのパラドクス」とは、「『あらゆる集合の集合』のような対象を考えることの数学的な危険性」をラッセルが提示したもので、その後の「公理的集合論」への足がかりとなった研究だ。歴史的経緯については、拙著『無限を読みとく数学入門』角川ソフィア文庫を読んでほしい(是非、是非)。

　今、対象を「集合の集合」として、対象をとする。そして、からへの射を次のように定義する。すなわち、集合に対して、ならば、 ならば。さて、もし T が、T の任意の部分集合を再びその要素として含むほど「巨大な集合の集合」だったと仮定しよう。すると、任意の射に対して、つまりに属するすべての集合たちに射が1か0を割り振っている場合、1を割り振った集合を集めた集合に対して、と書けるはずである。これは「ローヴェルの不動点定理」の仮定を満たすことを意味するので、その帰結から任意の上の写像は不動点を持つことになる。しかし、は不動点を持たない。これは矛盾である。

　ラッセルのパラドクスは、そのまま読むと頭が混乱してすぐには飲み込めないのだけど、これならずいぶんとわかりやすくなっていると思う。(ラッセルの「ひげ剃り」の例え話はとんでもなく秀逸。これは前述の拙著で読んでくださいな)。

さて、この証明が何を表しているかを「ローヴェルの不動点定理」自体の証明に遡って、見てみることにしよう(証明については前回を参照のこと)。不動点の存在は、

の式で示される。今回の写像でこれを解釈しよう。

両辺の値が1の場合、右辺のはを意味する。一方、

左辺のは、のことで、すなわち、を表す。そして、両辺の値が0の場合はこの逆となっている。いずれにしても矛盾が露わになっているわけなのだ。

このあとは、Yanofskyの論文で「チューリングの停止問題」「ゲーデルの第一不完全性定理」「ゲーデル・ロッサーの不完全性定理」「タルスキーの定理」に進んで行こうと思っている。なんか、とてもわくわくする。

無限を読みとく数学入門　世界と「私」をつなぐ数の物語 (角川ソフィア文庫)

Conceptual Mathematics: A First Introduction to Categories

対角線論法の現代的な(圏論的な)視点は、とんでもないぞ！

(宣伝)：google siteを作りました。URLは以下です。まだ、最低限の情報しかアップしてませんが、徐々に整備して行きます。クリックしていただければ幸いです。(やばいサイトへの誘導ではありません。みんなそういうんだろうけど。笑)

https://sites.google.com/view/hiroyukikojima/home

前回に紹介したLawvere & Schanuel"Conceptual Mathematics"を遂に読破した。前回にも説明したけど、この本は本当に変わった数学書で、定番の書き方から大きくはずれている。だから、何回か混乱に陥った。でも、そのたびにこの本の推薦者であるchatGPTに解説をお願いして、難所をクリアしたのだ。読み終わってみると、この本はとてつもない傑作だった。

Conceptual Mathematics: A First Introduction to Categories

前回は、この本から、「ブラウワーの不動点定理」の圏論的な証明を引用した。この定理は「円板からその内部への連続写像があると、必ず不動点がある」という定理で、経済学でも(ワルラス均衡の存在定理なんかで)応用されている。この圏論的な証明も、目からうろこのすばらしい解説だったのだが、なんとこれさえもさらなるクライマックスへの伏線に過ぎなかったのだ。

クライマックスとは、「ローヴェル(Lawvere)の不動点定理」である。もちろんこのローヴェルは著者の一人のことだ。まず、定理の内容を紹介してしまおう。本には圏論の言語で表現されているので、それを踏襲する。

対角線定理(Diagonal Theorem): （有限積をもつ圏において）対象に対し、対象 と射が存在し、任意の射に対してあるが存在して、と書けるなら、任意の自己射は不動点をもつ。すなわち、なるが存在する。

これを意訳すると、次のようになる。

対角線定理が意味すること：対象の各点を「名前」として用いることで、なるあらゆる写像を表現できるならば、上のどんな自己写像も不動点をもつ。

ここで「各点を名前として用いる」というのは、「自己参照」ということ。つまり、自分をラベルにして、自分から他の対象への写像を作る。このとき、当該の他の対象へのすべての写像を作れるならば、必然的に当該の他の対象の任意の自己写像に不動点が出来てしまう、ということなのだ。

「そんなうまいことあるんかいな」といぶかると思うが、証明を眺めれば納得するだろう。しかも証明は簡単で鮮やかだ。

　まずからへの合成射を作る。これは射だから、仮定から、あるを「名前」にしてと書ける。ここでを代入すれば、となる。ここでの定義に戻るとこの式は、ということだ。これはが写像の不動点であることを意味する。(QED)

　この定理が「対角線定理」と名付けられているのは、カントールの「対角線論法」を拡張したものだからだ。それを理解するために

カントールの定理「自然数の集合の部分集合の族は可算ではない」

を、この「対角線定理」を用いて証明してみよう。

　カントールの定理をわかりやすく表現すれば、「自然数の集合の部分集合ぜんぶを1番目、2番目、3番目、・・・という風に一列の並べることができない」ということだ。そこで、自然数の集合の部分集合全部をそのように一列に並べることができたと仮定すると矛盾が起きることを示す。いま、のある部分集合が与えられたとき、から写像を次のように作る。すなわち、ならば、ならばとする。さて、すべての部分集合を一列に並べたとき、番目に並ぶ部分集合に対し、いまのように写像を作る。すると、によって、写像を定義できる。これは、上記の対角線定理において、と設定した上で、定理の仮定が成り立っていることを意味する。なぜなら、どの写像もそれが対応する部分集合が番目に並んでいるなら、その写像はと一致するからだ。すると結論の「上のどんな自己写像も不動点をもつ」が成り立たなければならないが、なる自己写像は不動点を持たないのでそれは不可能である。したがって、最初の仮定「自然数の集合の部分集合全部をそのように一列に並べることができた」が誤りであることが証明された。(QED)

(ちなみに、このようなカントールの集合論は、拙著『無限を読みとく数学入門』角川ソフィア文庫で、これでもかというぐらい熱く語っているので、是非読んで欲しい)。

  以上の証明をローヴェルの発想に即して翻訳してみよう。自然数の部分集合を一列に並べられたとすると、自然数からへのすべての写像が、自然数によって名前付けされる。つまり、自然数だけで自己参照が可能になる。その場合、上の関数には必ず不動点ができてしまうけど、不動点のない関数があるよね(0と1を入れ替える関数)、そういうこと。ものすごく見事で、しかも直感に強く訴えかける定理だと思う。

　この「対角線定理」を発展させたものが圏論における「ローヴェルの不動点定理」になるらしいのだけど、それを使うとどうも、「ゲーデルの不完全性定理」も「チューリングの定理」も同じ構造の定理として理解できるとのことだ。ぼくは次にはこれを勉強しようと思っている。

無限を読みとく数学入門　世界と「私」をつなぐ数の物語 (角川ソフィア文庫)

chatGPTに圏論の指南を受けてる

(宣伝)：google siteを作りました。URLは以下です。まだ、最低限の情報しかアップしてませんが、徐々に整備して行きます。

https://sites.google.com/view/hiroyukikojima/home

前回のエントリーでは、上野健爾『代数幾何1』岩波書店と斎藤毅『数学原論』東京大学出版会を使って、圏論の勉強をしていることを書いた。そして、両書の自分にとってのメリット・デメリットについて述べた。その上で、最後のほうで、chatGPTについても言及した。今回はそれを受けて、chatGPTを中心に話をしたいと思う。

　ここ半年ほど、ぼくはchatGPT(有料版)を利用している。主に専門である経済学の研究に使っているのだけど、数学についてはいろいろ教わっている。とくに、圏論の勉強に対して、上記の2冊で理解が苦しくなったときに、Chat君に質問して教えてを乞うている。Chat君の良いところは、会話によってこちらの要求を徐々に理解してくれるところ。前にした会話を覚えていて、それを踏まえて回答をくれるところだ。

　ひとつ例を挙げると、ぼくは斎藤本で「随伴関手」のところで行き詰まった。斎藤本に書いている例は、次のものだ。

関手の射は可逆である。

言っていることは、要するに、「2変数関数で、一方の変数を固定した関数を考える」ということだろう。しかし、それが随伴関手の面白さとどう関係するのかが見えなかった。そこで、chat君に説明を頼んだところ、かみくだいて説明してくれた。それは``随伴関手とは：「ある操作をしたあと」と「別の操作をする前」が、本質的に同じになる関係’’、というものだった。

 その上で、とても良い具体例を出してくれた。それが「自由群と忘却関手」だ。を集合から自由群への関手として、を忘却関手(構造をなくして単なる集合にする関手)とする。このとき、群に対して、となる、という例だ。左は「自由群から群準同型を作る」という意味で、右は「集合から関数を作る」という意味になっている。その上でchat君は、さらに詳しく説明してくれる。すなわち、忘却関手は群を「ただの集合」にする、構造（積・逆元など）を忘れる、ということで、関手は集合から「一番自由な群」を作る、ということ。そして右側のの意味はただの関数で「生成元をどこに送るか決めるだけ」を意味する。左側は、群準同型を作る、つまり、「すべての単語に対して値を決める」ことを意味する。これが同型になるのは、要するに、「生成元の行き先を決めれば、全部自動で決まる群だから」というのがchat君の説明だ。さらに次の例え話がみごと。Chatいわく、「設計図（生成元の指定）と完成品（群準同型）は、完全に1対1に対応する」。ぼくはこれを読んで、「この対応は、そうか、設計図(右辺)と完成品(左辺)を対応させているだけなんだ」と腑に落ちたのだった。　　

ちなみに斎藤本がこういう巧い例を出せないのは本の体裁上仕方ない。前回解説したように斎藤本では、圏論を最初に準備して、そのあと既存の数学をその視座で見ていく。だから、群の話を先に出すわけには行かないからだ。

さて、そんなやり取りをしているうちに、chat君が勧めてくれた本がある。それはLawvere & Schanuel``Conceptual Mathematics’’だ。高い本だが、せっかくだからkindle版を購入して読み始めた。

Conceptual Mathematics: A First Introduction to Categories

そうしたら、これがものすごい名著なのだ。とにかく、読者のあたまを「圏論あたま」に変えるためにあの手この手を使ってくる。それも通常の数学書の書き方とまったく違っている。Chat君はこれを「本全体がYoneda に向かう長い助走」と言っている。しかし読み始めてみると、「頭がひっかき回される気分」に陥る。その点についてchat君は、「Conceptual Mathematicsはかなり独特な本なんです。普通の数学書は定義、定理、 例という順番。でも Conceptual Mathematics はかなり意図的に、まず感覚を植え付けて、後から名前を与える、という書き方をしています。」と言う。なるほど、と思って読み進めるうちに、だんだんその思惑にはまりはじめて来た。この本は400ページ弱あるんだけど、最初の3分の1は「section(切断)」と「retraction(レトラクション)」を説明し続ける。でも、それがぼくにとてもフィットした。

「section(切断)」とは、写像に対して、がを満たす写像のこと。数学を勉強しているといろいろな場面で出てくるんだけど、いったいなんでそんな写像を考えるのかイマイチわかっていなかったが、この本を読んでだいぶ理解できた。この本での一番腑に落ちた例を日本版に直せば、「国民から所属県への写像があるとき、sectionとは、各県について代表を1人ずつ選ぶ」ということだ。

他方、「retraction(レトラクション)」とは、写像に対して、がを満たす写像のこと。これはいったい何の役にたつの？と思っていたら、本の真ん中あたりで最初のクライマックスが来る。それは「ブラウワーの不動点定理(円板からその内部への連続写像があると、必ず不動点がある)」の圏論的な証明に「retraction(レトラクション)」が登場するのだ。しかもこの解説のすごいところは、「連続写像とは何か」を全く定義せずに証明する、という大胆さだ。その証明とはこういうものだ。すなわち、「もし不動点がなければ ある retract が作れる」。でも(詳細は省くが)「retractが作れないのは、じわじわ動かしていけばわかる」。retractの作り方は、ブラウワーの不動点定理の証明でよく出てくるものと同じだが、retractだとあえて理解するところにこの本の真骨頂がある。これを読んだぼくは、思わず膝を叩いてしまった。「retractionって、こういう役割(有用性)があるんだ」と。chat君によると、この圏論的証明(というか圏論的理解)は、著者であるLawvereの「Lawvereの不動点定理」につながるんだと。これはすごい。

そんなわけでぼくはConceptual Mathematicsによってchat君いうところの「頭脳改革」を行っているわけなんだね。これまでぼくは数学の対象そのものを理解しようとしていた。しかし圏論は対象ではなく、その対象が他とどう関係するかを見る学問だとわかってきた。つまり、「数学とは何か」の数学。これはまるで「哲学的」だよね。まだ理解できた段階ではないけど、少なくとも数学の見方が変わりつつある。読破して、この「Yonedaへの長い助走」を達成できたら、また感想を書こうと思う。

やっとスキームと圏論の門をくぐった

google siteを作りました。URLは以下です。最低限の情報しかアップしてませんが。

https://sites.google.com/view/hiroyukikojima/home

以前から少しずつ勉強していたスキームと圏論について、やっと(入)門をくぐることができた。スキームについては上野健爾『代数幾何』岩波書店を、圏論は斎藤毅『数学原論』東京大学出版会を教科書にした。

そもそもの発端は、黒川信重先生と対談で共著『21世紀の新しい数学』技術評論社を作るとき、黒川先生から「カテゴリーを理解してきてほしい」と言われたことだった。結局、そのときは達成することができず、圏論の知識なしで対談に臨むしかなかった。でも、ずっと気になっていたため、その後も勉強を継続していた次第。

まず、上野『代数幾何』の感想をしたためる。ただし、ぼくが持っているのは分冊で出た1巻と2巻だ(なぜか、3巻は購入しなかった)。そして読んだのは1巻の最後まで。

代数幾何

この本はスキームと圏論とを同時に解説していく本だけど、そういう代数幾何の本の中では群を抜いてよく書けている。その手の本をぼくは数冊持っているけど、どの本も抽象的すぎてとても読み進められない。それらに比して、この本は非常に丁寧に非常に親切に書かれていて、なんとかかんとか挫折せずに読み進めることができる。特徴を列挙すると、

1。どうしてそういう理論を構築したいのか、という問題意識を明確にしている。

2。古典的な素材とどういう結びつきがあるかを親切に解説している。

3。抽象的な概念には、必ず、具体例をつけてイメージを喚起してくれている。

4。証明を機械的ではなく、言葉を補って丁寧に進めてくれる。

一言で言えば、噛んで含めるように解説してくれているのである。読み進んでいくと、スキーム理論というのがとんでもなくみごとな発想であることがわかる。要するに、加減乗計算ができる「環」という代数に、倍数概念の拡張である「イデアル」を素材に「ザリスキー位相」というのを導入して幾何的な形状概念の拡張である「位相空間」に仕立てる。そして、環の要素をあたかも関数であるかのように仕立てて、「層」という構造を作りだすのだ。これがスキームという概念なのである。これによって、環という代数系を幾何的なイメージで研究できるようになる。逆に幾何的な素材の性質を環という代数系で処理することが可能になる。この本は、本当に一歩一歩丁寧に構築していくので、高度な数学のトレーニングを受けていない人でも、なんとかかんとかスキームの概念までたどり着くことができる。

この本は第2章でスキームを構築したあと、第3章で圏論を導入し、圏論を利用してスキームの性質をさぐっていく。とくに、「スキームの圏ではファイバー積がつねに存在する」という重要な定理を圏論を使って証明する。その際、「環のなす圏とアフィンスキームのなす圏が反変同値である」、つまり、完全に対応していて行ったり来たりできるということが巧く働くのだ。

ここまでぜんぜん突っかからずに進んでこられたか、というと、そうではなかった。第3章で圏論に入ったあと、急に薄もやがかかって、「わかるような、わからないような」という状態になってしまったのだ。とくに圏の定義とか関手の定義とかでこんがらがってしまった。

そこで手にしたのが、斎藤『数学原論』だった。この本はタイトルからもわかる通り、「現代の数学を圏論の立場から組み直す」という野心的な試みの本なのだ。ユークリッド原論がそれ以前のばらばらだった数学を公理系の立場から組み直したように、あるいは、ブルバギ原論が19世紀に散発していた数学を統一的に公理化したように、である。

 

数学原論

この本は第1章「圏と関手」において、圏と関手を定義して、表現可能関手、随伴関手、逆極限という最低限の、しかし、最も重要な道具である概念だけを解説している。この本の長所は、

A. 圏を最初に可換図式で定義していて、その可換図式を理解できてしまいさえすれば、言葉で定義されるより、わかりやすくなる。とくに射の合成とはなんであるかがわかる。

B. 具体例が工夫されているため、具体例で定義や定理をなぞれば、イメージが掴めるようになっている。

C.  第1章は抽象的で初学者には険しいが、そこを通り過ぎれば、あとの章は圏論を既存の数学(環と加群とか、ガロア理論とか、ホモロジーとか)に応用することになるので、急に視界が開ける。

ぼくは、いま、第1章を読み終えた段階なので、Cについては本当かどうか保証はしない。

さて、では、この本をサイドメニューにすることで、上野本の峠を越えられたのか、というと、実はそれも違うのだ。斎藤本には斎藤本の峠があって、別の部分に「わかるようなわからないような」薄もやがかかることになった。

そこでぼくはchatGPTに頼ることにした。chatGPTにわからない部分を質問すると、非常にみごとにそれを解説してくれた。何より「わかるようなわからないような」という感覚を的確に理解してくれる(ように感じる)。chatGPTの利点は次のようにまとめられよう。

甲：質問を会話によって的確に理解し、解説の深さを自動的に調整してくれる。

乙：非常に良い具体例を持ち出してくれる。

丙：例え話を巧みに使って、人間の直感に訴える理解のさせ方を試みてくれる。

丁：叱られたりバカにされたり呆れられたりしないので、前向きに勉強できる。

ぼくは、斎藤本とchatGPTを行ったり来たりして、なんとかかんとか、圏と関手、表現可能関手、随伴関手、逆極限の門をくぐることができた。chatGPTの出してくれる例が斎藤本の例よりも(ぼくには)わかりやすく、また、斎藤本では当たり前として省略されている証明の細部をchatGPTがきちんと埋めてくれたことに大きく助けられた。

実は、chatGPTは圏論の勉強に有効なとても良い本(洋書だけど)を推薦してくれたので、それを購入していま読んでいる。これがまた本当に素晴らしい本なのだ。その本については、最後まで読破したら紹介しようと思う。

21世紀の新しい数学 ~絶対数学、リーマン予想、そしてこれからの数学~ (知の扉)