Formalisation of "Axiomatic Set Theory in Type Theory" by Gert Smolka

Version: 16 May 2015
Author: Dominik Kirst, Saarland University
This file covers Sections 2, 6 and 7 of the paper

Global Set Implicit Arguments.
Global
Require Export Classical_Pred_Type Classical_Prop.

Ltac indirect :=
  match goal with
    | [ |- ?H ] => destruct (classic H); auto; exfalso
  end.

Well-Orderings in Type Theory

Notation for sub-classes and sub-orderings

Notation "p '<<=' q" := (forall x, p x -> q x) (at level 70).
Notation "p '===' q" := (p <<= q /\ q <<= p) (at level 70).
Notation "R 'o=' S" := (forall x y, R x y -> S x y) (at level 70).
Notation "R 'o=o' S" := (R o = S /\ S o = R) (at level 70).

Lemma sub_trans1 X (p: X -> Prop) q r:
p <<= q -> q <<= r -> p <<= r.

Lemma sub_trans2 X Y (R: X -> Y -> Prop) S T:
R o = S -> S o = T -> R o = T.

Definitions for binary relations

Definition inv X Y (U: X -> Y -> Prop) x y :=
  U y x.

Definition dom X Y (U: X -> Y -> Prop) x :=
  exists y, U x y.

Definition functional X Y (U: X -> Y -> Prop) :=
  forall x y y', U x y -> U x y' -> y = y'.

Definition expansion X Y (U: X -> Y -> Prop) a b :=
  fun x y => U x y \/ x = a /\ y = b.

Lemma inv_sub X Y (U: X -> Y -> Prop) (V: X -> Y -> Prop):
  U o = V -> (inv U ) o = (inv V ).

Theory of Well-Orderings

Definitions for orderings

Definition reflexive X (R: X -> X -> Prop) :=
  forall x y, R x y -> R x x /\ R y y.

Definition antisym X (R: X -> X -> Prop) :=
  forall x y, R x y -> R y x -> x = y.

Definition transitive X (R: X -> X -> Prop) :=
  forall x y z, R x y -> R y z -> R x z.

Definition linear X (R: X -> X -> Prop) :=
  forall x y, dom R x -> dom R y -> R x y \/ R y x.

Definition porder X (R: X -> X -> Prop) :=
  reflexive R /\ antisym R /\ transitive R.

Definition Least X (R: X -> X -> Prop) p x :=
  p x /\ forall y, p y -> R x y.

Definition Segs X (R: X -> X -> Prop) (p: X -> Prop) :=
  (p <<= dom R ) /\ (forall x y, R x y -> p y -> p x ).

Definition Seg X (R: X -> X -> Prop) x y :=
  R y x /\ x <> y.

Definition res X (R: X -> X -> Prop) p x y :=
  p x /\ p y /\ R x y.

Definition least_inhab X (R: X -> X -> Prop) :=
  forall (p: X -> Prop), ex p -> p <<= dom R -> ex (Least R p).

Definition worder X (R: X -> X -> Prop) :=
  porder R /\ least_inhab R.

Definition res_seg X (R: X -> X -> Prop) a x y :=
  (Seg R a) x /\ (Seg R a) y /\ R x y.

Lemma res_sub1 X (R: X -> X -> Prop) p:
  dom (res R p) <<= dom R.

Lemma res_sub2 X (R: X -> X -> Prop) p:
  dom (res R p) <<= p.

Lemma res_sub X (R: X -> X -> Prop) (p: X -> Prop) x:
  worder R -> p x -> dom R x -> dom (res R p) x.

Lemma seg_segs X (R: X -> X -> Prop) x:
  worder R -> dom R x -> Segs R (Seg R x).

Facts about well-orderings (8)

Lemma least_inhab_linear X (R: X -> X -> Prop):
  least_inhab R -> linear R.

Lemma worder_linear X (R: X -> X -> Prop):
  worder R -> linear R.

Lemma linear_Segs X (R: X -> X -> Prop) p q:
  linear R -> Segs R p -> Segs R q -> p <<= q \/ q <<= p.

Lemma worder_Segs X (R: X -> X -> Prop) p:
  worder R -> Segs R p -> (p === dom R ) \/ (exists x, dom R x /\ p === Seg R x ).

Lemma worder_sub X (R: X -> X -> Prop) p:
  worder R -> worder (res R p).

Lemma worder_equiv X (R: X -> X -> Prop) (S: X -> X -> Prop):
  worder R -> R o =o S -> worder S.

Well-founded induction (9)

Inductive W X (R: X -> X -> Prop) x: Prop :=
| WI: Seg R x <<= W R -> W R x.

Definition wfounded X (R: X -> X -> Prop) :=
dom R <<= W R.

Lemma worder_wfounded X (R: X -> X -> Prop):
worder R -> wfounded R.

Similarities and Isomorphisms

Definitions of Similarities

Definition simulative X Y (U: X -> Y -> Prop) R S :=
  forall x x' y, U x y -> R x' x -> exists y', U x' y' /\ S y' y.

Definition simulation X Y (U: X -> Y -> Prop) R S :=
  dom U <<= dom R /\ simulative U R S.

Definition similarity X Y (U: X -> Y -> Prop) R S :=
  simulation U R S /\ functional U /\
  simulation (inv U) S R /\ functional (inv U).

