Miscellaneous work using gst.
Overview
 Miscellaneous proof work using the gst axioms.
 Introduction Proof of a putative strong infinity axiom for HOL and a speculative axiomatisation for the surreal numbers in HOL. Strong Infinity in HOL This section demonstrates the truth of a proposed strong infinity principle.
 Axioms for the Surreal Numbers This section supplies an axiomatisation of surreal numbers independent of set theory. Listing of Theory gst-misc Listing of Theory surreal
Introduction
 Proof of a putative strong infinity axiom for HOL and a speculative axiomatisation for the surreal numbers in HOL.
Motivation
The idea here is that instead of axiomatising set theory in Higher Order Logic you chose a strong axiom of infinity and then develop one or more set theories by conservative extension.
The Theory gst-misc

 xl-sml open_theory "gst-ax"; force_new_theory "gst-misc"; force_new_pc "gst-misc"; merge_pcs ["xl_cs_∃_conv"] "gst-misc"; set_merge_pcs ["basic_hol", "gst-ax", "gst-misc"];

Strong Infinity in HOL
 This section demonstrates the truth of a proposed strong infinity principle.
Strong Infinity using Sets
The purpose of this section is to verify the consistency of a proposed axiom of infinity relative to the axioms of GST in HOL by proving that the axiom is true of the type GS. (It is intended to be asserted of IND). The axiom will then be asserted in a theory higher up the tree, and eventually the axiomatization of GST will be replaced by a conservative extension of that theory.
 xl-sml set_goal([], ⌜∃e: GS → GS → BOOL• ∀p• ∃q• (e p q ∧ (∀x• e x q ⇒ ( (∃y• e y q ∧ ∀Z• ∃z• e z y ∧ ∀v• e v z ≡ e v x ∧ (Z v)) ∧ (∀f•(∀u• e u x ⇒ e (f u) q) ⇒ ∃y• e y q ∧ ∀u• e u x ⇒ e (f u) y)))) ⌝); a (∃_tac ⌜\$∈g⌝ THEN strip_tac); a (strip_asm_tac (∀_elim ⌜p⌝ galaxies_∃_thm)); a (∃_tac ⌜g⌝ THEN REPEAT strip_tac); (* *** Goal "1" *** *) a (∃_tac ⌜℘g x⌝ THEN REPEAT strip_tac); (* *** Goal "1.1" *** *) a (all_fc_tac [get_spec ⌜galaxy⌝]); (* *** Goal "1.2" *** *) a (∃_tac ⌜Sep x Z⌝ THEN rewrite_tac[gst_relext_clauses] THEN REPEAT strip_tac); (* *** Goal "2" *** *) a (∃_tac ⌜Imagep f x⌝ THEN rewrite_tac[] THEN REPEAT strip_tac); (* *** Goal "2.1" *** *) a (lemma_tac ⌜Imagep f x ⊆g g⌝ THEN1 (rewrite_tac [get_spec ⌜\$⊆g⌝, get_spec ⌜Imagep⌝] THEN REPEAT strip_tac THEN asm_rewrite_tac[] THEN REPEAT (asm_fc_tac[]))); a (fc_tac[GImagepC]); a (list_spec_nth_asm_tac 1 [⌜x⌝, ⌜f⌝]); (* *** Goal "2.2" *** *) a (∃_tac ⌜u⌝ THEN asm_rewrite_tac[]); val strong_infinity_thm = save_pop_thm "strong_infinity_thm";

Strong Infinity using Ordinals
A version of the strong infinity axiom phrased as if about ordinal numbers has also been formulated, and may be found documented but not asserted in the theory "strong_infinity".
Axioms for the Surreal Numbers
 This section supplies an axiomatisation of surreal numbers independent of set theory.
Introduction
Primitive Types and Constants

 xl-sml new_theory "surreal"; new_parent "wf_relp"; new_type ("No", 0); new_const ("∅s", No⌝); declare_alias ("∅", ⌜∅s⌝); new_const ("

Definitions

 xl-holconstrank: No → No ∀n• rank n = IC (λx•T) n

 xl-holconst\$<<: No → No → BOOL ∀n m• n << m = rank n < rank m
The Zero Axiom

 xl-sml new_axiom (["SZeroAx"], ⌜∀x• rank x = ∅ ≡ x = ∅⌝ );

The Cut Axiom
The following axiom states that, for:
1. any property p of surreals and
2. surreal n such that p is downward closed on the surreals of lower rank than n
there exists a surreal number (IC p n) such that:
• (IC p n) is in between the surreals of rank less than n with the property and those of rank less than n without the property, and
• where p and q define the same cut on the surreals of rank less than n then (IC p n) is the same surreal as (IC q n).

 xl-sml new_axiom (["SCutAx"], ⌜∀p: No → BOOL; n: No• (∀x y: No• x << n ∧ y << n ∧ x < y ∧ p y ⇒ p x) ⇒ (∀x: No• x << n ⇒ (p x ≡ x < (IC p n)) ∧ (¬ p x ≡ (IC p n) < x)) ∧ (∀q: No → BOOL• (∀x• x << n ⇒ (p x ≡ q x)) ≡ (IC p n) = (IC q n)) ⌝);

The Induction Axiom

The following axiom states that for any property p of surreals, if p holds for a surreal n whenever it holds for all the surreals of lower rank than n, then it holds for all surreals.

This is the same as Conway's induction axiom since the union of the two sides of the canonical cuts ("games") on which this axiomatization is based is the set of all numbers of lower rank.

 xl-sml new_axiom (["SIndAx"], ⌜well_founded \$<<⌝);

Strong Infinity
This is the ordinal version of my strong infinity for HOL axiom, asserted of the surreals rather than the individuals. I have a fairly low level of confidence in this as yet. I don't know whether it's best to assert it of "<<", or of "<<" restricted to ordinals.
 xl-sml declare_infix (240, "e"); new_axiom (["SInfAx"], ⌜∀p:No• ∃q• (p << q ∧ (∀x• x << q ⇒ ( (∃y \$e• y << q ∧ (∀Z• ∃u• u << y ∧ (∀v• v << x ⇒ (v e u ≡ Z v)))) ∧ (∀G•(∀u• u << x ⇒ (G u) << q) ⇒ ∃y• y << q ∧ ∀u• u << x ⇒ (G u) << y)))) ⌝);