« ケネディと天使の問題を Isabelle で証明 その2 気まぐれ天使問題 | トップページ

2020年6月22日 (月)

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

概要


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

これは「その3」で、気まぐれ天使問題について悪戦苦闘した私の「失敗」を扱う。
ブラックボックス登場


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

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

私はずっと以前、大学院にいたころ、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 表記法がいるってことは変数書き換えが必要なんだな…といったところから、「その2」に述べたような環境を変数に取ることを考えついた。

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


結論


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

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

(配布物・参考文献・ライセンス・更新の情報は「その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)

批評や挨拶のためのネットコミュニティ

  • はてなブックマーク(って何?) このエントリーをはてなブックマークに追加 このエントリーを含むはてなブックマーク このエントリーを含むはてなブックマーク
  • Twitter (って何?)

コメント

コメントを書く



(メールアドレス形式)


※匿名投稿を許可しています。ゆるめのコメント管理のポリシーを持っています。この記事にまったく関係のないコメントはこのリンク先で受け付けています。
※暗号化パスワードを設定すれば、後に「削除」、すなわち JavaScript で非表示に設定できます。暗号解読者を気にしないならメールアドレスでもかまいません。この設定は平文のメールで管理者に届きます。
※コメントを書くために漢字[かんじ]でルビが、[google: キーワード] で検索指定が使えます。


ランダムことわざ: 七転び八起き。