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

# Library Equivalence

Require Import Zermelo1904 Zermelo1908.
Set Implicit Arguments.

## Equivalence

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.
Proof.
destruct X_wo as [[I _] _].
destruct (I a a) as [_ J]; unfold X'; trivial.
now apply J.
Qed.

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

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

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).
Proof.
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).
Qed.

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.
Proof.
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.
Qed.

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.
Proof.
split.
- 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.
Qed.

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.
Proof.
intros I. destruct (R_lin a b) as [J|J]; tauto.
Qed.

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.
Proof.
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.
Qed.

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.
Proof.
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.
Qed.

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.
Proof.
split.
- apply impl_equi. apply impl.
- apply impl.
Qed.