Formalisation of "Axiomatic Set Theory in Type Theory" by Gert Smolka
• Version: 16 May 2015
• Author: Dominik Kirst, Saarland University
• This file covers Sections 8 and 9 of the paper
• Acknowlegments: The linearity proof of the class Tower is a porting of the more general proof given by Gert Smolka, Steven SchÃ¤fer and Christian Doczkal (https://www.ps.uni-saarland.de/extras/itp15/)

Require Export orderings sets.

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

General Results of the Paper

Well-Orderings on Sets

Classical set theory, further facts about replacement

Lemma sub_el x y:
~ (x <<= y) -> exists z, z el x /\ ~ z el y.

Lemma sing_el x y:
x <> sing y -> inhab x -> exists z, z el x /\ y <> z.

Definition sur R x :=
forall y, y el x -> exists z, R z y.

Lemma rep_rep x R:
sur R x -> functional R -> functional (inv R) -> x = rep (rep x (inv R)) R.

Lemma rep_equal R S x:
R o=o S -> rep x R = rep x S.

Transitive and well-founded sets

Definition trans x :=
forall y, y el x -> y <<= x.

Inductive WF x: Prop :=
| WFI: subsc x WF -> WF x.

Lemma trans_union x:
subsc x trans -> trans (union x).

Lemma WF_union x:
WF x -> WF (union x).

Lemma WF_no_loop x:
WF x -> x el x -> False.

Properties of orderings

Definition orealizable R :=
realizable (dom R).

Definition complete R :=
~ orealizable R /\ forall x, dom R x -> realizable (Seg R x).

Lemma simi_realizable_iff R S:
simi R S -> orealizable R -> orealizable S.

Lemma complete_simi R S:
worder R -> worder S -> complete R -> complete S -> simi R S.

Lemma real_unreal_seg R S:
worder R -> worder S -> orealizable R -> ~ orealizable S
-> exists x, dom S x /\ simi R (res_seg S x).

Properties of classes

Definition Inc p :=
res sub p.

Definition ctrans p :=
forall x, p x -> subsc x p.

Definition ccum p :=
forall x y, p x -> p y -> (x el y <-> x << y).

Definition cWF p :=
subcc p WF.

Definition clinear p :=
forall x y, p x -> p y -> x <<= y \/ y <<= x.

Definition wordered p :=
worder (Inc p).

Facts about the inclusion ordering (18)

Lemma inc_dom p:
dom (Inc p) === p.

Lemma inc_seg p x:
subcs (Seg (Inc p) x) (pow x).

Lemma cum_seg p x:
ccum p -> subcs (Seg (Inc p) x) x.

Lemma seg_equiv p x:
p x -> ctrans p -> ccum p -> Seg (Inc p) x === class x.

Lemma Inc_partial p:
porder (Inc p).

Lemma Inc_linear p:
clinear p -> linear (Inc p).

Lemma Inc_seg_real p x:
realizable (Seg (Inc p) x).

Lemma Inc_complete p:
~ realizable p -> complete (Inc p).

Linear, cumulative and well-founded classes are well-ordered (20)

Lemma Inc_worder p:
clinear p -> ccum p -> cWF p -> worder (Inc p).

Towers

Section Tower.

Definition increasing f :=
forall x, x <<= f x.

Definition cumulative f :=
forall x, x el f x.

Definition trans_pres f :=
forall x, trans x -> trans (f x).

Definition WF_pres f :=
forall x, WF x -> WF (f x).

Variable f: set -> set.

Inductive Tower: set -> Prop :=
| TU x: subsc x Tower -> Tower (union x)
| TS x: Tower x -> Tower (f x).

Lemma tower_trans x:
trans_pres f -> Tower x -> trans x.

Lemma tower_WF:
WF_pres f -> cWF Tower.

Linearity of the tower class 1. Generalised tower construction
Inductive SegB x: set -> Prop :=
| SBB: SegB x x
| SFB y: SegB x y -> SegB x (f y)
| SLB M: (forall y, y el M -> SegB x y) -> inhab M -> SegB x (union M).

2. The chain that starts on the empty set is exactly the class cum
Lemma tower_SegB x:
Tower x -> (SegB (eset x)) x.

3. The tower construction refines set inclusion
Lemma SegB_sub x y:
increasing f -> SegB x y -> x <<= y.

4. Two lemmas that ease the linearity proof
Definition bounded x M :=
forall y, y el M -> exists z, z el M /\ y <<= z /\ SegB x z.

Lemma relax x M:
inhab M -> bounded x M -> SegB x (union M).

Lemma step x y:
increasing f -> SegB x y -> x = y \/ SegB (f x) y.

Lemma shift x y:
increasing f -> (SegB x y \/ SegB y x) -> (SegB (f x) y \/ SegB y (f x)).

5. Linearity proof
Lemma SegB_linearity_aux M N:
increasing f -> (forall x, x el M -> SegB x (union N) \/ SegB (union N) x) ->
(union M <<= union N -> SegB (union M) (union N) \/ SegB (union N) (union M)) ->
SegB (union M) (union N) \/ SegB (union N) (union M).

Theorem linearity_SegB x y z:
increasing f -> SegB x y -> SegB x z -> SegB y z \/ SegB z y.

Corollary tower_linear:
increasing f -> clinear Tower.

Lemma tower_sandwich x y:
increasing f -> Tower x -> Tower y -> x << y -> f x <<= y.

Well-ordering and representation theorem of towers