The theory of ordinals in GST
Overview
 This document introduces definitions and derives results relating to ordinal numbers in galactic set theory.
 Introduction A new "ord" theory is created as a child of "gst-ax". The theory will contain the definitions of ordinals and related material for general use, roughly following "Set Theory" by Frank Drake, chapter 2 section 2. The subsections in this document correspondend to the subsections in the book. Definitions 2.1 and 2.3 An ordinal is defined as a transitive and connected set. The usual ordering over the ordinals is defined and also the successor function. Theorem 2.2 We prove that the empty set is an ordinal, and that the members of an ordinal and the successor of an ordinal are ordinals. Theorem 2.4 We prove that the ordinals are linearly ordered by \$
 Theorem 2.7 Induction theorems over ordinals and natural numbers. Theorem 2.8 The set of natural numbers. The Definition of Rank We define the rank of a set. Proof Context In this section we define a proof context for ordinals. Listing of Theory ord
Introduction
 A new "ord" theory is created as a child of "gst-ax". The theory will contain the definitions of ordinals and related material for general use, roughly following "Set Theory" by Frank Drake, chapter 2 section 2. The subsections in this document correspondend to the subsections in the book.
 Motivation This is really motivated purely by interest and self-education. Since its so fundamental I think it likely to turn out handy. Some of the material required is not specific to set theory and is quite widely applicable (in which case I actually develop it elsewhere and then just use it here. Well-foundedness and induction over well-founded relations is the obvious case relevant to this part of Drake. The recursion theorem is the important more general result which appears in the next section in Drake. "more general" means "can be developed as a polymorphic theory in HOL and applied outside the context of set theory". In fact these things have to be developed in the more general context to be used in the ways they are required in the development of set theory, since, for example, one wants to do definitions by recursion over the set membership relation where neither the function defined nor the relevant well-founded relation are actually sets.
Divergence

I have not followed Drake slavishly. More or less, I follow him where it works out OK and looks reasonable and doesn't trigger any of my prejudices.

Sometimes the context in which I am doing the work makes some divergence desirable or necessary. For example, I am doing the work in the context of a slightly eccentric set theory ("Galactic Set Theory") which mainly makes no difference, but has a non-standard formulation of the axiom of foundation. Mainly this is covered by deriving the standard formulation and its consequences and using them where this is used by Drake (in proving the trichotomy theorem). However, the machinery for dealing with well-foundedness makes a difference to how induction principles are best formulated and derived.

Sometimes I look at what he has done and I think, "no way am I going to do that". Not necessarily big things, for example, I couldn't use his definition of successor ordinal which he pretty much admits himself is what we nerds call a kludge.

The Theory ord
The new theory is first created, together with a proof context which we will build up as we develop the theory.
 xl-sml open_theory "gst-ax"; force_new_theory "ord"; new_parent "wf_recp"; force_new_pc "ord"; merge_pcs ["xl_cs_∃_conv"] "ord"; set_merge_pcs ["basic_hol", "gst-ax", "ord"];

Definitions 2.1 and 2.3
 An ordinal is defined as a transitive and connected set. The usual ordering over the ordinals is defined and also the successor function.
The Definition
The concept of transitive set has already been defined in theory gst-ax. The concepts connected and ordinal are now defined.
 xl-holconst connected : GS → BOOL ∀s :GS• connected s ⇔ ∀t u :GS• t ∈g s ∧ u ∈g s ⇒ t ∈g u ∨ t = u ∨ u ∈g t

 xl-holconst ordinal : GS → BOOL ∀s :GS• ordinal s ⇔ transitive s ∧ connected s
We now introduce infix ordering relations over ordinals.
 xl-sml declare_infix(240,"

 xl-holconst \$

 xl-holconst \$≤o : GS → GS → BOOL ∀x y:GS• x ≤o y ⇔ ordinal x ∧ ordinal y ∧ x ∈g y ∨ x = y
The following definition gives the successor function over the ordinals (this appears later in Drake).
 xl-holconst suco : GS → GS ∀x:GS• suco x = x ∪g (Unit x)
Theorem 2.2
 We prove that the empty set is an ordinal, and that the members of an ordinal and the successor of an ordinal are ordinals.
The Empty Set is an Ordinal
First we prove that the empty set is an ordinal, which requires only rewriting with the relevant definitions.
 xl-sml set_goal([],⌜ordinal ∅g⌝); a (rewrite_tac[get_spec ⌜ordinal⌝, get_spec ⌜transitive⌝, get_spec ⌜connected⌝]); val ordinal_∅g = save_pop_thm "ordinal_∅g";

The Successor of an Ordinal is an Ordinal
Next we prove that the successor of an ordinal is an ordinal. This is done in two parts, transitivity and connectedness.
 xl-sml set_goal([], ⌜∀ x:GS• transitive x ⇒ transitive (suco x)⌝);

(proof omitted)
 xl-sml set_goal([],⌜∀ x:GS• connected x ⇒ connected (suco x) ⌝);

(proof omitted)
These together enable us to prove:
 xl-sml set_goal([],⌜∀ x:GS• ordinal x ⇒ ordinal (suco x)⌝);

The proof expands using the definition of ordinal, strips the goal and reasons forward from the resulting assumptions using the two lemmas proved above.
 xl-sml a (rewrite_tac[get_spec ⌜ordinal⌝] THEN REPEAT strip_tac THEN fc_tac [trans_suc_trans, conn_suc_conn]); val ord_suc_ord_thm = save_pop_thm "ord_suc_ord_thm";

The members of an Ordinal are Ordinals
We now aim to prove that the members of an ordinal are ordinals. We do this by proving first that they are connected and then that they are transitive. First however, we show that any subset of a connected set is connected.
 xl-sml set_goal([],⌜ ∀ x:GS• connected x ⇒ ∀ y:GS• y ⊆g x ⇒ connected y ⌝);

The proof consists of expanding appropriate definitions, stripping the goal and then reasoning forward from the assumptions.
 xl-sml a (rewrite_tac (map get_spec [⌜connected⌝, ⌜\$⊆g⌝]) THEN REPEAT_N 7 strip_tac);

 xl-gft (* *** Goal "" *** *) (* 4 *) ⌜∀ t u• t ∈g x ∧ u ∈g x ⇒ t ∈g u ∨ t = u ∨ u ∈g t⌝ (* 3 *) ⌜∀ e• e ∈g y ⇒ e ∈g x⌝ (* 2 *) ⌜t ∈g y⌝ (* 1 *) ⌜u ∈g y⌝ (* ?⊢ *) ⌜t ∈g u ∨ t = u ∨ u ∈g t⌝

 xl-sml a (all_asm_fc_tac[]); a (REPEAT_N 2 (asm_fc_tac[]) THEN REPEAT strip_tac); val conn_sub_conn = save_pop_thm "conn_sub_conn";

Now we show that any member of an ordinal is an ordinal.
 xl-sml set_goal([],⌜ ∀ x:GS• ordinal x ⇒ ∀ y:GS• y ∈g x ⇒ connected y ⌝);

Expanding the definition of ordinal and making use of transitivity enables us to infer that members of an ordinals are subsets and permits application of the previous result to obtain connectedness.
 xl-sml a (rewrite_tac (map get_spec [⌜ordinal⌝, ⌜transitive⌝]) THEN REPEAT strip_tac); a (all_asm_fc_tac []); a (all_asm_fc_tac [conn_sub_conn]); val conn_mem_ord = save_pop_thm "conn_mem_ord";

To prove that the members of an ordinal are transitive, well-foundedness is needed. First we prove the particular consequences of well-foundedness which are required (these results really belong somewhere else).
 xl-sml set_goal([], ⌜ ∀ x:GS• ¬ x ∈g x ⌝);

The proof uses well-founded transfinite induction over the membership relation.
 xl-sml a (asm_tac (gs_wf_ind_thm)); a (spec_nth_asm_tac 1 ⌜λx• ¬ x ∈g x⌝);

 xl-gft (* *** Goal "1" *** *) (* 3 *) ⌜∀ s• (∀ x• (∀ y• y ∈g x ⇒ s y) ⇒ s x) ⇒ (∀ x• s x)⌝ (* 2 *) ⌜∀ y• y ∈g x ⇒ (λ x• ¬ x ∈g x) y⌝ (* 1 *) ⌜¬ (λ x• ¬ x ∈g x) x⌝ (* ?⊢ *) ⌜∀ x• ¬ x ∈g x⌝

 xl-sml a (swap_nth_asm_concl_tac 1 THEN rewrite_tac[] THEN swap_nth_asm_concl_tac 1 THEN ALL_ASM_FC_T (MAP_EVERY ante_tac) [] THEN asm_rewrite_tac[]);

 xl-gft (* *** Goal "2" *** *) (* 2 *) ⌜∀ s• (∀ x• (∀ y• y ∈g x ⇒ s y) ⇒ s x) ⇒ (∀ x• s x)⌝ (* 1 *) ⌜∀ x• (λ x• ¬ x ∈g x) x⌝ (* ?⊢ *) ⌜∀ x• ¬ x ∈g x⌝

 xl-sml a (strip_tac THEN swap_nth_asm_concl_tac 1 THEN rewrite_tac[] THEN REPEAT strip_tac THEN ∃_tac ⌜x⌝ THEN asm_rewrite_tac[]); val wf_l1 = save_pop_thm "wf_l1";

 xl-sml set_goal([], ⌜∀ x y:GS• ¬ (x ∈g y ∧ y ∈g x)⌝);

 xl-sml set_goal([], ⌜∀ x y z:GS• ¬ (x ∈g y ∧ y ∈g z ∧ z ∈g x)⌝);

Now we are ready to prove that the members of an ordinal are transitive.
 xl-sml set_goal([], ⌜∀ x:GS• ordinal x ⇒ ∀ y:GS• y ∈g x ⇒ transitive y⌝);

Finally we prove that all members of an ordinal are ordinals.
 xl-sml set_goal([], ⌜∀ x:GS• ordinal x ⇒ ∀ y:GS• y ∈g x ⇒ ordinal y⌝);

Galaxies are Closed under the Successor Relationship
We need this result later to show that the natural numbers are a set.
 xl-sml set_goal([], ⌜∀g x• galaxy g ∧ x ∈g g ⇒ suco x ∈g g⌝); a (REPEAT strip_tac THEN rewrite_tac [get_spec ⌜suco⌝]); a (REPEAT (all_asm_fc_tac [GCloseUnit, GClose∪g])); val GCloseSuco = save_pop_thm "GCloseSuco";

Theorem 2.4
 We prove that the ordinals are linearly ordered by \$
First we prove some lemmas:
 xl-sml set_goal([], ⌜∀ x y:GS• transitive x ∧ transitive y ⇒ transitive (x ∩g y)⌝);

 xl-sml set_goal([], ⌜∀ x y:GS• transitive x ∧ transitive y ⇒ transitive (x ∪g y)⌝);

 xl-sml set_goal([], ⌜∀ x y:GS• connected x ∧ connected y ⇒ connected (x ∩g y)⌝);

 xl-sml set_goal([], ⌜∀ x y:GS• ordinal x ∧ ordinal y ⇒ ordinal (x ∩g y)⌝);

 xl-sml set_goal([], ⌜∀ x y:GS• ordinal x ∧ ordinal y ∧ x ⊆g y ∧ ¬ x = y ⇒ x ∈g y⌝);

 xl-sml set_goal([], ⌜∀ x y:GS• ordinal x ∧ ordinal y ⇒ ordinal (x ∪g y)⌝);

 xl-sml set_goal([], ⌜∀ x y:GS• ordinal x ∧ ordinal y ⇒ x

Definition 2.6
 Successor and limit ordinals are defined. Natural numbers are defined.
These definitions are not the ones used by Drake, and not only the names but the concepts differ. My successor predicate does not hold of the empty set. I use the name "natural number" where he talks of integers, and generally I'm chosing longer names.
 xl-holconst successor : GS → BOOL ∀s :GS• successor s ⇔ ∃t• ordinal t ∧ s = suco t

 xl-holconst limit_ordinal : GS → BOOL ∀s :GS• limit_ordinal s ⇔ ordinal s ∧ ¬ successor s ∧ ¬ s = ∅g

 xl-holconst natural_number : GS → BOOL ∀s :GS• natural_number s ⇔ s = ∅g ∨ (successor s ∧ ∀t• t∈g s ⇒ t = ∅g ∨ successor t)
Theorem 2.7
 Induction theorems over ordinals and natural numbers.
Successors are Ordinals

 xl-sml set_goal([],⌜∀ x:GS• successor x ⇒ ordinal x⌝); a (rewrite_tac[get_spec ⌜successor⌝] THEN REPEAT strip_tac THEN fc_tac [ord_suc_ord_thm] THEN asm_rewrite_tac[]); val successor_ord_thm = save_pop_thm "successor_ord_thm";

Well-foundedness of the ordinals
First we prove that <o is well-founded.
 xl-sml set_goal([],⌜well_founded \$

Ordering the Natural Numbers
To get an induction principle for the natural numbers we first define a well-founded ordering over them. Since I don't plan to use this a lot I use the name <gn (less than over the natural numbers defined in galactic set theory).
 xl-sml declare_infix(240,"

 xl-holconst \$
Now we try to find a better proof that the one above that this is well-founded. And fail, this is just a more compact rendition of the same proof.
 xl-sml set_goal([],⌜well_founded \$

This allows us to do well-founded induction over the natural number which the way I have implemented it is "course-of-values" induction. However, for the sake of form I will prove that induction principle as an explicit theorem. This is just what you get by expanding the definition of well-foundedness in the above theorem.
 xl-sml val nat_induct_thm = save_thm ("nat_induct_thm", (rewrite_rule [get_spec ⌜well_founded⌝] wf_nat_thm));

Note that this theorem can only be used to prove properties which are true of all sets, so you have to make it conditional (natural_number n ⇒ whatever). I suppose I'd better do another one.
 xl-sml set_goal([], ⌜∀ p• (∀ x• natural_number x ∧ (∀ y• y

I've tried using that principle and it too has disadvantages. Because <gn is used the induction hypothesis is more awkward to use (weaker) than it would have been if ∈g had been used. Unfortunately the proof of an induction theorem using plain set membership is not entirely trivial, so its proof has to be left til later.
 xl-sml set_goal([], ⌜∀ p• (∀ x• natural_number x ∧ (∀ y• y ∈g x ⇒ p y) ⇒ p x) ⇒ (∀ x• natural_number x ⇒ p x)⌝);

Theorem 2.8
 The set of natural numbers.
Natural Numbers are Ordinals

 xl-sml set_goal ([], ⌜∀n• natural_number n ⇒ ordinal n⌝); a (rewrite_tac [get_spec ⌜natural_number⌝, get_spec ⌜successor⌝]); a (REPEAT strip_tac THEN_TRY asm_rewrite_tac[ordinal_∅g]); a (all_fc_tac [ord_suc_ord_thm]); val ord_nat_thm = save_pop_thm "ord_nat_thm";

Members of Natural Numbers are Ordinals

 xl-sml set_goal ([], ⌜∀n• natural_number n ⇒ ∀m• m ∈g n ⇒ ordinal m⌝); a (REPEAT strip_tac); a (REPEAT (all_fc_tac[ord_nat_thm, ord_mem_ord])); val mem_nat_ord_thm = save_pop_thm "mem_nat_ord_thm";

An Ordinal is Zero, a successor or a limit

 xl-sml set_goal ([], ⌜∀n• ordinal n ⇒ n = ∅g ∨ successor n ∨ limit_ordinal n⌝); a (rewrite_tac [get_spec ⌜limit_ordinal⌝, get_spec ⌜successor⌝]); a (REPEAT strip_tac); a (spec_nth_asm_tac 2 ⌜t⌝); val ordinal_kind_thm = save_pop_thm "ordinal_kind_thm";

A Natural Number is not a Limit Ordinal

 xl-sml set_goal ([], ⌜∀n• natural_number n ⇒ ¬ limit_ordinal n⌝); a (rewrite_tac [get_spec ⌜limit_ordinal⌝, get_spec ⌜natural_number⌝]); a (REPEAT strip_tac); val nat_not_lim_thm = save_pop_thm "nat_not_lim_thm";

A Natural Number is zero or a successor

 xl-sml set_goal ([], ⌜∀n• natural_number n ⇒ successor n ∨ n = ∅g⌝); a (rewrite_tac [get_spec ⌜natural_number⌝]); a (REPEAT strip_tac); val nat_zero_or_suc_thm = save_pop_thm "nat_zero_or_suc_thm";

A Non-empty set is not the Empty Set

 xl-sml set_goal ([], ⌜∀m n• m ∈g n ⇒ ¬ n = ∅g⌝); a (prove_tac [gst_opext_clauses, gst_relext_clauses]); val mem_not_empty_thm = save_pop_thm "mem_not_empty_thm";

A Natural Number does not contain a Limit Ordinal

 xl-sml set_goal ([], ⌜∀m n• natural_number n ∧ m ∈g n ⇒ ¬ limit_ordinal m⌝); a (rewrite_tac [get_spec ⌜limit_ordinal⌝, get_spec ⌜natural_number⌝]); a (REPEAT strip_tac); (* *** Goal "1" *** *) a (all_fc_tac [mem_not_empty_thm]); (* *** Goal "2" *** *) a (all_asm_fc_tac[]); val mem_nat_not_lim_thm = save_pop_thm "mem_nat_not_lim_thm";

All Members of Natural Numbers are Natural Numbers

 xl-sml set_goal ([], ⌜∀n• natural_number n ⇒ ∀m• m ∈g n ⇒ natural_number m⌝); a (rewrite_tac [get_spec ⌜natural_number⌝]); a (REPEAT strip_tac THEN_TRY all_asm_fc_tac [mem_not_empty_thm]); a (lemma_tac ⌜transitive n⌝ THEN1 (REPEAT (all_fc_tac [get_spec ⌜ordinal⌝, successor_ord_thm]))); a (lemma_tac ⌜t ∈g n⌝ THEN1 (EVERY [all_fc_tac [get_spec ⌜transitive⌝], POP_ASM_T ante_tac, rewrite_tac [gst_relext_clauses], asm_prove_tac[]])); a (all_asm_fc_tac[]); val mem_nat_nat_thm = save_pop_thm "mem_nat_nat_thm";

Galaxies are Closed under suc

 xl-sml set_goal ([], ⌜∀g• galaxy g ⇒ ∀x• x ∈g g ⇒ suco x ∈g g⌝); a (rewrite_tac [get_spec ⌜suco⌝]); a (REPEAT strip_tac); a (REPEAT (all_fc_tac [GClose∪g, GCloseUnit])); val GCloseSuc = save_pop_thm "GCloseSuc";

Natural Numbers are in the Smallest Galaxy

 xl-sml set_goal ([], ⌜∀n• natural_number n ⇒ n ∈g Gx ∅g⌝); a (strip_tac THEN gen_induction_tac1 nat_induct_thm2); a (fc_tac [nat_zero_or_suc_thm]); (* *** Goal "1" *** *) a (fc_tac [get_spec ⌜successor⌝]); a (lemma_tac ⌜t

The Existence of w
This comes from the axiom of infinity, however, in galactic set theory we get that from the existence of galaxies, so the following proof is a little unusual.
 xl-sml set_goal ([], ⌜∃w• ∀z• z ∈g w ⇔ natural_number z⌝); a (∃_tac ⌜Sep (Gx ∅g) natural_number⌝ THEN rewrite_tac [gst_opext_clauses]); a (rewrite_tac [all_∀_intro (taut_rule ⌜(a ∧ b ⇔ b) ⇔ b ⇒ a⌝)]); a strip_tac; a (gen_induction_tac1 nat_induct_thm2); a (fc_tac [nat_zero_or_suc_thm]); (* *** Goal "1" *** *) a (fc_tac [get_spec ⌜successor⌝, nat_in_G∅g_thm]); (* *** Goal "2" *** *) a (asm_rewrite_tac []); a (asm_tac (∀_elim ⌜∅g⌝ galaxy_Gx)); a (all_asm_fc_tac[G∅gC]); val w_exists_thm = save_pop_thm "w_exists_thm";

The Definition of Rank
 We define the rank of a set.
The Consistency Proof
Before introducing the definition of rank we undertake the proof necessary to establish that the definition is conservative. The key lemma in this proof is the proof that the relevant functional "respects" the membership relation.
 xl-sml set_goal([],⌜(λf• λx• ⋃g (Imagep (suco o f) x)) respects \$∈g⌝); a (rewrite_tac [get_spec ⌜\$respects⌝] THEN REPEAT strip_tac); a (once_rewrite_tac [gst_relext_clauses] THEN REPEAT strip_tac); (* *** Goal "1" *** *) a (∃_tac ⌜e'⌝ THEN REPEAT strip_tac); a (∃_tac ⌜e''⌝ THEN REPEAT strip_tac); a (POP_ASM_T ante_tac THEN rewrite_tac[get_spec⌜\$o⌝] THEN strip_tac); a (lemma_tac ⌜h e'' = g e''⌝ THEN1 (REPEAT_N 2 (asm_fc_tac[tc_incr_thm]) THEN asm_rewrite_tac[])); a (asm_rewrite_tac[]); (* *** Goal "2" *** *) a (∃_tac ⌜e'⌝ THEN REPEAT strip_tac); a (∃_tac ⌜e''⌝ THEN REPEAT strip_tac); a (POP_ASM_T ante_tac THEN rewrite_tac[get_spec⌜\$o⌝] THEN strip_tac); a (lemma_tac ⌜h e'' = g e''⌝ THEN1 (REPEAT_N 2 (asm_fc_tac[tc_incr_thm]) THEN asm_rewrite_tac[])); a (asm_rewrite_tac[]); val respect_lemma = pop_thm();

Armed with that lemma we can now prove that the function which we will call "rank" exists.
 xl-sml set_goal([],⌜∃rank• ∀x• rank x = ⋃g (Imagep (suco o rank) x)⌝); a (∃_tac ⌜fix (λf• λx• ⋃g (Imagep (suco o f) x))⌝ THEN strip_tac); a (asm_tac gs_wf_axiom); a (asm_tac respect_lemma); a (fc_tac [∀_elim ⌜λf• λx• ⋃g (Imagep (suco o f) x)⌝ (get_spec ⌜fix⌝)]); a (asm_fc_tac []); a (POP_ASM_T (rewrite_thm_tac o rewrite_rule [ext_thm])); val _ = xl_set_cs_∃_thm (pop_thm());

 xl-holconst rank : GS → GS ∀x• rank x = ⋃g (Imagep (suco o rank) x)
Proof Context
 In this section we define a proof context for ordinals.
Proof Context

 xl-sml add_pc_thms "ord" ([]); set_merge_pcs ["basic_hol", "gst-ax", "ord"]; commit_pc "ord";