More than 1 year has passed since last update.
概要
直観主義論理 と 古典主義論理 の違いは、<排中律> を公理として採用するか否かです。そして、採用する公理は<二重否定除去> でもよいとも知られています。
つまり、直感主義論理の導出関係において、<排中律>と<二重否定除去>は同値です。同様に<パースの法則> や ドモルガンの法則（のうちのひとつ）も同値な論理式です。
そこで、これら 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 風に書き下します:
DefinitionLEM:=forall(P:Prop),P\/~P.(* law of the excluded middle *)DefinitionDNE:=forall(P:Prop),~~P->P.(* double negation elemination *)DefinitionPEIRCE:=forall(PQ:Prop),((P->Q)->P)->P.(* law of Peirce *)DefinitionIMPCASE:=forall(PQ:Prop),(P->Q)->~P\/Q.DefinitionMORGAN4:=forall(PQ:Prop),~(~P/\~Q)->P\/Q.同値性の証明
以下のようないくつかの循環ができるので同値性の証明ができます
- 循環1:
LEM → DNE,DNE → MORGAN4,MORGAN4 → LEM - 循環2:
LEM → IMPCASE,IMPCASE → LEM - 循環3:
LEM-> PEIRCE,PEIRCE -> DNE, 1の循環を利用
上記の循環を意識して同値性の証明を記載しておきます:
DefinitionLEM:=forall(P:Prop),P\/~P.(* law of the excluded middle *)DefinitionDNE:=forall(P:Prop),~~P->P.(* double negation elemination *)DefinitionPEIRCE:=forall(PQ:Prop),((P->Q)->P)->P.(* law of Peirce *)DefinitionIMPCASE:=forall(PQ:Prop),(P->Q)->~P\/Q.DefinitionMORGAN4:=forall(PQ:Prop),~(~P/\~Q)->P\/Q.Lemmal_d:LEM->DNE.Proof.introslemPH.destruct(lemP).assumption.contradiction.Qed.Lemmad_m:DNE->MORGAN4.Proof.introsdnePQH.applydne.introsH1.applyH.split;intros?;applyH1;[left|right];assumption.Qed.Lemmam_l:MORGAN4->LEM.Proof.introsmorP.applymor.intros[H1H2].contradiction.Qed.Lemmai_l:IMPCASE->LEM.Proof.introsimpP.applyor_comm.applyimp.intros;assumption.Qed.Lemmal_i:LEM->IMPCASE.Proof.introslemPQH.destruct(lemP).right.applyH.assumption.left.assumption.Qed.Lemmap_d:PEIRCE->DNE.Proof.introsHPH1.applyHwith(Q:=False).intros.contradiction.Qed.Lemmal_p:LEM->PEIRCE.Proof.intros????.destruct(HP).assumption.applyH0.intros.contradiction.Qed.Theoremlem_dne_iff:LEM<->DNE.Proof.split.applyl_d.intros.apply(m_l(d_mH)).Qed.Theoremlem_peirce_iff:LEM<->PEIRCE.Proof.split.applyl_p.intros.apply(m_l(d_m(p_dH))).Qed.Theoremlem_impc_iff:LEM<->IMPCASE.Proof.split.applyl_i.applyi_l.Qed.Theoremlem_morgan4_iff:LEM<->MORGAN4.Proof.split.intros.apply(d_m(l_dH)).applym_l.Qed.参考文献
- Coq 標準ライブラリでの実装: lem -> その他の定理 の証明の参考にしました
- Software Foundations の練習問題 : 本稿はこの練習問題を少しアレンジしたものです
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme