Introduction

Primitive Types and Constants

Definitions

The Zero Axiom
xlsml
new_axiom (["SZeroAx"], ⌜∀x• rank x = ∅ ≡ x = ∅⌝ );


The Cut Axiom
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).

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.
xlsml
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.
xlsml
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))))
⌝);


