プログラマのための「ゲーデルの不完全性定理」(4)：「展望」への緊急パッチ（オハナシだよ）

yoriyukiさんとの一連のやりとりで、「プログラマのための『ゲーデルの不完全性定理』」シリーズ第2回「速攻速習編」の「ゲーデルの不完全性定理への（ほんの少し）展望」に問題があると判明しました。その問題とは主に次の2点です。

あまりにも説明をはしょっている。そのため、誤解・誤読のリスクが高い。
「ゲーデル」という、歴史上実在の人物を表す固有名詞の使い方が間違っている。

1番目に関しては、ていねいな説明を書く以外の対策がなく、手短な展望としてはいかんともしがたいです。ただし、ある程度の予備知識を仮定してよいなら、次が補足説明になっています。

2番目に関しては、この緊急パッチ(?)編で修正します。ただし、原論文や歴史的事実を調べる手間をかけたくない（怠け者）ので、実在のゲーデルはもう出さないことにします。架空のキャラクタ達によるオハナシ（フィクション）として記述します。第2回「速攻速習編」の、1節から6節までは読んでいることを仮定します。その続き（つまり、7節の置き換え）がこのオハナシです。

※ 印刷時にはサイドバーは消えるはずです、お試しください。
今回の内容：

ルデーゲ氏登場
ダボーラ氏も登場
ダボーラ氏のwillStop関数
ダボーラ氏の蹉跌
ルデーゲ氏のtryProof関数
ルデーゲ氏の証明エンジン
ダボーラ氏、捲土重来なるか

●ルデーゲ氏登場

ルデーゲ氏は、論理学者にしてプログラマ。彼は温厚で誠実な人。一方で、社交的でおしゃべりな男でもあります。

お分かりのとおり、“ゲ・ー・デ・ル”をひっくり返した名前ですが、「社交的でおしゃべり」というキャラクタ設定が、実在のゲーデルと逆になっています（たぶん）。通説によれば、ゲーデルは非社交的で無口だったようですから。

●ダボーラ氏も登場

ダボーラ氏（これは、そのまんま「駄法螺」から）は、優秀なエンジニアにして経営者ですが、自分の会社の評判／価値を上げるためなら手段を選ばない、不正も辞せずな人です。いずれは司直のお世話になりそうな人物ですが、今のところ、ルデーゲ氏のライバルとみなされています。

●ダボーラ氏のwillStop関数

ダボーラ氏は、あるライブラリの3ヶ月後リリースを発表しました。そのライブラリの主要な関数であるwillStopは、willStop(プログラムのソースコード文字列, 引数)として呼び出すと、そのプログラムが停止するかどうかを判定します。

記者「そのwillStop関数は、どんなプログラムの停止性も判定できるのですか。」
ダボーラ「もちろんですとも。willStopは、どんなプログラムにどんな引数を組み合わせても、常に正しい結果を出します。」
記者「willStop関数の用途はどんなもんですか。」
ダボーラ「例えばテスト／デバッグです。多くのプログラムは停止すべきですが、バグで停止しないこともありますね。willStopを使えば、バグのある／なしが、たちどころに分かりますよ。」
記者「このライブラリはオープンソースですか。」
ダボーラ「我が社で開発した画期的なアルゴリズムを使用していますからね、ソースは開示できませんね。」

●ダボーラ氏の蹉跌

このニュースを聞いたルデーゲ氏は言いました。

ルデーゲ「ほう。そんな関数があれば確かに素晴らしいね。」
弟子「でしょう。すごいですよね。」
ルデーゲ「そんな関数が“あれば”ね。」
弟子「3ヶ月後にはリリースだそうですよ。」
ルデーゲ「もし、仕様どおりのwillStopがリリースされたら、それを使って面白い関数を書けるよ。」

と言って、ルデーゲ氏は弟子に説明をはじめました。

弟子「えーっ！止まる場合は止まらない！」
弟子「ええええーっ！！止まらない場合は止まるーー！！」
弟子「せっ、先生、どっ、どういうことですか、これ？」
ルデーゲ「ダボーラさんの発表通りのライブラリは永久にリリースされないってことだよ。もし、彼が言うとおりのwillStopが実在するなら、『止まる場合は止まり、止まらない場合は止まる』関数mysteryFuncも作れるだろう。でもmysteryFuncの存在が許されないのだから、willStopの存在も許されない。それだけのこと。」
弟子「じゃ、ダボーラ氏はウソをついているのですか。」
ルデーゲ「さあどうかな。悪意があるかどうかは分からないが、ありえないものをリリース予定と言っていることは確かだね。」
弟子「なんて奴だ、ダボーラ。僕、この件を新聞記者にたれ込んできます。」（すぐさま飛び出す）

