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.
  intros I. subst y. contradiction.
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.