ケネディと天使の問題を Isabelle で証明 その３ 悪戦苦闘編

■

概要

ケネディと天使の問題、または、うそつき天使問題、気まぐれ天使問題、三人の天使問題…と言われているものを、定理証明システム Isabelle でその答えが正しいかチェック(証明)した。

これは「その３」で、気まぐれ天使問題について悪戦苦闘した私の「失敗」を扱う。

■	ブラックボックス登場

野崎昭弘『詭弁論理学』(中公新書)の p.14-16, 148-154 に、「ケネディの問題」があり、その「うそつき天使」問題を「その１」で、「気まぐれ天使」問題を「その２」で説明した。

さて、スターリンが登場した「気まぐれ天使」問題を記号論理で解くには紆余曲折があった。

私はずっと以前、大学院にいたころ、PTS (Pure Type System) にブラックボックス ■ を導入することを考えたことがある。

ある P の証明 p があるとき、Γ |- p : P となるのだが、このとき p は何でも良いので、Γ |- ■ : P と書くとする。そして、Γ |- (λx:A. ■) : (Π x:A. P) となったとしたら、これも Γ |- ■: (Π x:A. P) と書き換えてよいとする。結果 (λx. ■) = ■、■(f) = ■ などとしていくわけである。

結果、■ はなんだかわらかないがとにかくそこにある「ブラックボックス」を表す。こういうのを導入してもいいはずだ…と考えていた。

今回のスターリンはまさに、■ だ！ というのが最初の直感だった。しかし、問題が出てくる。B がスターリンかどうかを尋ねるというのが解答に出てくるが、それは B が ■ かどうかを問うということ。これが難しいのだ。

■	ホワイトボックス登場

ある x が ■ なら真となる関数を □(x) と定義しよう。簡単に □x と書く。

ところが、■というのは「メタレベル」の話であって、それを判定する□はメタに判定しなければならないのに、それを地のロジックで使うとなれば、当然に矛盾が出てくる。

つまり、Γ |- a: B とすると、Γ |- ■: B ということだった。今、□ で判定できるということだから、Γ |- ■ : ¬□ a、Γ |- ■ : □ ■ でなければならないということになる。

Γ = Δ, a: B だったとすると、Δ |- ■: (Π a:B. ¬□ a) になるが、Γ |- ■: B だったから Γ |- ■■: ¬□ ■ で、これは Γ |- ■: ¬□ ■ になる。これは Γ |- ■ : □ ■ と矛盾する。

■	矛盾を生じないようにするには？

矛盾を生じないようにするにはどうすればよいのだろうか？

問題は、¬□ a の a に ■ を代入するときに起きていると考えれば、de Bruijn 表記法のようなものを □ ■ に導入することが考えられる。

つまり、□ = □_0、 ■ = ■_0 だったとして、□_0 a の a に ■_0 代入しようと思えば 0 がぶつかるため、■ の数値を増やさねばならない。よって、¬ □_0 a [a:= ■_0] = ¬ □_0 ■_1 と考え、これは ¬ □_0 ■_0 とは別のものと考えるのである。

…ただ、これが、ちゃんと無矛盾なロジックになっているかは、確認していない。

■

スマートな方法

ここまで考えたところで、de Bruijn 表記法がいるってことは変数書き換えが必要なんだな…といったところから、「その２」に述べたような環境を変数に取ることを考えついた。

逆に言えば、■ は、環境を変数に扱うような意味論で定式化できるのかもしれない…と直感的には思う。上で見るようにあてにならない直感だが。

■

結論

昔考えた「ブラックボックス」が正しかったのかさえ、疑問に思うようになった。

ここまで読んでいただきありがとうございます。

(配布物・参考文献・ライセンス・更新の情報は「その１」にあります。)

更新：	2020-06-22
初公開：	2020年06月22日 08:10:45
最新版：	2020年06月23日 00:15:09