今回は、直観主義論理＋外延性公理,分出公理図式,対公理だけで次の2つが同値になることをCoqで示します。
・排中律
・互いに素な空でない集合族{ $a,b$ }から要素を選べる
　（2点集合についての選択集合の存在）
おまけで選択公理⇒排中律を示します。
（なんでや！無限集合関係ないやろ！）
(*
このプログラムは外延性公理,分出公理図式,対公理のみで
排中律と弱い選択公理が同値になることを一から証明しています。
系として選択公理->排中律を示しています。

予備知識はCoqの使い方だけと思います。
他のライブラリは必要ありません。
*)

(*関係記号∈*)
Axiom In : Set -> Set -> Prop.

(*集合の存在*) (*一階述語論理では定理*)
Axiom Ax_Exists : exists x : Set, x = x.

(*外延性公理/axiom of extensionality*)
Axiom Ax_Ex : forall x y : Set, (forall z : Set, In z x <-> In z y) -> x = y.

(*分出公理図式/axiom schema of separation*)
Axiom Ax_S_S : forall (P : Set -> Prop)(x : Set),
 exists y, forall z : Set, In z y <-> In z x /\ P z.

(*対公理/axiom of pairing*)
Axiom Ax_Pairing : forall a b : Set,
 exists p, forall z : Set, In z p <-> z = a \/ z = b.


(*選択公理/axiom of choice(選択集合の存在)*)
Definition AC_Set := forall a : Set,
 (forall x : Set, In x a -> exists w, In w x) ->
 (forall x y z : Set, In x a -> In y a -> In z x -> In z y -> x = y) ->
 exists c, forall x : Set, In x a -> exists! y, In y c /\ In y x.

(*2点集合についての選択公理(選択集合の存在)*)
Definition AC_Set_2 := forall v w a b : Set,
 In v a -> In w b -> (forall z : Set, In z a -> In z b -> a = b) ->
 exists c, (exists ! y, In y c /\ In y a) /\ (exists ! y, In y c /\ In y b).


(*選択公理->二点集合についての選択公理*)
Theorem AC_Set_AC_Set_2 : AC_Set -> AC_Set_2.
Proof.
unfold AC_Set_2.
intros.
destruct (Ax_Pairing a b). (*対*)
destruct (H x).

intros.
apply H3 in H4.
destruct H4.
rewrite H4.
exists v.
apply H0.
rewrite H4.
exists w.
apply H1.

intros.
apply H3 in H4.
apply H3 in H5.
destruct H4.
destruct H4.
destruct H5.
symmetry.
apply H4.
destruct H4.
apply (H2 z H6 H7).
destruct H4.
destruct H5.
destruct H4.
symmetry.
apply (H2 z H7 H6).
symmetry.
destruct H4.
split.

exists x0.
split.
apply H4.
apply H3.
left.
split.
apply H4.
apply H3.
right.
split.
Qed.


(*排中律<->2点集合に対する選択公理*)
Theorem Middle_Iff_AC_Set_2 : (forall P : Prop, P \/ ~P) <-> AC_Set_2.
Proof.
split.
unfold AC_Set_2.
intros.
destruct (H (exists z, In z a /\ In z b)).
destruct H3.
rewrite <- (H2 x).
destruct (Ax_Pairing v v). (*対*)
exists x0.
assert (exists ! y : Set, In y x0 /\ In y a).
exists v.
split.
split.
apply H4.
left.
split.
apply H0.
intros.
destruct H5.
apply H4 in H5.
symmetry.
destruct H5.
apply H5.
apply H5.
split.
apply H5.
apply H5.
apply H3.
apply H3.

assert (v <> w).
intro.
apply H3.
exists v.
split.
apply H0.
rewrite H4.
apply H1.

destruct (Ax_Pairing v w).  (*対*)
exists x.

split.
exists v.
split.
split.
apply H5.
left.
split.
apply H0.
intros.
destruct H6.
apply H5 in H6.
destruct H6.
symmetry.
apply H6.
destruct H3.
exists w.
split.
rewrite <- H6.
apply H7.
apply H1.

exists w.
split.
split.
apply H5.
right.
split.
apply H1.
intros.
destruct H6.
apply H5 in H6.
destruct H6.
destruct H3.
exists v.
split.
apply H0.
rewrite <- H6.
apply H7.
symmetry.
apply H6.




assert (exists x y : Set, x <> y). (*0≠1*)
destruct Ax_Exists. (*集合の存在*)
destruct (Ax_S_S (fun z => z <> z) x). (*分出*)
destruct (Ax_Pairing x0 x0). (*対*)
exists x0, x1.
intro.
apply (H0 x0).
destruct H2.
apply H1.
left.
split.
split.
destruct H.
destruct H.

intros.
destruct (Ax_Pairing x x0). (*対*)
destruct (Ax_S_S (fun z => z = x \/ P) x1). (*分出*)
destruct (Ax_S_S (fun z => z = x0 \/ P) x1). (*分出*)
destruct (H0 x x0 x2 x3).
apply H2.
split.
apply H1.
left.
split.
left.
split.
apply H3.
split.
apply H1.
right.
split.
left.
split.

assert (P -> x2 = x3).
intro.
apply Ax_Ex. (*外延*)
split.
intro.
apply H3.
apply H2 in H5.
split.
apply H5.
right.
apply H4.

intro.
apply H2.
apply H3 in H5.
split.
apply H5.
right.
apply H4.

intros.
apply H2 in H5.
apply H3 in H6.
destruct H5.
destruct H6. clear H6.
destruct H7.
destruct H8.
destruct H.
rewrite <- H6.
apply H7.
apply (H4 H7).
apply (H4 H6).

destruct H4.
destruct H4.
destruct H4.
destruct H4.
destruct H5.
destruct H5.
destruct H5.
apply H2 in H7.
apply H3 in H9.

destruct H7.
destruct H10.
destruct H10.
destruct H9.
destruct H10.
right.
intro.
apply H.
apply H6.
split.
rewrite <- H10.
apply H5.
apply H2.
split.
apply H1.
right.
split.
right.
apply H11.

left.
apply H10.
left.
apply H10.
Qed.

(*選択公理->排中律*)
Theorem AC_Set_Middle : AC_Set -> forall P : Prop, P \/ ~P.
Proof.
intro.
apply Middle_Iff_AC_Set_2.
apply (AC_Set_AC_Set_2 H).
Qed.
参考文献
Diaconescu's theorem
https://en.wikipedia.org/wiki/Diaconescu%27s_theorem