Coqで証明　排中律周辺の命題

古典論理では~a∨bとa->bは同値だが直観主義論理では片方の->しか証明できない。

Goal forall a b,~a\/b->a->b.
Proof.
intros.
case H.
intro.
contradiction.
trivial.
Qed.

逆向きの->はある種の排中律の一般化になっている

Definition 排中律:=forall a:Prop,a\/~a.

Definition 一般排中律:=forall a b:Prop,(a->b)->~a\/b.

Goal 一般排中律->排中律.
Proof.
intros H a.
case(H a a).
trivial.
right.
assumption.
left.
assumption.
Qed.

逆に排中律から一般排中律を導くこともできる。

Goal 排中律->一般排中律.
Proof.
intros H a b H0.
case(H a).
right.
exact(H0 H1).
left.
assumption.
Qed.

排中律の一般化として次のような命題もある。（ちなみにこの命題はTwitterで話題になってたの見て知りました。）

Definition 一般排中律':=forall a b c:Prop,(a->b)\/(b->c).

Goal 一般排中律'->排中律.
Proof.
intros H a.
case(H True a False).
left.
apply H0.
split.
right.
assumption.
Qed.

これも排中律と同値。

Goal 排中律->一般排中律'.
Proof.
intros H a b c.
case(H b).
left.
trivial.
right.
intro.
contradiction.
Qed.

パースの法則も排中律と同値の命題として有名。（Twitterの名前に入れてる大学の先生がいる。）

Definition パース:=forall a b:Prop,((a->b)->a)->a.

Goal 排中律<->パース.
Proof.
split.
intros H a b H0.
case(H a).
trivial.
intro.
apply H0.
intro.
contradiction.
intros H a.
apply(H(a\/~a)(~a)).
intro.
right.
intro.
case H0.
left.
assumption.
assumption.
Qed.

・排中律と同値な命題で他に有名なやつがあったら知りたい。
・ある命題が排中律と同値であるか判定する方法はある？