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 ⇒ ∀x ∈ A, xB 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, XYYXX = Y
Axiom. (In_ind) We take the following as an axiom:
∀P : setprop, (∀X : set, (∀x ∈ X, 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, xEmpty
Primitive. The name is a term of type setset.
Axiom. (UnionEq) We take the following as an axiom:
∀X x, x X∃Y, xYYX
Primitive. The name 𝒫 is a term of type setset.
Axiom. (PowerEq) We take the following as an axiom:
∀X Y : set, Y𝒫 XYX
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|x ∈ A}∃x ∈ A, y = F x
Definition. We define TransSet to be λU : set∀x ∈ U, xU of type setprop.
Definition. We define Union_closed to be λU : set∀X : set, XU XU of type setprop.
Definition. We define Power_closed to be λU : set∀X : set, XU𝒫 XU of type setprop.
Definition. We define Repl_closed to be λU : set∀X : set, XU∀F : setset, (∀x : set, xXF xU){F x|x ∈ X}U of type setprop.
Definition. We define ZF_closed to be λU : setUnion_closed UPower_closed URepl_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, NUnivOf 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, NUTransSet UZF_closed UUnivOf NU
Axiom. (FalseE) We take the following as an axiom:
False∀p : prop, p
Axiom. (TrueI) We take the following as an axiom:
True
Axiom. (notI) We take the following as an axiom:
∀A : prop, (AFalse)¬ A
Axiom. (notE) We take the following as an axiom:
∀A : prop, ¬ AAFalse
Axiom. (andI) We take the following as an axiom:
∀A B : prop, ABAB
Axiom. (andEL) We take the following as an axiom:
∀A B : prop, ABA
Axiom. (andER) We take the following as an axiom:
∀A B : prop, ABB
Axiom. (orIL) We take the following as an axiom:
∀A B : prop, AAB
Axiom. (orIR) We take the following as an axiom:
∀A B : prop, BAB
Axiom. (orE) We take the following as an axiom:
∀A B C : prop, (AC)(BC)ABC
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (and3I) We take the following as an axiom:
P1P2P3P1P2P3
Axiom. (and3E) We take the following as an axiom:
P1P2P3(∀p : prop, (P1P2P3p)p)
Axiom. (or3I1) We take the following as an axiom:
P1P1P2P3
Axiom. (or3I2) We take the following as an axiom:
P2P1P2P3
Axiom. (or3I3) We take the following as an axiom:
P3P1P2P3
Axiom. (or3E) We take the following as an axiom:
P1P2P3(∀p : prop, (P1p)(P2p)(P3p)p)
Variable P4 : prop
Axiom. (and4I) We take the following as an axiom:
P1P2P3P4P1P2P3P4
Axiom. (and4E) We take the following as an axiom:
P1P2P3P4(∀p : prop, (P1P2P3P4p)p)
Axiom. (or4I1) We take the following as an axiom:
P1P1P2P3P4
Axiom. (or4I2) We take the following as an axiom:
P2P1P2P3P4
Axiom. (or4I3) We take the following as an axiom:
P3P1P2P3P4
Axiom. (or4I4) We take the following as an axiom:
P4P1P2P3P4
Axiom. (or4E) We take the following as an axiom:
P1P2P3P4(∀p : prop, (P1p)(P2p)(P3p)(P4p)p)
Variable P5 : prop
Axiom. (and5I) We take the following as an axiom:
P1P2P3P4P5P1P2P3P4P5
Axiom. (and5E) We take the following as an axiom:
P1P2P3P4P5(∀p : prop, (P1P2P3P4P5p)p)
Axiom. (or5I1) We take the following as an axiom:
P1P1P2P3P4P5
Axiom. (or5I2) We take the following as an axiom:
P2P1P2P3P4P5
Axiom. (or5I3) We take the following as an axiom:
P3P1P2P3P4P5
Axiom. (or5I4) We take the following as an axiom:
P4P1P2P3P4P5
Axiom. (or5I5) We take the following as an axiom:
P5P1P2P3P4P5
Axiom. (or5E) We take the following as an axiom:
P1P2P3P4P5(∀p : prop, (P1p)(P2p)(P3p)(P4p)(P5p)p)
Variable P6 : prop
Axiom. (and6I) We take the following as an axiom:
P1P2P3P4P5P6P1P2P3P4P5P6
Axiom. (and6E) We take the following as an axiom:
P1P2P3P4P5P6(∀p : prop, (P1P2P3P4P5P6p)p)
Variable P7 : prop
Axiom. (and7I) We take the following as an axiom:
P1P2P3P4P5P6P7P1P2P3P4P5P6P7
Axiom. (and7E) We take the following as an axiom:
P1P2P3P4P5P6P7(∀p : prop, (P1P2P3P4P5P6P7p)p)
End of Section PropN
Axiom. (iffI) We take the following as an axiom:
∀A B : prop, (AB)(BA)(AB)
Axiom. (iffEL) We take the following as an axiom:
∀A B : prop, (AB)AB
Axiom. (iffER) We take the following as an axiom:
∀A B : prop, (AB)BA
Axiom. (iff_ref) We take the following as an axiom:
∀A : prop, AA
Axiom. (neq_i_sym) We take the following as an axiom:
∀x y, xyyx
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 xQ x)P = Q
Axiom. (prop_ext_2) We take the following as an axiom:
∀p q : prop, (pq)(qp)p = q
Axiom. (pred_ext_2) We take the following as an axiom:
∀P Q : setprop, PQQPP = Q
Axiom. (Subq_ref) We take the following as an axiom:
∀X : set, XX
Axiom. (Subq_tra) We take the following as an axiom:
∀X Y Z : set, XYYZXZ
Axiom. (Subq_contra) We take the following as an axiom:
∀X Y z : set, XYzYzX
Axiom. (EmptyE) We take the following as an axiom:
∀x : set, xEmpty
Axiom. (Subq_Empty) We take the following as an axiom:
∀X : set, EmptyX
Axiom. (Empty_Subq_eq) We take the following as an axiom:
∀X : set, XEmptyX = Empty
Axiom. (Empty_eq) We take the following as an axiom:
∀X : set, (∀x, xX)X = Empty
Axiom. (UnionI) We take the following as an axiom:
∀X x Y : set, xYYXx X
Axiom. (UnionE) We take the following as an axiom:
∀X x : set, x X∃Y : set, xYYX
Axiom. (UnionE_impred) We take the following as an axiom:
∀X x : set, x X∀p : prop, (∀Y : set, xYYXp)p
Axiom. (Union_Empty) We take the following as an axiom:
Empty = Empty
Axiom. (PowerI) We take the following as an axiom:
∀X Y : set, YXY𝒫 X
Axiom. (PowerE) We take the following as an axiom:
∀X Y : set, Y𝒫 XYX
Axiom. (Power_Subq) We take the following as an axiom:
∀X Y : set, XY𝒫 X𝒫 Y
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. (Union_Power_Subq) 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. (imp_not_or) We take the following as an axiom:
∀p q : prop, (pq)¬ pq
Axiom. (not_and_or_demorgan) We take the following as an axiom:
∀p q : prop, ¬ (pq)¬ p¬ q
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_impI1) We take the following as an axiom:
∀A B : prop, (A¬ B)(¬ AB)exactly1of2 A B
Axiom. (exactly1of2_impI2) We take the following as an axiom:
∀A B : prop, (B¬ A)(¬ BA)exactly1of2 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 BAB
Axiom. (exactly1of2_impn12) We take the following as an axiom:
∀A B : prop, exactly1of2 A BA¬ B
Axiom. (exactly1of2_impn21) We take the following as an axiom:
∀A B : prop, exactly1of2 A BB¬ A
Axiom. (exactly1of2_nimp12) We take the following as an axiom:
∀A B : prop, exactly1of2 A B¬ AB
Axiom. (exactly1of2_nimp21) We take the following as an axiom:
∀A B : prop, exactly1of2 A B¬ BA
Primitive. The name exactly1of3 is a term of type propproppropprop.
Axiom. (exactly1of3_I1) We take the following as an axiom:
∀A B C : prop, A¬ B¬ Cexactly1of3 A B C
Axiom. (exactly1of3_I2) We take the following as an axiom:
∀A B C : prop, ¬ AB¬ Cexactly1of3 A B C
Axiom. (exactly1of3_I3) We take the following as an axiom:
∀A B C : prop, ¬ A¬ BCexactly1of3 A B C
Axiom. (exactly1of3_impI1) We take the following as an axiom:
∀A B C : prop, (A¬ B)(A¬ C)(B¬ C)(¬ ABC)exactly1of3 A B C
Axiom. (exactly1of3_impI2) We take the following as an axiom:
∀A B C : prop, (B¬ A)(B¬ C)(A¬ C)(¬ BAC)exactly1of3 A B C
Axiom. (exactly1of3_impI3) We take the following as an axiom:
∀A B C : prop, (C¬ A)(C¬ B)(A¬ B)(¬ AB)exactly1of3 A B C
Axiom. (exactly1of3_E) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B C∀p : prop, (A¬ B¬ Cp)(¬ AB¬ Cp)(¬ A¬ BCp)p
Axiom. (exactly1of3_or) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B CABC
Axiom. (exactly1of3_impn12) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B CA¬ B
Axiom. (exactly1of3_impn13) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B CA¬ C
Axiom. (exactly1of3_impn21) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B CB¬ A
Axiom. (exactly1of3_impn23) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B CB¬ C
Axiom. (exactly1of3_impn31) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B CC¬ A
Axiom. (exactly1of3_impn32) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B CC¬ B
Axiom. (exactly1of3_nimp1) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B C¬ ABC
Axiom. (exactly1of3_nimp2) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B C¬ BAC
Axiom. (exactly1of3_nimp3) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B C¬ CAB
Axiom. (ReplI) We take the following as an axiom:
∀A : set, ∀F : setset, ∀x : set, xAF x{F x|x ∈ A}
Axiom. (ReplE) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y{F x|x ∈ A}∃x ∈ A, y = F x
Axiom. (ReplE_impred) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y{F x|x ∈ A}∀p : prop, (∀x : set, xAy = F xp)p
Axiom. (Repl_Empty) We take the following as an axiom:
∀F : setset, {F x|x ∈ Empty} = Empty
Axiom. (ReplEq_ext_sub) We take the following as an axiom:
∀X, ∀F G : setset, (∀x ∈ X, F x = G x){F x|x ∈ X}{G x|x ∈ X}
Axiom. (ReplEq_ext) We take the following as an axiom:
∀X, ∀F G : setset, (∀x ∈ X, F x = G x){F x|x ∈ X} = {G x|x ∈ 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
Axiom. (If_i_eta) We take the following as an axiom:
∀p : prop, ∀x : set, (if p then x else x) = x
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 = yx = 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}
Axiom. (UPair_com) We take the following as an axiom:
∀x y : set, {x,y} = {y,x}
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, zXzXY
Axiom. (binunionI2) We take the following as an axiom:
∀X Y z : set, zYzXY
Axiom. (binunionE) We take the following as an axiom:
∀X Y z : set, zXYzXzY
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.
Axiom. (Power_0_Sing_0) We take the following as an axiom:
𝒫 Empty = {Empty}
Axiom. (Repl_UPair) We take the following as an axiom:
∀F : setset, ∀x y : set, {F z|z ∈ {x,y}} = {F x,F y}
Axiom. (Repl_Sing) We take the following as an axiom:
∀F : setset, ∀x : set, {F z|z ∈ {x}} = {F x}
Axiom. (Repl_restr) We take the following as an axiom:
∀X : set, ∀F G : setset, (∀x : set, xXF x = G x){F x|x ∈ X} = {G x|x ∈ X}
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, xXyF xyx ∈ XF x
Axiom. (famunionE) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀y : set, y(x ∈ XF x)∃x ∈ X, yF x
Axiom. (famunionE_impred) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀y : set, y(x ∈ XF x)∀p : prop, (∀x, xXyF xp)p
Axiom. (UnionEq_famunionId) We take the following as an axiom:
∀X : set, X = x ∈ Xx
Axiom. (ReplEq_famunion_Sing) We take the following as an axiom:
∀X : set, ∀F : (setset), {F x|x ∈ X} = x ∈ X{F x}
Axiom. (Power_Sing) We take the following as an axiom:
∀x : set, 𝒫 {x} = {Empty,{x}}
Axiom. (Power_Sing_0) We take the following as an axiom:
𝒫 {Empty} = {Empty,{Empty}}
Primitive. The name Sep is a term of type set(setprop)set.
Notation. {xA | B} is notation for Sep Ax . B).
Axiom. (SepI) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, xXP xx{x ∈ X|P x}
Axiom. (SepE) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x{x ∈ X|P x}xXP x
Axiom. (SepE1) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x{x ∈ X|P x}xX
Axiom. (SepE2) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x{x ∈ X|P x}P x
Axiom. (Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : setprop, {x ∈ X|P x}X
Axiom. (Sep_In_Power) We take the following as an axiom:
∀X : set, ∀P : setprop, {x ∈ X|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, xXP xF x{F x|x ∈ X, P x}
Axiom. (ReplSepE) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y{F x|x ∈ X, P x}∃x : set, xXP xy = F x
Axiom. (ReplSepE_impred) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y{F x|x ∈ X, P x}∀p : prop, (∀x ∈ X, P xy = F xp)p
Primitive. The name ReplSep2 is a term of type set(setset)(setsetprop)(setsetset)set.
Axiom. (ReplSep2I) We take the following as an axiom:
∀A, ∀B : setset, ∀P : setsetprop, ∀F : setsetset, ∀x ∈ A, ∀y ∈ B x, P x yF x yReplSep2 A B P F
Axiom. (ReplSep2E_impred) We take the following as an axiom:
∀A, ∀B : setset, ∀P : setsetprop, ∀F : setsetset, ∀r ∈ ReplSep2 A B P F, ∀p : prop, (∀x ∈ A, ∀y ∈ B x, P x yr = F x yp)p
Axiom. (ReplSep2E) We take the following as an axiom:
∀A, ∀B : setset, ∀P : setsetprop, ∀F : setsetset, ∀r ∈ ReplSep2 A B P F, ∃x ∈ A, ∃y ∈ B x, P x yr = F x y
Axiom. (binunion_asso) We take the following as an axiom:
∀X Y Z : set, X(YZ) = (XY)Z
Axiom. (binunion_com) We take the following as an axiom:
∀X Y : set, XY = YX
Axiom. (binunion_idl) We take the following as an axiom:
∀X : set, EmptyX = X
Axiom. (binunion_idr) We take the following as an axiom:
∀X : set, XEmpty = X
Axiom. (binunion_idem) We take the following as an axiom:
∀X : set, XX = X
Axiom. (binunion_Subq_1) We take the following as an axiom:
∀X Y : set, XXY
Axiom. (binunion_Subq_2) We take the following as an axiom:
∀X Y : set, YXY
Axiom. (binunion_Subq_min) We take the following as an axiom:
∀X Y Z : set, XZYZXYZ
Axiom. (Subq_binunion_eq) We take the following as an axiom:
∀X Y, (XY) = (XY = Y)
Axiom. (binunion_nIn_I) We take the following as an axiom:
∀X Y z : set, zXzYzXY
Axiom. (binunion_nIn_E) We take the following as an axiom:
∀X Y z : set, zXYzXzY
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, zXzYzXY
Axiom. (binintersectE) We take the following as an axiom:
∀X Y z, zXYzXzY
Axiom. (binintersectE1) We take the following as an axiom:
∀X Y z, zXYzX
Axiom. (binintersectE2) We take the following as an axiom:
∀X Y z, zXYzY
Axiom. (binintersect_Subq_1) We take the following as an axiom:
∀X Y : set, XYX
Axiom. (binintersect_Subq_2) We take the following as an axiom:
∀X Y : set, XYY
Axiom. (binintersect_Subq_eq_1) We take the following as an axiom:
∀X Y, XYXY = X
Axiom. (binintersect_Subq_max) We take the following as an axiom:
∀X Y Z : set, ZXZYZXY
Axiom. (binintersect_asso) We take the following as an axiom:
∀X Y Z : set, X(YZ) = (XY)Z
Axiom. (binintersect_com) We take the following as an axiom:
∀X Y : set, XY = YX
Axiom. (binintersect_annil) We take the following as an axiom:
∀X : set, EmptyX = Empty
Axiom. (binintersect_annir) We take the following as an axiom:
∀X : set, XEmpty = Empty
Axiom. (binintersect_idem) We take the following as an axiom:
∀X : set, XX = X
Axiom. (binintersect_binunion_distr) We take the following as an axiom:
∀X Y Z : set, X(YZ) = XYXZ
Axiom. (binunion_binintersect_distr) We take the following as an axiom:
∀X Y Z : set, XYZ = (XY)(XZ)
Axiom. (Subq_binintersection_eq) We take the following as an axiom:
∀X Y : set, (XY) = (XY = X)
Axiom. (binintersect_nIn_I1) We take the following as an axiom:
∀X Y z : set, zXzXY
Axiom. (binintersect_nIn_I2) We take the following as an axiom:
∀X Y z : set, zYzXY
Axiom. (binintersect_nIn_E) We take the following as an axiom:
∀X Y z : set, zXYzXzY
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, (zX)(zY)zXY
Axiom. (setminusE) We take the following as an axiom:
∀X Y z, (zXY)zXzY
Axiom. (setminusE1) We take the following as an axiom:
∀X Y z, (zXY)zX
Axiom. (setminusE2) We take the following as an axiom:
∀X Y z, (zXY)zY
Axiom. (setminus_Subq) We take the following as an axiom:
∀X Y : set, XYX
Axiom. (setminus_Subq_contra) We take the following as an axiom:
∀X Y Z : set, ZYXYXZ
Axiom. (setminus_nIn_I1) We take the following as an axiom:
∀X Y z, zXzXY
Axiom. (setminus_nIn_I2) We take the following as an axiom:
∀X Y z, zYzXY
Axiom. (setminus_nIn_E) We take the following as an axiom:
∀X Y z, zXYzXzY
Axiom. (setminus_selfannih) We take the following as an axiom:
∀X : set, (XX) = Empty
Axiom. (setminus_binintersect) We take the following as an axiom:
∀X Y Z : set, XYZ = (XY)(XZ)
Axiom. (setminus_binunion) We take the following as an axiom:
∀X Y Z : set, XYZ = (XY)Z
Axiom. (binintersect_setminus) We take the following as an axiom:
∀X Y Z : set, (XY)Z = X(YZ)
Axiom. (binunion_setminus) We take the following as an axiom:
∀X Y Z : set, XYZ = (XZ)(YZ)
Axiom. (setminus_setminus) We take the following as an axiom:
∀X Y Z : set, X(YZ) = (XY)(XZ)
Axiom. (setminus_annil) We take the following as an axiom:
∀X : set, EmptyX = Empty
Axiom. (setminus_idr) We take the following as an axiom:
∀X : set, XEmpty = X
Axiom. (In_irref) We take the following as an axiom:
∀x, xx
Axiom. (In_no2cycle) We take the following as an axiom:
∀x y, xyyxFalse
Axiom. (In_no3cycle) We take the following as an axiom:
∀x y z, xyyzzxFalse
Primitive. The name ordsucc is a term of type setset.
Axiom. (ordsuccI1) We take the following as an axiom:
∀x : set, xordsucc x
Axiom. (ordsuccI2) We take the following as an axiom:
∀x : set, xordsucc x
Axiom. (ordsuccE) We take the following as an axiom:
∀x y : set, yordsucc xyxy = 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, 0ordsucc a
Axiom. (neq_ordsucc_0) We take the following as an axiom:
∀a : set, ordsucc a0
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, abordsucc aordsucc b
Axiom. (In_0_1) We take the following as an axiom:
01
Axiom. (In_0_2) We take the following as an axiom:
02
Axiom. (In_1_2) We take the following as an axiom:
12
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_3) We take the following as an axiom:
nat_p 3
Axiom. (nat_4) We take the following as an axiom:
nat_p 4
Axiom. (nat_5) We take the following as an axiom:
nat_p 5
Axiom. (nat_6) We take the following as an axiom:
nat_p 6
Axiom. (nat_0_in_ordsucc) We take the following as an axiom:
∀n, nat_p n0ordsucc n
Axiom. (nat_ordsucc_in_ordsucc) We take the following as an axiom:
∀n, nat_p n∀m ∈ n, ordsucc mordsucc 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) We take the following as an axiom:
∀n, nat_p nn = 0∃x, nat_p xn = ordsucc x
Axiom. (nat_complete_ind) We take the following as an axiom:
∀p : setprop, (∀n, nat_p n(∀m ∈ n, p m)p n)∀n, nat_p np n
Axiom. (nat_p_trans) We take the following as an axiom:
∀n, nat_p n∀m ∈ n, nat_p m
Axiom. (nat_trans) We take the following as an axiom:
∀n, nat_p n∀m ∈ n, mn
Axiom. (nat_ordsucc_trans) We take the following as an axiom:
∀n, nat_p n∀m ∈ ordsucc n, mn
Axiom. (Union_ordsucc_eq) We take the following as an axiom:
∀n, nat_p n (ordsucc n) = n
Axiom. (In_0_3) We take the following as an axiom:
03
Axiom. (In_1_3) We take the following as an axiom:
13
Axiom. (In_2_3) We take the following as an axiom:
23
Axiom. (In_0_4) We take the following as an axiom:
04
Axiom. (In_1_4) We take the following as an axiom:
14
Axiom. (In_2_4) We take the following as an axiom:
24
Axiom. (In_3_4) We take the following as an axiom:
34
Axiom. (In_0_5) We take the following as an axiom:
05
Axiom. (In_1_5) We take the following as an axiom:
15
Axiom. (In_2_5) We take the following as an axiom:
25
Axiom. (In_3_5) We take the following as an axiom:
35
Axiom. (In_4_5) We take the following as an axiom:
45
Axiom. (In_0_6) We take the following as an axiom:
06
Axiom. (In_1_6) We take the following as an axiom:
16
Axiom. (In_2_6) We take the following as an axiom:
26
Axiom. (In_3_6) We take the following as an axiom:
36
Axiom. (In_4_6) We take the following as an axiom:
46
Axiom. (In_5_6) We take the following as an axiom:
56
Axiom. (cases_1) We take the following as an axiom:
∀i ∈ 1, ∀p : setprop, p 0p i
Axiom. (cases_2) We take the following as an axiom:
∀i ∈ 2, ∀p : setprop, p 0p 1p i
Axiom. (cases_3) We take the following as an axiom:
∀i ∈ 3, ∀p : setprop, p 0p 1p 2p i
Axiom. (cases_4) We take the following as an axiom:
∀i ∈ 4, ∀p : setprop, p 0p 1p 2p 3p i
Axiom. (cases_5) We take the following as an axiom:
∀i ∈ 5, ∀p : setprop, p 0p 1p 2p 3p 4p i
Axiom. (cases_6) We take the following as an axiom:
∀i ∈ 6, ∀p : setprop, p 0p 1p 2p 3p 4p 5p i
Axiom. (neq_0_1) We take the following as an axiom:
01
Axiom. (neq_0_2) We take the following as an axiom:
02
Axiom. (neq_1_2) We take the following as an axiom:
12
Axiom. (neq_1_0) We take the following as an axiom:
10
Axiom. (neq_2_0) We take the following as an axiom:
20
Axiom. (neq_2_1) We take the following as an axiom:
21
Axiom. (neq_3_0) We take the following as an axiom:
30
Axiom. (neq_3_1) We take the following as an axiom:
31
Axiom. (neq_3_2) We take the following as an axiom:
32
Axiom. (neq_4_0) We take the following as an axiom:
40
Axiom. (neq_4_1) We take the following as an axiom:
41
Axiom. (neq_4_2) We take the following as an axiom:
42
Axiom. (neq_4_3) We take the following as an axiom:
43
Axiom. (neq_5_0) We take the following as an axiom:
50
Axiom. (neq_5_1) We take the following as an axiom:
51
Axiom. (neq_5_2) We take the following as an axiom:
52
Axiom. (neq_5_3) We take the following as an axiom:
53
Axiom. (neq_5_4) We take the following as an axiom:
54
Axiom. (ZF_closed_I) We take the following as an axiom:
∀U, Union_closed UPower_closed URepl_closed UZF_closed U
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∀X ∈ U, XU
Axiom. (ZF_Power_closed) We take the following as an axiom:
∀U, ZF_closed U∀X ∈ U, 𝒫 XU
Axiom. (ZF_Repl_closed) We take the following as an axiom:
∀U, ZF_closed U∀X ∈ U, ∀F : setset, (∀x ∈ X, F xU){F x|x ∈ X}U
Axiom. (ZF_UPair_closed) We take the following as an axiom:
∀U, ZF_closed U∀x y ∈ U, {x,y}U
Axiom. (ZF_Sing_closed) We take the following as an axiom:
∀U, ZF_closed U∀x ∈ U, {x}U
Axiom. (ZF_binunion_closed) We take the following as an axiom:
∀U, ZF_closed U∀X Y ∈ U, (XY)U
Axiom. (ZF_ordsucc_closed) We take the following as an axiom:
∀U, ZF_closed U∀x ∈ U, ordsucc xU
Axiom. (nat_p_UnivOf_Empty) We take the following as an axiom:
∀n : set, nat_p nnUnivOf 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∀beta ∈ alpha, TransSet beta of type setprop.
Axiom. (ordinal_TransSet) We take the following as an axiom:
∀alpha : set, ordinal alphaTransSet alpha
Axiom. (ordinal_In_TransSet) We take the following as an axiom:
∀alpha : set, ordinal alpha∀beta ∈ alpha, TransSet beta
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∀beta ∈ alpha, 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∀x ∈ X, ordsucc xX
Axiom. (ordinal_ordsucc_In_Subq) We take the following as an axiom:
∀alpha, ordinal alpha∀beta ∈ alpha, ordsucc betaalpha
Axiom. (ordinal_trichotomy_or) We take the following as an axiom:
∀alpha beta : set, ordinal alphaordinal betaalphabetaalpha = betabetaalpha
Axiom. (ordinal_In_Or_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalphabetabetaalpha
Axiom. (ordinal_linear) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalphabetabetaalpha
Axiom. (ordinal_ordsucc_In_eq) We take the following as an axiom:
∀alpha beta, ordinal alphabetaalphaordsucc betaalphaalpha = ordsucc beta
Axiom. (ordinal_lim_or_succ) We take the following as an axiom:
∀alpha, ordinal alpha(∀beta ∈ alpha, ordsucc betaalpha)(∃beta ∈ alpha, alpha = ordsucc beta)
Axiom. (ordinal_ordsucc_In) We take the following as an axiom:
∀alpha, ordinal alpha∀beta ∈ alpha, ordsucc betaordsucc alpha
Axiom. (ordinal_Union) We take the following as an axiom:
∀X, (∀x ∈ X, ordinal x)ordinal ( X)
Axiom. (ordinal_famunion) We take the following as an axiom:
∀X, ∀F : setset, (∀x ∈ X, ordinal (F x))ordinal (x ∈ XF x)
Axiom. (ordinal_binintersect) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaordinal (alphabeta)
Axiom. (ordinal_binunion) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaordinal (alphabeta)
Axiom. (ordinal_Sep) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, (∀beta ∈ alpha, ∀gamma ∈ beta, p betap gamma)ordinal {beta ∈ alpha|p beta}
Definition. We define inj to be λX Y f ⇒ (∀u ∈ X, f uY)(∀u v ∈ X, f u = f vu = v) of type setset(setset)prop.
Definition. We define surj to be λX Y f ⇒ (∀u ∈ X, f uY)(∀w ∈ Y, ∃u ∈ X, f u = w) of type setset(setset)prop.
Definition. We define bij to be λX Y f ⇒ (∀u ∈ X, f uY)(∀u v ∈ X, f u = f vu = v)(∀w ∈ Y, ∃u ∈ X, f u = w) of type setset(setset)prop.
Axiom. (bijI) We take the following as an axiom:
∀X Y, ∀f : setset, (∀u ∈ X, f uY)(∀u v ∈ X, f u = f vu = v)(∀w ∈ Y, ∃u ∈ X, 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, ((∀u ∈ X, f uY)(∀u v ∈ X, f u = f vu = v)(∀w ∈ Y, ∃u ∈ X, 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, (∀w ∈ Y, ∃u ∈ X, f u = w)∀y ∈ Y, inv X f yXf (inv X f y) = y
Axiom. (inj_linv) We take the following as an axiom:
∀X Y, ∀f : setset, (∀u v ∈ X, f u = f vu = v)∀x ∈ X, 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_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))
Axiom. (bij_id) We take the following as an axiom:
∀X, bij X X (λx ⇒ x)
Axiom. (bij_inj) We take the following as an axiom:
∀X Y, ∀f : setset, bij X Y finj X Y f
Axiom. (bij_surj) We take the following as an axiom:
∀X Y, ∀f : setset, bij X Y fsurj X Y f
Axiom. (inj_surj_bij) We take the following as an axiom:
∀X Y, ∀f : setset, inj X Y fsurj X Y fbij X Y f
Axiom. (surj_inv_inj) We take the following as an axiom:
∀X Y, ∀f : setset, (∀y ∈ Y, ∃x ∈ X, f x = y)inj Y X (inv X f)
Definition. We define atleastp to be λX Y : set∃f : setset, inj X Y f of type setsetprop.
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
Definition. We define finite to be λX ⇒ ∃n ∈ ω, equip X n of type setprop.
Definition. We define infinite to be λX ⇒ ¬ finite X of type setprop.
Axiom. (KnasterTarski_set) We take the following as an axiom:
∀A, ∀F : setset, (∀U ∈ 𝒫 A, F U𝒫 A)(∀U V ∈ 𝒫 A, UVF UF V)∃Y ∈ 𝒫 A, F Y = Y
Axiom. (image_In_Power) We take the following as an axiom:
∀A B, ∀f : setset, (∀x ∈ A, f xB)∀U ∈ 𝒫 A, {f x|x ∈ U}𝒫 B
Axiom. (image_monotone) We take the following as an axiom:
∀f : setset, ∀U V, UV{f x|x ∈ U}{f x|x ∈ V}
Axiom. (setminus_In_Power) We take the following as an axiom:
∀A U, AU𝒫 A
Axiom. (setminus_antimonotone) We take the following as an axiom:
∀A U V, UVAVAU
Axiom. (SchroederBernstein) We take the following as an axiom:
∀A B, ∀f g : setset, inj A B finj B A gequip A B
Axiom. (f_eq_i) We take the following as an axiom:
∀f : setset, ∀x y, x = yf x = f y
Axiom. (f_eq_i_i) We take the following as an axiom:
∀f : setsetset, ∀x y z w, x = yz = wf x z = f y w
Axiom. (eq_i_tra) We take the following as an axiom:
∀x y z, x = yy = zx = z
Definition. We define nSubq to be λX Y ⇒ ¬ Subq X Y of type setsetprop.
Notation. We use as an infix operator with priority 502 and no associativity corresponding to applying term nSubq.
Axiom. (Sing_inv) We take the following as an axiom:
∀x Y, {x} = YxY∀y ∈ Y, y = x
Axiom. (TransSet_In_ordsucc_Subq) We take the following as an axiom:
∀x y, TransSet yxordsucc yxy
Axiom. (inv_Repl_eq) We take the following as an axiom:
∀X, ∀f g : setset, (∀x ∈ X, f (g x) = x){f y|y ∈ {g x|x ∈ X}} = X
Axiom. (invol_Repl_eq) We take the following as an axiom:
∀X, ∀f : setset, (∀x ∈ X, f (f x) = x){f y|y ∈ {f x|x ∈ X}} = X
Axiom. (Eps_i_set_R) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀x ∈ X, P xEps_i (λx ⇒ xXP x)XP (Eps_i (λx ⇒ xXP x))
Axiom. (exandE_i) We take the following as an axiom:
∀P Q : setprop, (∃x, P xQ 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 xQ 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 xQ 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 xQ x)∀p : prop, (∀x : setsetsetset, P xQ xp)p
Axiom. (exandE_iio) We take the following as an axiom:
∀P Q : (setsetprop)prop, (∃x : setsetprop, P xQ x)∀p : prop, (∀x : setsetprop, P xQ xp)p
Axiom. (exandE_iiio) We take the following as an axiom:
∀P Q : (setsetsetprop)prop, (∃x : setsetsetprop, P xQ x)∀p : prop, (∀x : setsetsetprop, 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_iio
Variable P : (setsetprop)prop
Primitive. The name Descr_iio is a term of type setsetprop.
Hypothesis Pex : ∃f : setsetprop, P f
Hypothesis Puniq : ∀f g : setsetprop, P fP gf = g
Axiom. (Descr_iio_prop) We take the following as an axiom:
End of Section Descr_iio
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 Descr_Vo2
Variable P : Vo 2prop
Primitive. The name Descr_Vo2 is a term of type Vo 2.
Hypothesis Pex : ∃f : Vo 2, P f
Hypothesis Puniq : ∀f g : Vo 2, P fP gf = g
Axiom. (Descr_Vo2_prop) We take the following as an axiom:
End of Section Descr_Vo2
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 If_Vo1
Variable p : prop
Variable f g : Vo 1
Primitive. The name If_Vo1 is a term of type Vo 1.
Axiom. (If_Vo1_1) We take the following as an axiom:
pIf_Vo1 = f
Axiom. (If_Vo1_0) We take the following as an axiom:
¬ pIf_Vo1 = g
End of Section If_Vo1
Beginning of Section If_iio
Variable p : prop
Variable f g : setsetprop
Primitive. The name If_iio is a term of type setsetprop.
Axiom. (If_iio_1) We take the following as an axiom:
pIf_iio = f
Axiom. (If_iio_0) We take the following as an axiom:
¬ pIf_iio = g
End of Section If_iio
Beginning of Section If_Vo2
Variable p : prop
Variable f g : Vo 2
Primitive. The name If_Vo2 is a term of type Vo 2.
Axiom. (If_Vo2_1) We take the following as an axiom:
pIf_Vo2 = f
Axiom. (If_Vo2_0) We take the following as an axiom:
¬ pIf_Vo2 = g
End of Section If_Vo2
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, (∀x ∈ X, 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), (∀x ∈ X, 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), (∀x ∈ X, 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 EpsilonRec_iio
Variable F : set(set(setsetprop))(setsetprop)
Primitive. The name In_rec_iio is a term of type set(setsetprop).
Hypothesis Fr : ∀X : set, ∀g h : set(setsetprop), (∀x ∈ X, g x = h x)F X g = F X h
Axiom. (In_rec_iio_eq) We take the following as an axiom:
∀X : set, In_rec_iio X = F X In_rec_iio
End of Section EpsilonRec_iio
Beginning of Section EpsilonRec_Vo1
Variable F : set(setVo 1)Vo 1
Primitive. The name In_rec_Vo1 is a term of type setVo 1.
Hypothesis Fr : ∀X : set, ∀g h : setVo 1, (∀x ∈ X, g x = h x)F X g = F X h
Axiom. (In_rec_Vo1_eq) We take the following as an axiom:
∀X : set, In_rec_Vo1 X = F X In_rec_Vo1
End of Section EpsilonRec_Vo1
Beginning of Section EpsilonRec_Vo2
Variable F : set(setVo 2)Vo 2
Primitive. The name In_rec_Vo2 is a term of type setVo 2.
Hypothesis Fr : ∀X : set, ∀g h : setVo 2, (∀x ∈ X, g x = h x)F X g = F X h
Axiom. (In_rec_Vo2_eq) We take the following as an axiom:
∀X : set, In_rec_Vo2 X = F X In_rec_Vo2
End of Section EpsilonRec_Vo2
Beginning of Section If_Vo3
Variable p : prop
Variable f g : Vo 3
Primitive. The name If_Vo3 is a term of type Vo 3.
Axiom. (If_Vo3_1) We take the following as an axiom:
pIf_Vo3 = f
Axiom. (If_Vo3_0) We take the following as an axiom:
¬ pIf_Vo3 = g
End of Section If_Vo3
Beginning of Section Descr_Vo3
Variable P : Vo 3prop
Primitive. The name Descr_Vo3 is a term of type Vo 3.
Hypothesis Pex : ∃f : Vo 3, P f
Hypothesis Puniq : ∀f g : Vo 3, P fP gf = g
Axiom. (Descr_Vo3_prop) We take the following as an axiom:
End of Section Descr_Vo3
Beginning of Section EpsilonRec_Vo3
Variable F : set(setVo 3)Vo 3
Primitive. The name In_rec_Vo3 is a term of type setVo 3.
Hypothesis Fr : ∀X : set, ∀g h : setVo 3, (∀x ∈ X, g x = h x)F X g = F X h
Axiom. (In_rec_Vo3_eq) We take the following as an axiom:
∀X : set, In_rec_Vo3 X = F X In_rec_Vo3
End of Section EpsilonRec_Vo3
Beginning of Section If_Vo4
Variable p : prop
Variable f g : Vo 4
Primitive. The name If_Vo4 is a term of type Vo 4.
Axiom. (If_Vo4_1) We take the following as an axiom:
pIf_Vo4 = f
Axiom. (If_Vo4_0) We take the following as an axiom:
¬ pIf_Vo4 = g
End of Section If_Vo4
Beginning of Section Descr_Vo4
Variable P : Vo 4prop
Primitive. The name Descr_Vo4 is a term of type Vo 4.
Hypothesis Pex : ∃f : Vo 4, P f
Hypothesis Puniq : ∀f g : Vo 4, P fP gf = g
Axiom. (Descr_Vo4_prop) We take the following as an axiom:
End of Section Descr_Vo4
Beginning of Section EpsilonRec_Vo4
Variable F : set(setVo 4)Vo 4
Primitive. The name In_rec_Vo4 is a term of type setVo 4.
Hypothesis Fr : ∀X : set, ∀g h : setVo 4, (∀x ∈ X, g x = h x)F X g = F X h
Axiom. (In_rec_Vo4_eq) We take the following as an axiom:
∀X : set, In_rec_Vo4 X = F X In_rec_Vo4
End of Section EpsilonRec_Vo4
Definition. We define bigintersect to be λ(D : (setprop)prop)(x : set) ⇒ ∀P : setprop, D PP x.
Definition. We define reflexive to be λR ⇒ ∀x : set, R x x of type (setsetprop)prop.
Definition. We define irreflexive to be λR ⇒ ∀x : set, ¬ R x x of type (setsetprop)prop.
Definition. We define symmetric to be λR ⇒ ∀x y : set, R x yR y x of type (setsetprop)prop.
Definition. We define antisymmetric to be λR ⇒ ∀x y : set, R x yR y xx = y of type (setsetprop)prop.
Definition. We define transitive to be λR ⇒ ∀x y z : set, R x yR y zR x z of type (setsetprop)prop.
Definition. We define eqreln to be λR ⇒ reflexive Rsymmetric Rtransitive R of type (setsetprop)prop.
Definition. We define per to be λR ⇒ symmetric Rtransitive R of type (setsetprop)prop.
Definition. We define linear to be λR ⇒ ∀x y : set, R x yR y x of type (setsetprop)prop.
Definition. We define trichotomous_or to be λR ⇒ ∀x y : set, R x yx = yR y x of type (setsetprop)prop.
Definition. We define partialorder to be λR ⇒ reflexive Rantisymmetric Rtransitive R of type (setsetprop)prop.
Definition. We define totalorder to be λR ⇒ partialorder Rlinear R of type (setsetprop)prop.
Definition. We define strictpartialorder to be λR ⇒ irreflexive Rtransitive R of type (setsetprop)prop.
Definition. We define stricttotalorder to be λR ⇒ strictpartialorder Rtrichotomous_or R of type (setsetprop)prop.
Axiom. (per_sym) We take the following as an axiom:
∀R : setsetprop, per Rsymmetric R
Axiom. (per_tra) We take the following as an axiom:
∀R : setsetprop, per Rtransitive R
Axiom. (per_stra1) We take the following as an axiom:
∀R : setsetprop, per R∀x y z : set, R y xR y zR x z
Axiom. (per_stra2) We take the following as an axiom:
∀R : setsetprop, per R∀x y z : set, R x yR z yR x z
Axiom. (per_stra3) We take the following as an axiom:
∀R : setsetprop, per R∀x y z : set, R y xR z yR x z
Axiom. (per_ref1) We take the following as an axiom:
∀R : setsetprop, per R∀x y : set, R x yR x x
Axiom. (per_ref2) We take the following as an axiom:
∀R : setsetprop, per R∀x y : set, R x yR y y
Axiom. (partialorder_strictpartialorder) We take the following as an axiom:
∀R : setsetprop, partialorder Rstrictpartialorder (λx y ⇒ R x yxy)
Definition. We define reflclos to be λR x y ⇒ R x yx = y of type (setsetprop)(setsetprop).
Axiom. (reflclos_refl) We take the following as an axiom:
∀R : setsetprop, reflexive (reflclos R)
Axiom. (reflclos_min) We take the following as an axiom:
∀R S : setsetprop, RSreflexive Sreflclos RS
Axiom. (strictpartialorder_partialorder_reflclos) We take the following as an axiom:
∀R : setsetprop, strictpartialorder Rpartialorder (reflclos R)
Axiom. (stricttotalorder_totalorder_reflclos) We take the following as an axiom:
∀R : setsetprop, stricttotalorder Rtotalorder (reflclos R)
Beginning of Section Zermelo1908
Primitive. The name ZermeloWO is a term of type setsetprop.
Axiom. (ZermeloWO_Eps) We take the following as an axiom:
∀a : set, (Eps_i (ZermeloWO a)) = a
Axiom. (ZermeloWO_ref) We take the following as an axiom:
Axiom. (ZermeloWO_lin) We take the following as an axiom:
Axiom. (ZermeloWO_tra) We take the following as an axiom:
Axiom. (ZermeloWO_antisym) We take the following as an axiom:
Axiom. (ZermeloWO_partialorder) We take the following as an axiom:
Axiom. (ZermeloWO_totalorder) We take the following as an axiom:
Axiom. (ZermeloWO_wo) We take the following as an axiom:
∀p : setprop, (∃x : set, p x)∃x : set, p x∀y : set, p yZermeloWO x y
Definition. We define ZermeloWOstrict to be λa b : setZermeloWO a bab.
Axiom. (ZermeloWOstrict_trich) We take the following as an axiom:
Axiom. (ZermeloWOstrict_stricttotalorder) We take the following as an axiom:
Axiom. (ZermeloWOstrict_wo) We take the following as an axiom:
∀p : setprop, (∃x : set, p x)∃x : set, p x∀y : set, p yyxZermeloWOstrict x y
Axiom. (Zermelo_WO) We take the following as an axiom:
∃r : setsetprop, totalorder r(∀p : setprop, (∃x : set, p x)∃x : set, p x∀y : set, p yr x y)
Axiom. (Zermelo_WO_strict) We take the following as an axiom:
∃r : setsetprop, stricttotalorder r(∀p : setprop, (∃x : set, p x)∃x : set, p x∀y : set, p yyxr x y)
End of Section Zermelo1908
Axiom. (eq_imp_or) We take the following as an axiom:
(λx y : prop(xy)) = (λx y : prop(¬ xy))
Axiom. (famunion_Empty) We take the following as an axiom:
∀F : setset, (x ∈ 0F x) = 0
Axiom. (Empty_or_ex) We take the following as an axiom:
∀X : set, X = Empty∃x : set, xX
Axiom. (nIn_0_0) We take the following as an axiom:
00
Axiom. (nIn_1_0) We take the following as an axiom:
10
Axiom. (nIn_2_0) We take the following as an axiom:
20
Axiom. (nIn_1_1) We take the following as an axiom:
11
Axiom. (nIn_2_2) We take the following as an axiom:
22
Axiom. (Subq_0_0) We take the following as an axiom:
00
Axiom. (Subq_0_1) We take the following as an axiom:
01
Axiom. (Subq_0_2) We take the following as an axiom:
02
Axiom. (nSubq_1_0) We take the following as an axiom:
10
Axiom. (Subq_1_1) We take the following as an axiom:
11
Axiom. (Subq_1_2) We take the following as an axiom:
12
Axiom. (nSubq_2_0) We take the following as an axiom:
20
Axiom. (nSubq_2_1) We take the following as an axiom:
21
Axiom. (Subq_2_2) We take the following as an axiom:
22
Axiom. (In_0_7) We take the following as an axiom:
07
Axiom. (In_1_7) We take the following as an axiom:
17
Axiom. (In_2_7) We take the following as an axiom:
27
Axiom. (In_3_7) We take the following as an axiom:
37
Axiom. (In_4_7) We take the following as an axiom:
47
Axiom. (In_5_7) We take the following as an axiom:
57
Axiom. (In_6_7) We take the following as an axiom:
67
Axiom. (In_0_8) We take the following as an axiom:
08
Axiom. (In_1_8) We take the following as an axiom:
18
Axiom. (In_2_8) We take the following as an axiom:
28
Axiom. (In_3_8) We take the following as an axiom:
38
Axiom. (In_4_8) We take the following as an axiom:
48
Axiom. (In_5_8) We take the following as an axiom:
58
Axiom. (In_6_8) We take the following as an axiom:
68
Axiom. (In_7_8) We take the following as an axiom:
78
Axiom. (In_0_9) We take the following as an axiom:
09
Axiom. (In_1_9) We take the following as an axiom:
19
Axiom. (In_2_9) We take the following as an axiom:
29
Axiom. (In_3_9) We take the following as an axiom:
39
Axiom. (In_4_9) We take the following as an axiom:
49
Axiom. (In_5_9) We take the following as an axiom:
59
Axiom. (In_6_9) We take the following as an axiom:
69
Axiom. (In_7_9) We take the following as an axiom:
79
Axiom. (In_8_9) We take the following as an axiom:
89
Beginning of Section NatRec
Variable z : set
Variable f : setsetset
Let F : set(setset)setλn g ⇒ if nn 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, (∀x ∈ X, 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_asso) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p m∀k : set, nat_p k(n + m) + k = n + (m + k)
Axiom. (add_nat_0L) We take the following as an axiom:
∀m : set, nat_p m0 + m = m
Axiom. (add_nat_SL) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p mordsucc n + m = ordsucc (n + m)
Axiom. (add_nat_com) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p mn + m = m + n
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)
Axiom. (mul_nat_0L) We take the following as an axiom:
∀m : set, nat_p m0 * m = 0
Axiom. (mul_nat_SL) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p mordsucc n * m = n * m + m
Axiom. (mul_nat_com) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p mn * m = m * n
Axiom. (mul_add_nat_distrL) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p m∀k : set, nat_p kn * (m + k) = n * m + n * k
Axiom. (mul_add_nat_distrR) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p m∀k : set, nat_p k(n + m) * k = n * k + m * k
Axiom. (mul_nat_asso) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p m∀k : set, nat_p k(n * m) * k = n * (m * k)
Axiom. (add_nat_1_1_2) We take the following as an axiom:
1 + 1 = 2
Definition. We define divides_nat to be λm n ⇒ mωnω∃k ∈ ω, m * k = n of type setsetprop.
Definition. We define prime_nat to be λn ⇒ nω1n∀k ∈ ω, divides_nat k nk = 1k = n of type setprop.
Definition. We define coprime_nat to be λa b ⇒ aωbω∀x ∈ ω1, divides_nat x adivides_nat x bx = 1 of type setsetprop.
Definition. We define equiv_nat_mod to be λm k n ⇒ mωkωnω((∃q ∈ ω, m + q * n = k)(∃q ∈ ω, k + q * n = m)) of type setsetsetprop.
Definition. We define exp_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_nat.
Definition. We define even_nat to be λn ⇒ nω∃m ∈ ω, n = 2 * m of type setprop.
Definition. We define odd_nat to be λn ⇒ nω∀m ∈ ω, n2 * m of type setprop.
Definition. We define nat_factorial to be λn ⇒ nat_primrec 1 (λk r ⇒ ordsucc k * r) n of type setset.
End of Section NatArith
Axiom. (PigeonHole_nat) We take the following as an axiom:
∀n, nat_p n∀f : setset, (∀i ∈ ordsucc n, f in)¬ (∀i j ∈ ordsucc n, f i = f ji = j)
Axiom. (PigeonHole_nat_bij) We take the following as an axiom:
∀n, nat_p n∀f : setset, (∀i ∈ n, f in)(∀i j ∈ n, f i = f ji = j)bij n n f
Axiom. (cases_7) We take the following as an axiom:
∀i ∈ 7, ∀p : setprop, p 0p 1p 2p 3p 4p 5p 6p i
Axiom. (cases_8) We take the following as an axiom:
∀i ∈ 8, ∀p : setprop, p 0p 1p 2p 3p 4p 5p 6p 7p i
Axiom. (cases_9) We take the following as an axiom:
∀i ∈ 9, ∀p : setprop, p 0p 1p 2p 3p 4p 5p 6p 7p 8p i
Axiom. (nIn_2_1) We take the following as an axiom:
21
Axiom. (neq_6_0) We take the following as an axiom:
60
Axiom. (neq_6_1) We take the following as an axiom:
61
Axiom. (neq_6_2) We take the following as an axiom:
62
Axiom. (neq_6_3) We take the following as an axiom:
63
Axiom. (neq_6_4) We take the following as an axiom:
64
Axiom. (neq_6_5) We take the following as an axiom:
65
Axiom. (neq_7_0) We take the following as an axiom:
70
Axiom. (neq_7_1) We take the following as an axiom:
71
Axiom. (neq_7_2) We take the following as an axiom:
72
Axiom. (neq_7_3) We take the following as an axiom:
73
Axiom. (neq_7_4) We take the following as an axiom:
74
Axiom. (neq_7_5) We take the following as an axiom:
75
Axiom. (neq_7_6) We take the following as an axiom:
76
Axiom. (neq_8_0) We take the following as an axiom:
80
Axiom. (neq_8_1) We take the following as an axiom:
81
Axiom. (neq_8_2) We take the following as an axiom:
82
Axiom. (neq_8_3) We take the following as an axiom:
83
Axiom. (neq_8_4) We take the following as an axiom:
84
Axiom. (neq_8_5) We take the following as an axiom:
85
Axiom. (neq_8_6) We take the following as an axiom:
86
Axiom. (neq_8_7) We take the following as an axiom:
87
Axiom. (neq_9_0) We take the following as an axiom:
90
Axiom. (neq_9_1) We take the following as an axiom:
91
Axiom. (neq_9_2) We take the following as an axiom:
92
Axiom. (neq_9_3) We take the following as an axiom:
93
Axiom. (neq_9_4) We take the following as an axiom:
94
Axiom. (neq_9_5) We take the following as an axiom:
95
Axiom. (neq_9_6) We take the following as an axiom:
96
Axiom. (neq_9_7) We take the following as an axiom:
97
Axiom. (neq_9_8) We take the following as an axiom:
98
Axiom. (Subq_1_Sing0) We take the following as an axiom:
1{0}
Axiom. (Subq_Sing0_1) We take the following as an axiom:
{0}1
Axiom. (eq_1_Sing0) We take the following as an axiom:
1 = {0}
Axiom. (Subq_2_UPair01) We take the following as an axiom:
2{0,1}
Axiom. (Subq_UPair01_2) We take the following as an axiom:
{0,1}2
Axiom. (eq_2_UPair01) We take the following as an axiom:
2 = {0,1}
Axiom. (ordinal_ind) We take the following as an axiom:
∀p : setprop, (∀alpha, ordinal alpha(∀beta ∈ alpha, p beta)p alpha)∀alpha, ordinal alphap alpha
Axiom. (least_ordinal_ex) We take the following as an axiom:
∀p : setprop, (∃alpha, ordinal alphap alpha)∃alpha, ordinal alphap alpha∀beta ∈ alpha, ¬ p beta
Axiom. (ordinal_trichotomy_or_impred) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p : prop, (alphabetap)(alpha = betap)(betaalphap)p
Axiom. (ordinal_trichotomy) We take the following as an axiom:
∀alpha beta : set, ordinal alphaordinal betaexactly1of3 (alphabeta) (alpha = beta) (betaalpha)
Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0}{f x|x ∈ X}) of type setset.
Axiom. (Inj1_eq) We take the following as an axiom:
∀X : set, Inj1 X = {0}{Inj1 x|x ∈ X}
Axiom. (Inj1I1) We take the following as an axiom:
∀X : set, 0Inj1 X
Axiom. (Inj1I2) We take the following as an axiom:
∀X x : set, xXInj1 xInj1 X
Axiom. (Inj1E) We take the following as an axiom:
∀X y : set, yInj1 Xy = 0∃x ∈ X, y = Inj1 x
Axiom. (Inj1NE1) We take the following as an axiom:
∀x : set, Inj1 x0
Axiom. (Inj1NE2) We take the following as an axiom:
∀x : set, Inj1 x{0}
Definition. We define Inj0 to be λX ⇒ {Inj1 x|x ∈ X} of type setset.
Axiom. (Inj0I) We take the following as an axiom:
∀X x : set, xXInj1 xInj0 X
Axiom. (Inj0E) We take the following as an axiom:
∀X y : set, yInj0 X∃x : set, xXy = Inj1 x
Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|x ∈ X{0}}) of type setset.
Axiom. (Unj_eq) We take the following as an axiom:
∀X : set, Unj X = {Unj x|x ∈ X{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 XInj1 Y
Definition. We define setsum to be λX Y ⇒ {Inj0 x|x ∈ X}{Inj1 y|y ∈ Y} 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, xXInj0 xX + Y
Axiom. (Inj1_setsum) We take the following as an axiom:
∀X Y y : set, yYInj1 yX + Y
Axiom. (setsum_Inj_inv) We take the following as an axiom:
∀X Y z : set, zX + Y(∃x ∈ X, z = Inj0 x)(∃y ∈ Y, z = Inj1 y)
Axiom. (Inj0_setsum_0L) We take the following as an axiom:
∀X : set, 0 + X = Inj0 X
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
Axiom. (setsum_mon) We take the following as an axiom:
∀X Y W Z, XWYZX + YW + Z
Definition. We define combine_funcs to be λX Y f g z ⇒ if z = Inj0 (Unj z) then f (Unj z) else g (Unj z) of type setset(setset)(setset)setset.
Axiom. (combine_funcs_eq1) We take the following as an axiom:
∀X Y, ∀f g : setset, ∀x, combine_funcs X Y f g (Inj0 x) = f x
Axiom. (combine_funcs_eq2) We take the following as an axiom:
∀X Y, ∀f g : setset, ∀y, combine_funcs X Y f g (Inj1 y) = g y
Beginning of Section pair_setsum
Let pair ≝ setsum
Axiom. (pair_0_0) We take the following as an axiom:
pair 0 0 = 0
Axiom. (pair_1_0_1) We take the following as an axiom:
pair 1 0 = 1
Axiom. (pair_1_1_2) We take the following as an axiom:
pair 1 1 = 2
Axiom. (nat_pair1_ordsucc) We take the following as an axiom:
∀n : set, nat_p npair 1 n = ordsucc n
Definition. We define proj0 to be λZ ⇒ {Unj z|z ∈ Z, ∃x : set, Inj0 x = z} of type setset.
Definition. We define proj1 to be λZ ⇒ {Unj z|z ∈ Z, ∃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, xXpair 0 xpair X Y
Axiom. (pairI1) We take the following as an axiom:
∀X Y y, yYpair 1 ypair X Y
Axiom. (pairE) We take the following as an axiom:
∀X Y z, zpair X Y(∃x ∈ X, z = pair 0 x)(∃y ∈ Y, z = pair 1 y)
Axiom. (pairE0) We take the following as an axiom:
∀X Y x, pair 0 xpair X YxX
Axiom. (pairE1) We take the following as an axiom:
∀X Y y, pair 1 ypair X YyY
Axiom. (pairEq) We take the following as an axiom:
∀X Y z, zpair X Y(∃x ∈ X, z = pair 0 x)(∃y ∈ Y, z = pair 1 y)
Axiom. (pairSubq) We take the following as an axiom:
∀X Y W Z, XWYZpair X Ypair W Z
Axiom. (proj0I) We take the following as an axiom:
∀w u : set, pair 0 uwuproj0 w
Axiom. (proj0E) We take the following as an axiom:
∀w u : set, uproj0 wpair 0 uw
Axiom. (proj1I) We take the following as an axiom:
∀w u : set, pair 1 uwuproj1 w
Axiom. (proj1E) We take the following as an axiom:
∀w u : set, uproj1 wpair 1 uw
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
Axiom. (pair_inj) We take the following as an axiom:
∀x y w z : set, pair x y = pair w zx = wy = z
Axiom. (pair_eta_Subq_proj) We take the following as an axiom:
∀w, pair (proj0 w) (proj1 w)w
Definition. We define Sigma to be λX Y ⇒ x ∈ X{pair x y|y ∈ 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 Sigma.
Axiom. (pair_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀x ∈ X, ∀y ∈ Y x, pair x y∑x ∈ X, Y x
Axiom. (Sigma_eta_proj0_proj1) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = zproj0 zXproj1 zY (proj0 z)
Axiom. (proj_Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z ∈ (∑x ∈ X, 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(∑x ∈ X, Y x)proj0 zX
Axiom. (proj1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z(∑x ∈ X, Y x)proj1 zY (proj0 z)
Axiom. (pair_Sigma_E0) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀x y : set, pair x y(∑x ∈ X, Y x)xX
Axiom. (pair_Sigma_E1) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀x y : set, pair x y(∑x ∈ X, Y x)yY x
Axiom. (Sigma_E) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z(∑x ∈ X, Y x)∃x ∈ X, ∃y ∈ Y x, z = pair x y
Axiom. (Sigma_Eq) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z(∑x ∈ X, Y x)∃x ∈ X, ∃y ∈ Y x, z = pair x y
Axiom. (Sigma_mon) We take the following as an axiom:
∀X Y : set, XY∀Z W : setset, (∀x ∈ X, Z xW x)(∑x ∈ X, Z x)∑y ∈ Y, W y
Axiom. (Sigma_mon0) We take the following as an axiom:
∀X Y : set, XY∀Z : setset, (∑x ∈ X, Z x)∑y ∈ Y, Z y
Axiom. (Sigma_mon1) We take the following as an axiom:
∀X : set, ∀Z W : setset, (∀x, xXZ xW x)(∑x ∈ X, Z x)∑x ∈ X, W x
Axiom. (Sigma_Power_1) We take the following as an axiom:
∀X : set, X𝒫 1∀Y : setset, (∀x ∈ X, Y x𝒫 1)(∑x ∈ X, Y x)𝒫 1
Definition. We define setprod to be λX Y : set∑x ∈ X, 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.
Axiom. (pair_setprod) We take the following as an axiom:
∀X Y : set, ∀(x ∈ X)(y ∈ Y), pair x yXY
Axiom. (proj0_setprod) We take the following as an axiom:
∀X Y : set, ∀z ∈ XY, proj0 zX
Axiom. (proj1_setprod) We take the following as an axiom:
∀X Y : set, ∀z ∈ XY, proj1 zY
Axiom. (pair_setprod_E0) We take the following as an axiom:
∀X Y x y : set, pair x yXYxX
Axiom. (pair_setprod_E1) We take the following as an axiom:
∀X Y x y : set, pair x yXYyY
Let lam : set(setset)setSigma
Definition. We define ap to be λf x ⇒ {proj1 z|z ∈ f, ∃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).
Axiom. (lamI) We take the following as an axiom:
∀X : set, ∀F : setset, ∀x ∈ X, ∀y ∈ F x, pair x yλx ∈ XF x
Axiom. (lamE) We take the following as an axiom:
∀X : set, ∀F : setset, ∀z : set, z(λx ∈ XF x)∃x ∈ X, ∃y ∈ F x, z = pair x y
Axiom. (lamEq) We take the following as an axiom:
∀X : set, ∀F : setset, ∀z, z(λx ∈ XF x)∃x ∈ X, ∃y ∈ F x, z = pair x y
Axiom. (apI) We take the following as an axiom:
∀f x y, pair x yfyf x
Axiom. (apE) We take the following as an axiom:
∀f x y, yf xpair x yf
Axiom. (apEq) We take the following as an axiom:
∀f x y, yf xpair x yf
Axiom. (beta) We take the following as an axiom:
∀X : set, ∀F : setset, ∀x : set, xX(λx ∈ XF x) x = F x
Axiom. (beta0) We take the following as an axiom:
∀X : set, ∀F : setset, ∀x : set, xX(λx ∈ XF x) x = 0
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. (pair_ap_n2) We take the following as an axiom:
∀x y i : set, i2(pair x y) i = 0
Axiom. (ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z(∑x ∈ X, Y x)(z 0)X
Axiom. (ap1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z(∑x ∈ X, 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. (pair_p_I2) We take the following as an axiom:
∀w, (∀u ∈ w, pair_p uu 02)pair_p w
Axiom. (pair_p_In_ap) We take the following as an axiom:
∀w f, pair_p wwfw 1ap f (w 0)
Definition. We define tuple_p to be λn u ⇒ ∀z ∈ u, ∃i ∈ n, ∃x : set, z = pair i x of type setsetprop.
Axiom. (pair_p_tuple2) We take the following as an axiom:
Axiom. (tuple_p_2_tuple) We take the following as an axiom:
∀x y : set, tuple_p 2 (x,y)
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 ∈ 𝒫 (∑x ∈ X, (Y x))|∀x ∈ X, f xY 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, (∀u ∈ f, pair_p uu 0X)(∀x ∈ X, f xY x)f∏x ∈ X, Y x
Axiom. (PiE) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, f(∏x ∈ X, Y x)(∀u ∈ f, pair_p uu 0X)(∀x ∈ X, f xY x)
Axiom. (PiEq) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, fPi X Y(∀u ∈ f, pair_p uu 0X)(∀x ∈ X, f xY x)
Axiom. (lam_Pi) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀F : setset, (∀x ∈ X, F xY x)(λx ∈ XF x)(∏x ∈ X, Y x)
Axiom. (ap_Pi) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, ∀x : set, f(∏x ∈ X, Y x)xXf xY x
Axiom. (Pi_ext_Subq) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f g ∈ (∏x ∈ X, Y x), (∀x ∈ X, f xg x)fg
Axiom. (Pi_ext) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f g ∈ (∏x ∈ X, Y x), (∀x ∈ X, f x = g x)f = g
Axiom. (Pi_eta) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, f(∏x ∈ X, Y x)(λx ∈ Xf x) = f
Definition. We define setexp to be λX Y : set∏y ∈ Y, 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, ∀x ∈ X, ∀y ∈ F x, (x,y)λx ∈ XF x
Axiom. (lamE2) We take the following as an axiom:
∀X, ∀F : setset, ∀z : set, z(λx ∈ XF x)∃x ∈ X, ∃y ∈ F x, z = (x,y)
Axiom. (tuple_2_inj) We take the following as an axiom:
∀x y w z : set, (x,y) = (w,z)x = wy = z
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
Definition. We define Sep2 to be λX Y R ⇒ {u ∈ ∑x ∈ X, Y x|R (u 0) (u 1)} of type set(setset)(setsetprop)set.
Axiom. (Sep2I) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀x ∈ X, ∀y ∈ Y x, R x y(x,y)Sep2 X Y R
Axiom. (Sep2E) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀u ∈ Sep2 X Y R, ∃x ∈ X, ∃y ∈ Y x, u = (x,y)R x y
Axiom. (Sep2E') We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀x y, (x,y)Sep2 X Y RxXyY xR x y
Axiom. (Sep2E'1) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀x y, (x,y)Sep2 X Y RxX
Axiom. (Sep2E'2) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀x y, (x,y)Sep2 X Y RyY x
Axiom. (Sep2E'3) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀x y, (x,y)Sep2 X Y RR x y
Definition. We define set_of_pairs to be λX ⇒ ∀x ∈ X, ∃y z, x = (y,z) of type setprop.
Axiom. (set_of_pairs_ext) We take the following as an axiom:
∀X Y, set_of_pairs Xset_of_pairs Y(∀v w, (v,w)X(v,w)Y)X = Y
Axiom. (Sep2_set_of_pairs) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, set_of_pairs (Sep2 X Y R)
Axiom. (Sep2_ext) We take the following as an axiom:
∀X, ∀Y : setset, ∀R R' : setsetprop, (∀x ∈ X, ∀y ∈ Y x, R x yR' x y)Sep2 X Y R = Sep2 X Y R'
Axiom. (lam_ext_sub) We take the following as an axiom:
∀X, ∀F G : setset, (∀x ∈ X, F x = G x)(λx ∈ XF x)(λx ∈ XG x)
Axiom. (lam_ext) We take the following as an axiom:
∀X, ∀F G : setset, (∀x ∈ X, F x = G x)(λx ∈ XF x) = (λx ∈ XG x)
Axiom. (lam_eta) We take the following as an axiom:
∀X, ∀F : setset, (λx ∈ X(λx ∈ XF x) x) = (λx ∈ XF x)
Axiom. (tuple_2_eta) We take the following as an axiom:
∀x y, (λi ∈ 2(x,y) i) = (x,y)
Definition. We define lam2 to be λX Y F ⇒ λx ∈ Xλy ∈ Y xF x y of type set(setset)(setsetset)set.
Axiom. (beta2) We take the following as an axiom:
∀X, ∀Y : setset, ∀F : setsetset, ∀x ∈ X, ∀y ∈ Y x, lam2 X Y F x y = F x y
Axiom. (lam2_ext) We take the following as an axiom:
∀X, ∀Y : setset, ∀F G : setsetset, (∀x ∈ X, ∀y ∈ Y x, F x y = G x y)lam2 X Y F = lam2 X Y G
Definition. We define encode_u to be lam of type set(setset)set.
Definition. We define decode_u to be ap of type setsetset.
Definition. We define encode_b to be λX F ⇒ lam2 X (λ_ ⇒ X) F of type set(setsetset)set.
Definition. We define decode_b to be λF x y ⇒ F x y of type setsetsetset.
Definition. We define encode_p to be λX P ⇒ Sep X P of type set(setprop)set.
Definition. We define decode_p to be λP x ⇒ xP of type setsetprop.
Definition. We define encode_r to be λX R ⇒ Sep2 X (λ_ ⇒ X) R of type set(setsetprop)set.
Definition. We define decode_r to be λR x y ⇒ (x,y)R of type setsetsetprop.
Definition. We define encode_c to be λX C ⇒ Sep (𝒫 X) (λU ⇒ (C (λx ⇒ xU))) of type set((setprop)prop)set.
Definition. We define decode_c to be λC U ⇒ ∃V, (∀x, U xxV)VC of type set(setprop)prop.
Axiom. (decode_encode_u) We take the following as an axiom:
∀X, ∀F : setset, ∀x ∈ X, decode_u (encode_u X F) x = F x
Axiom. (encode_u_ext) We take the following as an axiom:
∀X, ∀F F' : setset, (∀x ∈ X, F x = F' x)encode_u X F = encode_u X F'
Axiom. (decode_encode_b) We take the following as an axiom:
∀X, ∀F : setsetset, ∀x y ∈ X, decode_b (encode_b X F) x y = F x y
Axiom. (encode_b_ext) We take the following as an axiom:
∀X, ∀F F' : setsetset, (∀x y ∈ X, F x y = F' x y)encode_b X F = encode_b X F'
Axiom. (decode_encode_p) We take the following as an axiom:
∀X, ∀P : setprop, ∀x ∈ X, (decode_p (encode_p X P) x) = (P x)
Axiom. (encode_p_ext) We take the following as an axiom:
∀X, ∀P P' : setprop, (∀x ∈ X, P xP' x)encode_p X P = encode_p X P'
Axiom. (decode_encode_r) We take the following as an axiom:
∀X, ∀R : setsetprop, ∀x y ∈ X, (decode_r (encode_r X R) x y) = (R x y)
Axiom. (encode_r_ext) We take the following as an axiom:
∀X, ∀R R' : setsetprop, (∀x y ∈ X, R x yR' x y)encode_r X R = encode_r X R'
Axiom. (decode_encode_c) We take the following as an axiom:
∀X, ∀C : (setprop)prop, ∀U : setprop, (∀x, U xxX)(decode_c (encode_c X C) U) = (C U)
Axiom. (encode_c_ext) We take the following as an axiom:
∀X, ∀C C' : (setprop)prop, (∀U : setprop, (∀x, U xxX)(C UC' U))encode_c X C = encode_c X C'
Axiom. (setprod_mon) We take the following as an axiom:
∀X Y : set, XY∀Z W : set, ZWXZYW
Axiom. (setprod_mon0) We take the following as an axiom:
∀X Y : set, XY∀Z : set, XZYZ
Axiom. (setprod_mon1) We take the following as an axiom:
∀X : set, ∀Z W : set, ZWXZXW
Axiom. (pair_eta_Subq) We take the following as an axiom:
∀w, pair (w 0) (w 1)w
Axiom. (Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z ∈ (∑x ∈ X, Y x), pair (z 0) (z 1) = z
Axiom. (ReplEq_setprod_ext) We take the following as an axiom:
∀X Y, ∀F G : setsetset, (∀x ∈ X, ∀y ∈ Y, F x y = G x y){F (w 0) (w 1)|w ∈ XY} = {G (w 0) (w 1)|w ∈ XY}
Axiom. (tuple_p_3_tuple) We take the following as an axiom:
∀x y z : set, tuple_p 3 (x,y,z)
Axiom. (tuple_p_4_tuple) We take the following as an axiom:
∀x y z w : set, tuple_p 4 (x,y,z,w)
Axiom. (Pi_Power_1) We take the following as an axiom:
∀X : set, ∀Y : setset, (∀x ∈ X, Y x𝒫 1)(∏x ∈ X, Y x)𝒫 1
Axiom. (Pi_0_dom_mon) We take the following as an axiom:
∀X Y : set, ∀A : setset, XY(∀y ∈ Y, yX0A y)(∏x ∈ X, A x)∏y ∈ Y, A y
Axiom. (Pi_cod_mon) We take the following as an axiom:
∀X : set, ∀A B : setset, (∀x ∈ X, A xB x)(∏x ∈ X, A x)∏x ∈ X, B x
Axiom. (Pi_0_mon) We take the following as an axiom:
∀X Y : set, ∀A B : setset, (∀x ∈ X, A xB x)XY(∀y ∈ Y, yX0B y)(∏x ∈ X, A x)∏y ∈ Y, B y
Axiom. (setexp_2_eq) We take the following as an axiom:
∀X : set, XX = X2
Axiom. (setexp_0_dom_mon) We take the following as an axiom:
∀A : set, 0A∀X Y : set, XYAXAY
Axiom. (setexp_0_mon) We take the following as an axiom:
∀X Y A B : set, 0BABXYAXBY
Axiom. (nat_in_setexp_mon) We take the following as an axiom:
∀A : set, 0A∀n, nat_p n∀m ∈ n, AmAn
Axiom. (tupleI0) We take the following as an axiom:
∀X Y x, xX(0,x)(X,Y)
Axiom. (tupleI1) We take the following as an axiom:
∀X Y y, yY(1,y)(X,Y)
Axiom. (tupleE) We take the following as an axiom:
∀X Y z, z(X,Y)(∃x ∈ X, z = (0,x))(∃y ∈ Y, z = (1,y))
Axiom. (tuple_2_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀x ∈ X, ∀y ∈ Y x, (x,y)∑x ∈ X, Y x
Axiom. (tuple_2_setprod) We take the following as an axiom:
∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y)XY
Axiom. (tuple_Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z ∈ (∑x ∈ X, Y x), (z 0,z 1) = z
Axiom. (apI2) We take the following as an axiom:
∀f x y, (x,y)fyf x
Axiom. (apE2) We take the following as an axiom:
∀f x y, yf x(x,y)f
Axiom. (ap_const_0) We take the following as an axiom:
∀x, 0 x = 0
Axiom. (tuple_2_in_A_2) We take the following as an axiom:
∀x y A, xAyA(x,y)A2
Axiom. (tuple_2_bij_2) We take the following as an axiom:
∀x y, x2y2xybij 2 2 (λi ⇒ (x,y) i)
Axiom. (tuple_3_eta) We take the following as an axiom:
∀x y z, (λi ∈ 3(x,y,z) i) = (x,y,z)
Axiom. (tuple_4_eta) We take the following as an axiom:
∀x y z w, (λi ∈ 4(x,y,z,w) i) = (x,y,z,w)
Beginning of Section Tuples
Variable x0 x1 x2 : set
Axiom. (tuple_3_0_eq) We take the following as an axiom:
(x0,x1,x2) 0 = x0
Axiom. (tuple_3_1_eq) We take the following as an axiom:
(x0,x1,x2) 1 = x1
Axiom. (tuple_3_2_eq) We take the following as an axiom:
(x0,x1,x2) 2 = x2
Variable x3 : set
Axiom. (tuple_4_0_eq) We take the following as an axiom:
(x0,x1,x2,x3) 0 = x0
Axiom. (tuple_4_1_eq) We take the following as an axiom:
(x0,x1,x2,x3) 1 = x1
Axiom. (tuple_4_2_eq) We take the following as an axiom:
(x0,x1,x2,x3) 2 = x2
Axiom. (tuple_4_3_eq) We take the following as an axiom:
(x0,x1,x2,x3) 3 = x3
Variable x4 : set
Axiom. (tuple_5_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4) 0 = x0
Axiom. (tuple_5_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4) 1 = x1
Axiom. (tuple_5_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4) 2 = x2
Axiom. (tuple_5_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4) 3 = x3
Axiom. (tuple_5_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4) 4 = x4
Variable x5 : set
Axiom. (tuple_6_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 0 = x0
Axiom. (tuple_6_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 1 = x1
Axiom. (tuple_6_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 2 = x2
Axiom. (tuple_6_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 3 = x3
Axiom. (tuple_6_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 4 = x4
Axiom. (tuple_6_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 5 = x5
Variable x6 : set
Axiom. (tuple_7_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 0 = x0
Axiom. (tuple_7_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 1 = x1
Axiom. (tuple_7_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 2 = x2
Axiom. (tuple_7_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 3 = x3
Axiom. (tuple_7_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 4 = x4
Axiom. (tuple_7_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 5 = x5
Axiom. (tuple_7_6_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 6 = x6
Variable x7 : set
Axiom. (tuple_8_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 0 = x0
Axiom. (tuple_8_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 1 = x1
Axiom. (tuple_8_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 2 = x2
Axiom. (tuple_8_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 3 = x3
Axiom. (tuple_8_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 4 = x4
Axiom. (tuple_8_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 5 = x5
Axiom. (tuple_8_6_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 6 = x6
Axiom. (tuple_8_7_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 7 = x7
Variable x8 : set
Axiom. (tuple_9_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 0 = x0
Axiom. (tuple_9_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 1 = x1
Axiom. (tuple_9_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 2 = x2
Axiom. (tuple_9_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 3 = x3
Axiom. (tuple_9_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 4 = x4
Axiom. (tuple_9_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 5 = x5
Axiom. (tuple_9_6_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 6 = x6
Axiom. (tuple_9_7_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 7 = x7
Axiom. (tuple_9_8_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 8 = x8
End of Section Tuples
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.
Axiom. (tuple_3_in_A_3) We take the following as an axiom:
∀x y z A, xAyAzA(x,y,z)A3
Axiom. (tuple_3_bij_3) We take the following as an axiom:
∀x y z, x3y3z3xyxzyzbij 3 3 (λi ⇒ (x,y,z) i)
Axiom. (tuple_4_in_A_4) We take the following as an axiom:
∀x y z w A, xAyAzAwA(x,y,z,w)A4
Axiom. (tuple_4_bij_4) We take the following as an axiom:
∀x y z w, x4y4z4w4xyxzxwyzywzwbij 4 4 (λi ⇒ (x,y,z,w) i)
Axiom. (iff_refl) We take the following as an axiom:
∀A : prop, AA
Axiom. (iff_sym) We take the following as an axiom:
∀A B : prop, (AB)(BA)
Axiom. (iff_trans) We take the following as an axiom:
∀A B C : prop, (AB)(BC)(AC)
Axiom. (not_or_and_demorgan) We take the following as an axiom:
∀A B : prop, ¬ (AB)¬ A¬ B
Axiom. (and_not_or_demorgan) We take the following as an axiom:
∀A B : prop, ¬ A¬ B¬ (AB)
Axiom. (not_ex_all_demorgan_i) We take the following as an axiom:
∀P : setprop, (¬ ∃x, P x)∀x, ¬ P x
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 EpsR_i_i_1 is a term of type (setsetprop)set.
Primitive. The name EpsR_i_i_2 is a term of type (setsetprop)set.
Axiom. (EpsR_i_i_12) We take the following as an axiom:
∀R : setsetprop, (∃x y, R x y)R (EpsR_i_i_1 R) (EpsR_i_i_2 R)
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 ⇒ ∀beta ∈ alpha, p betaq 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∀beta ∈ alpha, PNoEq_ alpha p qPNoEq_ beta p q
Definition. We define PNoLt_ to be λalpha p q ⇒ ∃beta ∈ alpha, PNoEq_ beta p q¬ p betaq 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, betaalphaPNoEq_ 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∀beta ∈ alpha, 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 qPNoEq_ alpha p qPNoLt_ 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_ (alphabeta) p qPNoLt alpha p beta q
Axiom. (PNoLtI2) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, alphabetaPNoEq_ alpha p qq alphaPNoLt alpha p beta q
Axiom. (PNoLtI3) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, betaalphaPNoEq_ 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_ (alphabeta) p qR)(alphabetaPNoEq_ alpha p qq alphaR)(betaalphaPNoEq_ beta p q¬ p betaR)R
Axiom. (PNoLtE2) We take the following as an axiom:
∀alpha, ∀p q : setprop, PNoLt alpha p alpha qPNoLt_ alpha p q
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 qalpha = betaPNoEq_ alpha p qPNoLt 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 qalpha = betaPNoEq_ 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 = betaPNoEq_ 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. (PNoLeEq_tra) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoLe alpha p beta qPNoEq_ beta q 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 qPNoLe 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 qPNoLe 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 ⇒ ∀beta ∈ alpha, ∀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 ⇒ ∀beta ∈ alpha, ∀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 pPNo_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, ∀beta ∈ alpha, 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, ∀beta ∈ alpha, 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, ∀beta ∈ alpha, 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 deltadeltaalpha)PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p deltadelta = 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 deltadeltaalpha)
Axiom. (PNo_extend1_eq) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoEq_ alpha p (λdelta ⇒ p deltadelta = 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)(∃tau ∈ alpha, ∃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 pbetaalpha 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 deltadeltaalpha)
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 deltadelta = 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∃beta ∈ ordsucc 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 pPNo_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∀beta ∈ ordsucc 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∀beta ∈ ordsucc 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∀beta ∈ ordsucc 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. (ordinal_PNo_strict_imv) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, (∀beta ∈ alpha, p beta)(∀beta, ordinal beta∀q : setprop, L beta qbetaalpha)(∀beta ∈ alpha, L beta p)(∀beta, ordinal beta∀q : setprop, ¬ R beta q)PNo_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∃beta ∈ ordsucc alpha, ∃p : setprop, PNo_strict_imv L R beta p
Definition. We define PNo_least_rep to be λL R beta p ⇒ ordinal betaPNo_strict_imv L R beta p∀gamma ∈ beta, ∀q : setprop, ¬ PNo_strict_imv L R gamma q of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Axiom. (PNo_lenbdd_least_rep_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∃beta, ∃p : setprop, PNo_least_rep L R beta p
Definition. We define PNo_least_rep2 to be λL R beta p ⇒ PNo_least_rep L R beta p∀x, xbeta¬ 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∀beta ∈ alpha, p betaq 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_ord) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha Rordinal (PNo_bd L R)
Axiom. (PNo_bd_pred_strict_imv) 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_strict_imv L R (PNo_bd L R) (PNo_pred L R)
Axiom. (PNo_bd_least_imv) 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∀gamma ∈ PNo_bd L R, ∀q : setprop, ¬ PNo_strict_imv L R gamma q
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 Rordsucc alpha
Definition. We define PNoCutL to be λalpha p beta q ⇒ betaalphaPNoLt beta q alpha p of type set(setprop)set(setprop)prop.
Definition. We define PNoCutR to be λalpha p beta q ⇒ betaalphaPNoLt alpha p beta q of type set(setprop)set(setprop)prop.
Axiom. (PNoCutL_lenbdd) We take the following as an axiom:
∀alpha, ∀p : setprop, PNo_lenbdd alpha (PNoCutL alpha p)
Axiom. (PNoCutR_lenbdd) We take the following as an axiom:
∀alpha, ∀p : setprop, PNo_lenbdd alpha (PNoCutR alpha p)
Axiom. (PNoCut_pwise) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, PNoLt_pwise (PNoCutL alpha p) (PNoCutR alpha p)
Axiom. (PNoCut_strict_imv) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, PNo_strict_imv (PNoCutL alpha p) (PNoCutR alpha p) alpha p
Axiom. (PNoCut_bd_eq) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, PNo_bd (PNoCutL alpha p) (PNoCutR alpha p) = alpha
Axiom. (PNoCut_pred_eq) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, PNoEq_ alpha p (PNo_pred (PNoCutL alpha p) (PNoCutR alpha p))
Beginning of Section TaggedSets
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Axiom. (not_TransSet_Sing1) We take the following as an axiom:
¬ TransSet {1}
Axiom. (not_ordinal_Sing1) We take the following as an axiom:
¬ ordinal {1}
Axiom. (tagged_not_ordinal) We take the following as an axiom:
∀y, ¬ ordinal (y ')
Axiom. (tagged_notin_ordinal) We take the following as an axiom:
∀alpha y, ordinal alpha(y ')alpha
Axiom. (tagged_eqE_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaalpha ' = beta 'alphabeta
Axiom. (tagged_eqE_eq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha ' = beta 'alpha = beta
Axiom. (tagged_ReplE) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betabeta '{gamma '|gamma ∈ alpha}betaalpha
Axiom. (ordinal_notin_tagged_Repl) We take the following as an axiom:
∀alpha Y, ordinal alphaalpha{y '|y ∈ Y}
Definition. We define SNoElts_ to be λalpha ⇒ alpha{beta '|beta ∈ alpha} of type setset.
Axiom. (SNoElts_mon) We take the following as an axiom:
∀alpha beta, alphabetaSNoElts_ alphaSNoElts_ beta
Definition. We define SNo_ to be λalpha x ⇒ xSNoElts_ alpha∀beta ∈ alpha, exactly1of2 (beta 'x) (betax) of type setsetprop.
Definition. We define PSNo to be λalpha p ⇒ {beta ∈ alpha|p beta}{beta '|beta ∈ alpha, ¬ p beta} of type set(setprop)set.
Axiom. (PNoEq_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, PNoEq_ alpha (λbeta ⇒ betaPSNo 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 ⇒ betax)
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 xalphabeta
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 ⇒ betax)
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 xSNoLev y(∀alpha ∈ SNoLev x, alphaxalphay)xy
Definition. We define SNoEq_ to be λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ betax) (λbeta ⇒ betay) of type setsetsetprop.
Axiom. (SNoEq_I) We take the following as an axiom:
∀alpha x y, (∀beta ∈ alpha, betaxbetay)SNoEq_ alpha x y
Axiom. (SNoEq_E) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x y∀beta ∈ alpha, betaxbetay
Axiom. (SNoEq_E1) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x y∀beta ∈ alpha, betaxbetay
Axiom. (SNoEq_E2) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x y∀beta ∈ alpha, betaybetax
Axiom. (SNoEq_antimon_) We take the following as an axiom:
∀alpha, ordinal alpha∀beta ∈ alpha, ∀x y, SNoEq_ alpha x ySNoEq_ beta 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
Let ctag : setsetλalpha ⇒ SetAdjoin alpha {2}
Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.
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:
{2}{{1}}
Axiom. (ctagged_notin_SNo) We take the following as an axiom:
∀x y, SNo x(y '')x
Axiom. (ctagged_eqE_eq) We take the following as an axiom:
∀x y, SNo xSNo y∀u ∈ x, ∀v ∈ y, u '' = v ''u = v
Definition. We define SNo_pair to be λx y ⇒ x{u ''|u ∈ y} of type setsetset.
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) 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_prop) We take the following as an axiom:
∀x1 y1 x2 y2, SNo x1SNo y1SNo x2SNo y2SNo_pair x1 y1 = SNo_pair x2 y2x1 = x2y1 = y2
Axiom. (SNo_pair_0) We take the following as an axiom:
∀x, SNo_pair x 0 = x
End of Section TaggedSets
Definition. We define SNoLt to be λx y ⇒ PNoLt (SNoLev x) (λbeta ⇒ betax) (SNoLev y) (λbeta ⇒ betay) 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 ⇒ betax) (SNoLev y) (λbeta ⇒ betay) 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 < yxy
Axiom. (SNoLeE) We take the following as an axiom:
∀x y, SNo xSNo yxyx < yx = y
Axiom. (SNoEq_ref_) We take the following as an axiom:
∀alpha x, SNoEq_ alpha x x
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 zSNoLev xSNoLev ySNoEq_ (SNoLev z) z xSNoEq_ (SNoLev z) z yx < zz < ySNoLev zxSNoLev zyp)(SNoLev xSNoLev ySNoEq_ (SNoLev x) x ySNoLev xyp)(SNoLev ySNoLev xSNoEq_ (SNoLev y) x ySNoLev yxp)p
Axiom. (SNoLtI2) We take the following as an axiom:
∀x y, SNoLev xSNoLev ySNoEq_ (SNoLev x) x ySNoLev xyx < y
Axiom. (SNoLtI3) We take the following as an axiom:
∀x y, SNoLev ySNoLev xSNoEq_ (SNoLev y) x ySNoLev yxx < y
Axiom. (SNoLt_irref) We take the following as an axiom:
∀x, ¬ SNoLt x x
Axiom. (SNoLt_trichotomy_or) We take the following as an axiom:
∀x y, SNo xSNo yx < yx = yy < x
Axiom. (SNoLt_trichotomy_or_impred) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (x < yp)(x = yp)(y < xp)p
Axiom. (SNoLt_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < yy < zx < z
Axiom. (SNoLe_ref) We take the following as an axiom:
∀x, SNoLe x x
Axiom. (SNoLe_antisym) We take the following as an axiom:
∀x y, SNo xSNo yxyyxx = y
Axiom. (SNoLtLe_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < yyzx < z
Axiom. (SNoLeLt_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zxyy < zx < z
Axiom. (SNoLe_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zxyyzxz
Axiom. (SNoLtLe_or) We take the following as an axiom:
∀x y, SNo xSNo yx < yyx
Axiom. (SNoLt_PSNo_PNoLt) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPSNo alpha p < PSNo beta qPNoLt alpha p beta q
Axiom. (PNoLt_SNoLt_PSNo) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNoLt alpha p beta qPSNo alpha p < PSNo beta q
Definition. We define SNoCut to be λL R ⇒ PSNo (PNo_bd (λalpha p ⇒ ordinal alphaPSNo alpha pL) (λalpha p ⇒ ordinal alphaPSNo alpha pR)) (PNo_pred (λalpha p ⇒ ordinal alphaPSNo alpha pL) (λalpha p ⇒ ordinal alphaPSNo alpha pR)) of type setsetset.
Definition. We define SNoCutP to be λL R ⇒ (∀x ∈ L, SNo x)(∀y ∈ R, SNo y)(∀x ∈ L, ∀y ∈ R, x < y) of type setsetprop.
Axiom. (SNoCutP_SNoCut) We take the following as an axiom:
∀L R, SNoCutP L RSNo (SNoCut L R)SNoLev (SNoCut L R)ordsucc ((x ∈ Lordsucc (SNoLev x))(y ∈ Rordsucc (SNoLev y)))(∀x ∈ L, x < SNoCut L R)(∀y ∈ R, SNoCut L R < y)(∀z, SNo z(∀x ∈ L, x < z)(∀y ∈ R, z < y)SNoLev (SNoCut L R)SNoLev zSNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)
Axiom. (SNoCutP_SNoCut_impred) We take the following as an axiom:
∀L R, SNoCutP L R∀p : prop, (SNo (SNoCut L R)SNoLev (SNoCut L R)ordsucc ((x ∈ Lordsucc (SNoLev x))(y ∈ Rordsucc (SNoLev y)))(∀x ∈ L, x < SNoCut L R)(∀y ∈ R, SNoCut L R < y)(∀z, SNo z(∀x ∈ L, x < z)(∀y ∈ R, z < y)SNoLev (SNoCut L R)SNoLev zSNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)p)p
Axiom. (SNoCutP_L_0) We take the following as an axiom:
∀L, (∀x ∈ L, SNo x)SNoCutP L 0
Axiom. (SNoCutP_0_R) We take the following as an axiom:
∀R, (∀x ∈ R, SNo x)SNoCutP 0 R
Axiom. (SNoCutP_0_0) We take the following as an axiom:
SNoCutP 0 0
Axiom. (SNoCut_0_0) We take the following as an axiom:
SNoCut 0 0 = 0
Axiom. (ordinal_SNoLt_In) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha < betaalphabeta
Axiom. (ordinal_SNoLe_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalphabetaalphabeta
Definition. We define SNoS_ to be λalpha ⇒ {x ∈ 𝒫 (SNoElts_ alpha)|∃beta ∈ alpha, SNo_ beta x} of type setset.
Axiom. (SNoS_E) We take the following as an axiom:
∀alpha, ordinal alpha∀x ∈ SNoS_ alpha, ∃beta ∈ alpha, SNo_ beta x
Beginning of Section TaggedSets2
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Axiom. (SNoS_I) We take the following as an axiom:
∀alpha, ordinal alpha∀x, ∀beta ∈ alpha, SNo_ beta xxSNoS_ alpha
Axiom. (SNoS_I2) We take the following as an axiom:
∀x y, SNo xSNo ySNoLev xSNoLev yxSNoS_ (SNoLev y)
Axiom. (SNoS_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalphabetaSNoS_ alphaSNoS_ 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∀x ∈ SNoS_ alpha, ∀p : prop, (SNoLev xalphaordinal (SNoLev x)SNo xSNo_ (SNoLev x) xp)p
Axiom. (SNoS_In_neq) We take the following as an axiom:
∀w, SNo w∀x ∈ SNoS_ (SNoLev w), xw
Axiom. (SNoS_SNoLev) We take the following as an axiom:
∀z, SNo zzSNoS_ (ordsucc (SNoLev z))
Definition. We define SNoL to be λz ⇒ {x ∈ SNoS_ (SNoLev z)|x < z} of type setset.
Definition. We define SNoR to be λz ⇒ {y ∈ SNoS_ (SNoLev z)|z < y} of type setset.
Axiom. (SNoCutP_SNoL_SNoR) We take the following as an axiom:
∀z, SNo zSNoCutP (SNoL z) (SNoR z)
Axiom. (SNoL_E) We take the following as an axiom:
∀x, SNo x∀w ∈ SNoL x, ∀p : prop, (SNo wSNoLev wSNoLev xw < xp)p
Axiom. (SNoR_E) We take the following as an axiom:
∀x, SNo x∀z ∈ SNoR x, ∀p : prop, (SNo zSNoLev zSNoLev xx < zp)p
Axiom. (SNoL_SNoS) We take the following as an axiom:
∀x, SNo x∀w ∈ SNoL x, wSNoS_ (SNoLev x)
Axiom. (SNoR_SNoS) We take the following as an axiom:
∀x, SNo x∀z ∈ SNoR x, zSNoS_ (SNoLev x)
Axiom. (SNoL_SNoS_) We take the following as an axiom:
∀z, SNoL zSNoS_ (SNoLev z)
Axiom. (SNoR_SNoS_) We take the following as an axiom:
∀z, SNoR zSNoS_ (SNoLev z)
Axiom. (SNoL_I) We take the following as an axiom:
∀z, SNo z∀x, SNo xSNoLev xSNoLev zx < zxSNoL z
Axiom. (SNoR_I) We take the following as an axiom:
∀z, SNo z∀y, SNo ySNoLev ySNoLev zz < yySNoR 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∀x ∈ L, x < SNoCut L R
Axiom. (SNoCutP_SNoCut_R) We take the following as an axiom:
∀L R, SNoCutP L R∀y ∈ R, SNoCut L R < y
Axiom. (SNoCutP_SNoCut_fst) We take the following as an axiom:
∀L R, SNoCutP L R∀z, SNo z(∀x ∈ L, x < z)(∀y ∈ R, z < y)SNoLev (SNoCut L R)SNoLev zSNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z
Axiom. (SNoCut_Le) We take the following as an axiom:
∀L1 R1 L2 R2, SNoCutP L1 R1SNoCutP L2 R2(∀w ∈ L1, w < SNoCut L2 R2)(∀z ∈ R2, SNoCut L1 R1 < z)SNoCut L1 R1SNoCut L2 R2
Axiom. (SNoCut_ext) We take the following as an axiom:
∀L1 R1 L2 R2, SNoCutP L1 R1SNoCutP L2 R2(∀w ∈ L1, w < SNoCut L2 R2)(∀z ∈ R1, SNoCut L2 R2 < z)(∀w ∈ L2, w < SNoCut L1 R1)(∀z ∈ R2, 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, (∀z ∈ SNoL y, zSNoR xp)(xSNoL yp)(ySNoR xp)p
Axiom. (SNoL_or_SNoR_impred) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (x = yp)(∀z ∈ SNoL y, zSNoR xp)(xSNoL yp)(ySNoR xp)(∀z ∈ SNoR y, zSNoL xp)(xSNoR yp)(ySNoL xp)p
Axiom. (ordinal_SNo_) We take the following as an axiom:
∀alpha, ordinal alphaSNo_ alpha 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. (ordinal_SNoCutP) We take the following as an axiom:
∀alpha, ordinal alphaSNoCutP (SNoS_ alpha) Empty
Axiom. (ordinal_SNoCut_eta) We take the following as an axiom:
∀alpha, ordinal alphaalpha = SNoCut (SNoS_ alpha) Empty
Axiom. (SNo_0) We take the following as an axiom:
SNo 0
Axiom. (SNoLev_0) We take the following as an axiom:
SNoLev 0 = 0
Axiom. (SNoL_0) We take the following as an axiom:
SNoL 0 = 0
Axiom. (SNoR_0) We take the following as an axiom:
SNoR 0 = 0
Axiom. (SNoL_1) We take the following as an axiom:
SNoL 1 = 1
Axiom. (SNoR_1) We take the following as an axiom:
SNoR 1 = 0
Axiom. (SNo_max_SNoLev) We take the following as an axiom:
∀x, SNo x(∀y ∈ SNoS_ (SNoLev x), y < x)SNoLev x = x
Axiom. (SNo_max_ordinal) We take the following as an axiom:
∀x, SNo x(∀y ∈ SNoS_ (SNoLev x), y < x)ordinal x
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ deltaxdeltaSNoLev x) of type setset.
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ deltaxdelta = SNoLev x) of type setset.
Axiom. (SNo_extend0_SNo_) We take the following as an axiom:
∀x, SNo xSNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)
Axiom. (SNo_extend1_SNo_) We take the following as an axiom:
∀x, SNo xSNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)
Axiom. (SNo_extend0_SNo) We take the following as an axiom:
∀x, SNo xSNo (SNo_extend0 x)
Axiom. (SNo_extend1_SNo) We take the following as an axiom:
∀x, SNo xSNo (SNo_extend1 x)
Axiom. (SNo_extend0_SNoLev) We take the following as an axiom:
∀x, SNo xSNoLev (SNo_extend0 x) = ordsucc (SNoLev x)
Axiom. (SNo_extend1_SNoLev) We take the following as an axiom:
∀x, SNo xSNoLev (SNo_extend1 x) = ordsucc (SNoLev x)
Axiom. (SNo_extend0_nIn) We take the following as an axiom:
∀x, SNo xSNoLev xSNo_extend0 x
Axiom. (SNo_extend1_In) We take the following as an axiom:
∀x, SNo xSNoLev xSNo_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. (SNo_extend0_Lt) We take the following as an axiom:
∀x, SNo xSNo_extend0 x < x
Axiom. (SNo_extend1_Gt) We take the following as an axiom:
∀x, SNo xx < SNo_extend1 x
Definition. We define eps_ to be λn ⇒ {0}{(ordsucc m) '|m ∈ n} of type setset.
Axiom. (eps_ordinal_In_eq_0) We take the following as an axiom:
∀n alpha, ordinal alphaalphaeps_ nalpha = 0
Axiom. (eps_0_1) We take the following as an axiom:
eps_ 0 = 1
Axiom. (SNo__eps_) We take the following as an axiom:
∀n ∈ ω, SNo_ (ordsucc n) (eps_ n)
Axiom. (SNo_eps_) We take the following as an axiom:
∀n ∈ ω, SNo (eps_ n)
Axiom. (SNoLev_eps_) We take the following as an axiom:
∀n ∈ ω, SNoLev (eps_ n) = ordsucc n
Axiom. (SNo_eps_SNoS_omega) We take the following as an axiom:
∀n ∈ ω, eps_ nSNoS_ ω
Axiom. (SNo_eps_decr) We take the following as an axiom:
∀n ∈ ω, ∀m ∈ n, 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∀x ∈ SNoS_ n, 0 < xeps_ n < x
End of Section TaggedSets2
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 zalphaz < alpha
Axiom. (ordinal_In_SNoLt) We take the following as an axiom:
∀alpha, ordinal alpha∀beta ∈ alpha, beta < alpha
Axiom. (ordinal_SNoLev_max_2) We take the following as an axiom:
∀alpha, ordinal alpha∀z, SNo zSNoLev zordsucc alphazalpha
Axiom. (ordinal_Subq_SNoLe) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalphabetaalphabeta
Axiom. (SNo_etaE) We take the following as an axiom:
∀z, SNo z∀p : prop, (∀L R, SNoCutP L R(∀x ∈ L, SNoLev xSNoLev z)(∀y ∈ R, SNoLev ySNoLev z)z = SNoCut L Rp)p
Axiom. (SNo_ind) We take the following as an axiom:
∀P : setprop, (∀L R, SNoCutP L R(∀x ∈ L, P x)(∀y ∈ R, P y)P (SNoCut L R))∀z, SNo zP z
Beginning of Section SurrealRecI
Variable F : set(setset)set
Primitive. The name SNo_rec_i is a term of type setset.
Hypothesis Fr : ∀z, SNo z∀g h : setset, (∀w ∈ SNoS_ (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)
Primitive. The name SNo_rec_ii is a term of type set(setset).
Hypothesis Fr : ∀z, SNo z∀g h : set(setset), (∀w ∈ SNoS_ (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
Primitive. The name SNo_rec2 is a term of type setsetset.
Hypothesis Fr : ∀w, SNo w∀z, SNo z∀g h : setsetset, (∀x ∈ SNoS_ (SNoLev w), ∀y, SNo yg x y = h x y)(∀y ∈ SNoS_ (SNoLev z), g w y = h w y)F w z g = F w z h
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∀x ∈ SNoS_ 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∀x ∈ SNoS_ alpha, ∀y ∈ SNoS_ 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∀x ∈ SNoS_ alpha, ∀y ∈ SNoS_ beta, ∀z ∈ SNoS_ 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(∀w ∈ SNoS_ (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(∀w ∈ SNoS_ (SNoLev x), P w y)(∀z ∈ SNoS_ (SNoLev y), P x z)(∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (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(∀u ∈ SNoS_ (SNoLev x), P u y z)(∀v ∈ SNoS_ (SNoLev y), P x v z)(∀w ∈ SNoS_ (SNoLev z), P x y w)(∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), P u v z)(∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), P u y w)(∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P x v w)(∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P u v w)P x y z)∀x y z, SNo xSNo ySNo zP x y z
Axiom. (SNo_1) We take the following as an axiom:
SNo 1
Axiom. (SNo_2) We take the following as an axiom:
SNo 2
Axiom. (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. (SNoLev_0_eq_0) We take the following as an axiom:
∀x, SNo xSNoLev x = 0x = 0
Axiom. (restr_SNo_) We take the following as an axiom:
∀x, SNo x∀alpha ∈ SNoLev x, SNo_ alpha (xSNoElts_ alpha)
Axiom. (restr_SNo) We take the following as an axiom:
∀x, SNo x∀alpha ∈ SNoLev x, SNo (xSNoElts_ alpha)
Axiom. (restr_SNoLev) We take the following as an axiom:
∀x, SNo x∀alpha ∈ SNoLev x, SNoLev (xSNoElts_ alpha) = alpha
Axiom. (restr_SNoEq) We take the following as an axiom:
∀x, SNo x∀alpha ∈ SNoLev x, SNoEq_ alpha (xSNoElts_ alpha) x
Axiom. (restr_SNo_SNoCut) We take the following as an axiom:
∀x, SNo x∀alpha ∈ SNoLev x, ∀p : prop, (SNoCutP {w ∈ SNoL x|SNoLev walpha} {z ∈ SNoR x|SNoLev zalpha}xSNoElts_ alpha = SNoCut {w ∈ SNoL x|SNoLev walpha} {z ∈ SNoR x|SNoLev zalpha}p)p
Primitive. The name pack_e is a term of type setsetset.
Axiom. (pack_e_0_eq) We take the following as an axiom:
∀S X, ∀c : set, S = pack_e X cX = S 0
Axiom. (pack_e_0_eq2) We take the following as an axiom:
∀X, ∀c : set, X = pack_e X c 0
Axiom. (pack_e_1_eq) We take the following as an axiom:
∀S X, ∀c : set, S = pack_e X cc = S 1
Axiom. (pack_e_1_eq2) We take the following as an axiom:
∀X, ∀c : set, c = pack_e X c 1
Axiom. (pack_e_inj) We take the following as an axiom:
∀X X', ∀c c', pack_e X c = pack_e X' c'X = X'c = c'
Definition. We define struct_e to be λS ⇒ ∀q : setprop, (∀X : set, ∀c : set, cXq (pack_e X c))q S of type setprop.
Axiom. (pack_struct_e_I) We take the following as an axiom:
∀X, ∀c : set, cXstruct_e (pack_e X c)
Axiom. (pack_struct_e_E1) We take the following as an axiom:
∀X, ∀c : set, struct_e (pack_e X c)cX
Axiom. (struct_e_eta) We take the following as an axiom:
∀S, struct_e SS = pack_e (S 0) (S 1)
Primitive. The name unpack_e_i is a term of type set(setsetset)set.
Axiom. (unpack_e_i_eq) We take the following as an axiom:
∀Phi : setsetset, ∀X, ∀c : set, unpack_e_i (pack_e X c) Phi = Phi X c
Primitive. The name unpack_e_o is a term of type set(setsetprop)prop.
Axiom. (unpack_e_o_eq) We take the following as an axiom:
∀Phi : setsetprop, ∀X, ∀c : set, unpack_e_o (pack_e X c) Phi = Phi X c
Primitive. The name pack_u is a term of type set(setset)set.
Axiom. (