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