Library Zermelo1908
1908 Proof by Dr. Chad E. Brown
We did some minimal re-arrangements, but all lemmas, proofs and comments were given by Chad Brown.Lemma epsr:forall p, ex p -> p (Eps p).
intros p [x I]. now apply (EpsR p x).
Qed.
Lemma pe:forall p q:X -> Prop, (forall x, p x <-> q x) -> p = q.
intros p q I. apply P_ext; firstorder.
Qed.
Lemma dn:forall p:Prop, ~~p -> p.
intros p I. destruct (classic p) as [J|J]; trivial. contradiction.
Qed.
Lemma xm:forall p:Prop, p \/ ~p.
intros p. apply dn. tauto.
Qed.
Definition prime (p:X -> Prop) (x:X) := p x /\ x <> Eps p.
Definition inter (D:(X -> Prop) -> Prop) (x:X) := forall p, D p -> p x.
Inductive C : (X -> Prop) -> Prop :=
| C2 p : C p -> C (prime p)
| C3 (D:(X -> Prop) -> Prop) : (forall p, D p -> C p) -> C (inter D).
Definition clos (p:X -> Prop) := inter (fun q => C q /\ forall x, p x -> q x).
Lemma clos_C (p:X -> Prop) : C (clos p).
apply C3. tauto.
Qed.
Lemma clos_subq (p:X -> Prop) : forall x, p x -> clos p x.
intros x H1 q [H2 H3]. apply H3. assumption.
Qed.
Lemma clos_Eps (p:X -> Prop) : ex p -> p (Eps (clos p)).
intros H0. apply dn. intros H1.
assert (L1:forall x, p x -> prime (clos p) x).
{ intros x H2. split.
revert H2. apply clos_subq.
intros H3. apply H1. rewrite <- H3. assumption.
}
assert (L2:C (prime (clos p)) /\ (forall x : X, p x -> prime (clos p) x)).
{ split.
- apply C2. apply clos_C.
- exact L1.
}
assert (L3:clos p (Eps (clos p))).
{ apply (epsr (p:=clos p)). destruct H0 as [x H0]. exists x. now apply clos_subq. }
generalize (L3 (prime (clos p)) L2). unfold prime. tauto.
Qed.
Lemma C_lin p : C p -> forall q, C q -> (forall x, q x -> p x) \/ (forall x, p x -> q x).
intros H. induction H as [p Hp IHp|D HD IHD].
- intros q Hq. induction Hq as [q Hq IHq|E HE IHE].
+ destruct IHq as [IHq1|IHq1].
* left. intros x [H1 _]. now apply IHq1.
* { destruct (xm (prime p (Eps q))) as [H1|H1].
- destruct (IHp (prime q) (C2 Hq)) as [IHp1|IHp1].
+ destruct (xm (q (Eps p))) as [H3|H3].
* { exfalso. destruct H1 as [H4 H5]. apply H5. f_equal.
apply pe. intros x. split.
- intros H6. destruct (xm (x = Eps q)) as [H7|H7].
+ congruence.
+ apply IHp1. split; assumption.
- intros H6. destruct (xm (x = Eps p)) as [H7|H7].
+ congruence.
+ apply IHq1. split; assumption.
}
* { left. intros x H4. split.
- now apply IHp1.
- destruct H4 as [H5 _]. congruence.
}
+ right. intros x [H2 _]. now apply IHp1.
- right. intros x H2. split.
+ now apply IHq1.
+ congruence.
}
+ destruct (xm (exists q, E q /\ exists x, prime p x /\ ~q x)) as [[q [H1 [x [H2 H3]]]]|H1].
* { destruct (IHE q H1) as [IHE1|IHE1].
- left. intros y H4. apply IHE1. apply (H4 q). assumption.
- exfalso. apply H3. now apply IHE1.
}
* right. intros x H2 q H3. apply dn. intros H4. apply H1. exists q. split; try assumption. exists x. tauto.
- intros q Hq.
destruct (xm (exists p, D p /\ forall x, p x -> q x)) as [[p [H1 H2]]|H1].
+ right. intros x H3. apply H2. now apply (H3 p).
+ left. intros x H2 p H3.
destruct (IHD p H3 q Hq) as [IHD1|IHD1].
* now apply IHD1.
* exfalso. apply H1. exists p. tauto.
Qed.
Definition R (a:X) : X -> Prop := clos (fun x => x = a).
Lemma CR : forall a, C (R a).
unfold R. intros a. apply (clos_C (fun x => x = a)).
Qed.
Lemma R_ref : forall a, R a a.
intros a. unfold R. apply clos_subq. reflexivity.
Qed.
Lemma R_Eps a : Eps (R a) = a.
apply (clos_Eps (p:=fun x => x = a)).
exists a. reflexivity.
Qed.
Lemma R_lin a b : R a b \/ R b a.
destruct (C_lin (CR a) (CR b)) as [H1|H1].
- left. apply H1. apply R_ref.
- right. apply H1. apply R_ref.
Qed.
Lemma R_tra a b c : R a b -> R b c -> R a c.
intros H1 H2 p H3. generalize (H1 p H3). intros H4.
apply (H2 p). split; try tauto.
intros x H5. subst. assumption.
Qed.
Lemma R_antisym a b : R a b -> R b a -> a = b.
intros H1 H2. rewrite <- (R_Eps a). rewrite <- (R_Eps b).
f_equal. apply pe. intros c. split.
- intros H3. now apply (R_tra H2 H3).
- intros H3. now apply (R_tra H1 H3).
Qed.
Lemma C_Eps p : C p -> forall q, C q -> q (Eps p) -> forall x, p x -> q x.
intros Hp q Hq H1. destruct (C_lin (p:=prime p) (C2 Hp) Hq) as [H2|H2].
- exfalso. destruct (H2 _ H1) as [_ H3]. congruence.
- intros x H3. destruct (xm (x = Eps p)) as [H4|H4].
+ congruence.
+ apply H2. split; assumption.
Qed.
Lemma R_wo (p:X -> Prop) : ex p -> exists x, p x /\ forall y, p y -> R x y.
intros H1. exists (Eps (clos p)). split.
- apply clos_Eps. exact H1.
- intros y H2 q [H3 H4]. apply (C_Eps (p:=clos p) (clos_C p) H3).
+ apply H4. reflexivity.
+ apply (clos_subq p y H2).
Qed.
Definition lt (a b:X) : Prop := R a b /\ a <> b.
Lemma lt_irref a : ~ lt a a.
intros [_ H1]. congruence.
Qed.
Lemma lt_tra a b c : lt a b -> lt b c -> lt a c.
intros [H1 H2] [H3 H4]. split.
- now apply (R_tra H1 H3).
- intros H5. rewrite <- H5 in H3. generalize (R_antisym H1 H3). assumption.
Qed.
Lemma lt_trich a b : lt a b \/ a = b \/ lt b a.
destruct (xm (a = b)) as [H1|H1].
- tauto.
- destruct (R_lin a b) as [H2|H2].
+ left. split; assumption.
+ right. right. split; try assumption. congruence.
Qed.
Lemma lt_wo (p:X -> Prop) : ex p -> exists x, p x /\ forall y, p y /\ y <> x -> lt x y.
intros H1. destruct (R_wo (p:=p) H1) as [x [H2 H3]]. exists x. split; try assumption.
intros y [H4 H5]. split.
- now apply H3.
- congruence.
Qed.
Theorem Zermelo_WO : exists r : X -> X -> Prop,
(forall a, r a a)
/\ (forall a b c, r a b -> r b c -> r a c)
/\ (forall a b, r a b \/ r b a)
/\ (forall a b, r a b -> r b a -> a = b)
/\ (forall p:X -> Prop, ex p -> exists x, p x /\ forall y, p y -> r x y).
exists R.
split; try exact R_ref.
split; try exact R_tra.
split; try exact R_lin.
split; try exact R_antisym.
exact R_wo.
Qed.
Theorem Zermelo_WO_strict : exists r : X -> X -> Prop,
(forall a, ~ r a a)
/\ (forall a b c, r a b -> r b c -> r a c)
/\ (forall a b, r a b \/ a = b \/ r b a)
/\ (forall p:X -> Prop, ex p -> exists x, p x /\ forall y, p y /\ y <> x -> r x y).
exists lt.
split; try exact lt_irref.
split; try exact lt_tra.
split; try exact lt_trich.
exact lt_wo.
Qed.