こうして、ダボーラ氏の会社の株は急上昇のあとに急降下しました、とさ。

●ルデーゲ氏のtryProof関数

※ canProveは誤解を招きやすい名前なので、tryProofに変えました。

記者「ルデーゲ先生、その関数はホントにどんな命題でも証明してしまうんですか？先日のダボーラ氏の件もありますからね。我々も疑り深くなってましてね。」
弟子「ダボーラとウチの先生を一緒にしないでください！ルデーゲ先生の関数tryProofは、どんな命題もちゃんと証明するんです。」
ルデーゲ「おいおい、君ねぇ。偽な命題は証明しないよ。証明できない命題はもちろんあるし、そうじゃなきゃ困るよ。」
記者「じゃ、tryProof関数は何をするんですか。」
ルデーゲ「tryProofは、述語を表現した式と引数を与えると、それから論理的な文を作るんだ。その文、まー命題と呼んでもいいけど、その証明を試みるんだ。」
記者「試みる？」
記者「そう。実際の証明作業は、証明サーバー上で動いている証明エンジンが頑張っている。それで、tryProofは証明エンジンに対して、命題が既に証明されているか、あるいは命題の否定が証明されているかを問い合わせる。」
記者「それだけ？」
ルデーゲ「うん、それだけ。証明エンジンがなかなか応答しないことがあるよ。証明エンジンはフル回転で頑張っているのだけど、結果が出るまで待つしかない。証明エンジンが命題を証明すれば、tryProof関数はtrueを返して戻るし、証明エンジンが命題の否定を証明したなら、tryProof関数はfalseを返して戻る。」
記者「時間がいくらかかってもいいなら、命題が真か偽の決着がつくんですね。」
弟子「あたりまえじゃないですか！」
ルデーゲ「いや、命題が真か偽の決着がつくとは言いきれない。」
記者、弟子「なっ、なんですってー!?」

●ルデーゲ氏の証明エンジン

記者「先生、tryProof関数とか証明エンジンとか、何の役にも立たないじゃないですか。」
ルデーゲ「そんなこともないよ。証明できるはずの命題なら、いずれは証明できるんだから。」
記者「じゃ、証明できるかどうかは、時間さえかければ分かるんですね。」
ルデーゲ「いや、証明できるかどうか分からないよ。証明できるものなら、待っていれば証明されるってだけ。反証、つまり否定の証明ができるなら、それも待っていれば、いずれ証明エンジンにより反証される。」
弟子「先生、僕もわけわかんないですよー。」
ルデーゲ「だからね、私は『どんな命題でも証明されるか、反証されるかのどっちかだ』って言ってないでしょ。証明される命題もある、反証される命題もある、どっちでもない命題もあるってこと。」
弟子、記者「ええーっ、どっちでもない!?」
ルデーゲ「うん。どっちでもない命題があるのはしょうがないよ。そういうもんだ。」
記者「あっ、わかりました、先生。証明エンジンがまだ未完成なんですね。今後のバージョンアップの予定は？」
ルデーゲ「ない。」
弟子「先生、そんなーぁ。」
ルデーゲ「パフォーマンスの改善はできそうだけど、私は興味ないし。パフォーマンスが上がったところで、本質的には何も変わらない。どうせ、証明も反証もできない命題は残るのだからね。」

●ダボーラ氏、捲土重来なるか

と、そこで記者の携帯電話が鳴った。

記者「ルデーゲ先生、ダボーラ氏が完璧な証明エンジンをリリース予定だそうです。どんな命題でも、その真偽を判定する関数を備えるそうですよ。こうしちゃいられない、失礼します。」

記者が去った後：

弟子「先生、ダボーラに負けちゃうじゃないですか。」
ルデーゲ「またダボーラか。勝ち負けはどうでもいいけど、ダボーラの証明エンジンはどうせリリースされないよ。」
弟子「どういうことですか？」
ルデーゲ「私の証明エンジンが最良だとは言わないけど、誰が作っても実は大差ないんだ。ダボーラがほんとに証明エンジンを作ったとしても、証明も反証もできない命題が残るんだ。だから、また彼はウソを言っているのだろう。万が一、ホントだとしたら、その証明エンジンは取るに足らないものさ。」
弟子「先生、どうしてダボーラの“完璧な証明エンジン”がウソだってわかるんですか。」
ルデーゲ「あー、説明しようか。いや、その前に自分で考えてごらん。」

次の記事
全体目次＋総論