# Zermelo's well-ordering theorem

The proof of Bourbaki's tower theorem (R, BL1, BL2, Bourbaki) follows the original proof in [Bourbaki 1949].
See the slides and the paper for ITP 2015 for more information (Transfinite constructions in classical type theory by Gert Smolka, Steven Schäfer, and Christian Doczkal).
Gert Smolka, August 2015

Set Implicit Arguments.

Require Setoid.

Parameter XM : P, P ¬ P.

Lemma DN P :
¬ ¬ P P.

Notation "'set' X" := (XProp) (at level 70).
Notation "p <<= q" := ( x, p xq x) (at level 70).
Definition inhab X (p : set X) := x, p x.

Partially ordered types

Structure pot :=
{ pot_X :> Type;
pot_le : pot_Xpot_XProp;
pot_refl : x, pot_le x x;
pot_anti : x y, pot_le x ypot_le y xx = y;
pot_trans : x y z, pot_le x ypot_le y zpot_le x z }.

Notation "x <= y" := (pot_le x y).
Notation "x < y" := (x y x y).

Section POT.
Variable X : pot.

Implicit Types x y z u : X.
Implicit Types p q : set X.

Definition sup p x := z, x z y, p yy z.
Definition min p x := p x ¬ y, p y y < x.
Definition chain p := x y, p xp yx y y x.
Definition wf p := q, q <<= pinhab qinhab (min q).
Definition well_order := chain (fun xTrue) wf (fun xTrue).

Fact le_lt x y :
x yx = y x < y.

Fact lt_neq x :
¬ x < x.

Fact lt_le x y :
x < yx y.

Fact lt_le' x y z :
x < yy zx < z.

Fact lt_not_le x y :
x < y¬ y x.

Fact chain_not_le p x y :
chain pp xp y¬ x yy < x.

Fact sup_le x p u :
p xsup p ux u.

Fact sup_le' x y p u :
x yp ysup p ux u.

Fact sup_ex p u x :
sup p ux < u y, p y ¬ y x.

Fact sup_ex' x u p :
sup p u¬ u x y, p y ¬ y x.

Inductive ind p : set X :=
| indI x : ( y, p yy < xind p y) → ind p x.

Lemma ind_iff p x :
ind p x y, p yy < xind p y .

Fact ind_wf p :
p <<= ind pwf p.

Fact wf_ind p :
wf pp <<= ind p.

End POT.

# Bourbaki's tower theorem

Section Bourbaki.
Variable X : pot.
Variable a : X.
Variable f : XX.
Variable f_inc : x, x f x.

Implicit Types x y z u : X.
Implicit Types p q : set X.

Inductive T : set X :=
| Ta : T a
| Tf x : T xT (f x)
| Tsup p u : p <<= Tinhab psup p uT u.

Fact f_inc' x y :
x yx f y.

Fact f_inc'' x y :
f x yx y.

Fact T_a_least x :
T xa x.

Definition R x := T x y, T yy < xf y x.

Lemma BL1 x y :
T xR yx y f y x.

Lemma BL2 :
T <<= R.

Theorem Bourbaki x y :
T xT yx y f y x.

Corollary T_chain :
chain T.

Corollary T_f_monotone x y :
T xT yx yf x f y.

Corollary T_f_succ x y :
T xT yx < f yx y.

Corollary T_sup u :
sup T uT u.

Corollary T_sup_FP u :
sup T u f u = u T u.

Lemma T_wf :
wf T.

Theorem Bourbaki_Witt :
( p, wf pchain p u, sup p u) → u, f u = u a u.

End Bourbaki.

Section SetStuff.
Variable X : Type.

Implicit Types x : X.
Implicit Types p q r : set X.
Implicit Types F : set (set X).

Definition sing x : set X := fun zz = x.
Definition comp p : set X := fun z¬ p z.
Definition union F : set X := fun x p, F p p x.
Definition unique p : Prop := x y, p xp yx = y.

Fact sing_eq x y :
sing x yx = y.

Fact sing_eq' x y :
sing x = sing yx = y.

Fact union_incl p F :
F pp <<= union F.

Fact incl_refl p :
p <<= p.

Fact incl_trans p q r :
p <<= qq <<= rp <<= r.

End SetStuff.

Extensional choice types

Structure ect :=
{ ect_X :> Type;
ect_ext : p q : set ect_X, p <<= qq <<= pp = q;
gamma : set ect_Xset ect_X;
gamma_unique : p, unique (gamma p);
gamma_incl : p, gamma p <<= p;
gamma_inhab : p, inhab pinhab (gamma p) }.

# Zermelo's well-ordering theorem

Section Zermelo.
Variable X : ect.

Definition xset : pot := @Build_pot (set X) (fun p qp <<= q)
(@incl_refl X) (@ect_ext X) (@incl_trans X).

Implicit Types x y z u : X.
Implicit Types p q r : xset.
Implicit Types F : set xset.

Fact sup_union F :
sup F (union F).

Fact unique_sing p x :
unique pp xp = sing x.

Definition eta p : xset := gamma (comp p).
Definition a : xset := fun xFalse.
Definition f p : xset := fun xp x eta p x.

Fact f_inc p :
p f p.

Fact T_union F :
F <<= T a fT a f (union F).

Definition seg x : xset := union (fun pT a f p ¬ p x).

Fact seg_T x :
T a f (seg x).

Fact seg_open x :
¬ seg x x.

Fact seg_eta x :
eta (seg x) x.

Fact eta_seg x :
eta (seg x) = sing x.

Fact seg_injective x y :
seg x = seg yx = y.

Definition le x y := seg x <<= seg y.
Lemma le_refl x : le x x.
Lemma le_anti x y : le x yle y xx = y.
Lemma le_trans x y z : le x yle y zle x z.

Definition poX : pot := @Build_pot X le le_refl le_anti le_trans.

Theorem Zermelo :
well_order poX.

End Zermelo.

Check Zermelo.
Print Assumptions Zermelo.