#背理法を絶対に認めない人たちの会
背理法ってありますよね。高校あたりで習ったような気がする。
Pでないと仮定する。そしたら、矛盾が生じた。
矛盾が生じたのは、Pでないと仮定したからだ。
なのでPである。
……いいんじゃないでしょうか。何が問題なんでしょうか?
ここで言っているのは、
"「Pではない」ではないならば、Pである"
つまり、否定を~で表すと「~~PならばP」だと言ってます。
……何か問題が?
けどこれ「二重否定の除去」といって、成り立つことが示せないんですよ。
いやいや、そんなはずはない。Pは真か偽かのどちらかなのだから、
Pが真ならば「~~PならばP」は真。
Pが偽ならば、~Pは真で~~Pは偽になるので「~~PならばP」は前提が偽なので真。
証明できるじゃないですか。
実は、「Pが真か偽かどちらか」というのが、二重否定の除去と等価な命題として知られています。
「排中律」と呼ばれる命題ですが、これもやはり、成り立つかどうかは示せないんです。
……ということで、排中律や二重否定の除去を決して認めない、背理法を認めない人たちがいます。
彼らの論理を、直観主義論理と呼びます。この論理はラムダ計算と等価であることも知られています。
一方で「Pが真か偽かどちらか」という、直観主義論理の立場からは決して導けないものを、
真であると信じ込む人たちの論理を、古典論理と呼びます。
古典論理では、二重否定の除去や、背理法も、何の問題もなく使うことができます。
ちなみに
Pであると仮定する。そしたら矛盾が生じた。
矛盾が生じたのは、Pであると仮定したからだ。
なのでPでない。(つまり~Pである)
この議論は、問題ありません。
P->Falseを~Pと同値とみなすのは、否定~の定義そのものです。
どう違うのか。P = ~Qを代入してみましょう。
~Qであると仮定する。そしたら矛盾が生じた。
矛盾が生じたのは、~Qであると仮定したからだ。
なので~Qでない。(つまり~~Qである)
ここで示されたのは、Qではなく~~Qです。
~~Qであることを示すには、これで問題ありません。
ですが「~~QだからQだ」と言うには、二重否定の除去が必要です。
パースの法則
排中律や二重否定の除去と等価な命題のひとつで、変なものとして、パースの法則があります。
任意の命題P, Qについて、
((P→Q)→P)→P
が成り立つ
『「PならばQ」ならばP』ならばP
なんか、パズルのような命題ですね。
さっぱりわけわからないですが。排中律を使って、つまり、Pが真の場合と偽の場合に場合分けすることで、これが成り立つことを示すことができます。
Pが真の場合、"『「PならばQ」ならばP』ならばP"は当然、真です。
Pが偽の場合、「PならばQ」は前提が偽なので真です。
"『「PならばQ」ならばP』ならばP"は"『「真」ならばP』ならばP"と書き換えられます。
さらに『「真」ならばP』は、つまり『P』ということなので"PならばP"と書き換えられます。これは真です。
(トートロジーだと考えることもできますし、前提が偽だから真と考えることもできます)
さて、これら3つが等価であることを形式的に示していきましょう。
Coqで示す
まずは、排中律、二重否定の除去、パースの法則を定義していきましょう。
ここでいう「定義」とは、命題に名前をつけることを言っていて、成り立つかどうかについては言っていません。
証明を付けて成り立つことを示す(この場合不可能です)にはTheoremを、証明なしに成り立つことにするにはAxiomなどを使います。
(* Law of Excluded Middle *)
Definition LEM : Prop :=
forall (P: Prop), P \/ ~P.
(* Double Negation Elimination *)
Definition DNE : Prop :=
forall (P: Prop), ~~P -> P.
(* Peirce's law *)
Definition Peirce : Prop :=
forall (P Q: Prop), ((P->Q)->P)->P.
続いて、これらがすべて等価であることを示します。
A, Bの2つの命題が等価であることを示すには、A -> BとB -> Aの両方を示します。
さらにCも等価であることを示すには、
-
A -> CかB -> Cのどちらか -
C -> AかC -> Bのどちらか
の両方を示すことが必要十分です。
(A -> CとB -> Cの両方を示す必要がある、と思う方もいるかもしれませんが、
例えばB -> Cを示せば、A -> Bは示されているので、A -> Cもいえます。他も同様です。)
なお、Coqには (A -> B) /\ (B -> A)を意味するA <-> Bという構文もありますが、どうせ分けて両方証明しなければいけないので、今回は1個ずつ証明していきます。
排中律が成り立てば、二重否定の除去も成り立つ
Theorem LEM_DNE :
LEM -> DNE.
Proof.
unfold LEM; unfold DNE.
intros LEM P nnp.
destruct (LEM P).
- assumption.
- destruct nnp.
assumption.
Qed.
~~P -> Pを示すために、排中律を使ってPを場合分けしています。
destruct (LEM P).の部分です。
Pの場合: ~~P -> Pは明らか
~Pの場合: ~~Pかつ~Pならば、Pであることを示したい。前提が偽であるのでそれが言える
二重否定の除去が成り立てば排中律が成り立つ
Theorem DNE_LEM :
DNE -> LEM.
Proof.
unfold LEM; unfold DNE.
intros LEM P.
apply LEM.
intros H.
apply H.
right.
intros p.
apply H.
left.
assumption.
Qed.
これは、割と面倒くさい証明です。
unfold LEM; unfold DNE.
までを見ると、
1 subgoal
LEM : forall P : Prop, ~ ~ P -> P
P : Prop
______________________________________(1/1)
P \/ ~ P
となっています。さらに
apply LEM.
intros H.
apply H.
が続くと、
1 subgoal
LEM : forall P : Prop, ~ ~ P -> P
P : Prop
H : ~ (P \/ ~ P)
______________________________________(1/1)
P \/ ~ P
となります。
示すべきことは何も変わっていないのですが、H : ~ (P \/ ~ P)という仮定が増えています。
命題Aを示すために、二重否定の除去を使うと~Aを仮定してもよくなる、というのは、確かに排中律っぽさがありますね。
ここからも、結構面倒くさい証明なんですが「排中律の悪魔」を知っていると面白いです。
昔々、悪魔が男のもとにきて言った。
「(a) 君に10億ドルあげるか、(b) もし君が10億ドルくれたらどんな願いでも叶えてあげよう。ただし、(a)か(b)のどちらを提示するかはおれが決める」
男は用心深く、魂を明け渡す必要があるか確認した。「いいや、君がする必要があるのは申し出を受け入れることだけだ」と悪魔は答えた。
男は考えた。もし(b)を提示された場合、願いを買うことはとてもできないが、しかしこのチャンスを利用したところで何か害があるわけでもない。結局、男は「受け入れます」と答えた。「それで(a)なのか？(b)なのか？」
悪魔は少し考えて「(b)だな」と答えた。
男は失望したが、驚くことはなかった。それはそうだと思った。しかしどんな願いでも叶えられるという申し出は男を蝕んだ。それから男は何年もお金を貯め始めた。時には悪いこともした。そしてそれこそが悪魔の狙いだったんだろうとぼんやりと思った。やがて男は10億ドルを手にし、そして悪魔が再び男の前に現れた。
「ここに10億ドルある」そう言って男はお金を手渡した。「願いを叶えてくれ！」
悪魔はお金を手に取り、男に言った、「あれ、おれは前に(b)なんて言ったっけ？ごめん、(a)のつもりだったんだ。君に10億ドルあげれてとても嬉しいよ」そういって悪魔は、今受け取ったお金をそのまま男へ返した。
---- Call-by-Value is Dual to Call-by-Name, Philip Wadler
引用元: Haskellの型と直観論理
はぁ? 何いってんだ?
今から示すべきことは、P \/ ~ Pでした。
1 subgoal
LEM : forall P : Prop, ~ ~ P -> P
P : Prop
H : ~ (P \/ ~ P)
______________________________________(1/1)
P \/ ~ P
「Pまたは~P」なので、Pか~Pか、どちらか好きな方を示せばいいことになります。
right.によって、右側の~Pを示すことにします。悪魔が「10億ドルくれたら願いを叶える」を選んだことに対応します。
intros p. apply H. によって、仮定にPを加えて、再び「Pまたは~P」に戻ってきます。
少し分かりにくいのですが。 ~P は、論理学では P -> Falseを意味します。
なのでintros p.は「Pを仮定してFalseを示そう」と言っていることになります。
同じくH: ~(P \/ ~P)は、H: (P \/ ~P) -> Falseを意味します。
apply H.によって「(P \/ ~P)を示すことでFalseを示す」と言っていることになります。
このようになりました。
1 subgoal
LEM : forall P : Prop, ~ ~ P -> P
P : Prop
H : ~ (P \/ ~ P)
p : P
______________________________________(1/1)
P \/ ~ P
なお、Pが仮定に加わったことは、男が10億ドルをがんばって稼いだことに対応します。
再びP \/ ~ Pの悪魔に出会いました。
そこから left. assumption. と続きます。
つまり、悪魔が今度は手のひら返しして「いや、10億ドル渡すと言った」と言います。
確かにそこには10億ドル(仮定p)があって、悪魔は約束を果たしたので、証明終了です。
排中律からパースの法則を導く
Theorem LEM_Peirce :
LEM -> Peirce.
Proof.
unfold LEM; unfold Peirce.
intros LEM P Q pq_p.
destruct (LEM P).
- assumption.
- apply pq_p.
intros p.
destruct H.
assumption.
Qed.
この証明は結構簡単です。
排中律を使って、Pを場合分けしています。
Pならば: パースの法則 ((P -> Q) -> P) -> Pは当然成り立ちます。
~Pならば:
~Pと((P->Q)->P)を仮定したとき、Pが成り立つことを示します。
仮定よりP->Qを示せばPが示せるので、これを示します。
P->Qを示すには、Pであることを仮定してQを示します。
Pという仮定と~Pという仮定がありますが、これは矛盾しているので、証明終了です。
パースの法則から排中律を導く
Theorem Peirce_LEM :
Peirce -> LEM.
Proof.
unfold Peirce; unfold LEM.
intros Peirce P.
apply (Peirce _ (~P)); intros.
right; intros p.
apply H.
left; assumption.
assumption.
Qed.
P, Qばかり出てきてややこしいので、この節では、パースの定理を ((A -> B) -> A) -> A と読み替えましょう。
A = P \/ ~P (排中律。これを導きたい)
B = ~P
を代入すると
(((P \/ ~P) -> ~P) -> (P \/ ~P)) -> (P \/ ~P)
になります。排中律、ややこしいのでLEMと書きましょう。
((LEM -> ~P) -> LEM) -> LEM
を使って、LEMを示します。
そのためには、
(LEM -> ~P) -> LEM
を示せばいい、つまり、
LEM -> ~Pを仮定してLEMを示せばいいことが分かります。
1 subgoal
Peirce : forall P Q : Prop,
((P -> Q) -> P) -> P
P : Prop
H : P \/ ~ P -> ~ P
______________________________________(1/1)
P \/ ~ P
以前の証明でも出てきましたが、仮定が増えた状態で元に戻ってきています。
さて、right.によって、~Pを示します。
~PはP -> Falseなので、Pを仮定してFalseを示します。
H : P \/ ~ P -> ~ P の末尾の~Pに注目すると
H : P \/ ~ P -> P -> False と同じ意味であることがわかります。
つまりP \/ ~ PとPを示せばいいことになります。
仮定にPがありますので、どちらもすぐに示せます。これで証明終了です。
まとめ
今回、排中律、二重否定の除去、パースの法則がそれぞれ等価であることを示してみました。
どれも、たらい回しにして、堂々巡りしているように見えて、何か仮定が増えているという不思議な感覚があります。