Hatena::Groupcoq

keigoiの日記

2010-08-29

「(AならばB) ⇔ (~A または B)」と直観主義論理

23:46

今日はCoq庵でした。演習の時間にやった証明でふと思い立ったので帰宅後にもCoqを触っています。

初等コンピュータサイエンスでは、論理結合子の「ならば」について、ざっくりと「A ならば B」は 「(not A) または B」 と同じだよーという感じの説明をすると思います(論理回路、離散数学、数理論理学etcetc)。で、真理値表を見て、ああそういう風に決まってるのね、とひとまず納得するんですが。

Coqでも確かめてみたいなと思い、次の2つの定理を書いてみた。

Theorem or_imply : forall P Q : Prop, ~P \/ Q -> P -> Q.
Theorem imply_or : forall P Q : Prop, (P -> Q) -> ~P \/ Q.

前者はごく平易に証明できた。

Coq < Theorem or_imply : forall P Q : Prop, ~P \/ Q -> P -> Q.
Proof.
intros.
case H.
 intro.
 contradiction .
 
 trivial.
Qed.

ところが後者((P -> Q) -> ~P \/ Q)はCoqの直観主義論理の世界では成立しないそうだ。 実際、証明のλ項を書き下そうとしてもP -> Q を関数と見立てた場合にPがないのでQが得られない。かといって~Pも証明できない。手詰まり。

(forall P Q, (P -> Q) -> ~P \/ Q) は古典論理でしか成立せず、排中律(forall P, ~P \/ P)と同値だそうです。なるほどそれはすごい。じゃそれを証明しよう。

Theorem exm_imply_or : (forall P : Prop, ~P \/ P) -> (forall P Q : Prop, (P -> Q) -> ~P \/ Q).
Theorem imply_or_exm : (forall P Q : Prop, (P -> Q) -> ~P \/ Q) -> (forall P : Prop, ~P \/ P).

前者は、古典論理の世界での forall P Q : Prop, (P -> Q) -> ~P \/ Q と同義です。後者はその逆。

Theorem exm_imply_or : (forall P : Prop, ~P \/ P) -> (forall P Q : Prop, (P -> Q) -> ~P \/ Q).
Proof.
intros.
case (H P).
 intro.
 left.
 apply H1.
 
 intro.
 right.
 apply (H0 H1).
Qed.

簡単です。

Theorem imply_or_exm : (forall P Q : Prop, (P -> Q) -> ~P \/ Q) -> (forall P : Prop, ~P \/ P).
Proof.
intros.
apply (H P P (fun x => x)).
Qed.

じゃ、直観主義論理における 「A ならば B」は 古典論理における 「~A または B」 のように ならば-free な形に書き換えられるのだろうか?

t6st6s2010/08/30 00:10直観主義だと∨∧¬→の内一つを他の3つで書くことは出来ないとhttp://www.amazon.co.jp/dp/4320016823のp.69にMcKinseyにattributeされて書かれています。がんばれば証明できるのでしょう

keigoikeigoi2010/08/30 00:34ありがとうです!そのようだね… wikipedia であれだけど、 http://en.wikipedia.org/wiki/Intuitionistic_logic#Non-interdefinability_of_operators