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

Library Equivalence

Require Import Zermelo1904 Zermelo1908.
Set Implicit Arguments.


We define the two orderings, W1 for 1904, W2 for 1908. There will be some technical overhead to unify the two developments, but the actual equivalence-proof is rather simple.

Definition W1 := W.
Definition W2 := lt.

We reformulate some simple properties of the orderings. They are already given in the respective developments and only need some minor refactoring.

Lemma W1_irref a: ~ W1 a a.
destruct X_wo as [[I _] _].
destruct (I a a) as [_ J]; unfold X'; trivial.
now apply J.

Lemma W1_asym a b: W1 a b -> ~ W1 b a.
destruct X_wo as [[I _] _].
destruct (I a b) as [J _]; unfold X'; trivial.
now apply J.

Lemma W2_asym a b: W2 a b -> ~ W2 b a.
intros I1 I2. apply (lt_irref (a:=a)). now apply (lt_tra (b:=b)).

This lemma induces our strategy: to prove the orderings equivalent, it suffices to prove one implication. The other is a consequence.

Lemma impl_equi: (forall a b, W2 a b -> W1 a b) -> (forall a b, W1 a b -> W2 a b).
intros I a b J. destruct (lt_trich a b) as [H|[H|H]]; trivial.
- subst b. contradiction (W1_irref J).
- specialize (I b a H). contradiction (W1_asym J).

We need one characterisation of W1 a b. It is a sufficient criterion if we find a gamma-set G, such that a is in G, but b is not.

Lemma char a b: (exists G W, GS G W /\ G a /\ ~ G b) -> W1 a b.
intros [G[W[I1[I2 I3]]]]. exists G, W. split; trivial. split; trivial.
intros Mb Rb J1 J2. destruct (IS_compare' I1 J1) as [H|H]; trivial.
- intros H. apply iseg_sub in H. apply I3. now apply H.
- subst Mb. contradiction.

We proof that W2 is a well-ordering for all subsets of X. The term wellOrdered is specified in the 1904 implementation and we need some technical refactoring to meet the actual requirements.

Lemma W2_WO U: wellOrdered U W2.
- split.
+ intros x y _ _. split; split; intros I.
* split; eauto using W2_asym. apply I.
* destruct I as [I1 I2]. destruct (lt_trich x y) as [H|[H|H]]; tauto.
* subst x. split; apply lt_irref.
* destruct I as [I1 I2]. destruct (lt_trich x y) as [H|[H|H]]; tauto.
+ intros x y z _ _ _. apply lt_tra.
- intros V I1 I2. destruct (lt_wo (p:=V)) as [x[X1 X2]].
+ assumption.
+ exists x. split; trivial. intros y Y1 Y2. apply (lt_irref (a:=y)).
  apply (lt_tra Y2). apply X2. split; trivial. apply Y2.

In the following, the sets of the form "R a" denote the specific element of T, the intersection of all theta-chains, which is the construction used in 1908. We first proof them linear, in the sense that a is in the rest of b, whenever b is not in the rest of a.

Lemma R_lin' a b: ~ R a b -> R b a.
intros I. destruct (R_lin a b) as [J|J]; tauto.

Now we can prove, that the complements of the sets "R a" are gamma-sets. By definition, we have to justify, the two properties of gamma-sets. We use W2 and find that the complements are well-ordered. It remains to show that the respective initial segments agrre with the choice function Eps, which is a consequence of the lemma clos_Eps, which states that Eps(R a) = a.

Lemma W2_GS a: GS (fun c => ~ R a c) W2.
split; eauto using W2_WO.
intros b B. apply R_lin' in B.
assert (J: IS (fun c => ~ R a c) b W2 = IS X' b W2).
{ apply pe. intros d. split; intros [I1 I2]; split; unfold X'; trivial.
  destruct I2 as [I2 I3]. intros HH. apply I3.
  apply R_antisym; trivial. now apply R_tra with (b:=a). }
assert (I: X' -- IS (fun c => ~ R a c) b W2 = R b).
{ rewrite J. apply pe. intros d. split; intros I.
- destruct (xm (d=b)) as [Y|N].
+ subst d. apply R_ref.
+ destruct I as [I1 I2]. apply R_lin'. intros DB. apply I2. repeat split; trivial.
- split; unfold X'; auto. intros [I1 I2]. destruct I2 as [I2 I3].
  apply I3. now apply R_antisym. }
rewrite I. symmetry. apply R_Eps.

Now it is easy to conclude the implication we want to prove: By the characterisation, it suffices to find the special gamma-set. The statement above shows that the complement of R a is a gamma-set, the two membership properties come from the definition of W2.

Lemma impl a b: W2 a b -> W1 a b.
intros I. apply char. pose (RC := fun c => ~ R b c).
exists RC, W2. split; eauto using W2_GS. split.
- intros J. destruct I as [I1 I2]. apply I2. now apply R_antisym.
- intros J. apply J. apply R_ref.

We conclude the equivalence of the two orderings. Note that stronger propositional extensionality implies equality.

Theorem equi a b: W1 a b <-> W2 a b.
- apply impl_equi. apply impl.
- apply impl.