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

概要 直観主義論理 と 古典主義論理 の違いは、<排中律> を公理として採用するか否かです。そして、採用する公理は<二重否定除去> でもよいとも知られています。 つまり、直感主義論理の導出関係において、<排中律>と<二重否定除去>は同値です。同様に<パースの法則> や ドモルガンの法則（のうちのひとつ）も同値な論理式です。 そこで、これら 5つの論理式の同値性を Coq を使って示します。これにより 5つのうちどれか一つを公理とすれば、直観主義論理の証明能力を 古典論理のそれに匹敵させるのに十分である ことを示します。 なお、Coq の標準ライブラリでは <排中律> を公理として、それ以外の論理式を証明しています。 参考: Coq 標準ライブラリでの実装 5つの論理式 5つの論理式を記載し、Coq上で扱う際の名前を付けます: $P \lor \lnot P.$ 排中律。識別子はLEM $\