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.

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.