Proof of a putative strong infinity axiom for HOL and a speculative axiomatisation for the surreal numbers in HOL.

This section demonstrates the truth of a proposed strong infinity principle.

This section supplies an axiomatisation of surreal numbers independent of set theory.

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.

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"];

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

BOOL

(e p q

(

e x q

(

e y q

e z y

e v z

e v x

(Z v))

(

e u x

e (f u) q)

e y q

e u x

e (f u) y))))

);
a (

_tac

THEN strip_tac);
a (strip_asm_tac (

_elim

galaxies_

_thm));
a (

_tac

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

, 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 [

]);
(* *** Goal "2.2" *** *)
a (

_tac

THEN asm_rewrite_tac[]);
val strong_infinity_thm = save_pop_thm "strong_infinity_thm";

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".

xl-sml

new_theory "surreal";
new_parent "wf_relp";
new_type ("No", 0);
new_const ("

_s",

);
declare_alias ("

);
new_const ("<_s",

BOOL

);
declare_alias ("<",

<_s

);
new_const ("IC",

(No

BOOL)

);
declare_infix (240, "<<");

xl-holconst

╷

rank: No

╷

rank n = IC (

T) n

xl-holconst

╷

$<<: No

BOOL

╷

n m

n << m = rank n < rank m

xl-sml

new_axiom (["SZeroAx"],

rank x =

x =

);

The following axiom states that, for:

any property p of surreals and
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 << n

(p x

q x))

(IC p n) = (IC q n))

);

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 $<<

);

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

(p << q

(

x << q

(

y $e

y << q

(

u << y

(

v << x

(v e u

Z v))))

(

u << x

(G u) << q)

y << q

u << x

(G u) << y))))

);