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


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

Lemma sigma_increasing:
  increasing sigma.

Lemma sigma_cumulative:
  cumulative sigma.

Lemma sigma_trans:
  trans_pres sigma.

Lemma sigma_WF:
  WF_pres sigma.

Hint Resolve sigma_increasing sigma_cumulative sigma_trans sigma_WF.

Definition Ord := Tower sigma.

Lemma Ord_WF:
  cWF Ord.

Lemma Ord_linear:
  clinear Ord.

Lemma Ord_cumulative:
  ccum Ord.

Lemma Ord_tricho x y:
  Ord x -> Ord y -> x el y \/ x = y \/ y el x.

Lemma Ord_wordered:
  wordered Ord.

Lemma Ord_unreal:
  ~ orealizable (Inc Ord).

Lemma Ord_el_trans x:
  Ord x -> trans x.

Lemma Ord_transitive:
  ctrans Ord.

Lemma Ord_seg_equiv x:
  Ord x -> Seg (Inc Ord) x === class x.

Lemma Ord_representation R:
  worder R -> orealizable R -> exists! x, Ord x /\ simi R (res_seg (Inc Ord) x).

Cumulative hierarchy

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

Lemma expower_increasing:
  increasing expower.

Lemma expower_cumulative:
  cumulative expower.

Lemma expower_trans:
  trans_pres expower.

Lemma expower_WF:
  WF_pres expower.

Hint Resolve expower_increasing expower_cumulative expower_trans expower_WF.

Definition Cum := Tower expower.

Lemma Cum_WF:
  cWF Cum.

Lemma Cum_linear:
  clinear Cum.

Lemma Cum_cumulative:
  ccum Cum.

Lemma Cum_tricho x y:
  Cum x -> Cum y -> x el y \/ x = y \/ y el x.

Lemma Cum_wordered:
  wordered Cum.

Lemma Cum_unreal:
  ~ orealizable (Inc Cum).

Lemma Cum_el_trans x:
  Cum x -> trans x.

Lemma Cum_representation R:
  worder R -> orealizable R -> exists! x, Cum x /\ simi R (res_seg (Inc Cum) x).

Equivalent characterization of cumulative sets (44)

Definition cum := Tower pow.

Lemma power_trans x :
  trans x -> trans (pow x).

Lemma trans_power X :
  trans X <-> X <<= pow X.

Lemma cum_trans x:
  cum x -> trans x.

Lemma cum_pow x:
  cum x -> pow x = expower x.

Lemma cum_Cum x:
  cum x -> Cum x.

Lemma Cum_cum x:
  Cum x -> cum x.

Lemma cum_WF x:
  cum x -> WF x.

Lemma cum_wordered:
  wordered cum.

Lemma cum_linear:
  clinear cum.

Lemma cum_sandwich x y:
  cum x -> cum y -> x << y -> pow x <<= y.

Lemma cum_sandwich' x y:
  cum x -> cum y -> x el y -> pow x <<= y.

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.

Corollary WF_cum_least x:
  WF x -> exists y, least y (fun z => cum z /\ x <<= z).

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.

Lemma F_functional:
  functional F.

Lemma WF_pow_sub x:
  WF x -> pow x <<= x -> False.

Lemma set_partition M:
  (exists x, greatest x (class M)) \/
  (forall x, x el M -> exists y, y el M /\ ~ y <<= x).

Lemma cum_sub_not x y:
  cum x -> cum y -> ~ x <<= y -> y << x.

Lemma cum_partition M:
  subsc M cum -> union M el M \/ M <<= union M.

Lemma cum_least a x:
  least x (fun z => cum z /\ a <<= z) -> a el x -> False.

Lemma F_injective a b x:
  F a x -> F b x -> a = b.

Lemma F_inv_func:
  functional (inv F).

Lemma F_pres1 a b x y:
  F a x -> F b y -> a <<= b -> x <<= y.

Lemma F_pres2 a b x y:
  F a x -> F b y -> x <<= y -> a <<= b.

Lemma sigma_pow a x:
  trans a -> a <<= x -> sigma a <<= pow x.

Lemma F_rec1 a x:
  F a x -> F (sigma a) (pow x).

Lemma F_rec2 x:
  subsc x Ord -> F (union x) (union (rep x F)).

Lemma F_surjective x:
  cum x -> exists a, F a x.

Lemma F_simi:
  similarity F (Inc Ord) (Inc cum).

Lemma F_canon_equiv:
  F o=o Canon (Inc Ord) (Inc cum).

Lemma F_unique U:
  isomorphism U (Inc Ord) (Inc cum) -> F o=o U.

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

Lemma iso_rec2 U x:
  isomorphism U (Inc Ord) (Inc cum) -> subsc x Ord -> U (union x) (union (rep x U)).