Formalisation of "Axiomatic Set Theory in Type Theory" by Gert Smolka
• Version: 16 May 2015
• Author: Dominik Kirst, Saarland University
• This file covers Sections 10 and 11 of the paper

Require Export cum.

Implicit Types x y z: set.
Implicit Types p q: set -> Prop.
Implicit Types R S U V: set -> set -> Prop.

# Two Instances

## Ordinals

Definition sigma x := bun x (sing x).

Lemma sigma_increasing:
increasing sigma.
Proof.
intros x. apply bun_incl'. now left.
Qed.

Lemma sigma_cumulative:
cumulative sigma.
Proof.
intros x. apply el_bun. right. now apply el_sing.
Qed.

Lemma sigma_trans:
trans_pres sigma.
Proof.
intros x XT y Y z Z. apply el_bun in Y as [Y|Y].
- apply el_bun. left. now apply (XT y).
- apply el_bun. left. apply el_sing in Y. now subst y.
Qed.

Lemma sigma_WF:
WF_pres sigma.
Proof.
intros x [XWF]. constructor. intros y Y.
apply el_bun in Y as [Y|Y]; auto using el_sing, WF.
Qed.

Hint Resolve sigma_increasing sigma_cumulative sigma_trans sigma_WF.

Definition Ord := Tower sigma.

Lemma Ord_WF:
cWF Ord.
Proof.
apply tower_WF; auto.
Qed.

Lemma Ord_linear:
clinear Ord.
Proof.
apply tower_linear; auto.
Qed.

Lemma Ord_cumulative:
ccum Ord.
Proof.
apply tower_cumulative; auto.
Qed.

Lemma Ord_tricho x y:
Ord x -> Ord y -> x el y \/ x = y \/ y el x.
Proof.
intros OX OY. destruct (classic (x=y)); try tauto.
destruct (Ord_linear OX OY) as [XY|YX]; firstorder using Ord_cumulative.
Qed.

Lemma Ord_wordered:
wordered Ord.
Proof.
apply tower_worder; auto.
Qed.

Lemma Ord_unreal:
~ orealizable (Inc Ord).
Proof.
apply Inc_complete. apply tower_unrealizable; auto.
Qed.

Lemma Ord_el_trans x:
Ord x -> trans x.
Proof.
apply tower_trans; auto.
Qed.

Lemma Ord_transitive:
ctrans Ord.
Proof.
intros x XO. induction XO as [x H IH| x H IH].
- intros y Y. apply Union in Y as [z[Z1 Z2]]. now apply (IH z).
- intros y Y. apply el_bun in Y as [Y|Y]; auto using Tower.
Qed.

Lemma Ord_seg_equiv x:
Ord x -> Seg (Inc Ord) x === class x.
Proof.
intros OX. apply seg_equiv; auto using Ord_transitive, Ord_cumulative.
Qed.

Lemma Ord_representation R:
worder R -> orealizable R -> exists! x, Ord x /\ simi R (res_seg (Inc Ord) x).
Proof.
intros WR OR. now apply tower_representation.
Qed.

## Cumulative hierarchy

Definition expower x := bun x (pow x).

Lemma expower_increasing:
increasing expower.
Proof.
intros x. apply bun_incl'. now left.
Qed.

Lemma expower_cumulative:
cumulative expower.
Proof.
intros x. apply el_bun. right. now apply Power.
Qed.

Lemma expower_trans:
trans_pres expower.
Proof.
intros x XT y Y z Z. apply el_bun in Y as [Y|Y].
- apply el_bun. left. now apply (XT y).
- apply el_bun. left. apply Power in Y. now apply Y.
Qed.

Lemma expower_WF:
WF_pres expower.
Proof.
intros x [XWF]. constructor. intros y Y.
apply el_bun in Y as [Y|Y]; firstorder using Power, WF.
Qed.

Hint Resolve expower_increasing expower_cumulative expower_trans expower_WF.

Definition Cum := Tower expower.

Lemma Cum_WF:
cWF Cum.
Proof.
apply tower_WF; auto.
Qed.

