Coqで証明　二重否定周りの証明

二重否定導入

Goal forall a:Prop,a->~~a.
Proof.
intros.
intro.
apply H0.
assumption.
Qed.

二重否定除去は証明できないが、三重否定除去は証明できる

Goal forall a:Prop,~~~a->~a.
Proof.
intros.
intro.
apply H.
intro.
apply H1.
assumption.
Qed.

二重否定除去の二重否定

Goal forall a:Prop,~~(~~a->a).
Proof.
intros.
intro.
apply H.
intro.
exfalso.
apply H0.
intro.
apply H.
intro.
assumption.
Qed.

二重否定除去と排中律は同値
つまり、古典論理を得るには直観主義論理にどちらを加えてもいい

Goal (forall a:Prop,~~a->a)<->(forall a:Prop,a\/~a).
Proof.
split.
intros.
apply H.
intro.
apply H0.
right.
contradict H0.
left.
assumption.
intros.
specialize(H a).
destruct H.
assumption.
contradiction.
Qed.