Beginning of Section SurrealAdd
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Primitive. The name
add_SNo is a term of type
set → set → set.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
L10Axiom. (
add_SNo_eq) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → x + y = SNoCut ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
L11Axiom. (
add_SNo_prop1) We take the following as an axiom:
∀x y, SNo x → SNo y → SNo (x + y) ∧ (∀u ∈ SNoL x, u + y < x + y) ∧ (∀u ∈ SNoR x, x + y < u + y) ∧ (∀u ∈ SNoL y, x + u < x + y) ∧ (∀u ∈ SNoR y, x + y < x + u) ∧ SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
L12Axiom. (
SNo_add_SNo) We take the following as an axiom:
∀x y, SNo x → SNo y → SNo (x + y)
L13Axiom. (
SNo_add_SNo_3) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → SNo (x + y + z)
L14Axiom. (
SNo_add_SNo_3c) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → SNo (x + y + - z)
L15Axiom. (
SNo_add_SNo_4) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → SNo (x + y + z + w)
L16Axiom. (
add_SNo_Lt1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < z → x + y < z + y
L17Axiom. (
add_SNo_Le1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ z → x + y ≤ z + y
L18Axiom. (
add_SNo_Lt2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → y < z → x + y < x + z
L19Axiom. (
add_SNo_Le2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → y ≤ z → x + y ≤ x + z
L20Axiom. (
add_SNo_Lt3a) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y ≤ w → x + y < z + w
L21Axiom. (
add_SNo_Lt3b) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y < w → x + y < z + w
L22Axiom. (
add_SNo_Lt3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y < w → x + y < z + w
L23Axiom. (
add_SNo_Le3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y ≤ w → x + y ≤ z + w
L24Axiom. (
add_SNo_SNoCutP) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
L25Axiom. (
add_SNo_com) We take the following as an axiom:
∀x y, SNo x → SNo y → x + y = y + x
L26Axiom. (
add_SNo_0L) We take the following as an axiom:
L27Axiom. (
add_SNo_0R) We take the following as an axiom:
L30Axiom. (
add_SNo_ordinal_SNoCutP) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → SNoCutP ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty
L31Axiom. (
add_SNo_ordinal_eq) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + beta = SNoCut ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty
L32Axiom. (
add_SNo_ordinal_ordinal) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ordinal (alpha + beta)
L33Axiom. (
add_SNo_ordinal_SL) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ordsucc alpha + beta = ordsucc (alpha + beta)
L34Axiom. (
add_SNo_ordinal_SR) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + ordsucc beta = ordsucc (alpha + beta)
L35Axiom. (
add_SNo_ordinal_InL) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ alpha, gamma + beta ∈ alpha + beta
L36Axiom. (
add_SNo_ordinal_InR) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ beta, alpha + gamma ∈ alpha + beta
L37Axiom. (
add_nat_add_SNo) We take the following as an axiom:
∀n m ∈ ω, add_nat n m = n + m
L40Axiom. (
add_SNo_SNoL_interpolate) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x + y), (∃v ∈ SNoL x, u ≤ v + y) ∨ (∃v ∈ SNoL y, u ≤ x + v)
L41Axiom. (
add_SNo_SNoR_interpolate) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x + y), (∃v ∈ SNoR x, v + y ≤ u) ∨ (∃v ∈ SNoR y, x + v ≤ u)
L42Axiom. (
add_SNo_assoc) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + (y + z) = (x + y) + z
L43Axiom. (
add_SNo_cancel_L) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y = x + z → y = z
L44Axiom. (
minus_SNo_0) We take the following as an axiom:
L47Axiom. (
add_SNo_Lev_bd) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoLev (x + y) ⊆ SNoLev x + SNoLev y
L49Axiom. (
add_SNo_minus_R2) We take the following as an axiom:
∀x y, SNo x → SNo y → (x + y) + - y = x
L50Axiom. (
add_SNo_minus_R2') We take the following as an axiom:
∀x y, SNo x → SNo y → (x + - y) + y = x
L51Axiom. (
add_SNo_minus_L2) We take the following as an axiom:
∀x y, SNo x → SNo y → - x + (x + y) = y
L52Axiom. (
add_SNo_minus_L2') We take the following as an axiom:
∀x y, SNo x → SNo y → x + (- x + y) = y
L53Axiom. (
add_SNo_Lt1_cancel) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y < z + y → x < z
L54Axiom. (
add_SNo_Lt2_cancel) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y < x + z → y < z
L55Axiom. (
add_SNo_assoc_4) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = (x + y + z) + w
L56Axiom. (
add_SNo_com_3_0_1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y + z = y + x + z
L57Axiom. (
add_SNo_com_3b_1_2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (x + y) + z = (x + z) + y
L58Axiom. (
add_SNo_com_4_inner_mid) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) + (z + w) = (x + z) + (y + w)
L59Axiom. (
add_SNo_rotate_3_1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y + z = z + x + y
L60Axiom. (
add_SNo_rotate_4_1) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = w + x + y + z
L61Axiom. (
add_SNo_rotate_5_1) We take the following as an axiom:
∀x y z w v, SNo x → SNo y → SNo z → SNo w → SNo v → x + y + z + w + v = v + x + y + z + w
L62Axiom. (
add_SNo_rotate_5_2) We take the following as an axiom:
∀x y z w v, SNo x → SNo y → SNo z → SNo w → SNo v → x + y + z + w + v = w + v + x + y + z
L67Axiom. (
add_SNo_minus_Lt1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + - y < z → x < z + y
L68Axiom. (
add_SNo_minus_Lt2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z < x + - y → z + y < x
L69Axiom. (
add_SNo_minus_Lt1b) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < z + y → x + - y < z
L70Axiom. (
add_SNo_minus_Lt2b) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z + y < x → z < x + - y
L71Axiom. (
add_SNo_minus_Lt1b3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y < w + z → x + y + - z < w
L72Axiom. (
add_SNo_minus_Lt2b3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → w + z < x + y → w < x + y + - z
L73Axiom. (
add_SNo_minus_Lt_lem) We take the following as an axiom:
∀x y z u v w, SNo x → SNo y → SNo z → SNo u → SNo v → SNo w → x + y + w < u + v + z → x + y + - z < u + v + - w
L74Axiom. (
add_SNo_minus_Le2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z ≤ x + - y → z + y ≤ x
L75Axiom. (
add_SNo_minus_Le2b) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z + y ≤ x → z ≤ x + - y
L76Axiom. (
add_SNo_Lt_subprop2) We take the following as an axiom:
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + u < z + v → y + v < w + u → x + y < z + w
L77Axiom. (
add_SNo_Lt_subprop3a) We take the following as an axiom:
∀x y z w u a, SNo x → SNo y → SNo z → SNo w → SNo u → SNo a → x + z < w + a → y + a < u → x + y + z < w + u
L78Axiom. (
add_SNo_Lt_subprop3b) We take the following as an axiom:
∀x y w u v a, SNo x → SNo y → SNo w → SNo u → SNo v → SNo a → x + a < w + v → y < a + u → x + y < w + u + v
L79Axiom. (
add_SNo_Lt_subprop3c) We take the following as an axiom:
∀x y z w u a b c, SNo x → SNo y → SNo z → SNo w → SNo u → SNo a → SNo b → SNo c → x + a < b + c → y + c < u → b + z < w + a → x + y + z < w + u
L80Axiom. (
add_SNo_Lt_subprop3d) We take the following as an axiom:
∀x y w u v a b c, SNo x → SNo y → SNo w → SNo u → SNo v → SNo a → SNo b → SNo c → x + a < b + v → y < c + u → b + c < w + a → x + y < w + u + v
L81Axiom. (
ordinal_ordsucc_SNo_eq) We take the following as an axiom:
∀alpha, ordinal alpha → ordsucc alpha = 1 + alpha
L82Axiom. (
add_SNo_3a_2b) We take the following as an axiom:
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → (x + y + z) + (w + u) = (u + y + z) + (w + x)
L84Axiom. (
add_SNo_eps_Lt) We take the following as an axiom:
∀x, SNo x → ∀n ∈ ω, x < x + eps_ n
L85Axiom. (
add_SNo_eps_Lt') We take the following as an axiom:
∀x y, SNo x → SNo y → ∀n ∈ ω, x < y → x < y + eps_ n
L86Axiom. (
SNoLt_minus_pos) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y → 0 < y + - x
L88Axiom. (
add_SNo_Lt4) We take the following as an axiom:
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x < w → y < u → z < v → x + y + z < w + u + v
L89Axiom. (
add_SNo_3_3_3_Lt1) We take the following as an axiom:
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → x + y < z + w → x + y + u < z + w + u
L90Axiom. (
add_SNo_3_2_3_Lt1) We take the following as an axiom:
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → y + x < z + w → x + u + y < z + w + u
L91Axiom. (
add_SNoCutP_lem) We take the following as an axiom:
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → SNoCutP ({w + y|w ∈ Lx} ∪ {x + w|w ∈ Ly}) ({z + y|z ∈ Rx} ∪ {x + z|z ∈ Ry}) ∧ x + y = SNoCut ({w + y|w ∈ Lx} ∪ {x + w|w ∈ Ly}) ({z + y|z ∈ Rx} ∪ {x + z|z ∈ Ry})
L92Axiom. (
add_SNoCutP_gen) We take the following as an axiom:
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → SNoCutP ({w + y|w ∈ Lx} ∪ {x + w|w ∈ Ly}) ({z + y|z ∈ Rx} ∪ {x + z|z ∈ Ry})
L93Axiom. (
add_SNoCut_eq) We take the following as an axiom:
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → x + y = SNoCut ({w + y|w ∈ Lx} ∪ {x + w|w ∈ Ly}) ({z + y|z ∈ Rx} ∪ {x + z|z ∈ Ry})
L94Axiom. (
add_SNo_SNoCut_L_interpolate) We take the following as an axiom:
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoL (x + y), (∃v ∈ Lx, u ≤ v + y) ∨ (∃v ∈ Ly, u ≤ x + v)
L95Axiom. (
add_SNo_SNoCut_R_interpolate) We take the following as an axiom:
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoR (x + y), (∃v ∈ Rx, v + y ≤ u) ∨ (∃v ∈ Ry, x + v ≤ u)
L96Axiom. (
add_SNo_minus_Lt12b3) We take the following as an axiom:
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + y + v < w + u + z → x + y + - z < w + u + - v
L97Axiom. (
add_SNo_Le1_cancel) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y ≤ z + y → x ≤ z
L98Axiom. (
add_SNo_minus_Le1b) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ z + y → x + - y ≤ z
L99Axiom. (
add_SNo_minus_Le1b3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y ≤ w + z → x + y + - z ≤ w
L100Axiom. (
add_SNo_minus_Le12b3) We take the following as an axiom:
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + y + v ≤ w + u + z → x + y + - z ≤ w + u + - v
End of Section SurrealAdd