The Coq Proof Assistant A Tutorial (4) 自然演繹法
前回までは，何の説明も無く，いきなり intro や apply を使って，非常に初歩的な命題論理の証明を行ってみました．
# ちなみに，本職の Logician の方々が見たら噴飯モノの，訳語とか概念に関する間違いや誤解，曖昧さがゴロゴロしていると思いますが，あんまり修正とか見直しとかはしないで，とりあえずどんどん進んでいこうかと思います．その過程で段々理解が進んできて，誤解も訂正されていくと思うので．必要以上に過去は振り返らないで，未来だけを見つめて行きましょう ! (耳障りが良い常套句 ｗ)
# とはいえもちろん，ツッコミやコメントは大歓迎です (⌒▽⌒)
けっこういろいろやったので，復習としてコマンドをメモしておきます．
また，Logic Programming ってのは，ようするに，本来は無限の空間を対象 (量化の論理) にして，オブジェクト間の関係 (述語) を記述する 「一階述語論理」 という滅茶苦茶抽象的で高度な論理体系を，スコーレム化とかホーン節変換とかあの手この手を駆使してエンコードして，融合原理 (SLD 導出) を用いて計算機で扱える手続きとして解釈してしまおう，というアバンギャルドなパラダイムだということにも，ちょっち触れました．
んで，Logic の世界では，一見「そんなことやっちゃって大丈夫なの ?」って感じがするようなことがいっぱい行われているわけですが，そこはとりあえず，ロビンソンさんやエルブランさんコワルスキさんやロイドさんなど，過去の偉大な Logician を信じましょう．
もちろん，ええかげんなことをやっているわけではなく，エルブランの定理によって述語論理を命題論理に還元できるとか，いろいろな理論的バックグラウンドがちゃんとあるわけですが，そういうコ難しいことはまぁ，おいおいということで (^^;
とりあえず今回は，この Minimal Logic (最小論理) について，もう少し詳しく見ていきましょう．
前回は，かなり行き当たりばったり，人間の直感･洞察が入りまくりで証明を進めていきましたが，ここからはもう少し形式的 (機械的) なやり方を採用していきます．
そのような証明戦略として，最小論理の体系では，自然演繹と呼ばれる手法が知られてします．
以下のサイトを参考サイトとしてあげておきます．この記事は，あくまでも Coq の解説なので，私の説明はかなり端よったテキトーなものになります．というわけで，各自適宜参考にするように (なぜ，突然講義資料風口調 ｗ)．
論理学の孤独な散歩道
自然演繹（命題論理）まとめ
自然演繹の体系 Natural Deduction System, N-System (PDF)
VII. 自然演繹（その１）
# とはいえ，Coq の Tutorial の通りに進めていったのでは，Logic に慣れていない人は完全に置いてけぼりになってしまうと思うので，それよりは，もう少し丁寧にやっていくつもりです．あの Tutorial は，完全に読者が Logician であることを前提にしてますよね ｗ 私のようなパンピーにはあまり役に立ちません （；^ω^）
「自然」演繹法は，実際の数学者が証明を行うやり方にけっこう近い定式化であるため，人間にとって自然ですよ，という意味です．
# それに対して，ロビンソンの融合原理 (Resolution) に基づいた証明手法には，「Machine-Oriented」という形容詞が付きます．こっちは，計算機にとって「自然」な証明の定式化というニュアンスが込められています (とはいえ，むしろ Resolution の方が考えやすく，人間にもやさしい ！という御方もいます (ちなみに，日本の第五世代コンピュータ開発計画の中心言語であった，並列論理型言語 GHC/KL1 の設計者です)．)．
自然演繹の体系では，さまざまな推論規則を使用します．しかし，どれもこれも，ちょっと数学をかじったことがあれば，ピンとくるものばかりだと思います (これが，自然演繹が，「自然」たる所以です)．
それに，紙とペンの世界とは異なり，Coq の上で証明を行っている限り，正しくないものが証明されてしまう恐れは皆無です．男は度胸．何でも試していきましょう．そのための Coq です．
各推論規則には名前が付いています．とりあえず列挙すると…
の，12 規則からなる体系を，最小論理と呼びます．
# しかし… これだけでは証明できない命題がたくさんあるので，「矛盾からは何でも導き出せる (Ex Falso Sequitur Quodlibet)」 (⊥ から P) を加えたいところですが… いろいろと微妙な問題が発生してしまうらしいので，とりあえず放置 (良いのか ｗ)．
∨ 除去，→ 導入，¬導入のあたりは，言葉で書くと意味不明ですね (汗) 証明図などを書くべきなのでしょうが… HTML で書くのはなかなか大変なので，参考サイトを見てください (手抜き)
無理やり説明すると…
自然演繹では，これまで扱ってきたような「×× を仮定すると，この結論 (ゴール) が成り立つ」という通常の意味の「仮定」の他に，仮の仮定を用いて，意図的に矛盾を導き出し，仮定をキャンセルしていくという，独特のやり方で証明を進めていきます．
この概念は，「背理法 (帰謬法)」として有名ですね (あんまり難しいことは言いたくないのですが，これ (排中立) が使えない体系 (直観主義) もあるので，厳密には異なるのですが…)．仮の仮定を使用するときは，外人になった気分で
「まぁまぁ，あまり固いことをいわずに，とりあえず P を仮定してみよう (let) じゃないか．するとどうなる ? ワーオ矛盾が生じてしまった ! ならば ¬ P だ．QED」
などと考えて ﾆﾔﾆﾔ していると変な人だと思われるので，普通に淡々とやっていきましょう (笑)
つまり，自然演繹の規則は，いわゆる具体的な (コンピュータで処理 (パタンマッチ) しやすい) 推論「ルール」ではなく，図式なんですねぇ．
人間は，こういうのをパッパパッパと処理できるのですが，コンピュータにやらせるのは，けっこう面倒なんです．まさに「自然」演繹．
# より形式的 (図ではなく，記号列) に表現したい場合は，前提の集合を Γ (ガンマ) などと置き，論理式 P が，「構文的に」 Γ から導き出せるということを，Γ |- P などと書いたりします (HTML で Logic を説明するのは，無理があるような気が段々してきた…)．
# あと，よく，くるるさんや sumii 先生のような凄い人達が，「ここらへんは面倒なとこだからこの本 (論文) 読んでね ♡」 と言うのを見るたびに，「そな殺生なー，生殺しやー．わてがそんなん読んだってわからんちゅーねん」と思ってきたのですが (失礼)，自分でやってみると，その気持ちが痛いほどよくわかります (笑)
# ブログなどの，Web 上で説明できる程度の概念の濃度なんて，極めて限られたものなんだなぁと… 改めて思いました．やっぱり Web 上だけで勉強するのは無理があります (特に日本語)．ちょっとした本を読めば，一番最初の数ページに書いてあるような内容でさえも，Web 上にはほとんど無い場合も多いと思います…．ちょっと専門的な内容に関しては，未だにインターネットは空っぽの洞窟なのかもしれませんね．だいたいにして，google で Proof Assistant Coq を日本語で検索すると，この私のヘボヘボブログが一番に出てくるんですよ，奥さん ｗ
う〜ん，前置きが長くなりすぎた… しかも，書けば書くほど，細かい部分が気になって気になって，ドツボにはまる．説明下手すぎ．
# このブログの読者様が読みたいのは，Coq のチュートリアルであって，論理厨の箸にも棒にもかからないクソミソ説明ではないぞ ! > 自分 ｗ
私の ぁゃιぃ 説明を読んで，変な誤解をしたり，時間を無駄にするくらいならば，
情報科学における論理
論理学をつくる
などを読んだほうが，1000 倍くらいためになると思います (苦笑) シーケントとかも非常に詳しく，わかりやすいです．どこの図書館にもあると思う，この分野では定番中の定番の名著なので，ぜひ !
# プログラマの方ならば，論理学の本を読むとき，Coq を使って証明を行っていけば，より理解が深まるとともに，プログラミング気分で論理を学べるので，長続きして良いのではないかと思います．ここらへんの構成的な数学は，ほとんどプログラミングとやっていることは変わらないですから．
# とか言っておいてアレですが，私が読んだのはだいぶ昔で，しかもちゃんとその時にはちゃんと理解できなかったので… (記事のクオリティを見れば，「こいつ何もわかっちゃねーのにな ﾌﾟｹﾞﾗ」というのは一目瞭然でしょうが…) 頼りなくてすみません．Coq を触りつつ，チュートリアルを書きながら，私自身も再入門中なんです （ ´∀｀）
では，延々と脱線してしまいましたが，本題に入りましょう．
と思いましたが，今日 (金曜日) はちょっと忙しい日なので，この辺で (おぃ)．時間が無い… (；つд`)
明日もボスと個別ゼミですよ．土日祝日GWなんて飾りです．院生に休みなど無いのです (T∀T*)
# 休んでも良いけど，後で死ぬ (YｗY*)
# ていうか，私はともかく，ボスの健康と家庭生活が心配な今日この頃．働きすぎですよ… （；^ω^）
次回こそは，ちゃんと Coq でナチュラルリダクりますので，何卒ご勘弁を (>д<；)
# Coq のチュートリアルのはずなのに，Coq について触れないというありえなさ ｗ もう本当にすみません (*´-ェ-)
このペースで行くと，Coq で第二不完全性定理を証明できる日は，いったいいつになることやら (永遠に来ません ｗ)．
追記
Coq のチュートリアルについて書いている方がおられました．
nosi さんのはてな日記 - えぷりくす word=*[Coq]
しかも，私なんかよりも，はるかにしっかりしてます… orz
これで，このチュートリアルを書いてきた意味が 50 % ぐらい無くなりましたね (苦笑) こっちの方が，よっぽど参考になると思います (^-^;)
# ちなみに，本職の Logician の方々が見たら噴飯モノの，訳語とか概念に関する間違いや誤解，曖昧さがゴロゴロしていると思いますが，あんまり修正とか見直しとかはしないで，とりあえずどんどん進んでいこうかと思います．その過程で段々理解が進んできて，誤解も訂正されていくと思うので．必要以上に過去は振り返らないで，未来だけを見つめて行きましょう ! (耳障りが良い常套句 ｗ)
# とはいえもちろん，ツッコミやコメントは大歓迎です (⌒▽⌒)
けっこういろいろやったので，復習としてコマンドをメモしておきます．
- Quit.
- Coq の終了．
- Check 識別子.
- 識別子の型を調べる．
- Section Declaration.
- 宣言セクションに入る．
- Variable varname : type.
- type型の変数varname (複数可) を宣言する．
- Hypothesis 前提識別子 : 宣言内容.
- 前堤を宣言する．
- Definition 定義識別子 := 定義ボディ.
- 定義を宣言する．
- forall 変数識別子 : 型， exists 変数識別子 : 型
- 量化された変数を宣言する．
- Section Minimal_Logic.
- 「最小論理」推論エンジンに入る．
- Goal 仮説．
- 仮説を証明するための内部ループに入る．
- intro H.
- P → Q の形のゴールの，P の部分を仮定 H として judgement ※ に加える．
※ さかいさんからのコメントによる注釈によると， 「〜の仮定の元、ゴールの〜が成り立つという主張を表現したもの」のこと．感謝 !
- intros H1, H2 .... Hn.
- intro を複数まとめて実行．
- apply 仮定識別子.
- 現在のサブゴールを成り立たせるために必要な仮定を選択し，その仮定を成り立たせるために，もう一段深いループに入る．
- exact 仮定識別子．
- 仮定に基づき，自明に成り立つゴールを消去．
- assumption.
- ローカルな仮定から，ゴールが成り立つことを示された (終了)．
- Save (定理識別子).
- 証明を保存する．あらかじめ仮説 (予想) に名前が付いていた場合は，名前を入力する必要はない．
- Lemma 定理名 : 予想本体．
- 予想に名前を付け，証明ループに入る．
- T1 ; T2
- T1 を現在のゴールに apply し，それによって生じたサブゴール全てに T2 を apply．
- T ; [T1 | T2 | ..... |Tn]
- T を現在のゴールに apply し，それによって生じた n 番目のサブゴールに対して，それぞれ Tn を apply．
- auto.
- 証明をシステムに委ねる．
- Abort.
- 証明を中断．
- Undo (n).
- n ステップ戻る．
- Inspect n.
- 最後から数えて n 番目までの宣言を表示．
また，Logic Programming ってのは，ようするに，本来は無限の空間を対象 (量化の論理) にして，オブジェクト間の関係 (述語) を記述する 「一階述語論理」 という滅茶苦茶抽象的で高度な論理体系を，スコーレム化とかホーン節変換とかあの手この手を駆使してエンコードして，融合原理 (SLD 導出) を用いて計算機で扱える手続きとして解釈してしまおう，というアバンギャルドなパラダイムだということにも，ちょっち触れました．
んで，Logic の世界では，一見「そんなことやっちゃって大丈夫なの ?」って感じがするようなことがいっぱい行われているわけですが，そこはとりあえず，ロビンソンさんやエルブランさんコワルスキさんやロイドさんなど，過去の偉大な Logician を信じましょう．
もちろん，ええかげんなことをやっているわけではなく，エルブランの定理によって述語論理を命題論理に還元できるとか，いろいろな理論的バックグラウンドがちゃんとあるわけですが，そういうコ難しいことはまぁ，おいおいということで (^^;
とりあえず今回は，この Minimal Logic (最小論理) について，もう少し詳しく見ていきましょう．
前回は，かなり行き当たりばったり，人間の直感･洞察が入りまくりで証明を進めていきましたが，ここからはもう少し形式的 (機械的) なやり方を採用していきます．
そのような証明戦略として，最小論理の体系では，自然演繹と呼ばれる手法が知られてします．
以下のサイトを参考サイトとしてあげておきます．この記事は，あくまでも Coq の解説なので，私の説明はかなり端よったテキトーなものになります．というわけで，各自適宜参考にするように (なぜ，突然講義資料風口調 ｗ)．
論理学の孤独な散歩道
自然演繹（命題論理）まとめ
自然演繹の体系 Natural Deduction System, N-System (PDF)
VII. 自然演繹（その１）
# とはいえ，Coq の Tutorial の通りに進めていったのでは，Logic に慣れていない人は完全に置いてけぼりになってしまうと思うので，それよりは，もう少し丁寧にやっていくつもりです．あの Tutorial は，完全に読者が Logician であることを前提にしてますよね ｗ 私のようなパンピーにはあまり役に立ちません （；^ω^）
「自然」演繹法は，実際の数学者が証明を行うやり方にけっこう近い定式化であるため，人間にとって自然ですよ，という意味です．
# それに対して，ロビンソンの融合原理 (Resolution) に基づいた証明手法には，「Machine-Oriented」という形容詞が付きます．こっちは，計算機にとって「自然」な証明の定式化というニュアンスが込められています (とはいえ，むしろ Resolution の方が考えやすく，人間にもやさしい ！という御方もいます (ちなみに，日本の第五世代コンピュータ開発計画の中心言語であった，並列論理型言語 GHC/KL1 の設計者です)．)．
自然演繹の体系では，さまざまな推論規則を使用します．しかし，どれもこれも，ちょっと数学をかじったことがあれば，ピンとくるものばかりだと思います (これが，自然演繹が，「自然」たる所以です)．
それに，紙とペンの世界とは異なり，Coq の上で証明を行っている限り，正しくないものが証明されてしまう恐れは皆無です．男は度胸．何でも試していきましょう．そのための Coq です．
各推論規則には名前が付いています．とりあえず列挙すると…
- → 導入
- 「これまでの仮定の中」に A があって，仮定 B ならば， A を消去して A → B
- → 除去
- 仮定 A と 仮定 A → B から B
- ∧ 導入
- 仮定 A と 仮定 B から，A ∧ B
- ∧ 除去
- 仮定 A ∧ B から，A (あるいは B)
- ∨ 導入
- 仮定 A から A ∨ B (あるいは仮定 B から A ∨ B)
- ∨ 除去
- 仮定 A から C，かつ仮定 B から C ならば，A と Bを消去して，新たに仮定 A ∨ B から C
- ¬ 導入
- 仮定 A から ⊥（矛盾）ならば，A を消去して ¬A
- ¬ 除去
- A と ¬A から ⊥（矛盾）
の，12 規則からなる体系を，最小論理と呼びます．
# しかし… これだけでは証明できない命題がたくさんあるので，「矛盾からは何でも導き出せる (Ex Falso Sequitur Quodlibet)」 (⊥ から P) を加えたいところですが… いろいろと微妙な問題が発生してしまうらしいので，とりあえず放置 (良いのか ｗ)．
∨ 除去，→ 導入，¬導入のあたりは，言葉で書くと意味不明ですね (汗) 証明図などを書くべきなのでしょうが… HTML で書くのはなかなか大変なので，参考サイトを見てください (手抜き)
無理やり説明すると…
自然演繹では，これまで扱ってきたような「×× を仮定すると，この結論 (ゴール) が成り立つ」という通常の意味の「仮定」の他に，仮の仮定を用いて，意図的に矛盾を導き出し，仮定をキャンセルしていくという，独特のやり方で証明を進めていきます．
この概念は，「背理法 (帰謬法)」として有名ですね (あんまり難しいことは言いたくないのですが，これ (排中立) が使えない体系 (直観主義) もあるので，厳密には異なるのですが…)．仮の仮定を使用するときは，外人になった気分で
「まぁまぁ，あまり固いことをいわずに，とりあえず P を仮定してみよう (let) じゃないか．するとどうなる ? ワーオ矛盾が生じてしまった ! ならば ¬ P だ．QED」
などと考えて ﾆﾔﾆﾔ していると変な人だと思われるので，普通に淡々とやっていきましょう (笑)
つまり，自然演繹の規則は，いわゆる具体的な (コンピュータで処理 (パタンマッチ) しやすい) 推論「ルール」ではなく，図式なんですねぇ．
人間は，こういうのをパッパパッパと処理できるのですが，コンピュータにやらせるのは，けっこう面倒なんです．まさに「自然」演繹．
# より形式的 (図ではなく，記号列) に表現したい場合は，前提の集合を Γ (ガンマ) などと置き，論理式 P が，「構文的に」 Γ から導き出せるということを，Γ |- P などと書いたりします (HTML で Logic を説明するのは，無理があるような気が段々してきた…)．
# あと，よく，くるるさんや sumii 先生のような凄い人達が，「ここらへんは面倒なとこだからこの本 (論文) 読んでね ♡」 と言うのを見るたびに，「そな殺生なー，生殺しやー．わてがそんなん読んだってわからんちゅーねん」と思ってきたのですが (失礼)，自分でやってみると，その気持ちが痛いほどよくわかります (笑)
# ブログなどの，Web 上で説明できる程度の概念の濃度なんて，極めて限られたものなんだなぁと… 改めて思いました．やっぱり Web 上だけで勉強するのは無理があります (特に日本語)．ちょっとした本を読めば，一番最初の数ページに書いてあるような内容でさえも，Web 上にはほとんど無い場合も多いと思います…．ちょっと専門的な内容に関しては，未だにインターネットは空っぽの洞窟なのかもしれませんね．だいたいにして，google で Proof Assistant Coq を日本語で検索すると，この私のヘボヘボブログが一番に出てくるんですよ，奥さん ｗ
う〜ん，前置きが長くなりすぎた… しかも，書けば書くほど，細かい部分が気になって気になって，ドツボにはまる．説明下手すぎ．
# このブログの読者様が読みたいのは，Coq のチュートリアルであって，論理厨の箸にも棒にもかからないクソミソ説明ではないぞ ! > 自分 ｗ
私の ぁゃιぃ 説明を読んで，変な誤解をしたり，時間を無駄にするくらいならば，
情報科学における論理
論理学をつくる
などを読んだほうが，1000 倍くらいためになると思います (苦笑) シーケントとかも非常に詳しく，わかりやすいです．どこの図書館にもあると思う，この分野では定番中の定番の名著なので，ぜひ !
# プログラマの方ならば，論理学の本を読むとき，Coq を使って証明を行っていけば，より理解が深まるとともに，プログラミング気分で論理を学べるので，長続きして良いのではないかと思います．ここらへんの構成的な数学は，ほとんどプログラミングとやっていることは変わらないですから．
# とか言っておいてアレですが，私が読んだのはだいぶ昔で，しかもちゃんとその時にはちゃんと理解できなかったので… (記事のクオリティを見れば，「こいつ何もわかっちゃねーのにな ﾌﾟｹﾞﾗ」というのは一目瞭然でしょうが…) 頼りなくてすみません．Coq を触りつつ，チュートリアルを書きながら，私自身も再入門中なんです （ ´∀｀）
では，延々と脱線してしまいましたが，本題に入りましょう．
と思いましたが，今日 (金曜日) はちょっと忙しい日なので，この辺で (おぃ)．時間が無い… (；つд`)
明日もボスと個別ゼミですよ．土日祝日GWなんて飾りです．院生に休みなど無いのです (T∀T*)
# 休んでも良いけど，後で死ぬ (YｗY*)
# ていうか，私はともかく，ボスの健康と家庭生活が心配な今日この頃．働きすぎですよ… （；^ω^）
次回こそは，ちゃんと Coq でナチュラルリダクりますので，何卒ご勘弁を (>д<；)
# Coq のチュートリアルのはずなのに，Coq について触れないというありえなさ ｗ もう本当にすみません (*´-ェ-)
このペースで行くと，Coq で第二不完全性定理を証明できる日は，いったいいつになることやら (永遠に来ません ｗ)．
追記
Coq のチュートリアルについて書いている方がおられました．
nosi さんのはてな日記 - えぷりくす word=*[Coq]
しかも，私なんかよりも，はるかにしっかりしてます… orz
これで，このチュートリアルを書いてきた意味が 50 % ぐらい無くなりましたね (苦笑) こっちの方が，よっぽど参考になると思います (^-^;)