Lemma Cum_linear:
clinear Cum.
Proof.
apply tower_linear; auto.
Qed.

Lemma Cum_cumulative:
ccum Cum.
Proof.
apply tower_cumulative; auto.
Qed.

Lemma Cum_tricho x y:
Cum x -> Cum y -> x el y \/ x = y \/ y el x.
Proof.
intros CX CY. destruct (classic (x=y)); try tauto.
destruct (Cum_linear CX CY) as [XY|YX]; firstorder using Cum_cumulative.
Qed.

Lemma Cum_wordered:
wordered Cum.
Proof.
apply tower_worder; auto.
Qed.

Lemma Cum_unreal:
~ orealizable (Inc Cum).
Proof.
apply Inc_complete. apply tower_unrealizable; auto.
Qed.

Lemma Cum_el_trans x:
Cum x -> trans x.
Proof.
apply tower_trans; auto.
Qed.

Lemma Cum_representation R:
worder R -> orealizable R -> exists! x, Cum x /\ simi R (res_seg (Inc Cum) x).
Proof.
intros WR OR. now apply tower_representation.
Qed.

Equivalent characterization of cumulative sets (44)

Definition cum := Tower pow.

Lemma power_trans x :
trans x -> trans (pow x).
Proof.
intros I y Y z Z. apply Power in Y.
apply Power. apply I. now apply Y.
Qed.

Lemma trans_power X :
trans X <-> X <<= pow X.
Proof.
split; intros A x; auto.
Qed.

Lemma cum_trans x:
cum x -> trans x.
Proof.
apply tower_trans. intros y. apply power_trans.
Qed.

Lemma cum_pow x:
cum x -> pow x = expower x.
Proof.
intros H. apply cum_trans in H.
apply Ext; intros y; split; intros Y.
- apply el_bun. now right.
- apply el_bun in Y as [Y|Y].
+ apply trans_power in H. now apply H.
+ assumption.
Qed.

Lemma cum_Cum x:
cum x -> Cum x.
Proof.
induction 1 as [x X IH| x X IH].
- now constructor.
- apply cum_pow in X. rewrite X. now apply TS.
Qed.

Lemma Cum_cum x:
Cum x -> cum x.
Proof.
induction 1 as [x X IH| x X IH].
- unfold cum in IH. now constructor.
- constructor. intros y Y. apply Upair in Y as [Y|Y].
+ now rewrite Y.
+ rewrite Y. now constructor.
Qed.

Lemma cum_WF x:
cum x -> WF x.
Proof.
intros H. apply Cum_WF. now apply cum_Cum.
Qed.

Lemma cum_wordered:
wordered cum.
Proof.
apply (worder_equiv Cum_wordered). firstorder using cum_Cum, Cum_cum.
Qed.

Lemma cum_linear:
clinear cum.
Proof.
intros x y XC YC. firstorder using cum_Cum, Cum_linear.
Qed.

Lemma cum_sandwich x y:
cum x -> cum y -> x << y -> pow x <<= y.
Proof.
intros CX CY XY. rewrite cum_pow; trivial.
apply cum_Cum in CX. apply cum_Cum in CY.
now apply (tower_sandwich expower_increasing).
Qed.

Lemma cum_sandwich' x y:
cum x -> cum y -> x el y -> pow x <<= y.
Proof.
intros CX CY XY. apply cum_sandwich; trivial.
apply Cum_cumulative; auto using cum_Cum.
Qed.

Hint Resolve cum_Cum Cum_cum.

Every well-founded set occurs in some cumulative set (41)

Theorem WF_cum x:
WF x -> exists y, cum y /\ x el y.
Proof.
induction 1 as [x H IH].
pose (R := (fun x' y => least y (fun z => cum z /\ x' el z))).
assert (FR: functional R) by (intros a b c A B; eauto using least_unique).
pose (u := union (rep x R)). exists (pow u). split.
- constructor. constructor. firstorder using rep_func.
- apply Power. intros y Y. specialize (IH y Y).
destruct Cum_wordered as [_ L]. apply L in IH as [l[[L1 L2] L3]]; firstorder.
apply Union. exists l. split; auto. apply rep_func; firstorder.
Qed.