Definition isomorphism X Y (U: X -> Y -> Prop) R S :=
  similarity U R S /\ dom R <<= dom U /\ dom S <<= dom (inv U).

Definition simi X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) :=
  exists U, isomorphism U R S.

Definition maxisim X Y (U: X -> Y -> Prop) R S :=
  similarity U R S /\ (dom R <<= dom U \/ dom S <<= dom (inv U)).

Definition Canon X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) x y :=
  exists U, similarity U R S /\ U x y.

Facts about similarities

Lemma simi_inv X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> similarity (inv U) S R.

Lemma iso_inv X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
isomorphism U R S -> isomorphism (inv U) S R.

Lemma simi_simu1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> simulative U R S.

Lemma simi_simu2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> simulative (inv U) S R.

Lemma simi_com X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  simi R S -> simi S R.

Lemma simulation_dom X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  simulation U R S -> Segs R (dom U).

Lemma simi_eq1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
  similarity U R S -> U x y -> U x' y' -> x = x' -> y = y'.

Lemma simi_eq2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
  similarity U R S -> U x y -> U x' y' -> y = y' -> x = x'.

Lemma simi_neq1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
  similarity U R S -> U x y -> U x' y' -> y <> y' -> x <> x'.

Lemma simi_neq2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
  similarity U R S -> U x y -> U x' y' -> x <> x' -> y <> y'.

Lemma simi_rewrite X Y (R: X -> X -> Prop) (S S': Y -> Y -> Prop) U:
  similarity U R S -> S o =o S' -> similarity U R S'.

Facts about domains and restrictions of similarities (13)

Lemma simi_dom1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  similarity U R S -> Segs R (dom U).

Lemma simi_dom2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  similarity U R S -> Segs S (dom (inv U)).

Lemma similarity_res X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  worder R -> worder S ->
  similarity U R S -> similarity U R (res S (dom (inv U))).

Lemma simi_res X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  worder R -> worder S ->
  similarity U R S -> dom U === dom R -> isomorphism U R (res S (dom (inv U))).

Lemma similarity_res' X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  worder R -> worder S ->
  similarity U R S -> similarity U (res R (dom U)) S.

Lemma simi_res' X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  worder R -> worder S ->
  similarity U R S -> dom (inv U) === dom S -> isomorphism U (res R (dom U)) S.

Agreement and linearity of similarities (14)

Lemma simi_wfounded X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y:
  worder R -> worder S ->
  similarity U R S -> U x y -> W R x.

Lemma simi_agree X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V x y y':
  worder R -> worder S ->
  similarity U R S -> similarity V R S -> U x y -> V x y' -> y = y'.

Lemma simi_domain_sub X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V:
  worder R -> worder S ->
  similarity U R S -> similarity V R S -> dom U <<= dom V -> U o = V.

Lemma simi_lin X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V:
  worder R -> worder S ->
  similarity U R S -> similarity V R S -> U o = V \/ V o = U.

Lemma maxi_sub X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V:
  worder R -> worder S -> similarity U R S -> maxisim V R S -> U o = V.

Embedding theorem (15)

Lemma canon_simulative1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  simulative (Canon R S) R S.

Lemma canon_simulative2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  simulative (inv (Canon R S)) S R.

Lemma canon_simi X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  worder R -> worder S -> similarity (Canon R S) R S.

Lemma exp_simulative1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U a b:
  worder R -> worder S -> similarity U R S ->
  Least R (fun c => dom R c /\ ~ dom U c) a ->
  Least S (fun c => dom S c /\ ~ dom (inv U) c) b ->
  simulative (expansion U a b) R S.

Lemma exp_simulative2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U a b:
  worder R -> worder S -> similarity U R S ->
  Least R (fun c => dom R c /\ ~ dom U c) a ->
  Least S (fun c => dom S c /\ ~ dom (inv U) c) b ->
  simulative (inv (expansion U a b)) S R.

Lemma exp_simi X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U a b:
  worder R -> worder S -> similarity U R S ->
  Least R (fun c => dom R c /\ ~ dom U c) a ->
  Least S (fun c => dom S c /\ ~ dom (inv U) c) b ->
  similarity (expansion U a b) R S.

Lemma canon_max X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  worder R -> worder S -> maxisim (Canon R S) R S.

Lemma canon_unique X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  worder R -> worder S -> maxisim U R S -> U o =o Canon R S.

Lemma embedding X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  worder R -> worder S ->
  (exists p, Segs R p /\ simi (res R p) S ) \/
  (exists q, Segs S q /\ simi R (res S q)).

Segments are equivalent iff they are isomorphic (16)

Lemma seg_equal X (R: X -> X -> Prop) x y:
  worder R -> dom R x -> dom R y -> Seg R x === Seg R y -> x = y.

Lemma simi_sub X (R: X -> X -> Prop) p q:
  worder R -> Segs R p -> Segs R q -> simi (res R p) (res R q) -> p <<= q.

Lemma simi_equiv X (R: X -> X -> Prop) p q:
  worder R -> Segs R p -> Segs R q -> simi (res R p) (res R q) -> p === q.

Lemma equiv_simi X (R: X -> X -> Prop) p q:
  worder R -> Segs R p -> Segs R q -> p === q -> simi (res R p) (res R q).

Lemma simi_trans X (R: X -> X -> Prop) (S1: X -> X -> Prop) (S2: X -> X -> Prop):
  simi R S1 -> simi R S2 -> simi S1 S2.