読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

直観主義論理での二重否定除去と排中律の同値性

同値性を示すためにそれぞれの矢印を示した。論理パズルみたいな問題だが、¬を扱ういい練習問題だと思う。

Lemma p10_left :
  (forall A, ~~A -> A) -> (forall A B, (~B -> ~A) -> (A -> B)).
Proof.
intros.
apply H.
intro.
elim (H0 H2).
apply H1.
Qed.

Lemma p10_right :
  (forall A B, (~B -> ~A) -> (A -> B)) -> (forall A, ~~A -> A).
Proof.
intros.
apply (H True A).
 intro.
   intro.
   elim H0.
   apply H1.
apply I.
Qed.