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 (

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

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)

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


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