直観主義論理 五つの定理の同値性

概要

直観主義論理 と 古典主義論理 の違いは <排中律> を公理として採用するか否かであると言われています。一方、<二重否定除去> を <排中律> の代わりに公理にしてもよいとも知られています。

そこで、<排中律> を含めた 5つの論理式の同値性を Coq を使って示します。つまり 5つのうちどれか一つを公理とすれば、直観主義論理の証明能力を 古典論理のそれに匹敵させるのに十分である ことを示します。（注：ここでの同値性とは、直観主義論理における導出関係 $\vdash_{\bf IL}$ における同値性です）

なお、Coq の標準ライブラリでは <排中律> を公理として、それ以外の論理式を証明しています。

• 参考: Coq 標準ライブラリでの実装

5つの論理式

5つの論理式を記載し、Coq上で扱う際の名前を付けます:

• $P \lor \lnot P.$ 排中律。識別子はlem。
• $\lnot\lnot P\to P.$二重否定除去。識別子は dne。
• $((P\to Q)\to P)\to P.$ パースの法則。識別子は peirce。
• $(P\to Q)\to\lnot P \lor Q.$ 含意の書き換え。識別子は imply_cases。
• $\lnot(\lnot P \land \lnot Q)\to P\lor Q.$ ドモルガン則の一例。識別子は morgan

5つのチョイスは Software Foundation の練習問題からです（が、さらに Coq'Art がその元ネタだそうです）。

Coq 風に書き下します:

Definition lem := forall (P:Prop), P \/ ~ P. (* law of the excluded middle *)
Definition dne := forall (P:Prop), ~ ~ P -> P. (* double negation elemination *)
Definition peirce := forall (P Q:Prop), ((P -> Q) -> P) -> P. (* law of Peirce *)
Definition imply_cases := forall (P Q:Prop), (P -> Q) -> ~ P \/ Q.
Definition morgan:= forall (P Q:Prop), ~(~P /\ ~Q) -> P\/Q.

同値性の証明

同値性の証明を記載します。Coqに通ることが重要で、具体的な証明図は重要ではありません（気になれば Show Proof 等で確認してみてください）:

Goal lem <-> dne.
Proof. split. 
- intros H P. elim (H P). + tauto. + tauto.
- intros H P. apply H. tauto. Qed.

Goal lem <-> peirce.
Proof. split.
- intros H P Q. elim (H P). + tauto. + tauto.
- intros H P. apply (H (P\/~P) False). tauto. Qed.

Goal lem <-> imply_cases.
Proof. split.
- intros H P. elim (H P). + tauto. + tauto.
- intros H P. assert (X: ~P\/P -> P\/~P). { tauto. } apply X. apply (H P P). tauto. Qed.

Goal lem  <-> morgan.
Proof. split.
- intros H P Q. elim (H (P \/ Q)). + tauto. + intros. exfalso. apply H1. tauto.
- intros H P. apply (H P (~P)). tauto. Qed.

参考文献

• Coq 標準ライブラリでの実装: lem -> その他の定理 の証明の参考にしました
• Software Foundations の練習問題 : 本稿はこの練習問題を少しアレンジしたものです

コード

tauto を使わないでやった証明を載せておきます。直観主義論理でも証明できる定理＜排中律の二重否定＞をよく使うので補助定理として最初に証明しています:

Module ILogicTest.
Definition lem := forall (P:Prop), P \/ ~ P. (* law of the excluded middle *)
Definition dne := forall (P:Prop), ~ ~ P -> P. (* double negation elemination *)
Definition peirce := forall (P Q:Prop), ((P -> Q) -> P) -> P.
Definition imply_cases := forall (P Q:Prop), (P -> Q) -> ~ P \/ Q.
Definition morgan:= forall (P Q:Prop), ~(~P /\ ~Q) -> P\/Q.

Theorem dnlem: forall (P:Prop), ~ ~ (P \/ ~ P).
Proof. intros. intro. apply H. right. intro. apply H. left. trivial. Qed.

Goal lem <-> dne.
Proof. split. 
- intros H P. destruct (H P). + trivial. + intro. contradiction.
- intros H P. apply H. apply dnlem. Qed.

Goal lem <-> peirce.
Proof. split.
- intros C P Q H. destruct (C P). + trivial. + apply H. intro. contradiction.
- intros H P. apply (H (P\/~P) False). intro. apply dnlem in H0. contradiction. Qed.

Goal lem <-> imply_cases.
Proof. split.
- intros H P Q H0. destruct (H P). + right. apply H0. trivial. + left. trivial.
- intros H P. assert (X: ~P \/ P -> P\/~P). { tauto. } apply X. apply (H P P). intro. trivial. Qed.

Goal lem  <-> morgan.
Proof. split.
- unfold morgan. intros. destruct (H (P \/ Q)).
 + trivial.
 + exfalso. apply H0. split. { intro. apply H1. left. trivial. } { intro. apply H1. right. trivial. }
- unfold lem. intros. apply (H P (~P)). intro. destruct H0. contradiction.
Qed.

End ILogicTest.