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
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).
Facts about completeness (17)
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)
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).
| 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
3. The tower construction refines set inclusion
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)).
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.
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
Lemma tower_cumulative:
increasing f -> cumulative f -> trans_pres f -> WF_pres f -> ccum Tower.
Lemma tower_unrealizable:
increasing f -> cumulative f -> WF_pres f -> ~ realizable Tower.
Lemma tower_norealizable:
increasing f -> cumulative f -> WF_pres f -> ~ orealizable (Inc Tower).
Theorem tower_worder:
increasing f -> cumulative f -> trans_pres f -> WF_pres f
-> wordered Tower /\ complete (Inc Tower).
Lemma tower_representation R:
increasing f -> cumulative f -> trans_pres f -> WF_pres f ->
worder R -> orealizable R -> exists! x, Tower x /\ simi R (res_seg (Inc Tower) x).
End Tower.