Corollary WF_cum_least x:
WF x -> exists y, least y (fun z => cum z /\ x <<= z).
Proof.
intros WX. apply WF_cum in WX as [y[Y1 Y2]]. apply Cum_el_trans in Y2; auto.
assert (exists y, cum y /\ x <<= y) by (exists y; split; assumption).
destruct Cum_wordered as [_ L]. apply L in H as [l[[L1 L2] L3]]; firstorder.
Qed.

Simple characterisation of the canonical similarity from O to Z (46)

Definition F a x :=
Ord a /\ least x (fun z => cum z /\ a <<= z).

Lemma F_total a:
Ord a -> exists x, F a x.
Proof.
intros H. assert (I: WF a) by auto using Ord_WF.
apply WF_cum_least in I as [x X].
exists x. split; assumption.
Qed.

Lemma F_functional:
functional F.
Proof.
intros a x y [_ H1] [_ H2]. apply sub_anti; firstorder.
Qed.

Lemma WF_pow_sub x:
WF x -> pow x <<= x -> False.
Proof.
intros WFX PX. apply (WF_no_loop WFX). apply PX. now apply Power.
Qed.

Lemma set_partition M:
(exists x, greatest x (class M)) \/
(forall x, x el M -> exists y, y el M /\ ~ y <<= x).
Proof.
destruct (classic (exists x, greatest x (class M))) as [H|H]; try now left.
right. indirect. apply not_all_ex_not in H0 as [x X]. apply H. exists x.
apply imply_to_and in X as [XM Y]. split; trivial. intros y YM.
indirect. apply Y. hnf in YM. exists y. split; assumption.
Qed.

Lemma cum_sub_not x y:
cum x -> cum y -> ~ x <<= y -> y << x.
Proof.
intros XC YC XY. destruct (@Cum_linear x y); firstorder using cum_Cum.
Qed.

Lemma cum_partition M:
subsc M cum -> union M el M \/ M <<= union M.
Proof.
intros MC. destruct (set_partition M) as [[x X]|H].
- left. cut (x = union M). { intros H. rewrite H in X. apply X. } apply sub_anti.
+ apply union_el_incl. apply X.
+ apply union_incl. apply X.
- right. intros x X. destruct (H x X) as [y[Y1 Y2]].
apply Union. exists y. split; trivial.
apply (Cum_cumulative); auto using cum_Cum, cum_sub_not.
Qed.

Lemma cum_least a x:
least x (fun z => cum z /\ a <<= z) -> a el x -> False.
Proof.
intros [[XC XA] L] H. induction XC as [M MC IH | x XC _].
- destruct (cum_partition MC) as [UM|UM]; try now apply (IH (union M)).
apply Union in H as [x[X1 X2]]. specialize (MC x X1).
apply (WF_no_loop (cum_WF MC)). apply L; firstorder using cum_trans.
- apply Power in H. apply (WF_pow_sub (cum_WF XC)). apply L. split; assumption.
Qed.

Lemma F_injective a b x:
F a x -> F b x -> a = b.
Proof.
intros [A1 A2] [B1 B2]. destruct (Ord_tricho A1 B1) as [H|[H|H]]; trivial.
- exfalso. apply (cum_least A2). firstorder.
- exfalso. apply (cum_least B2). firstorder.
Qed.

Lemma F_inv_func:
functional (inv F).
Proof.
firstorder using F_injective.
Qed.

Lemma F_pres1 a b x y:
F a x -> F b y -> a <<= b -> x <<= y.
Proof.
intros [H1 H2] [H3 H4] AB. destruct (@cum_linear x y); firstorder.
Qed.

Lemma F_pres2 a b x y:
F a x -> F b y -> x <<= y -> a <<= b.
Proof.
intros [H1 H2] [H3 H4] XY. destruct (@Ord_linear a b); trivial.
destruct (classic (a=b)) as [AB|AB]; subst; auto.
exfalso. apply (cum_least H4). apply XY.
destruct H2 as [[_ H2]_]. apply H2. firstorder using Ord_cumulative.
Qed.

