Natural Numbers are Ordinals
xlsml
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
xlsml
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
xlsml
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
xlsml
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
xlsml
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 Nonempty set is not the Empty Set
xlsml
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
xlsml
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
xlsml
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
xlsml
set_goal ([], ⌜∀g• galaxy g ⇒ ∀x• x ∈_{g} g ⇒ suc_{o} x ∈_{g} g⌝);
a (rewrite_tac [get_spec ⌜suc_{o}⌝]);
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
xlsml
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 <_{g}_{n} n⌝ THEN1 asm_rewrite_tac [get_spec ⌜$<_{g}_{n}⌝, get_spec ⌜suc_{o}⌝]);
(* *** Goal "1.1" *** *)
a (lemma_tac ⌜t ∈_{g} n⌝ THEN1 asm_rewrite_tac [get_spec ⌜suc_{o}⌝]);
a (all_fc_tac [mem_nat_nat_thm]);
(* *** Goal "1.2" *** *)
a (asm_tac (∀_elim ⌜∅_{g}⌝ galaxy_Gx));
a (asm_rewrite_tac[]);
a (REPEAT (all_asm_fc_tac[GCloseSuc]));
(* *** Goal "2" *** *)
a (asm_rewrite_tac[]);
a (asm_tac (∀_elim ⌜∅_{g}⌝ galaxy_Gx));
a (all_asm_fc_tac[G∅_{g}C]);
val nat_in_G∅_{g}_thm = save_pop_thm "nat_in_G∅_{g}_thm";


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.
xlsml
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∅_{g}C]);
val w_exists_thm = save_pop_thm "w_exists_thm";

