Primitive. The name Eps_i is a term of type (setprop)set.
Axiom. (Eps_i_ax) We take the following as an axiom:
∀P : setprop, ∀x : set, P xP (Eps_i P)
Definition. We define True to be ∀p : prop, pp of type prop.
Definition. We define False to be ∀p : prop, p of type prop.
Definition. We define not to be λA : propAFalse of type propprop.
Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.
Definition. We define and to be λA B : prop∀p : prop, (ABp)p of type proppropprop.
Notation. We use as an infix operator with priority 780 and which associates to the left corresponding to applying term and.
Definition. We define or to be λA B : prop∀p : prop, (Ap)(Bp)p of type proppropprop.
Notation. We use as an infix operator with priority 785 and which associates to the left corresponding to applying term or.
Definition. We define iff to be λA B : propand (AB) (BA) of type proppropprop.
Notation. We use as an infix operator with priority 805 and no associativity corresponding to applying term iff.
Beginning of Section Eq
Variable A : SType
Definition. We define eq to be λx y : A∀Q : AAprop, Q x yQ y x of type AAprop.
Definition. We define neq to be λx y : A¬ eq x y of type AAprop.
End of Section Eq
Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.
Notation. We use as an infix operator with priority 502 and no associativity corresponding to applying term neq.
Beginning of Section FE
Variable A B : SType
Axiom. (func_ext) We take the following as an axiom:
∀f g : AB, (∀x : A, f x = g x)f = g
End of Section FE
Beginning of Section Ex
Variable A : SType
Definition. We define ex to be λQ : Aprop∀P : prop, (∀x : A, Q xP)P of type (Aprop)prop.
End of Section Ex
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex.
Axiom. (prop_ext) We take the following as an axiom:
∀p q : prop, iff p qp = q
Primitive. The name In is a term of type setsetprop.
Notation. We use as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write xA, B to mean x : set, xAB.
Definition. We define Subq to be λA B ⇒ ∀xA, x B of type setsetprop.
Notation. We use as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write xA, B to mean x : set, xAB.
Axiom. (set_ext) We take the following as an axiom:
∀X Y : set, X YY XX = Y
Axiom. (In_ind) We take the following as an axiom:
∀P : setprop, (∀X : set, (∀xX, P x)P X)∀X : set, P X
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.
Primitive. The name Empty is a term of type set.
Axiom. (EmptyAx) We take the following as an axiom:
¬ ∃x : set, x Empty
Primitive. The name is a term of type setset.
Axiom. (UnionEq) We take the following as an axiom:
∀X x, x X ∃Y, x Y Y X
Primitive. The name 𝒫 is a term of type setset.
Axiom. (PowerEq) We take the following as an axiom:
∀X Y : set, Y 𝒫 X Y X
Primitive. The name Repl is a term of type set(setset)set.
Notation. {B| xA} is notation for Repl Ax . B).
Axiom. (ReplEq) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y {F x|xA} ∃xA, y = F x
Definition. We define TransSet to be λU : set∀xU, x U of type setprop.
Definition. We define Union_closed to be λU : set∀X : set, X U X U of type setprop.
Definition. We define Power_closed to be λU : set∀X : set, X U𝒫 X U of type setprop.
Definition. We define Repl_closed to be λU : set∀X : set, X U∀F : setset, (∀x : set, x XF x U){F x|xX} U of type setprop.
Definition. We define ZF_closed to be λU : setUnion_closed U Power_closed U Repl_closed U of type setprop.
Primitive. The name UnivOf is a term of type setset.
Axiom. (UnivOf_In) We take the following as an axiom:
∀N : set, N UnivOf N
Axiom. (UnivOf_TransSet) We take the following as an axiom:
∀N : set, TransSet (UnivOf N)
Axiom. (UnivOf_ZF_closed) We take the following as an axiom:
∀N : set, ZF_closed (UnivOf N)
Axiom. (UnivOf_Min) We take the following as an axiom:
∀N U : set, N UTransSet UZF_closed UUnivOf N U
Axiom. (FalseE) We take the following as an axiom:
False∀p : prop, p
Axiom. (TrueI) We take the following as an axiom:
True
Axiom. (andI) We take the following as an axiom:
∀A B : prop, ABA B
Axiom. (andEL) We take the following as an axiom:
∀A B : prop, A BA
Axiom. (andER) We take the following as an axiom:
∀A B : prop, A BB
Axiom. (orIL) We take the following as an axiom:
∀A B : prop, AA B
Axiom. (orIR) We take the following as an axiom:
∀A B : prop, BA B
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (and3I) We take the following as an axiom:
P1P2P3P1 P2 P3
Axiom. (and3E) We take the following as an axiom:
P1 P2 P3(∀p : prop, (P1P2P3p)p)
Axiom. (or3I1) We take the following as an axiom:
P1P1 P2 P3
Axiom. (or3I2) We take the following as an axiom:
P2P1 P2 P3
Axiom. (or3I3) We take the following as an axiom:
P3P1 P2 P3
Axiom. (or3E) We take the following as an axiom:
P1 P2 P3(∀p : prop, (P1p)(P2p)(P3p)p)
Variable P4 : prop
Axiom. (and4I) We take the following as an axiom:
P1P2P3P4P1 P2 P3 P4
Variable P5 : prop
Axiom. (and5I) We take the following as an axiom:
P1P2P3P4P5P1 P2 P3 P4 P5
End of Section PropN
Axiom. (not_or_and_demorgan) We take the following as an axiom:
∀A B : prop, ¬ (A B)¬ A ¬ B
Axiom. (not_ex_all_demorgan_i) We take the following as an axiom:
∀P : setprop, (¬ ∃x, P x)∀x, ¬ P x
Axiom. (iffI) We take the following as an axiom:
∀A B : prop, (AB)(BA)(A B)
Axiom. (iffEL) We take the following as an axiom:
∀A B : prop, (A B)AB
Axiom. (iffER) We take the following as an axiom:
∀A B : prop, (A B)BA
Axiom. (iff_refl) We take the following as an axiom:
∀A : prop, A A
Axiom. (iff_sym) We take the following as an axiom:
∀A B : prop, (A B)(B A)
Axiom. (iff_trans) We take the following as an axiom:
∀A B C : prop, (A B)(B C)(A C)
Axiom. (eq_i_tra) We take the following as an axiom:
∀x y z, x = yy = zx = z
Axiom. (f_eq_i) We take the following as an axiom:
∀f : setset, ∀x y, x = yf x = f y
Axiom. (neq_i_sym) We take the following as an axiom:
∀x y, x yy x
Definition. We define nIn to be λx X ⇒ ¬ In x X of type setsetprop.
Notation. We use as an infix operator with priority 502 and no associativity corresponding to applying term nIn.
Axiom. (Eps_i_ex) We take the following as an axiom:
∀P : setprop, (∃x, P x)P (Eps_i P)
Axiom. (pred_ext) We take the following as an axiom:
∀P Q : setprop, (∀x, P x Q x)P = Q
Axiom. (prop_ext_2) We take the following as an axiom:
∀p q : prop, (pq)(qp)p = q
Axiom. (Subq_ref) We take the following as an axiom:
∀X : set, X X
Axiom. (Subq_tra) We take the following as an axiom:
∀X Y Z : set, X YY ZX Z
Axiom. (Subq_contra) We take the following as an axiom:
∀X Y z : set, X Yz Yz X
Axiom. (EmptyE) We take the following as an axiom:
∀x : set, x Empty
Axiom. (Subq_Empty) We take the following as an axiom:
∀X : set, Empty X
Axiom. (Empty_Subq_eq) We take the following as an axiom:
∀X : set, X EmptyX = Empty
Axiom. (Empty_eq) We take the following as an axiom:
∀X : set, (∀x, x X)X = Empty
Axiom. (UnionI) We take the following as an axiom:
∀X x Y : set, x YY Xx X
Axiom. (UnionE) We take the following as an axiom:
∀X x : set, x X∃Y : set, x Y Y X
Axiom. (UnionE_impred) We take the following as an axiom:
∀X x : set, x X∀p : prop, (∀Y : set, x YY Xp)p
Axiom. (PowerI) We take the following as an axiom:
∀X Y : set, Y XY 𝒫 X
Axiom. (PowerE) We take the following as an axiom:
∀X Y : set, Y 𝒫 XY X
Axiom. (Empty_In_Power) We take the following as an axiom:
∀X : set, Empty 𝒫 X
Axiom. (Self_In_Power) We take the following as an axiom:
∀X : set, X 𝒫 X
Axiom. (xm) We take the following as an axiom:
∀P : prop, P ¬ P
Axiom. (dneg) We take the following as an axiom:
∀P : prop, ¬ ¬ PP
Axiom. (not_all_ex_demorgan_i) We take the following as an axiom:
∀P : setprop, ¬ (∀x, P x)∃x, ¬ P x
Axiom. (eq_or_nand) We take the following as an axiom:
or = (λx y : prop¬ (¬ x ¬ y))
Primitive. The name exactly1of2 is a term of type proppropprop.
Axiom. (exactly1of2_I1) We take the following as an axiom:
∀A B : prop, A¬ Bexactly1of2 A B
Axiom. (exactly1of2_I2) We take the following as an axiom:
∀A B : prop, ¬ ABexactly1of2 A B
Axiom. (exactly1of2_E) We take the following as an axiom:
∀A B : prop, exactly1of2 A B∀p : prop, (A¬ Bp)(¬ ABp)p
Axiom. (exactly1of2_or) We take the following as an axiom:
∀A B : prop, exactly1of2 A BA B
Axiom. (ReplI) We take the following as an axiom:
∀A : set, ∀F : setset, ∀x : set, x AF x {F x|xA}
Axiom. (ReplE) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y {F x|xA}∃xA, y = F x
Axiom. (ReplE_impred) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y {F x|xA}∀p : prop, (∀x : set, x Ay = F xp)p
Axiom. (ReplE') We take the following as an axiom:
∀X, ∀f : setset, ∀p : setprop, (∀xX, p (f x))∀y{f x|xX}, p y
Axiom. (Repl_Empty) We take the following as an axiom:
∀F : setset, {F x|xEmpty} = Empty
Axiom. (ReplEq_ext_sub) We take the following as an axiom:
∀X, ∀F G : setset, (∀xX, F x = G x){F x|xX} {G x|xX}
Axiom. (ReplEq_ext) We take the following as an axiom:
∀X, ∀F G : setset, (∀xX, F x = G x){F x|xX} = {G x|xX}
Axiom. (Repl_inv_eq) We take the following as an axiom:
∀P : setprop, ∀f g : setset, (∀x, P xg (f x) = x)∀X, (∀xX, P x){g y|y{f x|xX}} = X
Axiom. (Repl_invol_eq) We take the following as an axiom:
∀P : setprop, ∀f : setset, (∀x, P xf (f x) = x)∀X, (∀xX, P x){f y|y{f x|xX}} = X
Primitive. The name If_i is a term of type propsetsetset.
Notation. if cond then T else E is notation corresponding to If_i type cond T E where type is the inferred type of T.
Axiom. (If_i_correct) We take the following as an axiom:
∀p : prop, ∀x y : set, p (if p then x else y) = x ¬ p (if p then x else y) = y
Axiom. (If_i_0) We take the following as an axiom:
∀p : prop, ∀x y : set, ¬ p(if p then x else y) = y
Axiom. (If_i_1) We take the following as an axiom:
∀p : prop, ∀x y : set, p(if p then x else y) = x
Axiom. (If_i_or) We take the following as an axiom:
∀p : prop, ∀x y : set, (if p then x else y) = x (if p then x else y) = y
Primitive. The name UPair is a term of type setsetset.
Notation. {x,y} is notation for UPair x y.
Axiom. (UPairE) We take the following as an axiom:
∀x y z : set, x {y,z}x = y x = z
Axiom. (UPairI1) We take the following as an axiom:
∀y z : set, y {y,z}
Axiom. (UPairI2) We take the following as an axiom:
∀y z : set, z {y,z}
Primitive. The name Sing is a term of type setset.
Notation. {x} is notation for Sing x.
Axiom. (SingI) We take the following as an axiom:
∀x : set, x {x}
Axiom. (SingE) We take the following as an axiom:
∀x y : set, y {x}y = x
Primitive. The name binunion is a term of type setsetset.
Notation. We use as an infix operator with priority 345 and which associates to the left corresponding to applying term binunion.
Axiom. (binunionI1) We take the following as an axiom:
∀X Y z : set, z Xz X Y
Axiom. (binunionI2) We take the following as an axiom:
∀X Y z : set, z Yz X Y
Axiom. (binunionE) We take the following as an axiom:
∀X Y z : set, z X Yz X z Y
Axiom. (binunionE') We take the following as an axiom:
∀X Y z, ∀p : prop, (z Xp)(z Yp)(z X Yp)
Axiom. (binunion_asso) We take the following as an axiom:
∀X Y Z : set, X (Y Z) = (X Y) Z
Axiom. (binunion_com_Subq) We take the following as an axiom:
∀X Y : set, X Y Y X
Axiom. (binunion_com) We take the following as an axiom:
∀X Y : set, X Y = Y X
Axiom. (binunion_idl) We take the following as an axiom:
∀X : set, Empty X = X
Axiom. (binunion_idr) We take the following as an axiom:
∀X : set, X Empty = X
Axiom. (binunion_Subq_1) We take the following as an axiom:
∀X Y : set, X X Y
Axiom. (binunion_Subq_2) We take the following as an axiom:
∀X Y : set, Y X Y
Axiom. (binunion_Subq_min) We take the following as an axiom:
∀X Y Z : set, X ZY ZX Y Z
Axiom. (Subq_binunion_eq) We take the following as an axiom:
∀X Y, (X Y) = (X Y = Y)
Definition. We define SetAdjoin to be λX y ⇒ X {y} of type setsetset.
Notation. We now use the set enumeration notation {...,...,...} in general. If 0 elements are given, then Empty is used to form the corresponding term. If 1 element is given, then Sing is used to form the corresponding term. If 2 elements are given, then UPair is used to form the corresponding term. If more than elements are given, then SetAdjoin is used to reduce to the case with one fewer elements.
Primitive. The name famunion is a term of type set(setset)set.
Notation. We use x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using famunion.
Axiom. (famunionI) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀x y : set, x Xy F xy xXF x
Axiom. (famunionE) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)∃xX, y F x
Axiom. (famunionE_impred) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)∀p : prop, (∀x, x Xy F xp)p
Axiom. (famunion_Empty) We take the following as an axiom:
∀F : setset, (xEmptyF x) = Empty
Beginning of Section SepSec
Variable X : set
Variable P : setprop
Let z : setEps_i (λz ⇒ z X P z)
Let F : setsetλx ⇒ if P x then x else z
Primitive. The name Sep is a term of type set.
End of Section SepSec
Notation. {xA | B} is notation for Sep Ax . B).
Axiom. (SepI) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x XP xx {xX|P x}
Axiom. (SepE) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X P x
Axiom. (SepE1) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X
Axiom. (SepE2) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}P x
Axiom. (Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : setprop, {xX|P x} X
Axiom. (Sep_In_Power) We take the following as an axiom:
∀X : set, ∀P : setprop, {xX|P x} 𝒫 X
Primitive. The name ReplSep is a term of type set(setprop)(setset)set.
Notation. {B| xA, C} is notation for ReplSep Ax . C) (λ x . B).
Axiom. (ReplSepI) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀x : set, x XP xF x {F x|xX, P x}
Axiom. (ReplSepE) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}∃x : set, x X P x y = F x
Axiom. (ReplSepE_impred) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}∀p : prop, (∀xX, P xy = F xp)p
Primitive. The name binintersect is a term of type setsetset.
Notation. We use as an infix operator with priority 340 and which associates to the left corresponding to applying term binintersect.
Axiom. (binintersectI) We take the following as an axiom:
∀X Y z, z Xz Yz X Y
Axiom. (binintersectE) We take the following as an axiom:
∀X Y z, z X Yz X z Y
Axiom. (binintersectE1) We take the following as an axiom:
∀X Y z, z X Yz X
Axiom. (binintersectE2) We take the following as an axiom:
∀X Y z, z X Yz Y
Axiom. (binintersect_Subq_1) We take the following as an axiom:
∀X Y : set, X Y X
Axiom. (binintersect_Subq_2) We take the following as an axiom:
∀X Y : set, X Y Y
Axiom. (binintersect_Subq_eq_1) We take the following as an axiom:
∀X Y, X YX Y = X
Axiom. (binintersect_Subq_max) We take the following as an axiom:
∀X Y Z : set, Z XZ YZ X Y
Axiom. (binintersect_com_Subq) We take the following as an axiom:
∀X Y : set, X Y Y X
Axiom. (binintersect_com) We take the following as an axiom:
∀X Y : set, X Y = Y X
Primitive. The name setminus is a term of type setsetset.
Notation. We use as an infix operator with priority 350 and no associativity corresponding to applying term setminus.
Axiom. (setminusI) We take the following as an axiom:
∀X Y z, (z X)(z Y)z X Y
Axiom. (setminusE) We take the following as an axiom:
∀X Y z, (z X Y)z X z Y
Axiom. (setminusE1) We take the following as an axiom:
∀X Y z, (z X Y)z X
Axiom. (setminus_Subq) We take the following as an axiom:
∀X Y : set, X Y X
Axiom. (setminus_Subq_contra) We take the following as an axiom:
∀X Y Z : set, Z YX Y X Z
Axiom. (setminus_In_Power) We take the following as an axiom:
∀A U, A U 𝒫 A
Axiom. (In_irref) We take the following as an axiom:
∀x, x x
Axiom. (In_no2cycle) We take the following as an axiom:
∀x y, x yy xFalse
Primitive. The name ordsucc is a term of type setset.
Axiom. (ordsuccI1) We take the following as an axiom:
∀x : set, x ordsucc x
Axiom. (ordsuccI2) We take the following as an axiom:
∀x : set, x ordsucc x
Axiom. (ordsuccE) We take the following as an axiom:
∀x y : set, y ordsucc xy x y = x
Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.
Axiom. (neq_0_ordsucc) We take the following as an axiom:
∀a : set, 0 ordsucc a
Axiom. (neq_ordsucc_0) We take the following as an axiom:
∀a : set, ordsucc a 0
Axiom. (ordsucc_inj) We take the following as an axiom:
∀a b : set, ordsucc a = ordsucc ba = b
Axiom. (ordsucc_inj_contra) We take the following as an axiom:
∀a b : set, a bordsucc a ordsucc b
Axiom. (In_0_1) We take the following as an axiom:
0 1
Axiom. (In_0_2) We take the following as an axiom:
0 2
Axiom. (In_1_2) We take the following as an axiom:
1 2
Definition. We define nat_p to be λn : set∀p : setprop, p 0(∀x : set, p xp (ordsucc x))p n of type setprop.
Axiom. (nat_0) We take the following as an axiom:
nat_p 0
Axiom. (nat_ordsucc) We take the following as an axiom:
∀n : set, nat_p nnat_p (ordsucc n)
Axiom. (nat_1) We take the following as an axiom:
nat_p 1
Axiom. (nat_2) We take the following as an axiom:
nat_p 2
Axiom. (nat_0_in_ordsucc) We take the following as an axiom:
∀n, nat_p n0 ordsucc n
Axiom. (nat_ordsucc_in_ordsucc) We take the following as an axiom:
∀n, nat_p n∀mn, ordsucc m ordsucc n
Axiom. (nat_ind) We take the following as an axiom:
∀p : setprop, p 0(∀n, nat_p np np (ordsucc n))∀n, nat_p np n
Axiom. (nat_inv_impred) We take the following as an axiom:
∀p : setprop, p 0(∀n, nat_p np (ordsucc n))∀n, nat_p np n
Axiom. (nat_inv) We take the following as an axiom:
∀n, nat_p nn = 0 ∃x, nat_p x n = ordsucc x
Axiom. (nat_complete_ind) We take the following as an axiom:
∀p : setprop, (∀n, nat_p n(∀mn, p m)p n)∀n, nat_p np n
Axiom. (nat_p_trans) We take the following as an axiom:
∀n, nat_p n∀mn, nat_p m
Axiom. (nat_trans) We take the following as an axiom:
∀n, nat_p n∀mn, m n
Axiom. (nat_ordsucc_trans) We take the following as an axiom:
∀n, nat_p n∀mordsucc n, m n
Axiom. (Union_ordsucc_eq) We take the following as an axiom:
∀n, nat_p n (ordsucc n) = n
Axiom. (cases_1) We take the following as an axiom:
∀i1, ∀p : setprop, p 0p i
Axiom. (cases_2) We take the following as an axiom:
∀i2, ∀p : setprop, p 0p 1p i
Axiom. (cases_3) We take the following as an axiom:
∀i3, ∀p : setprop, p 0p 1p 2p i
Axiom. (neq_0_1) We take the following as an axiom:
0 1
Axiom. (neq_1_0) We take the following as an axiom:
1 0
Axiom. (neq_0_2) We take the following as an axiom:
0 2
Axiom. (neq_2_0) We take the following as an axiom:
2 0
Axiom. (neq_1_2) We take the following as an axiom:
1 2
Axiom. (ZF_closed_E) We take the following as an axiom:
∀U, ZF_closed U∀p : prop, (Union_closed UPower_closed URepl_closed Up)p
Axiom. (ZF_Union_closed) We take the following as an axiom:
∀U, ZF_closed U∀XU, X U
Axiom. (ZF_Power_closed) We take the following as an axiom:
∀U, ZF_closed U∀XU, 𝒫 X U
Axiom. (ZF_Repl_closed) We take the following as an axiom:
∀U, ZF_closed U∀XU, ∀F : setset, (∀xX, F x U){F x|xX} U
Axiom. (ZF_UPair_closed) We take the following as an axiom:
∀U, ZF_closed U∀x yU, {x,y} U
Axiom. (ZF_Sing_closed) We take the following as an axiom:
∀U, ZF_closed U∀xU, {x} U
Axiom. (ZF_binunion_closed) We take the following as an axiom:
∀U, ZF_closed U∀X YU, (X Y) U
Axiom. (ZF_ordsucc_closed) We take the following as an axiom:
∀U, ZF_closed U∀xU, ordsucc x U
Axiom. (nat_p_UnivOf_Empty) We take the following as an axiom:
∀n : set, nat_p nn UnivOf Empty
Primitive. The name ω is a term of type set.
Axiom. (omega_nat_p) We take the following as an axiom:
∀nω, nat_p n
Axiom. (nat_p_omega) We take the following as an axiom:
∀n : set, nat_p nn ω
Axiom. (omega_ordsucc) We take the following as an axiom:
∀nω, ordsucc n ω
Definition. We define ordinal to be λalpha : setTransSet alpha ∀betaalpha, TransSet beta of type setprop.
Axiom. (ordinal_TransSet) We take the following as an axiom:
∀alpha : set, ordinal alphaTransSet alpha
Axiom. (ordinal_Empty) We take the following as an axiom:
ordinal Empty
Axiom. (ordinal_Hered) We take the following as an axiom:
∀alpha : set, ordinal alpha∀betaalpha, ordinal beta
Axiom. (TransSet_ordsucc) We take the following as an axiom:
∀X : set, TransSet XTransSet (ordsucc X)
Axiom. (ordinal_ordsucc) We take the following as an axiom:
∀alpha : set, ordinal alphaordinal (ordsucc alpha)
Axiom. (nat_p_ordinal) We take the following as an axiom:
∀n : set, nat_p nordinal n
Axiom. (ordinal_1) We take the following as an axiom:
ordinal 1
Axiom. (ordinal_2) We take the following as an axiom:
ordinal 2
Axiom. (omega_TransSet) We take the following as an axiom:
TransSet ω
Axiom. (omega_ordinal) We take the following as an axiom:
ordinal ω
Axiom. (ordsucc_omega_ordinal) We take the following as an axiom:
ordinal (ordsucc ω)
Axiom. (TransSet_ordsucc_In_Subq) We take the following as an axiom:
∀X : set, TransSet X∀xX, ordsucc x X
Axiom. (ordinal_ordsucc_In_Subq) We take the following as an axiom:
∀alpha, ordinal alpha∀betaalpha, ordsucc beta alpha
Axiom. (ordinal_trichotomy_or) We take the following as an axiom:
∀alpha beta : set, ordinal alphaordinal betaalpha beta alpha = beta beta alpha
Axiom. (ordinal_trichotomy_or_impred) We take the following as an axiom:
∀alpha beta : set, ordinal alphaordinal beta∀p : prop, (alpha betap)(alpha = betap)(beta alphap)p
Axiom. (ordinal_In_Or_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha beta beta alpha
Axiom. (ordinal_linear) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha beta beta alpha
Axiom. (ordinal_ordsucc_In_eq) We take the following as an axiom:
∀alpha beta, ordinal alphabeta alphaordsucc beta alpha alpha = ordsucc beta
Axiom. (ordinal_lim_or_succ) We take the following as an axiom:
∀alpha, ordinal alpha(∀betaalpha, ordsucc beta alpha) (∃betaalpha, alpha = ordsucc beta)
Axiom. (ordinal_ordsucc_In) We take the following as an axiom:
∀alpha, ordinal alpha∀betaalpha, ordsucc beta ordsucc alpha
Axiom. (ordinal_famunion) We take the following as an axiom:
∀X, ∀F : setset, (∀xX, ordinal (F x))ordinal (xXF x)
Axiom. (ordinal_binintersect) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaordinal (alpha beta)
Axiom. (ordinal_binunion) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaordinal (alpha beta)
Axiom. (ordinal_ind) We take the following as an axiom:
∀p : setprop, (∀alpha, ordinal alpha(∀betaalpha, p beta)p alpha)∀alpha, ordinal alphap alpha
Axiom. (least_ordinal_ex) We take the following as an axiom:
∀p : setprop, (∃alpha, ordinal alpha p alpha)∃alpha, ordinal alpha p alpha ∀betaalpha, ¬ p beta
Definition. We define inj to be λX Y f ⇒ (∀uX, f u Y) (∀u vX, f u = f vu = v) of type setset(setset)prop.
Definition. We define bij to be λX Y f ⇒ (∀uX, f u Y) (∀u vX, f u = f vu = v) (∀wY, ∃uX, f u = w) of type setset(setset)prop.
Axiom. (bijI) We take the following as an axiom:
∀X Y, ∀f : setset, (∀uX, f u Y)(∀u vX, f u = f vu = v)(∀wY, ∃uX, f u = w)bij X Y f
Axiom. (bijE) We take the following as an axiom:
∀X Y, ∀f : setset, bij X Y f∀p : prop, ((∀uX, f u Y)(∀u vX, f u = f vu = v)(∀wY, ∃uX, f u = w)p)p
Primitive. The name inv is a term of type set(setset)setset.
Axiom. (surj_rinv) We take the following as an axiom:
∀X Y, ∀f : setset, (∀wY, ∃uX, f u = w)∀yY, inv X f y X f (inv X f y) = y
Axiom. (inj_linv) We take the following as an axiom:
∀X, ∀f : setset, (∀u vX, f u = f vu = v)∀xX, inv X f (f x) = x
Axiom. (bij_inv) We take the following as an axiom:
∀X Y, ∀f : setset, bij X Y fbij Y X (inv X f)
Axiom. (bij_id) We take the following as an axiom:
∀X, bij X X (λx ⇒ x)
Axiom. (bij_comp) We take the following as an axiom:
∀X Y Z : set, ∀f g : setset, bij X Y fbij Y Z gbij X Z (λx ⇒ g (f x))
Definition. We define equip to be λX Y : set∃f : setset, bij X Y f of type setsetprop.
Axiom. (equip_ref) We take the following as an axiom:
∀X, equip X X
Axiom. (equip_sym) We take the following as an axiom:
∀X Y, equip X Yequip Y X
Axiom. (equip_tra) We take the following as an axiom:
∀X Y Z, equip X Yequip Y Zequip X Z
Axiom. (equip_0_Empty) We take the following as an axiom:
∀X, equip X 0X = 0
Beginning of Section SchroederBernstein
Axiom. (KnasterTarski_set) We take the following as an axiom:
∀A, ∀F : setset, (∀U𝒫 A, F U 𝒫 A)(∀U V𝒫 A, U VF U F V)∃Y𝒫 A, F Y = Y
Axiom. (image_In_Power) We take the following as an axiom:
∀A B, ∀f : setset, (∀xA, f x B)∀U𝒫 A, {f x|xU} 𝒫 B
Axiom. (image_monotone) We take the following as an axiom:
∀f : setset, ∀U V, U V{f x|xU} {f x|xV}
Axiom. (setminus_antimonotone) We take the following as an axiom:
∀A U V, U VA V A U
Axiom. (SchroederBernstein) We take the following as an axiom:
∀A B, ∀f g : setset, inj A B finj B A gequip A B
End of Section SchroederBernstein
Beginning of Section PigeonHole
Axiom. (PigeonHole_nat) We take the following as an axiom:
∀n, nat_p n∀f : setset, (∀iordsucc n, f i n)¬ (∀i jordsucc n, f i = f ji = j)
Axiom. (PigeonHole_nat_bij) We take the following as an axiom:
∀n, nat_p n∀f : setset, (∀in, f i n)(∀i jn, f i = f ji = j)bij n n f
End of Section PigeonHole
Definition. We define finite to be λX ⇒ ∃nω, equip X n of type setprop.
Axiom. (finite_ind) We take the following as an axiom:
∀p : setprop, p Empty(∀X y, finite Xy Xp Xp (X {y}))∀X, finite Xp X
Axiom. (finite_Empty) We take the following as an axiom:
finite 0
Axiom. (adjoin_finite) We take the following as an axiom:
∀X y, finite Xfinite (X {y})
Axiom. (binunion_finite) We take the following as an axiom:
∀X, finite X∀Y, finite Yfinite (X Y)
Axiom. (famunion_nat_finite) We take the following as an axiom:
∀X : setset, ∀n, nat_p n(∀in, finite (X i))finite (inX i)
Axiom. (Subq_finite) We take the following as an axiom:
∀X, finite X∀Y, Y Xfinite Y
Axiom. (TransSet_In_ordsucc_Subq) We take the following as an axiom:
∀x y, TransSet yx ordsucc yx y
Axiom. (exandE_i) We take the following as an axiom:
∀P Q : setprop, (∃x, P x Q x)∀r : prop, (∀x, P xQ xr)r
Axiom. (exandE_ii) We take the following as an axiom:
∀P Q : (setset)prop, (∃x : setset, P x Q x)∀p : prop, (∀x : setset, P xQ xp)p
Axiom. (exandE_iii) We take the following as an axiom:
∀P Q : (setsetset)prop, (∃x : setsetset, P x Q x)∀p : prop, (∀x : setsetset, P xQ xp)p
Axiom. (exandE_iiii) We take the following as an axiom:
∀P Q : (setsetsetset)prop, (∃x : setsetsetset, P x Q x)∀p : prop, (∀x : setsetsetset, P xQ xp)p
Beginning of Section Descr_ii
Variable P : (setset)prop
Primitive. The name Descr_ii is a term of type setset.
Hypothesis Pex : ∃f : setset, P f
Hypothesis Puniq : ∀f g : setset, P fP gf = g
Axiom. (Descr_ii_prop) We take the following as an axiom:
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (setsetset)prop
Primitive. The name Descr_iii is a term of type setsetset.
Hypothesis Pex : ∃f : setsetset, P f
Hypothesis Puniq : ∀f g : setsetset, P fP gf = g
Axiom. (Descr_iii_prop) We take the following as an axiom:
End of Section Descr_iii
Beginning of Section Descr_Vo1
Variable P : Vo 1prop
Primitive. The name Descr_Vo1 is a term of type Vo 1.
Hypothesis Pex : ∃f : Vo 1, P f
Hypothesis Puniq : ∀f g : Vo 1, P fP gf = g
Axiom. (Descr_Vo1_prop) We take the following as an axiom:
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : setset
Primitive. The name If_ii is a term of type setset.
Axiom. (If_ii_1) We take the following as an axiom:
pIf_ii = f
Axiom. (If_ii_0) We take the following as an axiom:
¬ pIf_ii = g
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : setsetset
Primitive. The name If_iii is a term of type setsetset.
Axiom. (If_iii_1) We take the following as an axiom:
pIf_iii = f
Axiom. (If_iii_0) We take the following as an axiom:
¬ pIf_iii = g
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set(setset)set
Primitive. The name In_rec_i is a term of type setset.
Hypothesis Fr : ∀X : set, ∀g h : setset, (∀xX, g x = h x)F X g = F X h
Axiom. (In_rec_i_eq) We take the following as an axiom:
∀X : set, In_rec_i X = F X In_rec_i
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set(set(setset))(setset)
Primitive. The name In_rec_ii is a term of type set(setset).
Hypothesis Fr : ∀X : set, ∀g h : set(setset), (∀xX, g x = h x)F X g = F X h
Axiom. (In_rec_ii_eq) We take the following as an axiom:
∀X : set, In_rec_ii X = F X In_rec_ii
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set(set(setsetset))(setsetset)
Primitive. The name In_rec_iii is a term of type set(setsetset).
Hypothesis Fr : ∀X : set, ∀g h : set(setsetset), (∀xX, g x = h x)F X g = F X h
Axiom. (In_rec_iii_eq) We take the following as an axiom:
∀X : set, In_rec_iii X = F X In_rec_iii
End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : setsetset
Let F : set(setset)setλn g ⇒ if n n then f ( n) (g ( n)) else z
Definition. We define nat_primrec to be In_rec_i F of type setset.
Axiom. (nat_primrec_r) We take the following as an axiom:
∀X : set, ∀g h : setset, (∀xX, g x = h x)F X g = F X h
Axiom. (nat_primrec_0) We take the following as an axiom:
Axiom. (nat_primrec_S) We take the following as an axiom:
∀n : set, nat_p nnat_primrec (ordsucc n) = f n (nat_primrec n)
End of Section NatRec
Beginning of Section NatArith
Definition. We define add_nat to be λn m : setnat_primrec n (λ_ r ⇒ ordsucc r) m of type setsetset.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Axiom. (add_nat_0R) We take the following as an axiom:
∀n : set, n + 0 = n
Axiom. (add_nat_SR) We take the following as an axiom:
∀n m : set, nat_p mn + ordsucc m = ordsucc (n + m)
Axiom. (add_nat_p) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p mnat_p (n + m)
Axiom. (add_nat_1_1_2) We take the following as an axiom:
1 + 1 = 2
Definition. We define mul_nat to be λn m : setnat_primrec 0 (λ_ r ⇒ n + r) m of type setsetset.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
Axiom. (mul_nat_0R) We take the following as an axiom:
∀n : set, n * 0 = 0
Axiom. (mul_nat_SR) We take the following as an axiom:
∀n m : set, nat_p mn * ordsucc m = n + n * m
Axiom. (mul_nat_p) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p mnat_p (n * m)
End of Section NatArith
Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0} {f x|xX}) of type setset.
Axiom. (Inj1_eq) We take the following as an axiom:
∀X : set, Inj1 X = {0} {Inj1 x|xX}
Axiom. (Inj1I1) We take the following as an axiom:
∀X : set, 0 Inj1 X
Axiom. (Inj1I2) We take the following as an axiom:
∀X x : set, x XInj1 x Inj1 X
Axiom. (Inj1E) We take the following as an axiom:
∀X y : set, y Inj1 Xy = 0 ∃xX, y = Inj1 x
Axiom. (Inj1NE1) We take the following as an axiom:
∀x : set, Inj1 x 0
Axiom. (Inj1NE2) We take the following as an axiom:
∀x : set, Inj1 x {0}
Definition. We define Inj0 to be λX ⇒ {Inj1 x|xX} of type setset.
Axiom. (Inj0I) We take the following as an axiom:
∀X x : set, x XInj1 x Inj0 X
Axiom. (Inj0E) We take the following as an axiom:
∀X y : set, y Inj0 X∃x : set, x X y = Inj1 x
Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|xX {0}}) of type setset.
Axiom. (Unj_eq) We take the following as an axiom:
∀X : set, Unj X = {Unj x|xX {0}}
Axiom. (Unj_Inj1_eq) We take the following as an axiom:
∀X : set, Unj (Inj1 X) = X
Axiom. (Inj1_inj) We take the following as an axiom:
∀X Y : set, Inj1 X = Inj1 YX = Y
Axiom. (Unj_Inj0_eq) We take the following as an axiom:
∀X : set, Unj (Inj0 X) = X
Axiom. (Inj0_inj) We take the following as an axiom:
∀X Y : set, Inj0 X = Inj0 YX = Y
Axiom. (Inj0_0) We take the following as an axiom:
Inj0 0 = 0
Axiom. (Inj0_Inj1_neq) We take the following as an axiom:
∀X Y : set, Inj0 X Inj1 Y
Definition. We define setsum to be λX Y ⇒ {Inj0 x|xX} {Inj1 y|yY} of type setsetset.
Notation. We use + as an infix operator with priority 450 and which associates to the left corresponding to applying term setsum.
Axiom. (Inj0_setsum) We take the following as an axiom:
∀X Y x : set, x XInj0 x X + Y
Axiom. (Inj1_setsum) We take the following as an axiom:
∀X Y y : set, y YInj1 y X + Y
Axiom. (setsum_Inj_inv) We take the following as an axiom:
∀X Y z : set, z X + Y(∃xX, z = Inj0 x) (∃yY, z = Inj1 y)
Axiom. (Inj0_setsum_0L) We take the following as an axiom:
∀X : set, 0 + X = Inj0 X
Axiom. (Subq_1_Sing0) We take the following as an axiom:
1 {0}
Axiom. (Inj1_setsum_1L) We take the following as an axiom:
∀X : set, 1 + X = Inj1 X
Axiom. (nat_setsum1_ordsucc) We take the following as an axiom:
∀n : set, nat_p n1 + n = ordsucc n
Axiom. (setsum_0_0) We take the following as an axiom:
0 + 0 = 0
Axiom. (setsum_1_0_1) We take the following as an axiom:
1 + 0 = 1
Axiom. (setsum_1_1_2) We take the following as an axiom:
1 + 1 = 2
Beginning of Section pair_setsum
Let pair ≝ setsum
Definition. We define proj0 to be λZ ⇒ {Unj z|zZ, ∃x : set, Inj0 x = z} of type setset.
Definition. We define proj1 to be λZ ⇒ {Unj z|zZ, ∃y : set, Inj1 y = z} of type setset.
Axiom. (Inj0_pair_0_eq) We take the following as an axiom:
Inj0 = pair 0
Axiom. (Inj1_pair_1_eq) We take the following as an axiom:
Inj1 = pair 1
Axiom. (pairI0) We take the following as an axiom:
∀X Y x, x Xpair 0 x pair X Y
Axiom. (pairI1) We take the following as an axiom:
∀X Y y, y Ypair 1 y pair X Y
Axiom. (pairE) We take the following as an axiom:
∀X Y z, z pair X Y(∃xX, z = pair 0 x) (∃yY, z = pair 1 y)
Axiom. (pairE0) We take the following as an axiom:
∀X Y x, pair 0 x pair X Yx X
Axiom. (pairE1) We take the following as an axiom:
∀X Y y, pair 1 y pair X Yy Y
Axiom. (proj0I) We take the following as an axiom:
∀w u : set, pair 0 u wu proj0 w
Axiom. (proj0E) We take the following as an axiom:
∀w u : set, u proj0 wpair 0 u w
Axiom. (proj1I) We take the following as an axiom:
∀w u : set, pair 1 u wu proj1 w
Axiom. (proj1E) We take the following as an axiom:
∀w u : set, u proj1 wpair 1 u w
Axiom. (proj0_pair_eq) We take the following as an axiom:
∀X Y : set, proj0 (pair X Y) = X
Axiom. (proj1_pair_eq) We take the following as an axiom:
∀X Y : set, proj1 (pair X Y) = Y
Definition. We define Sigma to be λX Y ⇒ xX{pair x y|yY x} of type set(setset)set.
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
Axiom. (pair_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀xX, ∀yY x, pair x y xX, Y x
Axiom. (Sigma_eta_proj0_proj1) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z(xX, Y x), pair (proj0 z) (proj1 z) = z proj0 z X proj1 z Y (proj0 z)
Axiom. (proj_Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z(xX, Y x), pair (proj0 z) (proj1 z) = z
Axiom. (proj0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj0 z X
Axiom. (proj1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj1 z Y (proj0 z)
Axiom. (pair_Sigma_E1) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀x y : set, pair x y (xX, Y x)y Y x
Axiom. (Sigma_E) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)∃xX, ∃yY x, z = pair x y
Definition. We define setprod to be λX Y : setxX, Y of type setsetset.
Notation. We use as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Let lam : set(setset)setSigma
Definition. We define ap to be λf x ⇒ {proj1 z|zf, ∃y : set, z = pair x y} of type setsetset.
Notation. When x is a set, a term x y is notation for ap x y.
Notation. λ xAB is notation for the set Sigma Ax : set ⇒ B).
Notation. We now use n-tuple notation (a0,...,an-1) for n ≥ 2 for λ i ∈ n . if i = 0 then a0 else ... if i = n-2 then an-2 else an-1.
Axiom. (lamI) We take the following as an axiom:
∀X : set, ∀F : setset, ∀xX, ∀yF x, pair x y λxXF x
Axiom. (lamE) We take the following as an axiom:
∀X : set, ∀F : setset, ∀z : set, z (λxXF x)∃xX, ∃yF x, z = pair x y
Axiom. (apI) We take the following as an axiom:
∀f x y, pair x y fy f x
Axiom. (apE) We take the following as an axiom:
∀f x y, y f xpair x y f
Axiom. (beta) We take the following as an axiom:
∀X : set, ∀F : setset, ∀x : set, x X(λxXF x) x = F x
Axiom. (proj0_ap_0) We take the following as an axiom:
∀u, proj0 u = u 0
Axiom. (proj1_ap_1) We take the following as an axiom:
∀u, proj1 u = u 1
Axiom. (pair_ap_0) We take the following as an axiom:
∀x y : set, (pair x y) 0 = x
Axiom. (pair_ap_1) We take the following as an axiom:
∀x y : set, (pair x y) 1 = y
Axiom. (ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 0) X
Axiom. (ap1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 1) (Y (z 0))
Definition. We define pair_p to be λu : setpair (u 0) (u 1) = u of type setprop.
Axiom. (pair_p_I) We take the following as an axiom:
∀x y, pair_p (pair x y)
Axiom. (Subq_2_UPair01) We take the following as an axiom:
Axiom. (tuple_pair) We take the following as an axiom:
∀x y : set, pair x y = (x,y)
Definition. We define Pi to be λX Y ⇒ {f𝒫 (xX, (Y x))|∀xX, f x Y x} of type set(setset)set.
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
Axiom. (PiI) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, (∀uf, pair_p u u 0 X)(∀xX, f x Y x)f xX, Y x
Axiom. (lam_Pi) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀F : setset, (∀xX, F x Y x)(λxXF x) (xX, Y x)
Axiom. (ap_Pi) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, ∀x : set, f (xX, Y x)x Xf x Y x
Definition. We define setexp to be λX Y : setyY, X of type setsetset.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
Axiom. (pair_tuple_fun) We take the following as an axiom:
pair = (λx y ⇒ (x,y))
Axiom. (lamI2) We take the following as an axiom:
∀X, ∀F : setset, ∀xX, ∀yF x, (x,y) λxXF x
Beginning of Section Tuples
Variable x0 x1 : set
Axiom. (tuple_2_0_eq) We take the following as an axiom:
(x0,x1) 0 = x0
Axiom. (tuple_2_1_eq) We take the following as an axiom:
(x0,x1) 1 = x1
End of Section Tuples
Axiom. (ReplEq_setprod_ext) We take the following as an axiom:
∀X Y, ∀F G : setsetset, (∀xX, ∀yY, F x y = G x y){F (w 0) (w 1)|wX Y} = {G (w 0) (w 1)|wX Y}
Axiom. (tuple_2_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀xX, ∀yY x, (x,y) xX, Y x
Axiom. (tuple_2_setprod) We take the following as an axiom:
∀X : set, ∀Y : set, ∀xX, ∀yY, (x,y) X Y
End of Section pair_setsum
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
Notation. We use as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
Primitive. The name DescrR_i_io_1 is a term of type (set(setprop)prop)set.
Primitive. The name DescrR_i_io_2 is a term of type (set(setprop)prop)setprop.
Axiom. (DescrR_i_io_12) We take the following as an axiom:
∀R : set(setprop)prop, (∃x, (∃y : setprop, R x y) (∀y z : setprop, R x yR x zy = z))R (DescrR_i_io_1 R) (DescrR_i_io_2 R)
Definition. We define PNoEq_ to be λalpha p q ⇒ ∀betaalpha, p beta q beta of type set(setprop)(setprop)prop.
Axiom. (PNoEq_ref_) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoEq_ alpha p p
Axiom. (PNoEq_sym_) We take the following as an axiom:
∀alpha, ∀p q : setprop, PNoEq_ alpha p qPNoEq_ alpha q p
Axiom. (PNoEq_tra_) We take the following as an axiom:
∀alpha, ∀p q r : setprop, PNoEq_ alpha p qPNoEq_ alpha q rPNoEq_ alpha p r
Axiom. (PNoEq_antimon_) We take the following as an axiom:
∀p q : setprop, ∀alpha, ordinal alpha∀betaalpha, PNoEq_ alpha p qPNoEq_ beta p q
Definition. We define PNoLt_ to be λalpha p q ⇒ ∃betaalpha, PNoEq_ beta p q ¬ p beta q beta of type set(setprop)(setprop)prop.
Axiom. (PNoLt_E_) We take the following as an axiom:
∀alpha, ∀p q : setprop, PNoLt_ alpha p q∀R : prop, (∀beta, beta alphaPNoEq_ beta p q¬ p betaq betaR)R
Axiom. (PNoLt_irref_) We take the following as an axiom:
∀alpha, ∀p : setprop, ¬ PNoLt_ alpha p p
Axiom. (PNoLt_mon_) We take the following as an axiom:
∀p q : setprop, ∀alpha, ordinal alpha∀betaalpha, PNoLt_ beta p qPNoLt_ alpha p q
Axiom. (PNoLt_trichotomy_or_) We take the following as an axiom:
∀p q : setprop, ∀alpha, ordinal alphaPNoLt_ alpha p q PNoEq_ alpha p q PNoLt_ alpha q p
Axiom. (PNoLt_tra_) We take the following as an axiom:
∀alpha, ordinal alpha∀p q r : setprop, PNoLt_ alpha p qPNoLt_ alpha q rPNoLt_ alpha p r
Primitive. The name PNoLt is a term of type set(setprop)set(setprop)prop.
Axiom. (PNoLtI1) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, PNoLt_ (alpha beta) p qPNoLt alpha p beta q
Axiom. (PNoLtI2) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, alpha betaPNoEq_ alpha p qq alphaPNoLt alpha p beta q
Axiom. (PNoLtI3) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, beta alphaPNoEq_ beta p q¬ p betaPNoLt alpha p beta q
Axiom. (PNoLtE) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, PNoLt alpha p beta q∀R : prop, (PNoLt_ (alpha beta) p qR)(alpha betaPNoEq_ alpha p qq alphaR)(beta alphaPNoEq_ beta p q¬ p betaR)R
Axiom. (PNoLt_irref) We take the following as an axiom:
∀alpha, ∀p : setprop, ¬ PNoLt alpha p alpha p
Axiom. (PNoLt_trichotomy_or) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNoLt alpha p beta q alpha = beta PNoEq_ alpha p q PNoLt beta q alpha p
Axiom. (PNoLtEq_tra) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoLt alpha p beta qPNoEq_ beta q rPNoLt alpha p beta r
Axiom. (PNoEqLt_tra) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoEq_ alpha p qPNoLt alpha q beta rPNoLt alpha p beta r
Axiom. (PNoLt_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLt alpha p beta qPNoLt beta q gamma rPNoLt alpha p gamma r
Definition. We define PNoLe to be λalpha p beta q ⇒ PNoLt alpha p beta q alpha = beta PNoEq_ alpha p q of type set(setprop)set(setprop)prop.
Axiom. (PNoLeI1) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, PNoLt alpha p beta qPNoLe alpha p beta q
Axiom. (PNoLeI2) We take the following as an axiom:
∀alpha, ∀p q : setprop, PNoEq_ alpha p qPNoLe alpha p alpha q
Axiom. (PNoLe_ref) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoLe alpha p alpha p
Axiom. (PNoLe_antisym) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q : setprop, PNoLe alpha p beta qPNoLe beta q alpha palpha = beta PNoEq_ alpha p q
Axiom. (PNoLtLe_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLt alpha p beta qPNoLe beta q gamma rPNoLt alpha p gamma r
Axiom. (PNoLeLt_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLe alpha p beta qPNoLt beta q gamma rPNoLt alpha p gamma r
Axiom. (PNoEqLe_tra) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoEq_ alpha p qPNoLe alpha q beta rPNoLe alpha p beta r
Axiom. (PNoLe_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLe alpha p beta qPNoLe beta q gamma rPNoLe alpha p gamma r
Definition. We define PNo_downc to be λL alpha p ⇒ ∃beta, ordinal beta ∃q : setprop, L beta q PNoLe alpha p beta q of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_upc to be λR alpha p ⇒ ∃beta, ordinal beta ∃q : setprop, R beta q PNoLe beta q alpha p of type (set(setprop)prop)set(setprop)prop.
Axiom. (PNoLe_downc) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNo_downc L alpha pPNoLe beta q alpha pPNo_downc L beta q
Axiom. (PNo_downc_ref) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, L alpha pPNo_downc L alpha p
Axiom. (PNo_upc_ref) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, R alpha pPNo_upc R alpha p
Axiom. (PNoLe_upc) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNo_upc R alpha pPNoLe alpha p beta qPNo_upc R beta q
Definition. We define PNoLt_pwise to be λL R ⇒ ∀gamma, ordinal gamma∀p : setprop, L gamma p∀delta, ordinal delta∀q : setprop, R delta qPNoLt gamma p delta q of type (set(setprop)prop)(set(setprop)prop)prop.
Axiom. (PNoLt_pwise_downc_upc) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L RPNoLt_pwise (PNo_downc L) (PNo_upc R)
Definition. We define PNo_rel_strict_upperbd to be λL alpha p ⇒ ∀betaalpha, ∀q : setprop, PNo_downc L beta qPNoLt beta q alpha p of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_rel_strict_lowerbd to be λR alpha p ⇒ ∀betaalpha, ∀q : setprop, PNo_upc R beta qPNoLt alpha p beta q of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_rel_strict_imv to be λL R alpha p ⇒ PNo_rel_strict_upperbd L alpha p PNo_rel_strict_lowerbd R alpha p of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Axiom. (PNoEq_rel_strict_upperbd) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_rel_strict_upperbd L alpha pPNo_rel_strict_upperbd L alpha q
Axiom. (PNo_rel_strict_upperbd_antimon) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, ∀betaalpha, PNo_rel_strict_upperbd L alpha pPNo_rel_strict_upperbd L beta p
Axiom. (PNoEq_rel_strict_lowerbd) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_rel_strict_lowerbd R alpha pPNo_rel_strict_lowerbd R alpha q
Axiom. (PNo_rel_strict_lowerbd_antimon) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, ∀betaalpha, PNo_rel_strict_lowerbd R alpha pPNo_rel_strict_lowerbd R beta p
Axiom. (PNoEq_rel_strict_imv) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R alpha q
Axiom. (PNo_rel_strict_imv_antimon) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, ∀betaalpha, PNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R beta p
Definition. We define PNo_rel_strict_uniq_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R alpha p ∀q : setprop, PNo_rel_strict_imv L R alpha qPNoEq_ alpha p q of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Definition. We define PNo_rel_strict_split_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta alpha) PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta = alpha) of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Axiom. (PNo_extend0_eq) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoEq_ alpha p (λdelta ⇒ p delta delta alpha)
Axiom. (PNo_extend1_eq) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoEq_ alpha p (λdelta ⇒ p delta delta = alpha)
Axiom. (PNo_rel_imv_ex) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alpha(∃p : setprop, PNo_rel_strict_uniq_imv L R alpha p) (∃taualpha, ∃p : setprop, PNo_rel_strict_split_imv L R tau p)
Definition. We define PNo_lenbdd to be λalpha L ⇒ ∀beta, ∀p : setprop, L beta pbeta alpha of type set(set(setprop)prop)prop.
Axiom. (PNo_lenbdd_strict_imv_extend0) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∀p : setprop, PNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta alpha)
Axiom. (PNo_lenbdd_strict_imv_extend1) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∀p : setprop, PNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta = alpha)
Axiom. (PNo_lenbdd_strict_imv_split) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∀p : setprop, PNo_rel_strict_imv L R alpha pPNo_rel_strict_split_imv L R alpha p
Axiom. (PNo_rel_imv_bdd_ex) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∃betaordsucc alpha, ∃p : setprop, PNo_rel_strict_split_imv L R beta p
Definition. We define PNo_strict_upperbd to be λL alpha p ⇒ ∀beta, ordinal beta∀q : setprop, L beta qPNoLt beta q alpha p of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_strict_lowerbd to be λR alpha p ⇒ ∀beta, ordinal beta∀q : setprop, R beta qPNoLt alpha p beta q of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_strict_imv to be λL R alpha p ⇒ PNo_strict_upperbd L alpha p PNo_strict_lowerbd R alpha p of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Axiom. (PNoEq_strict_upperbd) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_strict_upperbd L alpha pPNo_strict_upperbd L alpha q
Axiom. (PNoEq_strict_lowerbd) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_strict_lowerbd R alpha pPNo_strict_lowerbd R alpha q
Axiom. (PNoEq_strict_imv) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_strict_imv L R alpha pPNo_strict_imv L R alpha q
Axiom. (PNo_strict_upperbd_imp_rel_strict_upperbd) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀betaordsucc alpha, ∀p : setprop, PNo_strict_upperbd L alpha pPNo_rel_strict_upperbd L beta p
Axiom. (PNo_strict_lowerbd_imp_rel_strict_lowerbd) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀betaordsucc alpha, ∀p : setprop, PNo_strict_lowerbd R alpha pPNo_rel_strict_lowerbd R beta p
Axiom. (PNo_strict_imv_imp_rel_strict_imv) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀betaordsucc alpha, ∀p : setprop, PNo_strict_imv L R alpha pPNo_rel_strict_imv L R beta p
Axiom. (PNo_rel_split_imv_imp_strict_imv) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, PNo_rel_strict_split_imv L R alpha pPNo_strict_imv L R alpha p
Axiom. (PNo_lenbdd_strict_imv_ex) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∃betaordsucc alpha, ∃p : setprop, PNo_strict_imv L R beta p
Definition. We define PNo_least_rep to be λL R beta p ⇒ ordinal beta PNo_strict_imv L R beta p ∀gammabeta, ∀q : setprop, ¬ PNo_strict_imv L R gamma q of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Definition. We define PNo_least_rep2 to be λL R beta p ⇒ PNo_least_rep L R beta p ∀x, x beta¬ p x of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Axiom. (PNo_strict_imv_pred_eq) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alpha∀p q : setprop, PNo_least_rep L R alpha pPNo_strict_imv L R alpha q∀betaalpha, p beta q beta
Axiom. (PNo_lenbdd_least_rep2_exuniq2) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∃beta, (∃p : setprop, PNo_least_rep2 L R beta p) (∀p q : setprop, PNo_least_rep2 L R beta pPNo_least_rep2 L R beta qp = q)
Primitive. The name PNo_bd is a term of type (set(setprop)prop)(set(setprop)prop)set.
Primitive. The name PNo_pred is a term of type (set(setprop)prop)(set(setprop)prop)setprop.
Axiom. (PNo_bd_pred_lem) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha RPNo_least_rep2 L R (PNo_bd L R) (PNo_pred L R)
Axiom. (PNo_bd_pred) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha RPNo_least_rep L R (PNo_bd L R) (PNo_pred L R)
Axiom. (PNo_bd_In) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha RPNo_bd L R ordsucc alpha
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:
Axiom. (not_ordinal_Sing1) We take the following as an axiom:
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 '|gammaalpha}beta alpha
Axiom. (ordinal_notin_tagged_Repl) We take the following as an axiom:
∀alpha Y, ordinal alphaalpha {y '|yY}
Definition. We define SNoElts_ to be λalpha ⇒ alpha {beta '|betaalpha} 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 ⇒ {betaalpha|p beta} {beta '|betaalpha, ¬ 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 x alpha 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 x beta 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 < y x = 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 x SNoLev ySNoEq_ (SNoLev z) z xSNoEq_ (SNoLev z) z yx < zz < ySNoLev z xSNoLev z yp)(SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yp)(SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev y xp)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 y xx < 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 < y x = y y < 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 < y y 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 alpha PSNo alpha p L) (λalpha p ⇒ ordinal alpha PSNo alpha p R)) (PNo_pred (λalpha p ⇒ ordinal alpha PSNo alpha p L) (λalpha p ⇒ ordinal alpha PSNo 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 ((xLordsucc (SNoLev x)) (yRordsucc (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 z SNoEq_ (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 ((xLordsucc (SNoLev x)) (yRordsucc (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 z SNoEq_ (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)|∃betaalpha, SNo_ beta x} of type setset.
Axiom. (SNoS_E) We take the following as an axiom:
∀alpha, ordinal alpha∀xSNoS_ alpha, ∃betaalpha, 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), x w
Axiom. (SNoS_SNoLev) We take the following as an axiom:
∀z, SNo zz SNoS_ (ordsucc (SNoLev z))
Definition. We define SNoL to be λz ⇒ {xSNoS_ (SNoLev z)|x < z} of type setset.
Definition. We define SNoR to be λz ⇒ {ySNoS_ (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 z SNoEq_ (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. (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:
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:
Axiom. (SNo_1) We take the following as an axiom:
Axiom. (SNo_2) We take the following as an axiom:
Axiom. (SNoLev_0) We take the following as an axiom:
Axiom. (SNoCut_0_0) We take the following as an axiom:
Axiom. (SNoL_0) We take the following as an axiom:
Axiom. (SNoR_0) We take the following as an axiom:
Axiom. (SNoL_1) We take the following as an axiom:
Axiom. (SNoR_1) We take the following as an axiom:
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
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta x delta SNoLev x) of type setset.
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta x delta = 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 x SNo_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
Definition. We define eps_ to be λn ⇒ {0} {(ordsucc m) '|mn} 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:
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:
Axiom. (SNoLev_eps_) We take the following as an axiom:
Axiom. (SNo_eps_SNoS_omega) We take the following as an axiom:
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∃mn, x = eps_ m
Axiom. (eps_SNoCutP) We take the following as an axiom:
Axiom. (eps_SNoCut) We take the following as an axiom:
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 (x SNoElts_ alpha)
Axiom. (restr_SNo) We take the following as an axiom:
∀x, SNo x∀alphaSNoLev x, SNo (x SNoElts_ alpha)
Axiom. (restr_SNoLev) We take the following as an axiom:
∀x, SNo x∀alphaSNoLev x, SNoLev (x SNoElts_ alpha) = alpha
Axiom. (restr_SNoEq) We take the following as an axiom:
∀x, SNo x∀alphaSNoLev x, SNoEq_ alpha (x SNoElts_ alpha) x
Axiom. (SNo_extend0_restr_eq) We take the following as an axiom:
∀x, SNo xx = SNo_extend0 x SNoElts_ (SNoLev x)
Axiom. (SNo_extend1_restr_eq) We take the following as an axiom:
∀x, SNo xx = SNo_extend1 x SNoElts_ (SNoLev x)
Beginning of Section SurrealMinus
Primitive. The name minus_SNo is a term of type setset.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Axiom. (minus_SNo_eq) We take the following as an axiom:
∀x, SNo x- x = SNoCut {- z|zSNoR x} {- w|wSNoL x}
Axiom. (minus_SNo_prop1) We take the following as an axiom:
∀x, SNo xSNo (- x) (∀uSNoL x, - x < - u) (∀uSNoR x, - u < - x) SNoCutP {- z|zSNoR x} {- w|wSNoL x}
Axiom. (SNo_minus_SNo) We take the following as an axiom:
∀x, SNo xSNo (- x)
Axiom. (minus_SNo_Lt_contra) We take the following as an axiom:
∀x y, SNo xSNo yx < y- y < - x
Axiom. (minus_SNo_Le_contra) We take the following as an axiom:
∀x y, SNo xSNo yx y- y - x
Axiom. (minus_SNo_SNoCutP) We take the following as an axiom:
∀x, SNo xSNoCutP {- z|zSNoR x} {- w|wSNoL x}
Axiom. (minus_SNo_SNoCutP_gen) We take the following as an axiom:
∀L R, SNoCutP L RSNoCutP {- z|zR} {- w|wL}
Axiom. (minus_SNo_Lev_lem1) We take the following as an axiom:
∀alpha, ordinal alpha∀xSNoS_ alpha, SNoLev (- x) SNoLev x
Axiom. (minus_SNo_Lev_lem2) We take the following as an axiom:
∀x, SNo xSNoLev (- x) SNoLev x
Axiom. (minus_SNo_invol) We take the following as an axiom:
∀x, SNo x- - x = x
Axiom. (minus_SNo_Lev) We take the following as an axiom:
∀x, SNo xSNoLev (- x) = SNoLev x
Axiom. (minus_SNo_SNo_) We take the following as an axiom:
∀alpha, ordinal alpha∀x, SNo_ alpha xSNo_ alpha (- x)
Axiom. (minus_SNo_SNoS_) We take the following as an axiom:
∀alpha, ordinal alpha∀x, x SNoS_ alpha- x SNoS_ alpha
Axiom. (minus_SNoCut_eq_lem) We take the following as an axiom:
∀v, SNo v∀L R, SNoCutP L Rv = SNoCut L R- v = SNoCut {- z|zR} {- w|wL}
Axiom. (minus_SNoCut_eq) We take the following as an axiom:
∀L R, SNoCutP L R- SNoCut L R = SNoCut {- z|zR} {- w|wL}
Axiom. (minus_SNo_Lt_contra1) We take the following as an axiom:
∀x y, SNo xSNo y- x < y- y < x
Axiom. (minus_SNo_Lt_contra2) We take the following as an axiom:
∀x y, SNo xSNo yx < - yy < - x
Axiom. (mordinal_SNoLev_min_2) We take the following as an axiom:
∀alpha, ordinal alpha∀z, SNo zSNoLev z ordsucc alpha- alpha z
Axiom. (minus_SNo_SNoS_omega) We take the following as an axiom:
Axiom. (SNoL_minus_SNoR) We take the following as an axiom:
∀x, SNo xSNoL (- x) = {- w|wSNoR x}
End of Section SurrealMinus
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 setsetset.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Axiom. (add_SNo_eq) We take the following as an axiom:
∀x, SNo x∀y, SNo yx + y = SNoCut ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Axiom. (add_SNo_prop1) We take the following as an axiom:
∀x y, SNo xSNo ySNo (x + y) (∀uSNoL x, u + y < x + y) (∀uSNoR x, x + y < u + y) (∀uSNoL y, x + u < x + y) (∀uSNoR y, x + y < x + u) SNoCutP ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Axiom. (SNo_add_SNo) We take the following as an axiom:
∀x y, SNo xSNo ySNo (x + y)
Axiom. (SNo_add_SNo_3) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zSNo (x + y + z)
Axiom. (SNo_add_SNo_3c) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zSNo (x + y + - z)
Axiom. (SNo_add_SNo_4) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wSNo (x + y + z + w)
Axiom. (add_SNo_Lt1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < zx + y < z + y
Axiom. (add_SNo_Le1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx zx + y z + y
Axiom. (add_SNo_Lt2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zy < zx + y < x + z
Axiom. (add_SNo_Le2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zy zx + y x + z
Axiom. (add_SNo_Lt3a) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx < zy wx + y < z + w
Axiom. (add_SNo_Lt3b) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx zy < wx + y < z + w
Axiom. (add_SNo_Lt3) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx < zy < wx + y < z + w
Axiom. (add_SNo_Le3) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx zy wx + y z + w
Axiom. (add_SNo_SNoCutP) We take the following as an axiom:
∀x y, SNo xSNo ySNoCutP ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Axiom. (add_SNo_com) We take the following as an axiom:
∀x y, SNo xSNo yx + y = y + x
Axiom. (add_SNo_0L) We take the following as an axiom:
∀x, SNo x0 + x = x
Axiom. (add_SNo_0R) We take the following as an axiom:
∀x, SNo xx + 0 = x
Axiom. (add_SNo_minus_SNo_linv) We take the following as an axiom:
∀x, SNo x- x + x = 0
Axiom. (add_SNo_minus_SNo_rinv) We take the following as an axiom:
∀x, SNo xx + - x = 0
Axiom. (add_SNo_ordinal_SNoCutP) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betaSNoCutP ({x + beta|xSNoS_ alpha} {alpha + x|xSNoS_ beta}) Empty
Axiom. (add_SNo_ordinal_eq) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betaalpha + beta = SNoCut ({x + beta|xSNoS_ alpha} {alpha + x|xSNoS_ beta}) Empty
Axiom. (add_SNo_ordinal_ordinal) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betaordinal (alpha + beta)
Axiom. (add_SNo_ordinal_SL) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betaordsucc alpha + beta = ordsucc (alpha + beta)
Axiom. (add_SNo_ordinal_SR) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betaalpha + ordsucc beta = ordsucc (alpha + beta)
Axiom. (add_SNo_ordinal_InL) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal beta∀gammaalpha, gamma + beta alpha + beta
Axiom. (add_SNo_ordinal_InR) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal beta∀gammabeta, alpha + gamma alpha + beta
Axiom. (add_nat_add_SNo) We take the following as an axiom:
∀n mω, add_nat n m = n + m
Axiom. (add_SNo_In_omega) We take the following as an axiom:
∀n mω, n + m ω
Axiom. (add_SNo_1_1_2) We take the following as an axiom:
1 + 1 = 2
Axiom. (add_SNo_SNoL_interpolate) We take the following as an axiom:
∀x y, SNo xSNo y∀uSNoL (x + y), (∃vSNoL x, u v + y) (∃vSNoL y, u x + v)
Axiom. (add_SNo_SNoR_interpolate) We take the following as an axiom:
∀x y, SNo xSNo y∀uSNoR (x + y), (∃vSNoR x, v + y u) (∃vSNoR y, x + v u)
Axiom. (add_SNo_assoc) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + (y + z) = (x + y) + z
Axiom. (add_SNo_cancel_L) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + y = x + zy = z
Axiom. (minus_SNo_0) We take the following as an axiom:
- 0 = 0
Axiom. (minus_add_SNo_distr) We take the following as an axiom:
∀x y, SNo xSNo y- (x + y) = (- x) + (- y)
Axiom. (minus_add_SNo_distr_3) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z- (x + y + z) = - x + - y + - z
Axiom. (add_SNo_Lev_bd) We take the following as an axiom:
∀x y, SNo xSNo ySNoLev (x + y) SNoLev x + SNoLev y
Axiom. (add_SNo_SNoS_omega) We take the following as an axiom:
∀x ySNoS_ ω, x + y SNoS_ ω
Axiom. (add_SNo_minus_R2) We take the following as an axiom:
∀x y, SNo xSNo y(x + y) + - y = x
Axiom. (add_SNo_minus_R2') We take the following as an axiom:
∀x y, SNo xSNo y(x + - y) + y = x
Axiom. (add_SNo_minus_L2) We take the following as an axiom:
∀x y, SNo xSNo y- x + (x + y) = y
Axiom. (add_SNo_minus_L2') We take the following as an axiom:
∀x y, SNo xSNo yx + (- x + y) = y
Axiom. (add_SNo_Lt1_cancel) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + y < z + yx < z
Axiom. (add_SNo_Lt2_cancel) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + y < x + zy < z
Axiom. (add_SNo_assoc_4) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx + y + z + w = (x + y + z) + w
Axiom. (add_SNo_com_3_0_1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + y + z = y + x + z
Axiom. (add_SNo_com_3b_1_2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(x + y) + z = (x + z) + y
Axiom. (add_SNo_com_4_inner_mid) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y) + (z + w) = (x + z) + (y + w)
Axiom. (add_SNo_rotate_3_1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + y + z = z + x + y
Axiom. (add_SNo_rotate_4_1) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx + y + z + w = w + x + y + z
Axiom. (add_SNo_rotate_5_1) We take the following as an axiom:
∀x y z w v, SNo xSNo ySNo zSNo wSNo vx + y + z + w + v = v + x + y + z + w
Axiom. (add_SNo_rotate_5_2) We take the following as an axiom:
∀x y z w v, SNo xSNo ySNo zSNo wSNo vx + y + z + w + v = w + v + x + y + z
Axiom. (add_SNo_minus_SNo_prop1) We take the following as an axiom:
∀x y, SNo xSNo y- x + x + y = y
Axiom. (add_SNo_minus_SNo_prop2) We take the following as an axiom:
∀x y, SNo xSNo yx + - x + y = y
Axiom. (add_SNo_minus_SNo_prop3) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y + z) + (- z + w) = x + y + w
Axiom. (add_SNo_minus_SNo_prop4) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y + z) + (w + - z) = x + y + w
Axiom. (add_SNo_minus_SNo_prop5) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y + - z) + (z + w) = x + y + w
Axiom. (add_SNo_minus_Lt1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + - y < zx < z + y
Axiom. (add_SNo_minus_Lt2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zz < x + - yz + y < x
Axiom. (add_SNo_minus_Lt1b) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < z + yx + - y < z
Axiom. (add_SNo_minus_Lt2b) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zz + y < xz < x + - y
Axiom. (add_SNo_minus_Lt1b3) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx + y < w + zx + y + - z < w
Axiom. (add_SNo_minus_Lt2b3) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo ww + z < x + yw < x + y + - z
Axiom. (add_SNo_minus_Lt_lem) We take the following as an axiom:
∀x y z u v w, SNo xSNo ySNo zSNo uSNo vSNo wx + y + w < u + v + zx + y + - z < u + v + - w
Axiom. (add_SNo_minus_Le2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zz x + - yz + y x
Axiom. (add_SNo_minus_Le2b) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zz + y xz x + - y
Axiom. (add_SNo_Lt_subprop2) We take the following as an axiom:
∀x y z w u v, SNo xSNo ySNo zSNo wSNo uSNo vx + u < z + vy + v < w + ux + y < z + w
Axiom. (add_SNo_Lt_subprop3a) We take the following as an axiom:
∀x y z w u a, SNo xSNo ySNo zSNo wSNo uSNo ax + z < w + ay + a < ux + y + z < w + u
Axiom. (add_SNo_Lt_subprop3b) We take the following as an axiom:
∀x y w u v a, SNo xSNo ySNo wSNo uSNo vSNo ax + a < w + vy < a + ux + y < w + u + v
Axiom. (add_SNo_Lt_subprop3c) We take the following as an axiom:
∀x y z w u a b c, SNo xSNo ySNo zSNo wSNo uSNo aSNo bSNo cx + a < b + cy + c < ub + z < w + ax + y + z < w + u
Axiom. (add_SNo_Lt_subprop3d) We take the following as an axiom:
∀x y w u v a b c, SNo xSNo ySNo wSNo uSNo vSNo aSNo bSNo cx + a < b + vy < c + ub + c < w + ax + y < w + u + v
Axiom. (ordinal_ordsucc_SNo_eq) We take the following as an axiom:
∀alpha, ordinal alphaordsucc alpha = 1 + alpha
Axiom. (add_SNo_3a_2b) We take the following as an axiom:
∀x y z w u, SNo xSNo ySNo zSNo wSNo u(x + y + z) + (w + u) = (u + y + z) + (w + x)
Axiom. (add_SNo_1_ordsucc) We take the following as an axiom:
∀nω, n + 1 = ordsucc n
Axiom. (add_SNo_eps_Lt) We take the following as an axiom:
∀x, SNo x∀nω, x < x + eps_ n
Axiom. (add_SNo_eps_Lt') We take the following as an axiom:
∀x y, SNo xSNo y∀nω, x < yx < y + eps_ n
Axiom. (SNoLt_minus_pos) We take the following as an axiom:
∀x y, SNo xSNo yx < y0 < y + - x
Axiom. (add_SNo_omega_In_cases) We take the following as an axiom:
∀m, ∀nω, ∀k, nat_p km n + km n m + - n k
Axiom. (add_SNo_Lt4) We take the following as an axiom:
∀x y z w u v, SNo xSNo ySNo zSNo wSNo uSNo vx < wy < uz < vx + y + z < w + u + v
Axiom. (add_SNo_3_3_3_Lt1) We take the following as an axiom:
∀x y z w u, SNo xSNo ySNo zSNo wSNo ux + y < z + wx + y + u < z + w + u
Axiom. (add_SNo_3_2_3_Lt1) We take the following as an axiom:
∀x y z w u, SNo xSNo ySNo zSNo wSNo uy + x < z + wx + u + y < z + w + u
End of Section SurrealAdd
Beginning of Section SurrealMul
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Definition. We define mul_SNo to be SNo_rec2 (λx y m ⇒ SNoCut ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|wSNoL x SNoL y} {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|zSNoR x SNoR y}) ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|wSNoL x SNoR y} {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|zSNoR x SNoL y})) of type setsetset.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Axiom. (mul_SNo_eq) We take the following as an axiom:
∀x, SNo x∀y, SNo yx * y = SNoCut ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|wSNoL x SNoL y} {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|zSNoR x SNoR y}) ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|wSNoL x SNoR y} {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|zSNoR x SNoL y})
Axiom. (mul_SNo_eq_2) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (∀L R, (∀u, u L(∀q : prop, (∀w0SNoL x, ∀w1SNoL y, u = w0 * y + x * w1 + - w0 * w1q)(∀z0SNoR x, ∀z1SNoR y, u = z0 * y + x * z1 + - z0 * z1q)q))(∀w0SNoL x, ∀w1SNoL y, w0 * y + x * w1 + - w0 * w1 L)(∀z0SNoR x, ∀z1SNoR y, z0 * y + x * z1 + - z0 * z1 L)(∀u, u R(∀q : prop, (∀w0SNoL x, ∀z1SNoR y, u = w0 * y + x * z1 + - w0 * z1q)(∀z0SNoR x, ∀w1SNoL y, u = z0 * y + x * w1 + - z0 * w1q)q))(∀w0SNoL x, ∀z1SNoR y, w0 * y + x * z1 + - w0 * z1 R)(∀z0SNoR x, ∀w1SNoL y, z0 * y + x * w1 + - z0 * w1 R)x * y = SNoCut L Rp)p
Axiom. (mul_SNo_prop_1) We take the following as an axiom:
∀x, SNo x∀y, SNo y∀p : prop, (SNo (x * y)(∀uSNoL x, ∀vSNoL y, u * y + x * v < x * y + u * v)(∀uSNoR x, ∀vSNoR y, u * y + x * v < x * y + u * v)(∀uSNoL x, ∀vSNoR y, x * y + u * v < u * y + x * v)(∀uSNoR x, ∀vSNoL y, x * y + u * v < u * y + x * v)p)p
Axiom. (SNo_mul_SNo) We take the following as an axiom:
∀x y, SNo xSNo ySNo (x * y)
Axiom. (SNo_mul_SNo_lem) We take the following as an axiom:
∀x y u v, SNo xSNo ySNo uSNo vSNo (u * y + x * v + - (u * v))
Axiom. (SNo_mul_SNo_3) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zSNo (x * y * z)
Axiom. (mul_SNo_eq_3) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (∀L R, SNoCutP L R(∀u, u L(∀q : prop, (∀w0SNoL x, ∀w1SNoL y, u = w0 * y + x * w1 + - w0 * w1q)(∀z0SNoR x, ∀z1SNoR y, u = z0 * y + x * z1 + - z0 * z1q)q))(∀w0SNoL x, ∀w1SNoL y, w0 * y + x * w1 + - w0 * w1 L)(∀z0SNoR x, ∀z1SNoR y, z0 * y + x * z1 + - z0 * z1 L)(∀u, u R(∀q : prop, (∀w0SNoL x, ∀z1SNoR y, u = w0 * y + x * z1 + - w0 * z1q)(∀z0SNoR x, ∀w1SNoL y, u = z0 * y + x * w1 + - z0 * w1q)q))(∀w0SNoL x, ∀z1SNoR y, w0 * y + x * z1 + - w0 * z1 R)(∀z0SNoR x, ∀w1SNoL y, z0 * y + x * w1 + - z0 * w1 R)x * y = SNoCut L Rp)p
Axiom. (mul_SNo_Lt) We take the following as an axiom:
∀x y u v, SNo xSNo ySNo uSNo vu < xv < yu * y + x * v < x * y + u * v
Axiom. (mul_SNo_Le) We take the following as an axiom:
∀x y u v, SNo xSNo ySNo uSNo vu xv yu * y + x * v x * y + u * v
Axiom. (mul_SNo_SNoL_interpolate) We take the following as an axiom:
∀x y, SNo xSNo y∀uSNoL (x * y), (∃vSNoL x, ∃wSNoL y, u + v * w v * y + x * w) (∃vSNoR x, ∃wSNoR y, u + v * w v * y + x * w)
Axiom. (mul_SNo_SNoL_interpolate_impred) We take the following as an axiom:
∀x y, SNo xSNo y∀uSNoL (x * y), ∀p : prop, (∀vSNoL x, ∀wSNoL y, u + v * w v * y + x * wp)(∀vSNoR x, ∀wSNoR y, u + v * w v * y + x * wp)p
Axiom. (mul_SNo_SNoR_interpolate) We take the following as an axiom:
∀x y, SNo xSNo y∀uSNoR (x * y), (∃vSNoL x, ∃wSNoR y, v * y + x * w u + v * w) (∃vSNoR x, ∃wSNoL y, v * y + x * w u + v * w)
Axiom. (mul_SNo_SNoR_interpolate_impred) We take the following as an axiom:
∀x y, SNo xSNo y∀uSNoR (x * y), ∀p : prop, (∀vSNoL x, ∀wSNoR y, v * y + x * w u + v * wp)(∀vSNoR x, ∀wSNoL y, v * y + x * w u + v * wp)p
Axiom. (mul_SNo_Subq_lem) We take the following as an axiom:
∀x y X Y Z W, ∀U U', (∀u, u U(∀q : prop, (∀w0X, ∀w1Y, u = w0 * y + x * w1 + - w0 * w1q)(∀z0Z, ∀z1W, u = z0 * y + x * z1 + - z0 * z1q)q))(∀w0X, ∀w1Y, w0 * y + x * w1 + - w0 * w1 U')(∀w0Z, ∀w1W, w0 * y + x * w1 + - w0 * w1 U')U U'
Axiom. (mul_SNo_zeroR) We take the following as an axiom:
∀x, SNo xx * 0 = 0
Axiom. (mul_SNo_oneR) We take the following as an axiom:
∀x, SNo xx * 1 = x
Axiom. (mul_SNo_com) We take the following as an axiom:
∀x y, SNo xSNo yx * y = y * x
Axiom. (mul_SNo_minus_distrL) We take the following as an axiom:
∀x y, SNo xSNo y(- x) * y = - x * y
Axiom. (mul_SNo_minus_distrR) We take the following as an axiom:
∀x y, SNo xSNo yx * (- y) = - (x * y)
Axiom. (mul_SNo_distrR) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(x + y) * z = x * z + y * z
Axiom. (mul_SNo_distrL) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx * (y + z) = x * y + x * z
Beginning of Section mul_SNo_assoc_lems
Variable M : setsetset
Hypothesis DL : ∀x y z, SNo xSNo ySNo zx * (y + z) = x * y + x * z
Hypothesis DR : ∀x y z, SNo xSNo ySNo z(x + y) * z = x * z + y * z
Hypothesis IL : ∀x y, SNo xSNo y∀uSNoL (x * y), ∀p : prop, (∀vSNoL x, ∀wSNoL y, u + v * w v * y + x * wp)(∀vSNoR x, ∀wSNoR y, u + v * w v * y + x * wp)p
Hypothesis IR : ∀x y, SNo xSNo y∀uSNoR (x * y), ∀p : prop, (∀vSNoL x, ∀wSNoR y, v * y + x * w u + v * wp)(∀vSNoR x, ∀wSNoL y, v * y + x * w u + v * wp)p
Hypothesis M_Lt : ∀x y u v, SNo xSNo ySNo uSNo vu < xv < yu * y + x * v < x * y + u * v
Hypothesis M_Le : ∀x y u v, SNo xSNo ySNo uSNo vu xv yu * y + x * v x * y + u * v
Axiom. (mul_SNo_assoc_lem1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(∀uSNoS_ (SNoLev x), u * (y * z) = (u * y) * z)(∀vSNoS_ (SNoLev y), x * (v * z) = (x * v) * z)(∀wSNoS_ (SNoLev z), x * (y * w) = (x * y) * w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), u * (v * z) = (u * v) * z)(∀uSNoS_ (SNoLev x), ∀wSNoS_ (SNoLev z), u * (y * w) = (u * y) * w)(∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), x * (v * w) = (x * v) * w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), u * (v * w) = (u * v) * w)∀L, (∀uL, ∀q : prop, (∀vSNoL x, ∀wSNoL (y * z), u = v * (y * z) + x * w + - v * wq)(∀vSNoR x, ∀wSNoR (y * z), u = v * (y * z) + x * w + - v * wq)q)∀uL, u < (x * y) * z
Axiom. (mul_SNo_assoc_lem2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(∀uSNoS_ (SNoLev x), u * (y * z) = (u * y) * z)(∀vSNoS_ (SNoLev y), x * (v * z) = (x * v) * z)(∀wSNoS_ (SNoLev z), x * (y * w) = (x * y) * w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), u * (v * z) = (u * v) * z)(∀uSNoS_ (SNoLev x), ∀wSNoS_ (SNoLev z), u * (y * w) = (u * y) * w)(∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), x * (v * w) = (x * v) * w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), u * (v * w) = (u * v) * w)∀R, (∀uR, ∀q : prop, (∀vSNoL x, ∀wSNoR (y * z), u = v * (y * z) + x * w + - v * wq)(∀vSNoR x, ∀wSNoL (y * z), u = v * (y * z) + x * w + - v * wq)q)∀uR, (x * y) * z < u
End of Section mul_SNo_assoc_lems
Axiom. (mul_SNo_assoc) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx * (y * z) = (x * y) * z
Axiom. (mul_nat_mul_SNo) We take the following as an axiom:
∀n mω, mul_nat n m = n * m
Axiom. (mul_SNo_In_omega) We take the following as an axiom:
∀n mω, n * m ω
Axiom. (mul_SNo_zeroL) We take the following as an axiom:
∀x, SNo x0 * x = 0
Axiom. (mul_SNo_oneL) We take the following as an axiom:
∀x, SNo x1 * x = x
Axiom. (pos_mul_SNo_Lt) We take the following as an axiom:
∀x y z, SNo x0 < xSNo ySNo zy < zx * y < x * z
Axiom. (nonneg_mul_SNo_Le) We take the following as an axiom:
∀x y z, SNo x0 xSNo ySNo zy zx * y x * z
Axiom. (neg_mul_SNo_Lt) We take the following as an axiom:
∀x y z, SNo xx < 0SNo ySNo zz < yx * y < x * z
Axiom. (pos_mul_SNo_Lt') We take the following as an axiom:
∀x y z, SNo xSNo ySNo z0 < zx < yx * z < y * z
Axiom. (mul_SNo_Lt1_pos_Lt) We take the following as an axiom:
∀x y, SNo xSNo yx < 10 < yx * y < y
Axiom. (nonneg_mul_SNo_Le') We take the following as an axiom:
∀x y z, SNo xSNo ySNo z0 zx yx * z y * z
Axiom. (mul_SNo_Le1_nonneg_Le) We take the following as an axiom:
∀x y, SNo xSNo yx 10 yx * y y
Axiom. (pos_mul_SNo_Lt2) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w0 < x0 < yx < zy < wx * y < z * w
Axiom. (nonneg_mul_SNo_Le2) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w0 x0 yx zy wx * y z * w
Axiom. (mul_SNo_pos_pos) We take the following as an axiom:
∀x y, SNo xSNo y0 < x0 < y0 < x * y
Axiom. (mul_SNo_pos_neg) We take the following as an axiom:
∀x y, SNo xSNo y0 < xy < 0x * y < 0
Axiom. (mul_SNo_neg_pos) We take the following as an axiom:
∀x y, SNo xSNo yx < 00 < yx * y < 0
Axiom. (mul_SNo_neg_neg) We take the following as an axiom:
∀x y, SNo xSNo yx < 0y < 00 < x * y
Axiom. (SNo_sqr_nonneg) We take the following as an axiom:
∀x, SNo x0 x * x
Axiom. (SNo_zero_or_sqr_pos) We take the following as an axiom:
∀x, SNo xx = 0 0 < x * x
Axiom. (SNo_foil) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y) * (z + w) = x * z + x * w + y * z + y * w
Axiom. (mul_SNo_minus_minus) We take the following as an axiom:
∀x y, SNo xSNo y(- x) * (- y) = x * y
Axiom. (mul_SNo_com_3_0_1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx * y * z = y * x * z
Axiom. (mul_SNo_com_3b_1_2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(x * y) * z = (x * z) * y
Axiom. (mul_SNo_com_4_inner_mid) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x * y) * (z * w) = (x * z) * (y * w)
Axiom. (mul_SNo_rotate_3_1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx * y * z = z * x * y
Axiom. (mul_SNo_rotate_4_1) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx * y * z * w = w * x * y * z
Axiom. (SNo_foil_mm) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + - y) * (z + - w) = x * z + - x * w + - y * z + y * w
Axiom. (mul_SNo_nonzero_cancel) We take the following as an axiom:
∀x y z, SNo xx 0SNo ySNo zx * y = x * zy = z
End of Section SurrealMul
Beginning of Section SurrealExp
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Definition. We define exp_SNo_nat to be λn m : setnat_primrec 1 (λ_ r ⇒ n * r) m of type setsetset.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Axiom. (exp_SNo_nat_0) We take the following as an axiom:
∀x, SNo xx ^ 0 = 1
Axiom. (exp_SNo_nat_S) We take the following as an axiom:
∀x, SNo x∀n, nat_p nx ^ (ordsucc n) = x * x ^ n
Axiom. (SNo_exp_SNo_nat) We take the following as an axiom:
∀x, SNo x∀n, nat_p nSNo (x ^ n)
Axiom. (nat_exp_SNo_nat) We take the following as an axiom:
∀x, nat_p x∀n, nat_p nnat_p (x ^ n)
Axiom. (eps_ordsucc_half_add) We take the following as an axiom:
∀n, nat_p neps_ (ordsucc n) + eps_ (ordsucc n) = eps_ n
Axiom. (eps_1_half_eq1) We take the following as an axiom:
Axiom. (eps_1_half_eq2) We take the following as an axiom:
Axiom. (double_eps_1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + x = y + zx = eps_ 1 * (y + z)
Axiom. (exp_SNo_1_bd) We take the following as an axiom:
∀x, SNo x1 x∀n, nat_p n1 x ^ n
Axiom. (exp_SNo_2_bd) We take the following as an axiom:
∀n, nat_p nn < 2 ^ n
Axiom. (mul_SNo_eps_power_2) We take the following as an axiom:
∀n, nat_p neps_ n * 2 ^ n = 1
Axiom. (eps_bd_1) We take the following as an axiom:
∀nω, eps_ n 1
Axiom. (mul_SNo_eps_power_2') We take the following as an axiom:
∀n, nat_p n2 ^ n * eps_ n = 1
Axiom. (exp_SNo_nat_mul_add) We take the following as an axiom:
∀x, SNo x∀m, nat_p m∀n, nat_p nx ^ m * x ^ n = x ^ (m + n)
Axiom. (exp_SNo_nat_mul_add') We take the following as an axiom:
∀x, SNo x∀m nω, x ^ m * x ^ n = x ^ (m + n)
Axiom. (exp_SNo_nat_pos) We take the following as an axiom:
∀x, SNo x0 < x∀n, nat_p n0 < x ^ n
Axiom. (mul_SNo_eps_eps_add_SNo) We take the following as an axiom:
∀m nω, eps_ m * eps_ n = eps_ (m + n)
Axiom. (SNoS_omega_Lev_equip) We take the following as an axiom:
∀n, nat_p nequip {xSNoS_ ω|SNoLev x = n} (2 ^ n)
Axiom. (SNoS_finite) We take the following as an axiom:
Axiom. (SNoS_omega_SNoL_finite) We take the following as an axiom:
Axiom. (SNoS_omega_SNoR_finite) We take the following as an axiom:
End of Section SurrealExp
Beginning of Section Int
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Primitive. The name int is a term of type set.
Axiom. (int_SNo_cases) We take the following as an axiom:
∀p : setprop, (∀nω, p n)(∀nω, p (- n))∀xint, p x
Axiom. (int_SNo) We take the following as an axiom:
∀xint, SNo x
Axiom. (Subq_omega_int) We take the following as an axiom:
Axiom. (int_minus_SNo_omega) We take the following as an axiom:
∀nω, - n int
Axiom. (int_add_SNo_lem) We take the following as an axiom:
∀nω, ∀m, nat_p m- n + m int
Axiom. (int_add_SNo) We take the following as an axiom:
∀x yint, x + y int
Axiom. (int_minus_SNo) We take the following as an axiom:
∀xint, - x int
Axiom. (int_mul_SNo) We take the following as an axiom:
∀x yint, x * y int
End of Section Int
Beginning of Section SurrealAbs
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Definition. We define abs_SNo to be λx ⇒ if 0 x then x else - x of type setset.
Axiom. (nonneg_abs_SNo) We take the following as an axiom:
∀x, 0 xabs_SNo x = x
Axiom. (not_nonneg_abs_SNo) We take the following as an axiom:
∀x, ¬ (0 x)abs_SNo x = - x
Axiom. (abs_SNo_0) We take the following as an axiom:
Axiom. (pos_abs_SNo) We take the following as an axiom:
∀x, 0 < xabs_SNo x = x
Axiom. (neg_abs_SNo) We take the following as an axiom:
∀x, SNo xx < 0abs_SNo x = - x
Axiom. (SNo_abs_SNo) We take the following as an axiom:
∀x, SNo xSNo (abs_SNo x)
Axiom. (abs_SNo_Lev) We take the following as an axiom:
∀x, SNo xSNoLev (abs_SNo x) = SNoLev x
Axiom. (abs_SNo_minus) We take the following as an axiom:
∀x, SNo xabs_SNo (- x) = abs_SNo x
Axiom. (abs_SNo_dist_swap) We take the following as an axiom:
∀x y, SNo xSNo yabs_SNo (x + - y) = abs_SNo (y + - x)
Axiom. (SNo_triangle) We take the following as an axiom:
∀x y, SNo xSNo yabs_SNo (x + y) abs_SNo x + abs_SNo y
Axiom. (SNo_triangle2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zabs_SNo (x + - z) abs_SNo (x + - y) + abs_SNo (y + - z)
End of Section SurrealAbs
Beginning of Section SNoMaxMin
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Definition. We define SNo_max_of to be λX x ⇒ x X SNo x ∀yX, SNo yy x of type setsetprop.
Definition. We define SNo_min_of to be λX x ⇒ x X SNo x ∀yX, SNo yx y of type setsetprop.
Axiom. (minus_SNo_max_min) We take the following as an axiom:
∀X y, (∀xX, SNo x)SNo_max_of X ySNo_min_of {- x|xX} (- y)
Axiom. (minus_SNo_max_min') We take the following as an axiom:
∀X y, (∀xX, SNo x)SNo_max_of {- x|xX} ySNo_min_of X (- y)
Axiom. (minus_SNo_min_max) We take the following as an axiom:
∀X y, (∀xX, SNo x)SNo_min_of X ySNo_max_of {- x|xX} (- y)
Axiom. (double_SNo_max_1) We take the following as an axiom:
∀x y, SNo xSNo_max_of (SNoL x) y∀z, SNo zx < zy + z < x + x∃wSNoR z, y + w = x + x
Axiom. (double_SNo_min_1) We take the following as an axiom:
∀x y, SNo xSNo_min_of (SNoR x) y∀z, SNo zz < xx + x < y + z∃wSNoL z, y + w = x + x
Axiom. (finite_max_exists) We take the following as an axiom:
∀X, (∀xX, SNo x)finite XX 0∃x, SNo_max_of X x
Axiom. (finite_min_exists) We take the following as an axiom:
∀X, (∀xX, SNo x)finite XX 0∃x, SNo_min_of X x
Axiom. (SNoS_omega_SNoL_max_exists) We take the following as an axiom:
∀xSNoS_ ω, SNoL x = 0 ∃y, SNo_max_of (SNoL x) y
Axiom. (SNoS_omega_SNoR_min_exists) We take the following as an axiom:
∀xSNoS_ ω, SNoR x = 0 ∃y, SNo_min_of (SNoR x) y
End of Section SNoMaxMin
Beginning of Section DiadicRationals
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Axiom. (nonneg_diadic_rational_p_SNoS_omega) We take the following as an axiom:
∀kω, ∀n, nat_p neps_ k * n SNoS_ ω
Definition. We define diadic_rational_p to be λx ⇒ ∃kω, ∃mint, x = eps_ k * m of type setprop.
Axiom. (diadic_rational_p_SNoS_omega) We take the following as an axiom:
Axiom. (int_diadic_rational_p) We take the following as an axiom:
Axiom. (omega_diadic_rational_p) We take the following as an axiom:
Axiom. (eps_diadic_rational_p) We take the following as an axiom:
Axiom. (minus_SNo_diadic_rational_p) We take the following as an axiom:
Axiom. (mul_SNo_diadic_rational_p) We take the following as an axiom:
Axiom. (add_SNo_diadic_rational_p) We take the following as an axiom:
Axiom. (SNoS_omega_diadic_rational_p_lem) We take the following as an axiom:
∀n, nat_p n∀x, SNo xSNoLev x = ndiadic_rational_p x
Axiom. (SNoS_omega_diadic_rational_p) We take the following as an axiom:
Axiom. (mul_SNo_SNoS_omega) We take the following as an axiom:
∀x ySNoS_ ω, x * y SNoS_ ω
End of Section DiadicRationals
Beginning of Section Reals
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Axiom. (SNoS_omega_drat_intvl) We take the following as an axiom:
∀xSNoS_ ω, ∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k
Axiom. (SNoS_ordsucc_omega_bdd_above) We take the following as an axiom:
∀xSNoS_ (ordsucc ω), x < ω∃Nω, x < N
Axiom. (SNoS_ordsucc_omega_bdd_below) We take the following as an axiom:
∀xSNoS_ (ordsucc ω), - ω < x∃Nω, - N < x
Axiom. (SNoS_ordsucc_omega_bdd_drat_intvl) We take the following as an axiom:
∀xSNoS_ (ordsucc ω), - ω < xx < ω∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k
Primitive. The name real is a term of type set.
Axiom. (real_I) We take the following as an axiom:
∀xSNoS_ (ordsucc ω), x ωx - ω(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)x real
Axiom. (real_E) We take the following as an axiom:
∀xreal, ∀p : prop, (SNo xSNoLev x ordsucc ωx SNoS_ (ordsucc ω)- ω < xx < ω(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)(∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k)p)p
Axiom. (real_SNo) We take the following as an axiom:
∀xreal, SNo x
Axiom. (real_SNoS_omega_prop) We take the following as an axiom:
∀xreal, ∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x
Axiom. (SNoS_omega_real) We take the following as an axiom:
Axiom. (real_0) We take the following as an axiom:
Axiom. (real_1) We take the following as an axiom:
Axiom. (SNoLev_In_real_SNoS_omega) We take the following as an axiom:
∀xreal, ∀w, SNo wSNoLev w SNoLev xw SNoS_ ω
Axiom. (minus_SNo_prereal_1) We take the following as an axiom:
∀x, SNo x(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)(∀qSNoS_ ω, (∀kω, abs_SNo (q + - - x) < eps_ k)q = - x)
Axiom. (minus_SNo_prereal_2) We take the following as an axiom:
∀x, SNo x(∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k)(∀kω, ∃qSNoS_ ω, q < - x - x < q + eps_ k)
Axiom. (SNo_prereal_incr_lower_pos) We take the following as an axiom:
∀x, SNo x0 < x(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)(∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k)∀kω, ∀p : prop, (∀qSNoS_ ω, 0 < qq < xx < q + eps_ kp)p
Axiom. (real_minus_SNo) We take the following as an axiom:
Axiom. (SNo_prereal_incr_lower_approx) We take the following as an axiom:
∀x, SNo x(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)(∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k)∃fSNoS_ ωω, ∀nω, f n < x x < f n + eps_ n ∀in, f i < f n
Axiom. (SNo_prereal_decr_upper_approx) We take the following as an axiom:
∀x, SNo x(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)(∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k)∃gSNoS_ ωω, ∀nω, g n + - eps_ n < x x < g n ∀in, g n < g i
Axiom. (SNoCutP_SNoCut_lim) We take the following as an axiom:
∀lambda, ordinal lambda(∀alphalambda, ordsucc alpha lambda)∀L RSNoS_ lambda, SNoCutP L RSNoLev (SNoCut L R) ordsucc lambda
Axiom. (SNoCutP_SNoCut_omega) We take the following as an axiom:
Axiom. (SNo_approx_real_lem) We take the following as an axiom:
∀f gSNoS_ ωω, (∀n mω, f n < g m)∀p : prop, (SNoCutP {f n|nω} {g n|nω}SNo (SNoCut {f n|nω} {g n|nω})SNoLev (SNoCut {f n|nω} {g n|nω}) ordsucc ωSNoCut {f n|nω} {g n|nω} SNoS_ (ordsucc ω)(∀nω, f n < SNoCut {f n|nω} {g n|nω})(∀nω, SNoCut {f n|nω} {g n|nω} < g n)p)p
Axiom. (SNo_approx_real) We take the following as an axiom:
∀x, SNo x∀f gSNoS_ ωω, (∀nω, f n < x)(∀nω, x < f n + eps_ n)(∀nω, ∀in, f i < f n)(∀nω, x < g n)(∀nω, ∀in, g n < g i)x = SNoCut {f n|nω} {g n|nω}x real
Axiom. (SNo_approx_real_rep) We take the following as an axiom:
∀xreal, ∀p : prop, (∀f gSNoS_ ωω, (∀nω, f n < x)(∀nω, x < f n + eps_ n)(∀nω, ∀in, f i < f n)(∀nω, g n + - eps_ n < x)(∀nω, x < g n)(∀nω, ∀in, g n < g i)SNoCutP {f n|nω} {g n|nω}x = SNoCut {f n|nω} {g n|nω}p)p
Axiom. (real_add_SNo) We take the following as an axiom:
∀x yreal, x + y real
Axiom. (SNoS_ordsucc_omega_bdd_eps_pos) We take the following as an axiom:
∀xSNoS_ (ordsucc ω), 0 < xx < ω∃Nω, eps_ N * x < 1
Axiom. (real_mul_SNo_pos) We take the following as an axiom:
∀x yreal, 0 < x0 < yx * y real
Axiom. (real_mul_SNo) We take the following as an axiom:
∀x yreal, x * y real
Axiom. (abs_SNo_intvl_bd) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx yy < x + zabs_SNo (y + - x) < z
Axiom. (pos_small_real_recip_ex) We take the following as an axiom:
∀xreal, 0 < xx < 1∃yreal, x * y = 1
Axiom. (pos_real_recip_ex) We take the following as an axiom:
∀xreal, 0 < x∃yreal, x * y = 1
Axiom. (nonzero_real_recip_ex) We take the following as an axiom:
∀xreal, x 0∃yreal, x * y = 1
Axiom. (real_Archimedean) We take the following as an axiom:
∀x yreal, 0 < x0 y∃nω, y n * x
Axiom. (real_complete1) We take the following as an axiom:
∀a brealω, (∀nω, a n b n a n a (ordsucc n) b (ordsucc n) b n)∃xreal, ∀nω, a n x x b n
Axiom. (real_complete2) We take the following as an axiom:
∀a brealω, (∀nω, a n b n a n a (n + 1) b (n + 1) b n)∃xreal, ∀nω, a n x x b n
End of Section Reals
Beginning of Section ComplexSNo
Beginning of Section CTaggedSets
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Axiom. (not_TransSet_Sing2) We take the following as an axiom:
Axiom. (not_ordinal_Sing2) We take the following as an axiom:
Axiom. (ctagged_not_ordinal) We take the following as an axiom:
∀y, ¬ ordinal (y '')
Axiom. (ctagged_notin_ordinal) We take the following as an axiom:
∀alpha y, ordinal alpha(y '') alpha
Axiom. (Sing2_notin_SingSing1) We take the following as an axiom:
Axiom. (ctagged_notin_SNo) We take the following as an axiom:
∀x y, SNo x(y '') x
Axiom. (ctagged_eqE_Subq) We take the following as an axiom:
∀x y, SNo xSNo y∀ux, ∀vy, u '' = v ''u v
Axiom. (ctagged_eqE_eq) We take the following as an axiom:
∀x y, SNo xSNo y∀ux, ∀vy, u '' = v ''u = v
Definition. We define SNo_pair to be λx y ⇒ x {u ''|uy} of type setsetset.
Axiom. (SNo_pair_prop_1_Subq) We take the following as an axiom:
∀x1 y1 x2 y2, SNo x1SNo_pair x1 y1 = SNo_pair x2 y2x1 x2
Axiom. (SNo_pair_prop_1) We take the following as an axiom:
∀x1 y1 x2 y2, SNo x1SNo x2SNo_pair x1 y1 = SNo_pair x2 y2x1 = x2
Axiom. (SNo_pair_prop_2_Subq) We take the following as an axiom:
∀x1 y1 x2 y2, SNo y1SNo x2SNo y2SNo_pair x1 y1 = SNo_pair x2 y2y1 y2
Axiom. (SNo_pair_prop_2) We take the following as an axiom:
∀x1 y1 x2 y2, SNo x1SNo y1SNo x2SNo y2SNo_pair x1 y1 = SNo_pair x2 y2y1 = y2
Axiom. (SNo_pair_0) We take the following as an axiom:
∀x, SNo_pair x 0 = x
End of Section CTaggedSets
Primitive. The name CSNo is a term of type setprop.
Axiom. (CSNo_I) We take the following as an axiom:
∀x y, SNo xSNo yCSNo (SNo_pair x y)
Axiom. (CSNo_E) We take the following as an axiom:
∀z, CSNo z∀p : setprop, (∀x y, SNo xSNo yz = SNo_pair x yp (SNo_pair x y))p z
Axiom. (SNo_CSNo) We take the following as an axiom:
∀x, SNo xCSNo x
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Primitive. The name Complex_i is a term of type set.
Primitive. The name CSNo_Re is a term of type setset.
Primitive. The name CSNo_Im is a term of type setset.
Let i ≝ Complex_i
Let Re : setsetCSNo_Re
Let Im : setsetCSNo_Im
Let pa : setsetsetSNo_pair
Axiom. (CSNo_Re1) We take the following as an axiom:
∀z, CSNo zSNo (Re z) ∃y, SNo y z = pa (Re z) y
Axiom. (CSNo_Re2) We take the following as an axiom:
∀x y, SNo xSNo yRe (pa x y) = x
Axiom. (CSNo_Im1) We take the following as an axiom:
∀z, CSNo zSNo (Im z) z = pa (Re z) (Im z)
Axiom. (CSNo_Im2) We take the following as an axiom:
∀x y, SNo xSNo yIm (pa x y) = y
Axiom. (CSNo_ReR) We take the following as an axiom:
∀z, CSNo zSNo (Re z)
Axiom. (CSNo_ImR) We take the following as an axiom:
∀z, CSNo zSNo (Im z)
Axiom. (CSNo_ReIm) We take the following as an axiom:
∀z, CSNo zz = pa (Re z) (Im z)
Axiom. (CSNo_ReIm_split) We take the following as an axiom:
∀z w, CSNo zCSNo wRe z = Re wIm z = Im wz = w
Primitive. The name minus_CSNo is a term of type setset.
Primitive. The name add_CSNo is a term of type setsetset.
Primitive. The name mul_CSNo is a term of type setsetset.
Let plus' ≝ add_CSNo
Let mult' ≝ mul_CSNo
Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term minus_CSNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_CSNo.
Notation. We use as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_CSNo.
Axiom. (CSNo_Complex_i) We take the following as an axiom:
Axiom. (minus_CSNo_CRe) We take the following as an axiom:
∀z, CSNo zRe (:-: z) = - Re z
Axiom. (minus_CSNo_CIm) We take the following as an axiom:
∀z, CSNo zIm (:-: z) = - Im z
Axiom. (add_CSNo_CRe) We take the following as an axiom:
∀z w, CSNo zCSNo wRe (plus' z w) = Re z + Re w
Axiom. (add_CSNo_CIm) We take the following as an axiom:
∀z w, CSNo zCSNo wIm (plus' z w) = Im z + Im w
Axiom. (CSNo_minus_CSNo) We take the following as an axiom:
∀z, CSNo zCSNo (minus_CSNo z)
Axiom. (SNo_Re) We take the following as an axiom:
∀x, SNo xRe x = x
Axiom. (SNo_Im) We take the following as an axiom:
∀x, SNo xIm x = 0
Axiom. (Re_0) We take the following as an axiom:
Re 0 = 0
Axiom. (Im_0) We take the following as an axiom:
Im 0 = 0
Axiom. (Re_1) We take the following as an axiom:
Re 1 = 1
Axiom. (Im_1) We take the following as an axiom:
Im 1 = 0
Axiom. (Re_i) We take the following as an axiom:
Re i = 0
Axiom. (Im_i) We take the following as an axiom:
Im i = 1
Axiom. (add_SNo_add_CSNo) We take the following as an axiom:
∀x y, SNo xSNo yx + y = add_CSNo x y
Axiom. (CSNo_add_CSNo) We take the following as an axiom:
∀z w, CSNo zCSNo wCSNo (add_CSNo z w)
Axiom. (add_CSNo_0L) We take the following as an axiom:
∀z, CSNo zadd_CSNo 0 z = z
Axiom. (add_CSNo_0R) We take the following as an axiom:
∀z, CSNo zadd_CSNo z 0 = z
Axiom. (add_CSNo_minus_CSNo_linv) We take the following as an axiom:
∀z, CSNo zadd_CSNo (minus_CSNo z) z = 0
Axiom. (add_CSNo_minus_CSNo_rinv) We take the following as an axiom:
∀z, CSNo zadd_CSNo z (minus_CSNo z) = 0
Axiom. (minus_SNo_minus_CSNo) We take the following as an axiom:
∀x, SNo x- x = minus_CSNo x
Axiom. (add_CSNo_com) We take the following as an axiom:
∀z w, CSNo zCSNo wz + w = w + z
Axiom. (add_CSNo_assoc) We take the following as an axiom:
∀z w v, CSNo zCSNo wCSNo vz + (w + v) = (z + w) + v
Axiom. (add_SNo_rotate_4_0312) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y) + (z + w) = (x + w) + (y + z)
Axiom. (mul_CSNo_ReR) We take the following as an axiom:
∀z w, CSNo zCSNo wSNo (Re z * Re w + - (Im z * Im w))
Axiom. (mul_CSNo_ImR) We take the following as an axiom:
∀z w, CSNo zCSNo wSNo (Re z * Im w + Im z * Re w)
Axiom. (mul_CSNo_CRe) We take the following as an axiom:
∀z w, CSNo zCSNo wRe (mult' z w) = Re z * Re w + - (Im z * Im w)
Axiom. (mul_CSNo_CIm) We take the following as an axiom:
∀z w, CSNo zCSNo wIm (mult' z w) = Re z * Im w + Im z * Re w
Axiom. (CSNo_mul_CSNo) We take the following as an axiom:
∀z w, CSNo zCSNo wCSNo (z w)
Axiom. (mul_CSNo_com) We take the following as an axiom:
∀z w, CSNo zCSNo wz w = w z
Axiom. (mul_CSNo_assoc) We take the following as an axiom:
∀z w v, CSNo zCSNo wCSNo vz (w v) = (z w) v
Axiom. (CSNo_0) We take the following as an axiom:
Axiom. (CSNo_1) We take the following as an axiom:
Axiom. (mul_CSNo_oneL) We take the following as an axiom:
∀z, CSNo z1 z = z
Axiom. (mul_CSNo_distrL) We take the following as an axiom:
∀z w v, CSNo zCSNo wCSNo vz (w + v) = z w + z v
Axiom. (mul_SNo_mul_CSNo) We take the following as an axiom:
∀x y, SNo xSNo yx * y = x y
Axiom. (Complex_i_sqr) We take the following as an axiom:
i i = :-: 1
Axiom. (CSNo_relative_recip) We take the following as an axiom:
∀z, CSNo z∀u, SNo u(Re z * Re z + Im z * Im z) * u = 1z (u Re z + :-: i u Im z) = 1
End of Section ComplexSNo
Beginning of Section Complex
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_CSNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_CSNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_CSNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Let i ≝ Complex_i
Let Re : setsetCSNo_Re
Let Im : setsetCSNo_Im
Let pa : setsetsetSNo_pair
Primitive. The name complex is a term of type set.
Axiom. (complex_I) We take the following as an axiom:
∀x yreal, pa x y complex
Axiom. (complex_E) We take the following as an axiom:
∀zcomplex, ∀p : prop, (∀x yreal, z = pa x yp)p
Axiom. (complex_CSNo) We take the following as an axiom:
Axiom. (real_complex) We take the following as an axiom:
Axiom. (complex_0) We take the following as an axiom:
Axiom. (complex_1) We take the following as an axiom:
Axiom. (complex_i) We take the following as an axiom:
Axiom. (complex_Re_eq) We take the following as an axiom:
∀x yreal, Re (pa x y) = x
Axiom. (complex_Im_eq) We take the following as an axiom:
∀x yreal, Im (pa x y) = y
Axiom. (complex_Re_real) We take the following as an axiom:
Axiom. (complex_Im_real) We take the following as an axiom:
Axiom. (complex_ReIm_split) We take the following as an axiom:
∀z wcomplex, Re z = Re wIm z = Im wz = w
Axiom. (complex_minus_CSNo) We take the following as an axiom:
Axiom. (complex_add_CSNo) We take the following as an axiom:
Axiom. (complex_mul_CSNo) We take the following as an axiom:
Axiom. (real_Re_eq) We take the following as an axiom:
∀xreal, Re x = x
Axiom. (real_Im_eq) We take the following as an axiom:
∀xreal, Im x = 0
Axiom. (mul_i_real_eq) We take the following as an axiom:
∀xreal, i * x = pa 0 x
Axiom. (real_Re_i_eq) We take the following as an axiom:
∀xreal, Re (i * x) = 0
Axiom. (real_Im_i_eq) We take the following as an axiom:
∀xreal, Im (i * x) = x
Axiom. (complex_eta) We take the following as an axiom:
∀zcomplex, z = Re z + i * Im z
Axiom. (nonzero_complex_recip_ex) We take the following as an axiom:
∀zcomplex, z 0∃wcomplex, z * w = 1
Axiom. (complex_real_set_eq) We take the following as an axiom:
End of Section Complex
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.