Lemma sigma_pow a x:
trans a -> a <<= x -> sigma a <<= pow x.
Proof.
intros TA AX b BA. apply el_bun in BA as [BA|BA].
- apply Power. apply (@sub_trans b a); auto.
- apply el_sing in BA. subst b. now apply Power.
Qed.

Lemma F_rec1 a x:
F a x -> F (sigma a) (pow x).
Proof.
intros [A1 A2]. split; try now apply TS.
assert (XC: cum x) by now apply A2.
assert (PC: cum (pow x)) by now apply TS.
repeat split; auto; try (apply sigma_pow; firstorder using Ord_el_trans).
intros y [Y1 Y2]. apply cum_sandwich; trivial. apply cum_sub_not; trivial.
intros YX. apply (cum_least A2). apply YX. apply Y2. auto.
Qed.

Lemma F_rec2 x:
subsc x Ord -> F (union x) (union (rep x F)).
Proof.
intros XO. assert (UO: Ord (union x)) by now apply TU. repeat split; trivial.
- apply TU. intros y Y. apply (rep_func F_functional) in Y as [a[A1 A2]]. apply A2.
- intros a A. apply Union in A as [b[B1 B2]]. destruct (F_total (XO b B1)) as [y Y].
apply Union. exists y. split.
+ apply (rep_func F_functional). exists b. split; assumption.
+ destruct Y as [_ [[_ Y] _]]. now apply Y.
- intros y [Y1 Y2]. intros z Z. apply Union in Z as [z'[Z1 Z2]].
apply (rep_func F_functional) in Z1 as [a[A1 A2]].
apply A2; trivial. split; trivial. apply (@sub_trans a (union x)); trivial.
now apply union_el_incl.
Qed.

Lemma F_surjective x:
cum x -> exists a, F a x.
Proof.
induction 1 as [x H IH| x H [a FA]].
- exists (union (rep x (inv F))).
rewrite (@rep_rep x F) at 2; eauto using F_inv_func, F_functional.
apply F_rec2. intros a A. now apply (rep_func F_inv_func) in A as [y[_ [AO _]]].
- exists (sigma a). now apply F_rec1.
Qed.

Lemma F_simi:
similarity F (Inc Ord) (Inc cum).
Proof.
repeat split.
- firstorder.
- intros a b x FAX BA. assert (OB: Ord b) by firstorder.
destruct (F_total OB) as [y Y]. exists y. split; firstorder using F_pres1.
- apply F_functional.
- firstorder.
- intros x y a FAX XY. assert (YC: cum y) by firstorder.
destruct (F_surjective YC) as [b B]. exists b. split; auto.
repeat split. now apply B. now apply FAX. apply (F_pres2 B FAX). apply XY.
- firstorder using F_injective.
Qed.

Lemma F_canon_equiv:
F o=o Canon (Inc Ord) (Inc cum).
Proof.
apply (canon_unique Ord_wordered cum_wordered). split; try apply F_simi.
left. intros a [b[A _]]. now apply F_total.
Qed.

Lemma F_unique U:
isomorphism U (Inc Ord) (Inc cum) -> F o=o U.
Proof.
intros [SI[D1 D2]]. split; intros a x AX.
- destruct (D1 a) as [y Y].
+ exists a. repeat split; auto; apply AX.
+ now rewrite (simi_agree Ord_wordered cum_wordered F_simi SI AX Y).
- apply F_canon_equiv. exists U. split; assumption.
Qed.

Recursion relations for O and Z (45)

Lemma iso_rec1 U a x:
isomorphism U (Inc Ord) (Inc cum) -> U a x -> U (sigma a) (pow x).
Proof.
intros UI AX. apply (F_unique UI). apply F_rec1. now apply (F_unique UI).
Qed.

Lemma iso_rec2 U x:
isomorphism U (Inc Ord) (Inc cum) -> subsc x Ord -> U (union x) (union (rep x U)).
Proof.
intros UI XO. rewrite <- (rep_equal x (F_unique UI)).
apply (F_unique UI). now apply F_rec2.
Qed.