Beginning of Section TaggedSets
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Axiom. (not_TransSet_Sing1) We take the following as an axiom:
¬ TransSet {1}
Axiom. (not_ordinal_Sing1) We take the following as an axiom:
¬ ordinal {1}
Axiom. (tagged_not_ordinal) We take the following as an axiom:
∀y, ¬ ordinal (y ')
Axiom. (tagged_notin_ordinal) We take the following as an axiom:
∀alpha y, ordinal alpha(y ')alpha
Axiom. (tagged_eqE_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaalpha ' = beta 'alpha beta
Axiom. (tagged_eqE_eq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha ' = beta 'alpha = beta
Axiom. (tagged_ReplE) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betabeta ' {gamma '|gamma ∈ alpha}beta alpha
Axiom. (ordinal_notin_tagged_Repl) We take the following as an axiom:
∀alpha Y, ordinal alphaalpha{y '|y ∈ Y}
Definition. We define SNoElts_ to be λalpha ⇒ alpha{beta '|beta ∈ alpha} of type setset.
Axiom. (SNoElts_mon) We take the following as an axiom:
∀alpha beta, alpha betaSNoElts_ alpha SNoElts_ beta
Definition. We define SNo_ to be λalpha x ⇒ x SNoElts_ alpha∀betaalpha, exactly1of2 (beta ' x) (beta x) of type setsetprop.
Definition. We define PSNo to be λalpha p ⇒ {beta ∈ alpha|p beta}{beta '|beta ∈ alpha, ¬ p beta} of type set(setprop)set.
Axiom. (PNoEq_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, PNoEq_ alpha (λbeta ⇒ beta PSNo alpha p) p
Axiom. (SNo_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, SNo_ alpha (PSNo alpha p)
Axiom. (SNo_PSNo_eta_) We take the following as an axiom:
∀alpha x, ordinal alphaSNo_ alpha xx = PSNo alpha (λbeta ⇒ beta x)
Primitive. The name SNo is a term of type setprop.
Axiom. (SNo_SNo) We take the following as an axiom:
∀alpha, ordinal alpha∀z, SNo_ alpha zSNo z
Primitive. The name SNoLev is a term of type setset.
Axiom. (SNoLev_uniq_Subq) We take the following as an axiom:
∀x alpha beta, ordinal alphaordinal betaSNo_ alpha xSNo_ beta xalpha beta
Axiom. (SNoLev_uniq) We take the following as an axiom:
∀x alpha beta, ordinal alphaordinal betaSNo_ alpha xSNo_ beta xalpha = beta
Axiom. (SNoLev_prop) We take the following as an axiom:
∀x, SNo xordinal (SNoLev x)SNo_ (SNoLev x) x
Axiom. (SNoLev_ordinal) We take the following as an axiom:
∀x, SNo xordinal (SNoLev x)
Axiom. (SNoLev_) We take the following as an axiom:
∀x, SNo xSNo_ (SNoLev x) x
Axiom. (SNo_PSNo_eta) We take the following as an axiom:
∀x, SNo xx = PSNo (SNoLev x) (λbeta ⇒ beta x)
Axiom. (SNoLev_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, SNoLev (PSNo alpha p) = alpha
Axiom. (SNo_Subq) We take the following as an axiom:
∀x y, SNo xSNo ySNoLev x SNoLev y(∀alphaSNoLev x, alpha xalpha y)x y
Definition. We define SNoEq_ to be λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta x) (λbeta ⇒ beta y) of type setsetsetprop.
Axiom. (SNoEq_I) We take the following as an axiom:
∀alpha x y, (∀betaalpha, beta xbeta y)SNoEq_ alpha x y
Axiom. (SNo_eq) We take the following as an axiom:
∀x y, SNo xSNo ySNoLev x = SNoLev ySNoEq_ (SNoLev x) x yx = y
End of Section TaggedSets
Definition. We define SNoLt to be λx y ⇒ PNoLt (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y) of type setsetprop.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Definition. We define SNoLe to be λx y ⇒ PNoLe (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y) of type setsetprop.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Axiom. (SNoLtLe) We take the following as an axiom:
∀x y, x < yx y
Axiom. (SNoLeE) We take the following as an axiom:
∀x y, SNo xSNo yx yx < yx = y
Axiom. (SNoEq_sym_) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x ySNoEq_ alpha y x
Axiom. (SNoEq_tra_) We take the following as an axiom:
∀alpha x y z, SNoEq_ alpha x ySNoEq_ alpha y zSNoEq_ alpha x z
Axiom. (SNoLtE) We take the following as an axiom:
∀x y, SNo xSNo yx < y∀p : prop, (∀z, SNo zSNoLev z SNoLev xSNoLev ySNoEq_ (SNoLev z) z xSNoEq_ (SNoLev z) z yx < zz < ySNoLev zxSNoLev z yp)(SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yp)(SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev yxp)p
Axiom. (SNoLtI2) We take the following as an axiom:
∀x y, SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yx < y
Axiom. (SNoLtI3) We take the following as an axiom:
∀x y, SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev yxx < y
Axiom. (SNoLt_irref) We take the following as an axiom:
∀x, ¬ SNoLt x x
Axiom. (SNoLt_trichotomy_or) We take the following as an axiom:
∀x y, SNo xSNo yx < yx = yy < x
Axiom. (SNoLt_trichotomy_or_impred) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (x < yp)(x = yp)(y < xp)p
Axiom. (SNoLt_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < yy < zx < z
Axiom. (SNoLe_ref) We take the following as an axiom:
∀x, SNoLe x x
Axiom. (SNoLe_antisym) We take the following as an axiom:
∀x y, SNo xSNo yx yy xx = y
Axiom. (SNoLtLe_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < yy zx < z
Axiom. (SNoLeLt_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx yy < zx < z
Axiom. (SNoLe_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx yy zx z
Axiom. (SNoLtLe_or) We take the following as an axiom:
∀x y, SNo xSNo yx < yy x
Axiom. (SNoLt_PSNo_PNoLt) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPSNo alpha p < PSNo beta qPNoLt alpha p beta q
Axiom. (PNoLt_SNoLt_PSNo) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNoLt alpha p beta qPSNo alpha p < PSNo beta q
Definition. We define SNoCut to be λL R ⇒ PSNo (PNo_bd (λalpha p ⇒ ordinal alphaPSNo alpha p L) (λalpha p ⇒ ordinal alphaPSNo alpha p R)) (PNo_pred (λalpha p ⇒ ordinal alphaPSNo alpha p L) (λalpha p ⇒ ordinal alphaPSNo alpha p R)) of type setsetset.
Definition. We define SNoCutP to be λL R ⇒ (∀xL, SNo x)(∀yR, SNo y)(∀xL, ∀yR, x < y) of type setsetprop.
Axiom. (SNoCutP_SNoCut) We take the following as an axiom:
∀L R, SNoCutP L RSNo (SNoCut L R)SNoLev (SNoCut L R) ordsucc ((x ∈ Lordsucc (SNoLev x))(y ∈ Rordsucc (SNoLev y)))(∀xL, x < SNoCut L R)(∀yR, SNoCut L R < y)(∀z, SNo z(∀xL, x < z)(∀yR, z < y)SNoLev (SNoCut L R) SNoLev zSNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)
Axiom. (SNoCutP_SNoCut_impred) We take the following as an axiom:
∀L R, SNoCutP L R∀p : prop, (SNo (SNoCut L R)SNoLev (SNoCut L R) ordsucc ((x ∈ Lordsucc (SNoLev x))(y ∈ Rordsucc (SNoLev y)))(∀xL, x < SNoCut L R)(∀yR, SNoCut L R < y)(∀z, SNo z(∀xL, x < z)(∀yR, z < y)SNoLev (SNoCut L R) SNoLev zSNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)p)p
Axiom. (SNoCutP_L_0) We take the following as an axiom:
∀L, (∀xL, SNo x)SNoCutP L 0
Axiom. (SNoCutP_0_R) We take the following as an axiom:
∀R, (∀xR, SNo x)SNoCutP 0 R
Axiom. (SNoCutP_0_0) We take the following as an axiom:
SNoCutP 0 0
Definition. We define SNoS_ to be λalpha ⇒ {x ∈ 𝒫 (SNoElts_ alpha)|∃beta ∈ alpha, SNo_ beta x} of type setset.
Axiom. (SNoS_E) We take the following as an axiom:
∀alpha, ordinal alpha∀xSNoS_ alpha, ∃beta ∈ alpha, SNo_ beta x
Beginning of Section TaggedSets2
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Axiom. (SNoS_I) We take the following as an axiom:
∀alpha, ordinal alpha∀x, ∀betaalpha, SNo_ beta xx SNoS_ alpha
Axiom. (SNoS_I2) We take the following as an axiom:
∀x y, SNo xSNo ySNoLev x SNoLev yx SNoS_ (SNoLev y)
Axiom. (SNoS_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha betaSNoS_ alpha SNoS_ beta
Axiom. (SNoLev_uniq2) We take the following as an axiom:
∀alpha, ordinal alpha∀x, SNo_ alpha xSNoLev x = alpha
Axiom. (SNoS_E2) We take the following as an axiom:
∀alpha, ordinal alpha∀xSNoS_ alpha, ∀p : prop, (SNoLev x alphaordinal (SNoLev x)SNo xSNo_ (SNoLev x) xp)p
Axiom. (SNoS_In_neq) We take the following as an axiom:
∀w, SNo w∀xSNoS_ (SNoLev w), xw
Axiom. (SNoS_SNoLev) We take the following as an axiom:
∀z, SNo zz SNoS_ (ordsucc (SNoLev z))
Definition. We define SNoL to be λz ⇒ {x ∈ SNoS_ (SNoLev z)|x < z} of type setset.
Definition. We define SNoR to be λz ⇒ {y ∈ SNoS_ (SNoLev z)|z < y} of type setset.
Axiom. (SNoCutP_SNoL_SNoR) We take the following as an axiom:
∀z, SNo zSNoCutP (SNoL z) (SNoR z)
Axiom. (SNoL_E) We take the following as an axiom:
∀x, SNo x∀wSNoL x, ∀p : prop, (SNo wSNoLev w SNoLev xw < xp)p
Axiom. (SNoR_E) We take the following as an axiom:
∀x, SNo x∀zSNoR x, ∀p : prop, (SNo zSNoLev z SNoLev xx < zp)p
Axiom. (SNoL_SNoS_) We take the following as an axiom:
∀z, SNoL z SNoS_ (SNoLev z)
Axiom. (SNoR_SNoS_) We take the following as an axiom:
∀z, SNoR z SNoS_ (SNoLev z)
Axiom. (SNoL_SNoS) We take the following as an axiom:
∀x, SNo x∀wSNoL x, w SNoS_ (SNoLev x)
Axiom. (SNoR_SNoS) We take the following as an axiom:
∀x, SNo x∀zSNoR x, z SNoS_ (SNoLev x)
Axiom. (SNoL_I) We take the following as an axiom:
∀z, SNo z∀x, SNo xSNoLev x SNoLev zx < zx SNoL z
Axiom. (SNoR_I) We take the following as an axiom:
∀z, SNo z∀y, SNo ySNoLev y SNoLev zz < yy SNoR z
Axiom. (SNo_eta) We take the following as an axiom:
∀z, SNo zz = SNoCut (SNoL z) (SNoR z)
Axiom. (SNoCutP_SNo_SNoCut) We take the following as an axiom:
∀L R, SNoCutP L RSNo (SNoCut L R)
Axiom. (SNoCutP_SNoCut_L) We take the following as an axiom:
∀L R, SNoCutP L R∀xL, x < SNoCut L R
Axiom. (SNoCutP_SNoCut_R) We take the following as an axiom:
∀L R, SNoCutP L R∀yR, SNoCut L R < y
Axiom. (SNoCutP_SNoCut_fst) We take the following as an axiom:
∀L R, SNoCutP L R∀z, SNo z(∀xL, x < z)(∀yR, z < y)SNoLev (SNoCut L R) SNoLev zSNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z
Axiom. (SNoCut_Le) We take the following as an axiom:
∀L1 R1 L2 R2, SNoCutP L1 R1SNoCutP L2 R2(∀wL1, w < SNoCut L2 R2)(∀zR2, SNoCut L1 R1 < z)SNoCut L1 R1 SNoCut L2 R2
Axiom. (SNoCut_ext) We take the following as an axiom:
∀L1 R1 L2 R2, SNoCutP L1 R1SNoCutP L2 R2(∀wL1, w < SNoCut L2 R2)(∀zR1, SNoCut L2 R2 < z)(∀wL2, w < SNoCut L1 R1)(∀zR2, SNoCut L1 R1 < z)SNoCut L1 R1 = SNoCut L2 R2
Axiom. (SNoLt_SNoL_or_SNoR_impred) We take the following as an axiom:
∀x y, SNo xSNo yx < y∀p : prop, (∀zSNoL y, z SNoR xp)(x SNoL yp)(y SNoR xp)p
Axiom. (SNoL_or_SNoR_impred) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (x = yp)(∀zSNoL y, z SNoR xp)(x SNoL yp)(y SNoR xp)(∀zSNoR y, z SNoL xp)(x SNoR yp)(y SNoL xp)p
Axiom. (SNoL_SNoCutP_ex) We take the following as an axiom:
∀L R, SNoCutP L R∀wSNoL (SNoCut L R), ∃w' ∈ L, w w'
Axiom. (SNoR_SNoCutP_ex) We take the following as an axiom:
∀L R, SNoCutP L R∀zSNoR (SNoCut L R), ∃z' ∈ R, z' z
Axiom. (ordinal_SNo_) We take the following as an axiom:
∀alpha, ordinal alphaSNo_ alpha alpha
Axiom. (ordinal_SNo) We take the following as an axiom:
∀alpha, ordinal alphaSNo alpha
Axiom. (ordinal_SNoLev) We take the following as an axiom:
∀alpha, ordinal alphaSNoLev alpha = alpha
Axiom. (ordinal_SNoLev_max) We take the following as an axiom:
∀alpha, ordinal alpha∀z, SNo zSNoLev z alphaz < alpha
Axiom. (ordinal_SNoL) We take the following as an axiom:
∀alpha, ordinal alphaSNoL alpha = SNoS_ alpha
Axiom. (ordinal_SNoR) We take the following as an axiom:
∀alpha, ordinal alphaSNoR alpha = Empty
Axiom. (nat_p_SNo) We take the following as an axiom:
∀n, nat_p nSNo n
Axiom. (omega_SNo) We take the following as an axiom:
∀nω, SNo n
Axiom. (omega_SNoS_omega) We take the following as an axiom:
ω SNoS_ ω
Axiom. (ordinal_In_SNoLt) We take the following as an axiom:
∀alpha, ordinal alpha∀betaalpha, beta < alpha
Axiom. (ordinal_SNoLev_max_2) We take the following as an axiom:
∀alpha, ordinal alpha∀z, SNo zSNoLev z ordsucc alphaz alpha
Axiom. (ordinal_Subq_SNoLe) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha betaalpha beta
Axiom. (ordinal_SNoLt_In) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha < betaalpha beta
Axiom. (omega_nonneg) We take the following as an axiom:
∀mω, 0 m
Axiom. (SNo_0) We take the following as an axiom:
SNo 0
Axiom. (SNo_1) We take the following as an axiom:
SNo 1
Axiom. (SNo_2) We take the following as an axiom:
SNo 2
Axiom. (SNoLev_0) We take the following as an axiom:
SNoLev 0 = 0
Axiom. (SNoCut_0_0) We take the following as an axiom:
SNoCut 0 0 = 0
Axiom. (SNoL_0) We take the following as an axiom:
SNoL 0 = 0
Axiom. (SNoR_0) We take the following as an axiom:
SNoR 0 = 0
Axiom. (SNoL_1) We take the following as an axiom:
SNoL 1 = 1
Axiom. (SNoR_1) We take the following as an axiom:
SNoR 1 = 0
Axiom. (SNo_max_SNoLev) We take the following as an axiom:
∀x, SNo x(∀ySNoS_ (SNoLev x), y < x)SNoLev x = x
Axiom. (SNo_max_ordinal) We take the following as an axiom:
∀x, SNo x(∀ySNoS_ (SNoLev x), y < x)ordinal x
Axiom. (pos_low_eq_one) We take the following as an axiom:
∀x, SNo x0 < xSNoLev x 1x = 1
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta xdeltaSNoLev x) of type setset.
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta xdelta = SNoLev x) of type setset.
Axiom. (SNo_extend0_SNo_) We take the following as an axiom:
∀x, SNo xSNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)
Axiom. (SNo_extend1_SNo_) We take the following as an axiom:
∀x, SNo xSNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)
Axiom. (SNo_extend0_SNo) We take the following as an axiom:
∀x, SNo xSNo (SNo_extend0 x)
Axiom. (SNo_extend1_SNo) We take the following as an axiom:
∀x, SNo xSNo (SNo_extend1 x)
Axiom. (SNo_extend0_SNoLev) We take the following as an axiom:
∀x, SNo xSNoLev (SNo_extend0 x) = ordsucc (SNoLev x)
Axiom. (SNo_extend1_SNoLev) We take the following as an axiom:
∀x, SNo xSNoLev (SNo_extend1 x) = ordsucc (SNoLev x)
Axiom. (SNo_extend0_nIn) We take the following as an axiom:
∀x, SNo xSNoLev xSNo_extend0 x
Axiom. (SNo_extend1_In) We take the following as an axiom:
∀x, SNo xSNoLev x SNo_extend1 x
Axiom. (SNo_extend0_SNoEq) We take the following as an axiom:
∀x, SNo xSNoEq_ (SNoLev x) (SNo_extend0 x) x
Axiom. (SNo_extend1_SNoEq) We take the following as an axiom:
∀x, SNo xSNoEq_ (SNoLev x) (SNo_extend1 x) x
Axiom. (SNoLev_0_eq_0) We take the following as an axiom:
∀x, SNo xSNoLev x = 0x = 0
Axiom. (SNo_0_eq_0) We take the following as an axiom:
∀q, SNo_ 0 qq = 0
Definition. We define eps_ to be λn ⇒ {0}{(ordsucc m) '|m ∈ n} of type setset.
Axiom. (eps_ordinal_In_eq_0) We take the following as an axiom:
∀n alpha, ordinal alphaalpha eps_ nalpha = 0
Axiom. (eps_0_1) We take the following as an axiom:
eps_ 0 = 1
Axiom. (SNo__eps_) We take the following as an axiom:
∀nω, SNo_ (ordsucc n) (eps_ n)
Axiom. (SNo_eps_) We take the following as an axiom:
∀nω, SNo (eps_ n)
Axiom. (SNo_eps_1) We take the following as an axiom:
SNo (eps_ 1)
Axiom. (SNoLev_eps_) We take the following as an axiom:
∀nω, SNoLev (eps_ n) = ordsucc n
Axiom. (SNo_eps_SNoS_omega) We take the following as an axiom:
∀nω, eps_ n SNoS_ ω
Axiom. (SNo_eps_decr) We take the following as an axiom:
∀nω, ∀mn, eps_ n < eps_ m
Axiom. (SNo_eps_pos) We take the following as an axiom:
∀nω, 0 < eps_ n
Axiom. (SNo_pos_eps_Lt) We take the following as an axiom:
∀n, nat_p n∀xSNoS_ (ordsucc n), 0 < xeps_ n < x
Axiom. (SNo_pos_eps_Le) We take the following as an axiom:
∀n, nat_p n∀xSNoS_ (ordsucc (ordsucc n)), 0 < xeps_ n x
Axiom. (eps_SNo_eq) We take the following as an axiom:
∀n, nat_p n∀xSNoS_ (ordsucc n), 0 < xSNoEq_ (SNoLev x) (eps_ n) x∃m ∈ n, x = eps_ m
Axiom. (eps_SNoCutP) We take the following as an axiom:
∀nω, SNoCutP {0} {eps_ m|m ∈ n}
Axiom. (eps_SNoCut) We take the following as an axiom:
∀nω, eps_ n = SNoCut {0} {eps_ m|m ∈ n}
End of Section TaggedSets2
Axiom. (SNo_etaE) We take the following as an axiom:
∀z, SNo z∀p : prop, (∀L R, SNoCutP L R(∀xL, SNoLev x SNoLev z)(∀yR, SNoLev y SNoLev z)z = SNoCut L Rp)p
Axiom. (SNo_ind) We take the following as an axiom:
∀P : setprop, (∀L R, SNoCutP L R(∀xL, P x)(∀yR, P y)P (SNoCut L R))∀z, SNo zP z
Beginning of Section SurrealRecI
Variable F : set(setset)set
Let default : setEps_i (λ_ ⇒ True)
Let G : set(setsetset)setsetλalpha g ⇒ If_ii (ordinal alpha) (λz : setif z SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : setdefault)
Primitive. The name SNo_rec_i is a term of type setset.
Hypothesis Fr : ∀z, SNo z∀g h : setset, (∀wSNoS_ (SNoLev z), g w = h w)F z g = F z h
Axiom. (SNo_rec_i_eq) We take the following as an axiom:
∀z, SNo zSNo_rec_i z = F z SNo_rec_i
End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set(set(setset))(setset)
Let default : (setset)Descr_ii (λ_ ⇒ True)
Let G : set(setset(setset))set(setset)λalpha g ⇒ If_iii (ordinal alpha) (λz : setIf_ii (z SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : setdefault)
Primitive. The name SNo_rec_ii is a term of type set(setset).
Hypothesis Fr : ∀z, SNo z∀g h : set(setset), (∀wSNoS_ (SNoLev z), g w = h w)F z g = F z h
Axiom. (SNo_rec_ii_eq) We take the following as an axiom:
∀z, SNo zSNo_rec_ii z = F z SNo_rec_ii
End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : setset(setsetset)set
Let G : set(setsetset)set(setset)setλw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y)
Let H : set(setsetset)setsetλw f z ⇒ if SNo z then SNo_rec_i (G w f) z else Empty
Primitive. The name SNo_rec2 is a term of type setsetset.
Hypothesis Fr : ∀w, SNo w∀z, SNo z∀g h : setsetset, (∀xSNoS_ (SNoLev w), ∀y, SNo yg x y = h x y)(∀ySNoS_ (SNoLev z), g w y = h w y)F w z g = F w z h
Axiom. (SNo_rec2_G_prop) We take the following as an axiom:
∀w, SNo w∀f k : setsetset, (∀xSNoS_ (SNoLev w), f x = k x)∀z, SNo z∀g h : setset, (∀uSNoS_ (SNoLev z), g u = h u)G w f z g = G w k z h
Axiom. (SNo_rec2_eq_1) We take the following as an axiom:
∀w, SNo w∀f : setsetset, ∀z, SNo zSNo_rec_i (G w f) z = G w f z (SNo_rec_i (G w f))
Axiom. (SNo_rec2_eq) We take the following as an axiom:
∀w, SNo w∀z, SNo zSNo_rec2 w z = F w z SNo_rec2
End of Section SurrealRec2
Axiom. (SNo_ordinal_ind) We take the following as an axiom:
∀P : setprop, (∀alpha, ordinal alpha∀xSNoS_ alpha, P x)(∀x, SNo xP x)
Axiom. (SNo_ordinal_ind2) We take the following as an axiom:
∀P : setsetprop, (∀alpha, ordinal alpha∀beta, ordinal beta∀xSNoS_ alpha, ∀ySNoS_ beta, P x y)(∀x y, SNo xSNo yP x y)
Axiom. (SNo_ordinal_ind3) We take the following as an axiom:
∀P : setsetsetprop, (∀alpha, ordinal alpha∀beta, ordinal beta∀gamma, ordinal gamma∀xSNoS_ alpha, ∀ySNoS_ beta, ∀zSNoS_ gamma, P x y z)(∀x y z, SNo xSNo ySNo zP x y z)
Axiom. (SNoLev_ind) We take the following as an axiom:
∀P : setprop, (∀x, SNo x(∀wSNoS_ (SNoLev x), P w)P x)(∀x, SNo xP x)
Axiom. (SNoLev_ind2) We take the following as an axiom:
∀P : setsetprop, (∀x y, SNo xSNo y(∀wSNoS_ (SNoLev x), P w y)(∀zSNoS_ (SNoLev y), P x z)(∀wSNoS_ (SNoLev x), ∀zSNoS_ (SNoLev y), P w z)P x y)∀x y, SNo xSNo yP x y
Axiom. (SNoLev_ind3) We take the following as an axiom:
∀P : setsetsetprop, (∀x y z, SNo xSNo ySNo z(∀uSNoS_ (SNoLev x), P u y z)(∀vSNoS_ (SNoLev y), P x v z)(∀wSNoS_ (SNoLev z), P x y w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), P u v z)(∀uSNoS_ (SNoLev x), ∀wSNoS_ (SNoLev z), P u y w)(∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), P x v w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), P u v w)P x y z)∀x y z, SNo xSNo ySNo zP x y z
Axiom. (SNo_omega) We take the following as an axiom:
SNo ω
Axiom. (SNoLt_0_1) We take the following as an axiom:
0 < 1
Axiom. (SNoLt_0_2) We take the following as an axiom:
0 < 2
Axiom. (SNoLt_1_2) We take the following as an axiom:
1 < 2
Axiom. (restr_SNo_) We take the following as an axiom:
∀x, SNo x∀alphaSNoLev x, SNo_ alpha (xSNoElts_ alpha)
Axiom. (restr_SNo) We take the following as an axiom:
∀x, SNo x∀alphaSNoLev x, SNo (xSNoElts_ alpha)
Axiom. (restr_SNoLev) We take the following as an axiom:
∀x, SNo x∀alphaSNoLev x, SNoLev (xSNoElts_ alpha) = alpha
Axiom. (restr_SNoEq) We take the following as an axiom:
∀x, SNo x∀alphaSNoLev x, SNoEq_ alpha (xSNoElts_ alpha) x
Axiom. (SNo_extend0_restr_eq) We take the following as an axiom:
∀x, SNo xx = SNo_extend0 xSNoElts_ (SNoLev x)
Axiom. (SNo_extend1_restr_eq) We take the following as an axiom:
∀x, SNo xx = SNo_extend1 xSNoElts_ (SNoLev x)