ケネディと天使の問題を Isabelle で証明 その3 悪戦苦闘編
■ |
概要
|
ケネディと天使の問題、または、うそつき天使問題、気まぐれ天使問題、三人の天使問題…と言われているものを、定理証明システム Isabelle でその答えが正しいかチェック(証明)した。
これは「その3」で、気まぐれ天使問題について悪戦苦闘した私の「失敗」を扱う。
■ |
ブラックボックス登場
|
さて、スターリンが登場した「気まぐれ天使」問題を記号論理で解くには紆余曲折があった。
ある 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 だったから Γ |- ■■: ¬□ ■ で、これは Γ |- ■: ¬□ ■ になる。これは Γ |- ■ : □ ■ と矛盾する。
■ |
矛盾を生じないようにするには?
|
矛盾を生じないようにするにはどうすればよいのだろうか?
つまり、□ = □_0、 ■ = ■_0 だったとして、□_0 a の a に ■_0 代入しようと思えば 0 がぶつかるため、■ の数値を増やさねばならない。よって、¬ □_0 a [a:= ■_0] = ¬ □_0 ■_1 と考え、これは ¬ □_0 ■_0 とは別のものと考えるのである。
…ただ、これが、ちゃんと無矛盾なロジックになっているかは、確認していない。
■ |
スマートな方法
|
逆に言えば、■ は、環境を変数に扱うような意味論で定式化できるのかもしれない…と直感的には思う。上で見るようにあてにならない直感だが。
■ |
結論
|
昔考えた「ブラックボックス」が正しかったのかさえ、疑問に思うようになった。
ここまで読んでいただきありがとうございます。
(配布物・参考文献・ライセンス・更新の情報は「その1」にあります。)
更新: | 2020-06-22 |
初公開: | 2020年06月22日 08:10:45 |
最新版: | 2020年06月23日 00:15:09 |
2020-06-22 08:10:47 (JST) in 関数型言語・定理証明器 | 固定リンク | コメント (0)
コメント