概要
直観主義論理 と 古典主義論理 の違いは、<排中律> を公理として採用するか否かです。そして、採用する公理は<二重否定除去> でもよいとも知られています。
つまり、直感主義論理の導出関係において、<排中律>と<二重否定除去>は同値です。同様に<パースの法則> や ドモルガンの法則（のうちのひとつ）も同値な論理式です。
そこで、これら 5つの論理式の同値性を Coq を使って示します。これにより 5つのうちどれか一つを公理とすれば、直観主義論理の証明能力を 古典論理のそれに匹敵させるのに十分である ことを示します。
なお、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.$ 含意の書き換え。識別子は
IMPCASE - $\lnot(\lnot P \land \lnot Q)\to P\lor Q.$ ドモルガン則の一例。識別子は
MORGAN4
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 IMPCASE := forall (P Q:Prop), (P -> Q) -> ~ P \/ Q.
Definition MORGAN4:= forall (P Q:Prop), ~(~P /\ ~Q) -> P\/Q.
同値性の証明
以下のようないくつかの循環ができるので同値性の証明ができます
- 循環1:
LEM → DNE,DNE → MORGAN4,MORGAN4 → LEM - 循環2:
LEM → IMPCASE,IMPCASE → LEM - 循環3:
LEM-> PEIRCE,PEIRCE -> DNE, 1の循環を利用
上記の循環を意識して同値性の証明を記載しておきます:
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 IMPCASE := forall (P Q:Prop), (P -> Q) -> ~ P \/ Q.
Definition MORGAN4:= forall (P Q:Prop), ~(~P /\ ~Q) -> P\/Q.
Lemma l_d: LEM -> DNE.
Proof. intros lem P H. destruct (lem P). assumption. contradiction. Qed.
Lemma d_m: DNE -> MORGAN4.
Proof. intros dne P Q H. apply dne. intros H1.
apply H. split;intros ?;apply H1;[left|right]; assumption. Qed.
Lemma m_l: MORGAN4->LEM.
Proof. intros mor P. apply mor. intros [H1 H2]. contradiction. Qed.
Lemma i_l: IMPCASE -> LEM.
Proof. intros imp P. apply or_comm. apply imp. intros; assumption. Qed.
Lemma l_i: LEM->IMPCASE.
Proof. intros lem P Q H. destruct (lem P). right. apply H. assumption.
left. assumption. Qed.
Lemma p_d: PEIRCE -> DNE.
Proof. intros H P H1. apply H with (Q:=False). intros. contradiction. Qed.
Lemma l_p: LEM-> PEIRCE.
Proof. intros ? ? ? ?. destruct (H P). assumption.
apply H0. intros. contradiction. Qed.
Theorem lem_dne_iff: LEM <->DNE.
Proof. split. apply l_d. intros. apply (m_l (d_m H)). Qed.
Theorem lem_peirce_iff : LEM <-> PEIRCE.
Proof. split. apply l_p. intros. apply (m_l (d_m (p_d H))). Qed.
Theorem lem_impc_iff: LEM <-> IMPCASE.
Proof. split. apply l_i. apply i_l. Qed.
Theorem lem_morgan4_iff: LEM <-> MORGAN4.
Proof. split. intros. apply (d_m (l_d H)). apply m_l. Qed.
参考文献
- Coq 標準ライブラリでの実装: lem -> その他の定理 の証明の参考にしました
- Software Foundations の練習問題 : 本稿はこの練習問題を少しアレンジしたものです