選択公理を使って排中律を証明する

CIC において、以下を仮定すると排中律が証明できるそうです。実際、Lean における排中律の証明項はそのようにして作られています→コード

• 強い選択公理(グローバルチョイス)
• 関数の外延性
• 命題の外延性
• Proof Irrevalence

勉強がてら Coq で書き直してみました:

Section AC_EM.

Variable gchoice : forall A P, (exists a, P a) -> {a:A | P a}.
Variable pext : forall (P Q:Prop), (P<->Q) -> P = Q.
Variable pirr : forall (P: Prop) (H1 H2: P), H1 = H2.
Variable fext : forall {A B} (f g:A->B), (forall x, f x = g x) -> f = g.

Variable P: Prop. (*will prove P \/ ~P*)

Definition U := fun x =>  x = True \/ P.
Definition V := fun x => x = False \/ P.
Definition inhU: exists a, U a.
  exists True. cbv. now left. Qed.
Definition inhV: exists a, V a.
  exists False. cbv. now left. Qed.
Definition u  := proj1_sig (gchoice _ _ inhU).
Definition Hu: U u  := proj2_sig (gchoice _ _ inhU).
Definition v  := proj1_sig (gchoice _ _ inhV).
Definition Hv: V v  := proj2_sig (gchoice _ _ inhV).

Lemma uvn_p: u<>v \/ P.
Proof. destruct Hu; destruct Hv; unfold U, V in*; simpl in *.
- left. rewrite H. rewrite H0. intro. rewrite <-H1. constructor.
- right. assumption.
- right. assumption.
- right. assumption.
Qed.

Lemma p_uv: P-> u=v.
Proof. intros HP.
assert (HeqUV: U=V). {
  apply fext. intros. cbv.
  apply pext. split; intros.
  right. assumption.
  right. assumption.
}
assert (H: forall H H',  proj1_sig (gchoice _ U H) = proj1_sig (gchoice _ V H')). {
  rewrite HeqUV.
  intros.
  enough (H=H') by (now subst).
  apply pirr.
}
 apply H.
Qed.

Theorem em : P \/ ~P.
Proof. destruct (uvn_p).
- right. intro. apply H. now apply p_uv.
- now left.
Qed.

End AC_EM.

補足

Diaconescu's theorem (→ en:Wikipedia )という直感主義論理上の公理的集合論の定理をカリーハワード対応させたもののようです。論理と計算ではやっぱりちょっぴり違うので（例：分出公理のCICでの対応物は？）、命題の外延性とかの公理が出てきたりするのでしょうか？

いずれにせよ、選択公理と排中律というなんかあまり関係がなさそうな二つが繋がっているというのはおもしろいですね