1.  はじめに

これまで,このセマンティックウェブ・ダイアリーで繰り返し述べてきたように,RDF 意味論の基礎には集合論があります.しかしセマンティックウェブの研究者のほとんどは,集合論を理解しないために,rdfs:Resource やrdfs:Class の解釈をめぐって議論と混乱があります.特に,RDF(S) はラッセルのパラドックスを招くという,攻撃が一部の陣営から繰り返し行われました.(最近はちょっと大人しくなっていますが.もう一時期の熱が冷めたのかな.でもまだ混乱は払しょくされていないと思う.)私自身は,SWCLOSにおいて難なくRDF 意味論を実現できたために(実は細かくいうとセマンティックウェブの原則にいくつかの問題点があるのですが),そういう批判の根拠を理解しようと,あるいはRDF 意味論を理解しようと,集合論やラッセルのパラドックスとは何であるかについて今まで勉強をしてきました.

ところが最近,ラッセルのパラドックスに関連して,チャイティンの「知の限界」という本にLISP で書いたゲーデルの不完全性定理のあることを知ったのです.翻訳者は黒川さん.ちょっと昔のLisper ならみんなご存知の方です.チャイティンという人は IBM ワトソン研究所にいるらしいのですが,今のいままでこういう人がいるというのを知らなかった.「ゲーデルの哲学」という素晴らしい新書版にもチャイティンのことは大きく取り上げられていて,今では,ゲーデルの不完全性定理 --> チューリングの計算不可能性 --> チャイティンのランダム性 という研究の流れになっているらしい.Lisp でゲーデルの不完全性定理が書けるのなら,さっそくやってみようと思ったのですが,このブログで紹介したように,歴史的には カントールの集合論 --> ラッセルのパラドックス --> ゲーデルの不完全性定理 という流れがあるため,そのまえにLisp で集合論をやったほうがいいのではないか,と思った次第なのです.そのほうが理論的によく理解できそう.セマンティックウェブの理論的基礎でもあるし.

論文にするなら,結果だけを書くのですが,ここはブログですから,現在進行形で,しかも Lisper の方にもためになるように,ということで「CLOS で学ぶ集合論」というタイトルにしました.これまでのPAIP-Lisp シリーズではCLOS を取り上げませんでした.強いて言えば,その理由はあまりよい例が見つからない,ということだったのですが,CLOS を知りたいという要求が強いということは理解していますから,そういう要求にも答えようと思っているわけです.

理論派の人は,特に論理学の分野の人は,論文にするなら証明しなければ駄目だと言います.これはもちろんその通りなのですが,得てして証明して終わり,では誤りがあったり,自己満足で終わってしまうこともあるのではないでしょうか.実践家はというかプログラマーは(私のこと),プログラムしてそれがきちんと動いたときに,はじめて問題を理解したと思います.ですから,もしゲーデルの不完全性定理がプログラムできるのなら,集合論がプログラムできるのなら,プログラムしてみよう,と思うわけです.RDF意味論の中でPat Hayes はこんなラッセルの言葉を引用しています.

証明の利点の一つは,証明された結果について確かな疑問を抱かせることである.(Bertrand Russell)

いい言葉ですね.証明終わり QED ではないということですね.