Agdaを使って論理証明1

　前回の続き。論理式をAgdaで証明していくのですが、実際にコードを書く前に論理式とはどうやって証明すればいいかのお話。

推論規則

　論証の妥当性を示すのに用いられる規則を推論規則と呼ぶ。以下は推論規則をを用いて論証の妥当性を示すための規則である。

->除去則について

->除去則とは次の性質を持つ規則。『 -> 』 とは 『ならば』のこと。

前提条件 A と 前提条件 A -> B が成り立つとき、Bを導いても良い

　考えれば当然のことである。具体的な例を用意してみる。Aを『水が存在する』Bを『生命が存在する』とする。
前提条件の A と A -> B が成り立つとは『水が存在し、水が存在するならば生命が存在するが成り立っている』と言い換えられる。ここから 『生命が存在する』 つまり B と求められるのは当然のことである。

　図っぽく描くと次のようになる

　　　　A　　A -> B
　　　---------------- -> E
　　　　　　B

　A , A -> B の二つが成り立っていればBを導ける。上で書いたことの反復になるがつまりそういうことである。

->導入則について

今度は逆に -> を導入してみる。-> とは次のこと。

A を仮定してその仮定のもとで B が導かれるとき、（Aという仮定無しで）A -> B を導くことができる。

　　　　　
ここはちょっと分かりづらいかもしれない。というわけでここも例題を上げる。

　　　前提条件 A -> B , 前提条件 B -> C があるとき A -> C が成り立つ

という命題があるとする。ここで A を 『水が存在する』, B を『生命が存在する』, C を 『食物連鎖がある』 とする。そのとき前提条件 A -> B は 『水が存在するなら生命が存在する』, 前提条件 B -> C は 『生命が存在するなら食物連鎖がある』、証明する A -> C は『水が存在するなら食物連鎖がある』となる。

　ではここで A を『仮定』してみよう。A と A -> B を 『->除去則』により B を証明できる（水が存在し、水が存在するばらば生命が存在する、つまり生命は存在する）。その B と B -> C を同様にして C が証明できる（生命が存在する、生命が存在するならば食物連鎖がある、つまり食物連鎖はある）。

　ここで A を仮定したことで、Cを導くことができた。つまりこれは A という仮定無しで A -> C (水が存在するならば食物連鎖がある)を導くことができる。ということになる。

これも同様に図っぽく描いてみる

　　　　　　[A]
　　--------------------
　　　　A　　　A -> B
　　---------------------- ->E
　　　　B　　　B -> C
　　---------------------- ->E
　　　　　　C
　　---------------------- ->I
　　　　　A -> C

　とりあえず今回はここまで。次は∧除去則、∧導入則の話です