Browse the appendix: Z1 Z2 EQ or go to main library or return to overview.

Library Zermelo1908

Require Import Zermelo1904.
Set Implicit Arguments.

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.