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.

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