Regularity & Epsilon induction.

.gitignore

@@ -0,0 +1,31 @@
+# Coq gitignore:
+.*.aux
+*.a
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+*.cmxs
+*.glob
+*.ml.d
+*.ml4.d
+*.mli.d
+*.mllib.d
+*.mlpack.d
+*.native
+*.o
+*.v.d
+*.vio
+*.vo
+.coq-native/
+.csdp.cache
+.lia.cache
+.nia.cache
+.nlia.cache
+.nra.cache
+csdp.cache
+lia.cache
+nia.cache
+nlia.cache
+nra.cache

3_Regularity.v

@@ -0,0 +1,160 @@
+(* PUBLIC DOMAIN
+The main source of the proofs:
+https://math.stackexchange.com/questions/452809/epsilon-induction-implies-axiom-of-foundation-or-regularity
+Author: Georgy Dunaev, [email protected]
+*)
+
+Require Import ZFC.Sets.
+Require Import Setoid.
+
+(* Requires for ClassicRegularity module. *)
+Require Classical_Prop.
+Require Classical_Pred_Type.
+
+(* Epsilon induction. *)
+Theorem eps_ind (R:Ens->Prop)
+(Sou_R:forall a b, EQ a b -> (R a <-> R b))
+: (forall x:Ens, (forall y, IN y x -> R y) -> R x)
+-> forall z, R z.
+Proof.
+intros.
+induction z.
+apply H.
+simpl.
+intros y q.
+destruct q as [a G].
+rewrite  (Sou_R y (e a)).
+apply H0.
+exact G.
+Defined.
+
+(* (P x) means "Set x is regular." *)
+Definition P x := forall u : Ens, (IN x u -> exists y,
+IN y u /\ forall z, IN z u -> ~ IN z y).
+
+(* Soundness of the definition of P. *)
+Theorem sou_P : forall a b : Ens, EQ a b -> P a <-> P b.
+Proof.
+intros.
+unfold P.
+split; intros.
++ apply IN_sound_left with (E':=a) in H1.
+  apply H0. apply H1.
+  apply EQ_sym. exact H.
++ apply IN_sound_left with (E':=b) in H1.
+  apply H0. apply H1.
+  exact H.
+Defined.
+
+(* Here I follow Zuhair's proof from source.
+https://math.stackexchange.com/users/489784/zuhair *)
+
+(* Unending chain *)
+Definition UC c := forall m, IN m c -> exists n, IN n m /\ IN n c.
+Definition WF x := ~(exists c, UC c /\ IN x c).
+
+(* Inductive step *)
+Theorem Zuhair_1 (a:Ens): (forall x, IN x a -> WF x) -> WF a.
+Proof.
+unfold WF.
+intros H K0.
+pose (K:=K0).
+destruct K as [c [M1 M2]].
+unfold UC in M1.
+pose (B:=M1 a M2).
+destruct B as [n [nina ninc]].
+apply (H n nina).
+exists c.
+split.
+exact M1.
+exact ninc.
+Defined.
+
+(* Soundness of WF *)
+Theorem sou_WF : forall a b : Ens, EQ a b -> WF a <-> WF b.
+Proof.
+intros.
+unfold WF.
+* split.
++ intros A B.
+  apply A.
+  destruct B as [c [a1 a2]].
+  exists c.
+  split. exact a1.
+  apply IN_sound_left with (E:=b).
+  apply EQ_sym. exact H.
+  exact a2.
++ intros A B.
+  apply A.
+  destruct B as [c [a1 a2]].
+  exists c.
+  split. exact a1.
+  apply IN_sound_left with (E:=a).
+  exact H.
+  exact a2.
+Defined.
+
+(* Induction. "Every set is well-founded." *)
+Theorem Zuhair_2 (y:Ens): WF y.
+Proof.
+apply eps_ind.
+- exact sou_WF.
+- intros a. exact (Zuhair_1 a).
+Defined.
+
+(* Formalization of Andreas Blass variant of proof. 
+https://math.stackexchange.com/users/48510/andreas-blass *)
+Module ClassicRegularity.
+
+Import Classical_Prop.
+Import Classical_Pred_Type.
+Theorem Blass x : P x.
+Proof.
+unfold P.
+pose (A:=Zuhair_2 x); unfold WF in A.
+intros u xinu.
+(* Series of the equivalent tranformations.*)
+apply not_ex_all_not with (n:=u) in A.
+apply not_and_or in A.
+ destruct A as [H1|H2].
+ 2 : destruct (H2 xinu).
+ unfold UC in H1.
+apply not_all_ex_not in H1.
+ destruct H1 as [yy yH].
+ exists yy.
+apply imply_to_and in yH.
+ destruct yH as [Ha Hb].
+ split. exact Ha.
+ intro z.
+apply not_ex_all_not with (n:=z) in Hb.
+apply not_and_or in Hb.
+ intro v.
+ destruct Hb as [L0|L1]. exact L0.
+ destruct (L1 v).
+Defined.
+
+(* Standard formulation of the regularity axiom. *)
+Theorem axreg (x:Ens) :
+(exists a, IN a x)->(exists y, IN y x /\ ~ exists z, IN z y /\ IN z x)
+.
+Proof.
+pose (Q:= Blass).
+unfold P in Q.
+intro e.
+destruct e as [z zinx].
+pose (f:= Q z x zinx).
+destruct f as [g G].
+exists g.
+destruct G as [G1 G2].
+split.
++ exact G1.
++ intro s.
+  destruct s as [w [W1 W2]].
+  exact (G2 w W2 W1).
+Defined.
+
+End ClassicRegularity.
+
+
+
+