Primitive. The name Eps_i is a term of type (setprop)set.
Axiom. (Eps_i_R) We take the following as an axiom:
∀P : setprop, ∀x : set, P xP (Eps_i P)
Primitive. The name False is a term of type prop.
Primitive. The name True is a term of type prop.
Primitive. The name not is a term of type propprop.
Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.
Axiom. (dneg) We take the following as an axiom:
∀p : prop, ¬ ¬ pp
Primitive. The name and is a term of type proppropprop.
Notation. We use as an infix operator with priority 780 and which associates to the left corresponding to applying term and.
Primitive. The name or is a term of type proppropprop.
Notation. We use as an infix operator with priority 785 and which associates to the left corresponding to applying term or.
Primitive. The name iff is a term 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 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.
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
Axiom. (prop_ext) We take the following as an axiom:
∀A B : prop, (A B)A = B
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.
Primitive. The name Subq is a term 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.
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.
Axiom. (set_ext) We take the following as an axiom:
∀X Y : set, X YY XX = Y
Primitive. The name is a term of type set.
Axiom. (EmptyAx) We take the following as an axiom:
¬ ∃x : set, x
Primitive. The name is a term of type setset.
Axiom. (UnionEq) We take the following as an axiom:
∀X : set, ∀x : set, x X ∃Y : set, x Y Y X
Primitive. The name 𝒫 is a term of type setset.
Axiom. (PowerEq) We take the following as an axiom:
∀X Y : set, Y 𝒫 X Y X
Primitive. The name Repl is a term of type set(setset)set.
Notation. {B| xA} is notation for Repl Ax . B).
Axiom. (ReplEq) We take the following as an axiom:
∀X : set, ∀F : setset, ∀y : set, y {F x|xX} ∃x : set, x X y = F x
Primitive. The name TransSet is a term of type setprop.
Axiom. (HF_Min) We take the following as an axiom:
∀p : setprop, (∀X, p X∀xX, p x)p (∀X, p Xp ( X))(∀X, p Xp (𝒫 X))(∀X, p X∀F : setset, (∀xX, p (F x))p {F x|xX})∀x, p x
Axiom. (In_ind) We take the following as an axiom:
∀P : setprop, (∀X : set, (∀x : set, x XP x)P X)∀X : set, P X
Primitive. The name atleast2 is a term of type setprop.
Primitive. The name atleast3 is a term of type setprop.
Primitive. The name atleast4 is a term of type setprop.
Primitive. The name atleast5 is a term of type setprop.
Primitive. The name atleast6 is a term of type setprop.
Primitive. The name exactly2 is a term of type setprop.
Primitive. The name exactly3 is a term of type setprop.
Primitive. The name exactly4 is a term of type setprop.
Primitive. The name exactly5 is a term of type setprop.
Primitive. The name exu_i is a term of type (setprop)prop.
Primitive. The name reflexive_i is a term of type (setsetprop)prop.
Primitive. The name irreflexive_i is a term of type (setsetprop)prop.
Primitive. The name symmetric_i is a term of type (setsetprop)prop.
Primitive. The name antisymmetric_i is a term of type (setsetprop)prop.
Primitive. The name transitive_i is a term of type (setsetprop)prop.
Primitive. The name eqreln_i is a term of type (setsetprop)prop.
Primitive. The name per_i is a term of type (setsetprop)prop.
Primitive. The name linear_i is a term of type (setsetprop)prop.
Primitive. The name trichotomous_or_i is a term of type (setsetprop)prop.
Primitive. The name partialorder_i is a term of type (setsetprop)prop.
Primitive. The name totalorder_i is a term of type (setsetprop)prop.
Primitive. The name strictpartialorder_i is a term of type (setsetprop)prop.
Primitive. The name stricttotalorder_i is a term of type (setsetprop)prop.
Primitive. The name If_i is a term of type propsetsetset.
Primitive. The name exactly1of2 is a term of type proppropprop.
Primitive. The name exactly1of3 is a term of type propproppropprop.
Primitive. The name nIn is a term of type setsetprop.
Primitive. The name nSubq is a term of type setsetprop.
Primitive. The name UPair is a term of type setsetset.
Primitive. The name Sing is a term of type setset.
Primitive. The name binunion is a term of type setsetset.
Primitive. The name SetAdjoin is a term of type setsetset.
Primitive. The name famunion is a term of type set(setset)set.
Primitive. The name Sep is a term of type set(setprop)set.
Notation. {xA | B} is notation for Sep Ax . B).
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).
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.
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.
Primitive. The name inj is a term of type setset(setset)prop.
Primitive. The name bij is a term of type setset(setset)prop.
Primitive. The name atleastp is a term of type setsetprop.
Primitive. The name equip is a term of type setsetprop.
Primitive. The name In_rec_G_i is a term of type (set(setset)set)setsetprop.
Primitive. The name In_rec_i is a term of type (set(setset)set)setset.
Primitive. The name ordsucc is a term of type setset.
Primitive. The name nat_p is a term of type setprop.
Primitive. The name nat_primrec is a term of type set(setsetset)setset.
Primitive. The name add_nat is a term of type setsetset.
Primitive. The name mul_nat is a term of type setsetset.
Primitive. The name ordinal is a term of type setprop.
Primitive. The name V_ is a term of type setset.
Primitive. The name Inj1 is a term of type setset.
Primitive. The name Inj0 is a term of type setset.
Primitive. The name Unj is a term of type setset.
Primitive. The name combine_funcs is a term of type setset(setset)(setset)setset.
Primitive. The name setsum is a term of type setsetset.
Primitive. The name proj0 is a term of type setset.
Primitive. The name proj1 is a term of type setset.
Primitive. The name binrep is a term of type setsetset.
Primitive. The name lam is a term of type set(setset)set.
Primitive. The name setprod is a term of type setsetset.
Primitive. The name ap is a term of type setsetset.
Primitive. The name setsum_p is a term of type setprop.
Primitive. The name tuple_p is a term of type setsetprop.
Primitive. The name Pi is a term of type set(setset)set.
Primitive. The name setexp is a term of type setsetset.
Primitive. The name Sep2 is a term of type set(setset)(setsetprop)set.
Primitive. The name set_of_pairs is a term of type setprop.
Primitive. The name lam2 is a term of type set(setset)(setsetset)set.
Primitive. The name PNoEq_ is a term of type set(setprop)(setprop)prop.
Primitive. The name PNoLt_ is a term of type set(setprop)(setprop)prop.
Primitive. The name PNoLt is a term of type set(setprop)set(setprop)prop.
Primitive. The name PNoLe is a term of type set(setprop)set(setprop)prop.
Primitive. The name PNo_downc is a term of type (set(setprop)prop)set(setprop)prop.
Primitive. The name PNo_upc is a term of type (set(setprop)prop)set(setprop)prop.
Primitive. The name SNoElts_ is a term of type setset.
Primitive. The name SNo_ is a term of type setsetprop.
Primitive. The name PSNo is a term of type set(setprop)set.
Primitive. The name SNo is a term of type setprop.
Primitive. The name SNoLev is a term of type setset.
Primitive. The name SNoEq_ is a term of type setsetsetprop.
Primitive. The name SNoLt is a term of type setsetprop.
Primitive. The name SNoLe is a term of type setsetprop.
Primitive. The name binop_on is a term of type set(setsetset)prop.
Primitive. The name Loop is a term of type set(setsetset)(setsetset)(setsetset)setprop.
Primitive. The name Loop_with_defs is a term of type set(setsetset)(setsetset)(setsetset)set(setsetset)(setsetsetset)(setsetset)(setsetsetset)(setsetsetset)(setsetset)(setsetset)(setsetset)(setsetset)prop.
Primitive. The name Loop_with_defs_cex1 is a term of type set(setsetset)(setsetset)(setsetset)set(setsetset)(setsetsetset)(setsetset)(setsetsetset)(setsetsetset)(setsetset)(setsetset)(setsetset)(setsetset)prop.
Primitive. The name Loop_with_defs_cex2 is a term of type set(setsetset)(setsetset)(setsetset)set(setsetset)(setsetsetset)(setsetset)(setsetsetset)(setsetsetset)(setsetset)(setsetset)(setsetset)(setsetset)prop.
Primitive. The name combinator is a term of type setprop.
Primitive. The name combinator_equiv is a term of type setsetprop.
Primitive. The name equip_mod is a term of type setsetsetprop.
Axiom. (False_def) We take the following as an axiom:
False = (∀P : prop, P)
Axiom. (True_def) We take the following as an axiom:
True = (∀X0 : prop, (X0X0))
Axiom. (not_def) We take the following as an axiom:
not = (λA : propAFalse)
Axiom. (and_def) We take the following as an axiom:
and = (λA B : prop∀P : prop, (ABP)P)
Axiom. (or_def) We take the following as an axiom:
or = (λA B : prop∀P : prop, (AP)(BP)P)
Axiom. (iff_def) We take the following as an axiom:
iff = (λA B : prop(AB) (BA))
Axiom. (Subq_def) We take the following as an axiom:
Subq = (λX Y ⇒ ∀x : set, x Xx Y)
Axiom. (TransSet_def) We take the following as an axiom:
TransSet = (λU : set∀X : set, X UX U)
Axiom. (atleast2_def) We take the following as an axiom:
atleast2 = (λX ⇒ ∃y, y X ¬ (X 𝒫 y))
Axiom. (atleast3_def) We take the following as an axiom:
atleast3 = (λX ⇒ ∃Y, Y X (¬ (X Y) atleast2 Y))
Axiom. (atleast4_def) We take the following as an axiom:
atleast4 = (λX ⇒ ∃Y, Y X (¬ (X Y) atleast3 Y))
Axiom. (atleast5_def) We take the following as an axiom:
atleast5 = (λX ⇒ ∃Y, Y X (¬ (X Y) atleast4 Y))
Axiom. (atleast6_def) We take the following as an axiom:
atleast6 = (λX ⇒ ∃Y, Y X (¬ (X Y) atleast5 Y))
Axiom. (exactly2_def) We take the following as an axiom:
exactly2 = (λX ⇒ atleast2 X ¬ atleast3 X)
Axiom. (exactly3_def) We take the following as an axiom:
exactly3 = (λX ⇒ atleast3 X ¬ atleast4 X)
Axiom. (exactly4_def) We take the following as an axiom:
exactly4 = (λX ⇒ atleast4 X ¬ atleast5 X)
Axiom. (exactly5_def) We take the following as an axiom:
exactly5 = (λX ⇒ atleast5 X ¬ atleast6 X)
Axiom. (exu_i_def) We take the following as an axiom:
exu_i = (λX0 : setprop(and (∃X1 : set, (X0 X1)) (∀X1 : set, (∀X2 : set, ((X0 X1)((X0 X2)(X1 = X2)))))))
Axiom. (reflexive_i_def) We take the following as an axiom:
reflexive_i = (λX0 : setsetprop(∀X1 : set, (X0 X1 X1)))
Axiom. (irreflexive_i_def) We take the following as an axiom:
irreflexive_i = (λX0 : setsetprop(∀X1 : set, (not (X0 X1 X1))))
Axiom. (symmetric_i_def) We take the following as an axiom:
symmetric_i = (λX0 : setsetprop(∀X1 : set, (∀X2 : set, ((X0 X1 X2)(X0 X2 X1)))))
Axiom. (antisymmetric_i_def) We take the following as an axiom:
antisymmetric_i = (λX0 : setsetprop(∀X1 : set, (∀X2 : set, ((X0 X1 X2)((X0 X2 X1)(X1 = X2))))))
Axiom. (transitive_i_def) We take the following as an axiom:
transitive_i = (λX0 : setsetprop(∀X1 : set, (∀X2 : set, (∀X3 : set, ((X0 X1 X2)((X0 X2 X3)(X0 X1 X3)))))))
Axiom. (eqreln_i_def) We take the following as an axiom:
eqreln_i = (λX0 : setsetprop(and (and (reflexive_i X0) (symmetric_i X0)) (transitive_i X0)))
Axiom. (per_i_def) We take the following as an axiom:
per_i = (λX0 : setsetprop(and (symmetric_i X0) (transitive_i X0)))
Axiom. (linear_i_def) We take the following as an axiom:
linear_i = (λX0 : setsetprop(∀X1 : set, (∀X2 : set, (or (X0 X1 X2) (X0 X2 X1)))))
Axiom. (trichotomous_or_i_def) We take the following as an axiom:
trichotomous_or_i = (λX0 : setsetprop(∀X1 : set, (∀X2 : set, (or (or (X0 X1 X2) (X1 = X2)) (X0 X2 X1)))))
Axiom. (partialorder_i_def) We take the following as an axiom:
partialorder_i = (λX0 : setsetprop(and (and (reflexive_i X0) (antisymmetric_i X0)) (transitive_i X0)))
Axiom. (totalorder_i_def) We take the following as an axiom:
totalorder_i = (λX0 : setsetprop(and (partialorder_i X0) (linear_i X0)))
Axiom. (strictpartialorder_i_def) We take the following as an axiom:
strictpartialorder_i = (λX0 : setsetprop(and (irreflexive_i X0) (transitive_i X0)))
Axiom. (stricttotalorder_i_def) We take the following as an axiom:
stricttotalorder_i = (λX0 : setsetprop(and (strictpartialorder_i X0) (trichotomous_or_i X0)))
Axiom. (If_i_def) We take the following as an axiom:
If_i = (λX0 : prop(λX1 : set(λX2 : set(Eps_i (λX3 : set(or (and X0 (X3 = X1)) (and (not X0) (X3 = X2))))))))
Axiom. (exactly1of2_def) We take the following as an axiom:
exactly1of2 = (λX0 : prop(λX1 : prop(or (and X0 (not X1)) (and (not X0) X1))))
Axiom. (exactly1of3_def) We take the following as an axiom:
exactly1of3 = (λX0 : prop(λX1 : prop(λX2 : prop(or (and (exactly1of2 X0 X1) (not X2)) (and (and (not X0) (not X1)) X2)))))
Axiom. (nIn_def) We take the following as an axiom:
nIn = (λX0 : set(λX1 : set(not (In X0 X1))))
Axiom. (nSubq_def) We take the following as an axiom:
nSubq = (λX0 : set(λX1 : set(not (Subq X0 X1))))
Axiom. (UPair_def) We take the following as an axiom:
UPair = (λX0 : set(λX1 : set(Repl (𝒫 (𝒫 )) (λX2 : set(If_i (In X2) X0 X1)))))
Axiom. (Sing_def) We take the following as an axiom:
Sing = (λX0 : set(UPair X0 X0))
Axiom. (binunion_def) We take the following as an axiom:
binunion = (λX0 : set(λX1 : set( (UPair X0 X1))))
Axiom. (SetAdjoin_def) We take the following as an axiom:
SetAdjoin = (λX0 : set(λX1 : set(binunion X0 (Sing X1))))
Axiom. (famunion_def) We take the following as an axiom:
famunion = (λX0 : set(λX1 : setset( (Repl X0 (λX2 : set(X1 X2))))))
Axiom. (Sep_def) We take the following as an axiom:
Sep = (λX0 : set(λX1 : setprop(If_i (∃X2 : set, (and (In X2 X0) (X1 X2))) (Repl X0 (λX2 : set((λX3 : set(If_i (X1 X3) X3 (Eps_i (λX4 : set(and (In X4 X0) (X1 X4)))))) X2))) )))
Axiom. (ReplSep_def) We take the following as an axiom:
ReplSep = (λX0 : set(λX1 : setprop(λX2 : setset(Repl (Sep X0 (λX3 : set(X1 X3))) (λX3 : set(X2 X3))))))
Axiom. (binintersect_def) We take the following as an axiom:
binintersect = (λX0 : set(λX1 : set(Sep X0 (λX2 : set(In X2 X1)))))
Axiom. (setminus_def) We take the following as an axiom:
setminus = (λX0 : set(λX1 : set(Sep X0 (λX2 : set(nIn X2 X1)))))
Axiom. (inj_def) We take the following as an axiom:
inj = (λX0 : set(λX1 : set(λX2 : setset(and (∀X3 : set, ((In X3 X0)(In (X2 X3) X1))) (∀X3 : set, ((In X3 X0)(∀X4 : set, ((In X4 X0)(((X2 X3) = (X2 X4))(X3 = X4))))))))))
Axiom. (bij_def) We take the following as an axiom:
bij = (λX0 : set(λX1 : set(λX2 : setset(and (inj X0 X1 X2) (∀X3 : set, ((In X3 X1)(∃X4 : set, (and (In X4 X0) ((X2 X4) = X3)))))))))
Axiom. (atleastp_def) We take the following as an axiom:
atleastp = λX Y : set∃f : setset, inj X Y f
Axiom. (equip_def) We take the following as an axiom:
equip = λX Y : set∃f : setset, bij X Y f
Axiom. (In_rec_G_i_def) We take the following as an axiom:
In_rec_G_i = (λX0 : set(setset)set(λX1 : set(λX2 : set(∀X3 : setsetprop, ((∀X4 : set, (∀X5 : setset, ((∀X6 : set, ((In X6 X4)(X3 X6 (X5 X6))))(X3 X4 (X0 X4 X5)))))(X3 X1 X2))))))
Axiom. (In_rec_i_def) We take the following as an axiom:
In_rec_i = (λX0 : set(setset)set(λX1 : set(Eps_i (λX2 : set(In_rec_G_i X0 X1 X2)))))
Axiom. (ordsucc_def) We take the following as an axiom:
ordsucc = (λX0 : set(binunion X0 (Sing X0)))
Axiom. (nat_p_def) We take the following as an axiom:
nat_p = (λX0 : set(∀X1 : setprop, ((X1 )((∀X2 : set, ((X1 X2)(X1 (ordsucc X2))))(X1 X0)))))
Axiom. (nat_primrec_def) We take the following as an axiom:
nat_primrec = (λX0 : set(λX1 : setsetset(In_rec_i (λX2 : set(λX3 : setset(If_i (In ( X2) X2) (X1 ( X2) (X3 ( X2))) X0))))))
Axiom. (add_nat_def) We take the following as an axiom:
add_nat = (λX0 : set(λX1 : set(nat_primrec X0 (λX2 : set(λX3 : set(ordsucc X3))) X1)))
Axiom. (mul_nat_def) We take the following as an axiom:
mul_nat = (λX0 : set(λX1 : set(nat_primrec (λX2 : set(λX3 : set(add_nat X0 X3))) X1)))
Axiom. (ordinal_def) We take the following as an axiom:
ordinal = (λX0 : set(and (TransSet X0) (∀X1 : set, ((In X1 X0)(TransSet X1)))))
Axiom. (V__def) We take the following as an axiom:
V_ = (In_rec_i (λX0 : set(λX1 : setset(famunion X0 (λX2 : set(𝒫 (X1 X2)))))))
Axiom. (Inj1_def) We take the following as an axiom:
Inj1 = (In_rec_i (λX0 : set(λX1 : setset(binunion (Sing ) (Repl X0 (λX2 : set(X1 X2)))))))
Axiom. (Inj0_def) We take the following as an axiom:
Inj0 = (λX0 : set(Repl X0 (λX1 : set(Inj1 X1))))
Axiom. (Unj_def) We take the following as an axiom:
Unj = (In_rec_i (λX0 : set(λX1 : setset(Repl (setminus X0 (Sing )) (λX2 : set(X1 X2))))))
Axiom. (combine_funcs_def) We take the following as an axiom:
combine_funcs = (λX Y f g z ⇒ If_i (z = Inj0 (Unj z)) (f (Unj z)) (g (Unj z)))
Axiom. (setsum_def) We take the following as an axiom:
setsum = (λX0 : set(λX1 : set(binunion (Repl X0 (λX2 : set(Inj0 X2))) (Repl X1 (λX2 : set(Inj1 X2))))))
Axiom. (proj0_def) We take the following as an axiom:
proj0 = (λX0 : set(ReplSep X0 (λX1 : set(∃X2 : set, ((Inj0 X2) = X1))) (λX1 : set(Unj X1))))
Axiom. (proj1_def) We take the following as an axiom:
proj1 = (λX0 : set(ReplSep X0 (λX1 : set(∃X2 : set, ((Inj1 X2) = X1))) (λX1 : set(Unj X1))))
Axiom. (binrep_def) We take the following as an axiom:
binrep = λX Y ⇒ setsum X (𝒫 Y)
Axiom. (lam_def) We take the following as an axiom:
lam = (λX0 : set(λX1 : setset(famunion X0 (λX2 : set(Repl (X1 X2) (λX3 : set(setsum X2 X3)))))))
Axiom. (setprod_def) We take the following as an axiom:
setprod = (λX0 : set(λX1 : set(lam X0 (λX2 : setX1))))
Axiom. (ap_def) We take the following as an axiom:
ap = (λX0 : set(λX1 : set(ReplSep X0 (λX2 : set(∃X3 : set, (X2 = (setsum X1 X3)))) (λX2 : set(proj1 X2)))))
Axiom. (setsum_p_def) We take the following as an axiom:
setsum_p = (λX0 : set((setsum (ap X0 ) (ap X0 (ordsucc ))) = X0))
Axiom. (tuple_p_def) We take the following as an axiom:
tuple_p = (λX0 : set(λX1 : set(∀X2 : set, ((In X2 X1)(∃X3 : set, (and (In X3 X0) (∃X4 : set, (X2 = (setsum X3 X4)))))))))
Axiom. (Pi_def) We take the following as an axiom:
Pi = (λX0 : set(λX1 : setset(Sep (𝒫 (lam X0 (λX2 : set( (X1 X2))))) (λX2 : set(∀X3 : set, ((In X3 X0)(In (ap X2 X3) (X1 X3))))))))
Axiom. (setexp_def) We take the following as an axiom:
setexp = (λX0 : set(λX1 : set(Pi X1 (λX2 : setX0))))
Axiom. (Sep2_def) We take the following as an axiom:
Sep2 = (λX0 : set(λX1 : setset(λX2 : setsetprop(Sep (lam X0 (λX3 : set(X1 X3))) (λX3 : set(X2 (ap X3 ) (ap X3 (ordsucc ))))))))
Axiom. (set_of_pairs_def) We take the following as an axiom:
set_of_pairs = (λX0 : set(∀X1 : set, ((In X1 X0)(∃X2 : set, (∃X3 : set, (X1 = (lam (ordsucc (ordsucc )) (λX4 : set(If_i (X4 = ) X2 X3)))))))))
Axiom. (lam2_def) We take the following as an axiom:
lam2 = (λX0 : set(λX1 : setset(λX2 : setsetset(lam X0 (λX3 : set(lam (X1 X3) (λX4 : set(X2 X3 X4))))))))
Axiom. (PNoEq__def) We take the following as an axiom:
PNoEq_ = (λX0 : set(λX1 : setprop(λX2 : setprop(∀X3 : set, ((In X3 X0)(iff (X1 X3) (X2 X3)))))))
Axiom. (PNoLt__def) We take the following as an axiom:
PNoLt_ = (λX0 : set(λX1 : setprop(λX2 : setprop(∃X3 : set, (and (In X3 X0) (and (and (PNoEq_ X3 X1 X2) (not (X1 X3))) (X2 X3)))))))
Axiom. (PNoLt_def) We take the following as an axiom:
PNoLt = (λX0 : set(λX1 : setprop(λX2 : set(λX3 : setprop(or (or (PNoLt_ (binintersect X0 X2) X1 X3) (and (and (In X0 X2) (PNoEq_ X0 X1 X3)) (X3 X0))) (and (and (In X2 X0) (PNoEq_ X2 X1 X3)) (not (X1 X2))))))))
Axiom. (PNoLe_def) We take the following as an axiom:
PNoLe = (λX0 : set(λX1 : setprop(λX2 : set(λX3 : setprop(or (PNoLt X0 X1 X2 X3) (and (X0 = X2) (PNoEq_ X0 X1 X3)))))))
Axiom. (PNo_downc_def) We take the following as an axiom:
PNo_downc = (λX0 : set(setprop)prop(λX1 : set(λX2 : setprop(∃X3 : set, (and (ordinal X3) (∃X4 : setprop, (and (X0 X3 X4) (PNoLe X1 X2 X3 X4))))))))
Axiom. (PNo_upc_def) We take the following as an axiom:
PNo_upc = (λX0 : set(setprop)prop(λX1 : set(λX2 : setprop(∃X3 : set, (and (ordinal X3) (∃X4 : setprop, (and (X0 X3 X4) (PNoLe X3 X4 X1 X2))))))))
Axiom. (SNoElts__def) We take the following as an axiom:
SNoElts_ = (λX0 : set(binunion X0 (Repl X0 (λX1 : set((λX2 : set(SetAdjoin X2 (Sing (ordsucc )))) X1)))))
Axiom. (SNo__def) We take the following as an axiom:
SNo_ = (λX0 : set(λX1 : set(and (Subq X1 (SNoElts_ X0)) (∀X2 : set, ((In X2 X0)(exactly1of2 (In ((λX3 : set(SetAdjoin X3 (Sing (ordsucc )))) X2) X1) (In X2 X1)))))))
Axiom. (PSNo_def) We take the following as an axiom:
PSNo = (λX0 : set(λX1 : setprop(binunion (Sep X0 (λX2 : set(X1 X2))) (ReplSep X0 (λX2 : set(not (X1 X2))) (λX2 : set((λX3 : set(SetAdjoin X3 (Sing (ordsucc )))) X2))))))
Axiom. (SNo_def) We take the following as an axiom:
SNo = (λX0 : set(∃X1 : set, (and (ordinal X1) (SNo_ X1 X0))))
Axiom. (SNoLev_def) We take the following as an axiom:
SNoLev = (λX0 : set(Eps_i (λX1 : set(and (ordinal X1) (SNo_ X1 X0)))))
Axiom. (SNoEq__def) We take the following as an axiom:
SNoEq_ = (λX0 : set(λX1 : set(λX2 : set(PNoEq_ X0 (λX3 : set(In X3 X1)) (λX3 : set(In X3 X2))))))
Axiom. (SNoLt_def) We take the following as an axiom:
SNoLt = (λX0 : set(λX1 : set(PNoLt (SNoLev X0) (λX2 : set(In X2 X0)) (SNoLev X1) (λX2 : set(In X2 X1)))))
Axiom. (SNoLe_def) We take the following as an axiom:
SNoLe = (λX0 : set(λX1 : set(PNoLe (SNoLev X0) (λX2 : set(In X2 X0)) (SNoLev X1) (λX2 : set(In X2 X1)))))
Axiom. (binop_on_def) We take the following as an axiom:
binop_on = (λX0 : set(λX1 : setsetset(∀X2 : set, ((In X2 X0)(∀X3 : set, ((In X3 X0)(In (X1 X2 X3) X0)))))))
Axiom. (Loop_def) We take the following as an axiom:
Loop = (λX : set(λm b s : setsetset(λe : setbinop_on X m binop_on X b binop_on X s (∀xX, (m e x = x m x e = x)) (∀x yX, (b x (m x y) = y m x (b x y) = y s (m x y) y = x m (s x y) y = x)))))
Axiom. (Loop_with_defs_def) We take the following as an axiom:
Loop_with_defs = λX m b s e K a T L R I1 J1 I2 J2 ⇒ Loop X m b s e (∀x yX, K x y = b (m y x) (m x y)) (∀x y zX, a x y z = b (m x (m y z)) (m (m x y) z)) (∀x uX, T x u = b x (m u x) I1 x u = m x (m u (b x e)) J1 x u = m (m (s e x) u) x I2 x u = m (b x u) (b (b x e) e) J2 x u = m (s e (s e x)) (s u x)) (∀x y uX, L x y u = b (m y x) (m y (m x u)) R x y u = s (m (m u x) y) (m x y))
Axiom. (Loop_with_defs_cex1_def) We take the following as an axiom:
Loop_with_defs_cex1 = λX m b s e K a T L R I1 J1 I2 J2 ⇒ Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 ∃u x y wX, ¬ (K (m (b (L x y u) e) u) w = e)
Axiom. (Loop_with_defs_cex2_def) We take the following as an axiom:
Loop_with_defs_cex2 = λX m b s e K a T L R I1 J1 I2 J2 ⇒ Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 ∃u x y z wX, ¬ (a w (m (s e u) (R x y u)) z = e)
Axiom. (combinator_def) We take the following as an axiom:
combinator = λX ⇒ ∀p : setprop, p (Inj0 )p (Inj0 (𝒫 ))(∀Y Z, p Yp Zp (Inj1 (setsum Y Z)))p X
Axiom. (combinator_equiv_def) We take the following as an axiom:
combinator_equiv = λX Y ⇒ ∀r : setsetprop, ((λK S : setλAp : setsetsetper_i r(∀Z, combinator Zr Z Z)(∀W1 Z1 W2 Z2, combinator W1combinator Z1combinator W2combinator Z2r W1 W2r Z1 Z2r (Ap W1 Z1) (Ap W2 Z2))(∀W Z, r (Ap (Ap K W) Z) W)(∀W Z V, r (Ap (Ap (Ap S W) Z) V) (Ap (Ap W V) (Ap Z V)))r X Y) (Inj0 ) (Inj0 (𝒫 )) (λW Z : setInj1 (setsum W Z)))
Axiom. (equip_mod_def) We take the following as an axiom:
equip_mod = λX Y M ⇒ ∃Z V, (equip (setsum X Z) Y equip (setprod V Z) M) (equip (setsum Y Z) X equip (setprod V Z) M)
Axiom. (TrueI) We take the following as an axiom:
True
Axiom. (FalseE) We take the following as an axiom:
False∀p : prop, p
Axiom. (notE) We take the following as an axiom:
∀A : prop, ¬ AAFalse
Axiom. (notI) We take the following as an axiom:
∀A : prop, (AFalse)¬ A
Axiom. (andE) We take the following as an axiom:
∀A B : prop, A B∀p : prop, (ABp)p
Axiom. (andI) We take the following as an axiom:
∀A B : prop, ABA B
Axiom. (orE) We take the following as an axiom:
∀A B : prop, A B∀p : prop, (Ap)(Bp)p
Axiom. (orIL) We take the following as an axiom:
∀A B : prop, AA B
Axiom. (orIR) We take the following as an axiom:
∀A B : prop, BA B
Axiom. (xm) We take the following as an axiom:
∀A : prop, A ¬ A
Axiom. (xmcases) We take the following as an axiom:
∀A p : prop, (Ap)(¬ Ap)p
Axiom. (iffE) We take the following as an axiom:
∀A B : prop, (A B)∀p : prop, (ABp)(¬ A¬ Bp)p
Axiom. (iffI) We take the following as an axiom:
∀A B : prop, (AB)(BA)(A B)
Notation. We use as an infix operator with priority 502 and no associativity corresponding to applying term nIn.
Notation. We use as an infix operator with priority 502 and no associativity corresponding to applying term nSubq.
Axiom. (dnegI) We take the following as an axiom:
∀p : prop, p¬ ¬ p
Axiom. (contra) We take the following as an axiom:
∀p : prop, (¬ pFalse)p
Axiom. (keepcopy) We take the following as an axiom:
∀p : prop, (¬ pp)p
Axiom. (orI_contra) We take the following as an axiom:
∀p q : prop, (¬ p¬ qFalse)p q
Axiom. (orI_imp1) We take the following as an axiom:
∀p q : prop, (pq)¬ p q
Axiom. (orI_imp2) We take the following as an axiom:
∀p q : prop, (qp)p ¬ q
Axiom. (tab_neg_True) We take the following as an axiom:
¬ TrueFalse
Axiom. (tab_pos_and) We take the following as an axiom:
∀A B : prop, (A B)(ABFalse)False
Axiom. (tab_pos_or) We take the following as an axiom:
∀A B : prop, (A B)(AFalse)(BFalse)False
Axiom. (tab_pos_imp) We take the following as an axiom:
∀A B : prop, (AB)(¬ AFalse)(BFalse)False
Axiom. (tab_pos_iff) We take the following as an axiom:
∀A B : prop, (A B)(ABFalse)(¬ A¬ BFalse)False
Axiom. (tab_neg_imp) We take the following as an axiom:
∀A B : prop, ¬ (AB)(A¬ BFalse)False
Axiom. (tab_neg_and) We take the following as an axiom:
∀A B : prop, ¬ (A B)(¬ AFalse)(¬ BFalse)False
Axiom. (tab_neg_or) We take the following as an axiom:
∀A B : prop, ¬ (A B)(¬ A¬ BFalse)False
Axiom. (tab_neg_iff) We take the following as an axiom:
∀A B : prop, ¬ (A B)(A¬ BFalse)(¬ ABFalse)False
Axiom. (prop_ext_2) We take the following as an axiom:
∀A B : prop, (AB)(BA)A = B
Axiom. (eqo_iff) We take the following as an axiom:
∀A B : prop, (A = B)(A B)
Axiom. (tab_pos_eqo) We take the following as an axiom:
∀A B : prop, (A = B)(ABFalse)(¬ A¬ BFalse)False
Axiom. (tab_neg_eqo) We take the following as an axiom:
∀A B : prop, ¬ (A = B)(A¬ BFalse)(¬ ABFalse)False
Axiom. (tab_pos_all_i) We take the following as an axiom:
∀P : setprop, ∀Y, (∀x, P x)(P YFalse)False
Axiom. (tab_neg_all_i) We take the following as an axiom:
∀P : setprop, ¬ (∀x, P x)(∀y, ¬ P yFalse)False
Axiom. (tab_pos_ex_i) We take the following as an axiom:
∀P : setprop, (∃x, P x)(∀y, P yFalse)False
Axiom. (tab_mat_i_o) We take the following as an axiom:
∀P : setprop, ∀X1 Y1, P X1¬ P Y1(¬ (X1 = Y1)False)False
Axiom. (tab_mat_i_i_o) We take the following as an axiom:
∀P : setsetprop, ∀X1 X2 Y1 Y2, P X1 X2¬ P Y1 Y2(¬ (X1 = Y1)False)(¬ (X2 = Y2)False)False
Axiom. (tab_confront) We take the following as an axiom:
∀X Y Z W, X = Y¬ (Z = W)(¬ (X = Z)¬ (Y = Z)False)(¬ (X = W)¬ (Y = W)False)False
Axiom. (f_equal_i_i) We take the following as an axiom:
∀F : setset, ∀X1 Y1, X1 = Y1F X1 = F Y1
Axiom. (tab_dec_i) We take the following as an axiom:
∀F : setset, ∀X1 Y1, ¬ (F X1 = F Y1)(¬ (X1 = Y1)False)False
Axiom. (f_equal_i_i_i) We take the following as an axiom:
∀F : setsetset, ∀X1 Y1 X2 Y2, X1 = Y1X2 = Y2F X1 X2 = F Y1 Y2
Axiom. (tab_dec_i_i) We take the following as an axiom:
∀F : setsetset, ∀X1 Y1 X2 Y2, ¬ (F X1 X2 = F Y1 Y2)(¬ (X1 = Y1)False)(¬ (X2 = Y2)False)False
Axiom. (tab_pos_eqf_i_i) We take the following as an axiom:
∀F G : setset, ∀X, (F = G)(F X = G XFalse)False
Axiom. (tab_pos_neqf_i_i) We take the following as an axiom:
∀F G : setset, ¬ (F = G)(∀x, ¬ (F x = G x)False)False
Axiom. (andEL) We take the following as an axiom:
∀A B : prop, A BA
Axiom. (andER) We take the following as an axiom:
∀A B : prop, A BB
Axiom. (iffEL) We take the following as an axiom:
∀A B : prop, (A B)AB
Axiom. (iffER) We take the following as an axiom:
∀A B : prop, (A B)BA
Axiom. (exandI_i) We take the following as an axiom:
∀P Q : setprop, ∀x, P xQ x(∃x, P x Q x)
Axiom. (exandE_i) We take the following as an axiom:
∀P Q : setprop, (∃x, P x Q x)∀p : prop, (∀x, P xQ xp)p
Axiom. (SubqI) We take the following as an axiom:
∀A B, (∀xA, x B)Subq A B
Axiom. (SubqE) We take the following as an axiom:
∀A B, Subq A B(∀xA, x B)
Axiom. (tab_pos_Subq) We take the following as an axiom:
∀A B, A B((∀xA, x B)False)False
Axiom. (tab_neg_Subq) We take the following as an axiom:
∀A B, ¬ (A B)(¬ (∀xA, x B)False)False
Axiom. (TransSetI) We take the following as an axiom:
∀U, (∀XU, X U)TransSet U
Axiom. (TransSetE) We take the following as an axiom:
∀U, TransSet U∀XU, X U
Axiom. (atleast2_I) We take the following as an axiom:
∀X y, y X(¬ (X 𝒫 y))atleast2 X
Axiom. (atleast2_E) We take the following as an axiom:
∀X, atleast2 X∃y, y X ¬ (X 𝒫 y)
Axiom. (atleast3_I) We take the following as an axiom:
∀X Y, Y X(¬ (X Y))atleast2 Yatleast3 X
Axiom. (atleast3_E) We take the following as an axiom:
∀X, atleast3 X∃Y, Y X (¬ (X Y) atleast2 Y)
Axiom. (atleast4_I) We take the following as an axiom:
∀X Y, Y X(¬ (X Y))atleast3 Yatleast4 X
Axiom. (atleast4_E) We take the following as an axiom:
∀X, atleast4 X∃Y, Y X (¬ (X Y) atleast3 Y)
Axiom. (atleast5_I) We take the following as an axiom:
∀X Y, Y X(¬ (X Y))atleast4 Yatleast5 X
Axiom. (atleast5_E) We take the following as an axiom:
∀X, atleast5 X∃Y, Y X (¬ (X Y) atleast4 Y)
Axiom. (atleast6_I) We take the following as an axiom:
∀X Y, Y X(¬ (X Y))atleast5 Yatleast6 X
Axiom. (atleast6_E) We take the following as an axiom:
∀X, atleast6 X∃Y, Y X (¬ (X Y) atleast5 Y)
Axiom. (exactly2_I) We take the following as an axiom:
∀X, atleast2 X¬ atleast3 Xexactly2 X
Axiom. (exactly2_E) We take the following as an axiom:
∀X, exactly2 Xatleast2 X ¬ atleast3 X
Axiom. (exactly3_I) We take the following as an axiom:
∀X, atleast3 X¬ atleast4 Xexactly3 X
Axiom. (exactly3_E) We take the following as an axiom:
∀X, exactly3 Xatleast3 X ¬ atleast4 X
Axiom. (exactly4_I) We take the following as an axiom:
∀X, atleast4 X¬ atleast5 Xexactly4 X
Axiom. (exactly4_E) We take the following as an axiom:
∀X, exactly4 Xatleast4 X ¬ atleast5 X
Axiom. (exactly5_I) We take the following as an axiom:
∀X, atleast5 X¬ atleast6 Xexactly5 X
Axiom. (exactly5_E) We take the following as an axiom:
∀X, exactly5 Xatleast5 X ¬ atleast6 X
Axiom. (nIn_I) We take the following as an axiom:
∀X Y, ¬ In X YnIn X Y
Axiom. (nIn_E) We take the following as an axiom:
∀X Y, nIn X Y¬ In X Y
Axiom. (nIn_I2) We take the following as an axiom:
∀X Y, (In X YFalse)nIn X Y
Axiom. (nIn_E2) We take the following as an axiom:
∀X Y, nIn X YIn X YFalse
Axiom. (contra_In) We take the following as an axiom:
∀X Y, (X YFalse)X Y
Axiom. (neg_nIn) We take the following as an axiom:
∀X Y, ¬ (X Y)X Y
Axiom. (nSubq_I) We take the following as an axiom:
∀X Y, ¬ Subq X YnSubq X Y
Axiom. (nSubq_E) We take the following as an axiom:
∀X Y, nSubq X Y¬ Subq X Y
Axiom. (nSubq_I2) We take the following as an axiom:
∀X Y, (Subq X YFalse)nSubq X Y
Axiom. (nSubq_E2) We take the following as an axiom:
∀X Y, nSubq X YSubq X YFalse
Axiom. (neg_nSubq) We take the following as an axiom:
∀X Y, ¬ (X Y)X Y
Axiom. (contra_Subq) We take the following as an axiom:
∀X Y, (X YFalse)X Y
Axiom. (Subq_ref) We take the following as an axiom:
∀X : set, X X
Axiom. (Subq_tra) We take the following as an axiom:
∀X Y Z : set, X YY ZX Z
Axiom. (Subq_contra) We take the following as an axiom:
∀X Y z : set, X Yz Yz X
Axiom. (EmptyE) We take the following as an axiom:
∀x : set, x False
Axiom. (nIn_Empty) We take the following as an axiom:
∀x : set, x
Axiom. (Subq_Empty) We take the following as an axiom:
∀X : set, X
Axiom. (Empty_Subq_eq) We take the following as an axiom:
∀X : set, X X =
Axiom. (Empty_eq) We take the following as an axiom:
∀X : set, (∀x, x X)X =
Axiom. (UnionE) We take the following as an axiom:
∀X x : set, x ( X)∃Y : set, x Y Y X
Axiom. (UnionE2) We take the following as an axiom:
∀X x : set, x ( X)∀p : prop, (∀Y : set, x YY Xp)p
Axiom. (UnionI) We take the following as an axiom:
∀X x Y : set, x YY Xx ( X)
Axiom. (tab_pos_Union) We take the following as an axiom:
∀X x, x X(∀Y, x YY XFalse)False
Axiom. (tab_neg_Union) We take the following as an axiom:
∀X x Y, x X(x YFalse)(Y XFalse)False
Axiom. (Union_Empty) We take the following as an axiom:
=
Axiom. (PowerE) We take the following as an axiom:
∀X Y : set, Y 𝒫 XY X
Axiom. (PowerI) We take the following as an axiom:
∀X Y : set, Y XY 𝒫 X
Axiom. (tab_pos_Power) We take the following as an axiom:
∀X Y, Y 𝒫 X(Y XFalse)False
Axiom. (tab_neg_Power) We take the following as an axiom:
∀X Y, Y 𝒫 X(Y XFalse)False
Axiom. (Empty_In_Power) We take the following as an axiom:
∀X : set, 𝒫 X
Axiom. (Self_In_Power) We take the following as an axiom:
∀X : set, X 𝒫 X
Axiom. (ReplE) We take the following as an axiom:
∀X : set, ∀F : setset, ∀y : set, y {F x|xX}∃x : set, x X y = F x
Axiom. (ReplE2) We take the following as an axiom:
∀X : set, ∀F : setset, ∀y : set, y {F x|xX}∀p : prop, (∀x : set, x Xy = F xp)p
Axiom. (ReplI) We take the following as an axiom:
∀X : set, ∀F : setset, ∀x : set, x XF x {F x|xX}
Axiom. (tab_pos_Repl) We take the following as an axiom:
∀X, ∀F : setset, ∀y, y {F x|xX}(∀x, x Xy = F xFalse)False
Axiom. (tab_neg_Repl) We take the following as an axiom:
∀X, ∀F : setset, ∀y x, y {F x|xX}(x XFalse)(¬ (y = F x)False)False
Axiom. (Repl_Empty) We take the following as an axiom:
∀F : setset, {F x|x} =
Axiom. (ReplEq_ext_sub) We take the following as an axiom:
∀X, ∀F G : setset, (∀xX, F x = G x){F x|xX} {G x|xX}
Axiom. (ReplEq_ext) We take the following as an axiom:
∀X, ∀F G : setset, (∀xX, F x = G x){F x|xX} = {G x|xX}
Axiom. (set_ext_2) We take the following as an axiom:
∀A B, (∀x, x Ax B)(∀x, x Bx A)A = B
Axiom. (neq_i_sym) We take the following as an axiom:
∀x y, ¬ (x = y)¬ (y = x)
Axiom. (tab_neq_i_sym) We take the following as an axiom:
∀x y, ¬ (x = y)(¬ (y = x)False)False
Axiom. (tab_Eps_i) We take the following as an axiom:
∀p : setprop, ((∀x, ¬ p x)False)(p (Eps_i p)False)False
Axiom. (If_i_0) We take the following as an axiom:
∀p : prop, ∀x y, ¬ pIf_i p x y = y
Axiom. (If_i_1) We take the following as an axiom:
∀p : prop, ∀x y, pIf_i p x y = x
Axiom. (If_i_or) We take the following as an axiom:
∀p : prop, ∀x y, If_i p x y = x If_i p x y = y
Axiom. (tab_If_i_lhs) We take the following as an axiom:
∀p : prop, ∀x y z, ¬ (If_i p x y = z)(p¬ (x = z)False)(¬ p¬ (y = z)False)False
Axiom. (tab_If_i_rhs) We take the following as an axiom:
∀p : prop, ∀x y z, ¬ (z = If_i p x y)(p¬ (z = x)False)(¬ p¬ (z = y)False)False
Notation. {x,y} is notation for UPair x y.
Axiom. (UPairE) We take the following as an axiom:
∀x y z : set, x {y,z}x = y x = z
Axiom. (UPairE_cases) We take the following as an axiom:
∀x y z : set, x {y,z}∀p : prop, (x = yp)(x = zp)p
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}
Axiom. (tab_pos_UPair) We take the following as an axiom:
∀x y z, z {x,y}(z = xFalse)(z = yFalse)False
Axiom. (tab_neg_UPair) We take the following as an axiom:
∀x y z, z {x,y}(¬ (z = x)¬ (z = y)False)False
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
Axiom. (tab_pos_Sing) We take the following as an axiom:
∀x y, y {x}(y = xFalse)False
Axiom. (tab_neg_Sing) We take the following as an axiom:
∀x y, y {x}(¬ (y = x)False)False
Notation. We use as an infix operator with priority 345 and which associates to the left corresponding to applying term binunion.
Axiom. (binunionI1) We take the following as an axiom:
∀X Y z : set, z Xz X Y
Axiom. (binunionI2) We take the following as an axiom:
∀X Y z : set, z Yz X Y
Axiom. (binunionE) We take the following as an axiom:
∀X Y z : set, z X Yz X z Y
Axiom. (binunionE_cases) We take the following as an axiom:
∀X Y z : set, z X Y∀p : prop, (z Xp)(z Yp)p
Axiom. (tab_pos_binunion) We take the following as an axiom:
∀X Y z, z X Y(z XFalse)(z YFalse)False
Axiom. (tab_neg_binunion) We take the following as an axiom:
∀X Y z, z X Y(z Xz YFalse)False
Notation. We now use the set enumeration notation {...,...,...} in general. If 0 elements are given, then 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:
𝒫 = {}
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}
Notation. We use x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using famunion.
Axiom. (famunionI) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀x y : set, x Xy F xy xXF x
Axiom. (famunionE) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)∃xX, y F x
Axiom. (famunionE2) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)∀p : prop, (∀x, x Xy F xp)p
Axiom. (UnionEq_famunionId) We take the following as an axiom:
∀X : set, X = xXx
Axiom. (ReplEq_famunion_Sing) We take the following as an axiom:
∀X : set, ∀F : (setset), {F x|xX} = xX{F x}
Axiom. (tab_pos_famunion) We take the following as an axiom:
∀X, ∀F : setset, ∀z, (z xXF x)(∀x, x Xz F xFalse)False
Axiom. (tab_neg_famunion) We take the following as an axiom:
∀X, ∀F : setset, ∀z x, (z xXF x)(x XFalse)(z F xFalse)False
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.
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (and3I) We take the following as an axiom:
P1P2P3P1 P2 P3
Axiom. (and3E) We take the following as an axiom:
P1 P2 P3(∀p : prop, (P1P2P3p)p)
Axiom. (or3I1) We take the following as an axiom:
P1P1 P2 P3
Axiom. (or3I2) We take the following as an axiom:
P2P1 P2 P3
Axiom. (or3I3) We take the following as an axiom:
P3P1 P2 P3
Axiom. (or3E) We take the following as an axiom:
P1 P2 P3(∀p : prop, (P1p)(P2p)(P3p)p)
Variable P4 : prop
Axiom. (and4I) We take the following as an axiom:
P1P2P3P4P1 P2 P3 P4
Axiom. (and4E) We take the following as an axiom:
P1 P2 P3 P4(∀p : prop, (P1P2P3P4p)p)
Axiom. (or4I1) We take the following as an axiom:
P1P1 P2 P3 P4
Axiom. (or4I2) We take the following as an axiom:
P2P1 P2 P3 P4
Axiom. (or4I3) We take the following as an axiom:
P3P1 P2 P3 P4
Axiom. (or4I4) We take the following as an axiom:
P4P1 P2 P3 P4
Axiom. (or4E) We take the following as an axiom:
P1 P2 P3 P4(∀p : prop, (P1p)(P2p)(P3p)(P4p)p)
Variable P5 : prop
Axiom. (and5I) We take the following as an axiom:
P1P2P3P4P5P1 P2 P3 P4 P5
Axiom. (and5E) We take the following as an axiom:
P1 P2 P3 P4 P5(∀p : prop, (P1P2P3P4P5p)p)
Axiom. (or5I1) We take the following as an axiom:
P1P1 P2 P3 P4 P5
Axiom. (or5I2) We take the following as an axiom:
P2P1 P2 P3 P4 P5
Axiom. (or5I3) We take the following as an axiom:
P3P1 P2 P3 P4 P5
Axiom. (or5I4) We take the following as an axiom:
P4P1 P2 P3 P4 P5
Axiom. (or5I5) We take the following as an axiom:
P5P1 P2 P3 P4 P5
Axiom. (or5E) We take the following as an axiom:
P1 P2 P3 P4 P5(∀p : prop, (P1p)(P2p)(P3p)(P4p)(P5p)p)
Variable P6 : prop
Axiom. (and6I) We take the following as an axiom:
P1P2P3P4P5P6P1 P2 P3 P4 P5 P6
Axiom. (and6E) We take the following as an axiom:
P1 P2 P3 P4 P5 P6(∀p : prop, (P1P2P3P4P5P6p)p)
Variable P7 : prop
Axiom. (and7I) We take the following as an axiom:
P1P2P3P4P5P6P7P1 P2 P3 P4 P5 P6 P7
Axiom. (and7E) We take the following as an axiom:
P1 P2 P3 P4 P5 P6 P7(∀p : prop, (P1P2P3P4P5P6P7p)p)
End of Section PropN
Axiom. (tab_neg_ex_i) We take the following as an axiom:
∀P : setprop, ∀Y, ¬ (∃x, P x)(¬ P YFalse)False
Axiom. (Eps_i_R2) We take the following as an axiom:
∀P : setprop, (∃x, P x)P (Eps_i P)
Axiom. (xmcases_In) We take the following as an axiom:
∀x X : set, ∀p : prop, (x Xp)(x Xp)p
Axiom. (SepI) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x XP xx {xX|P x}
Axiom. (SepE) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X P x
Axiom. (SepE_impred) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}∀q : prop, (x XP xq)q
Axiom. (SepE1) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X
Axiom. (SepE2) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}P x
Axiom. (Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : setprop, {xX|P x} X
Axiom. (Sep_In_Power) We take the following as an axiom:
∀X : set, ∀P : setprop, {xX|P x} 𝒫 X
Axiom. (tab_pos_Sep) We take the following as an axiom:
∀X, ∀P : setprop, ∀x, x {xX|P x}(x XP xFalse)False
Axiom. (tab_neg_Sep) We take the following as an axiom:
∀X, ∀P : setprop, ∀x, x {xX|P x}(x XFalse)(¬ P xFalse)False
Axiom. (ReplSepI) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀x : set, x XP xF x {F x|xX, P x}
Axiom. (ReplSepE) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}∃x : set, x X P x y = F x
Axiom. (ReplSepE_impred) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}∀p : prop, (∀xX, P xy = F xp)p
Axiom. (tab_pos_ReplSep) We take the following as an axiom:
∀X, ∀P : setprop, ∀F : setset, ∀y, y {F x|xX, P x}(∀x, x XP xy = F xFalse)False
Axiom. (tab_neg_ReplSep) We take the following as an axiom:
∀X, ∀P : setprop, ∀F : setset, ∀y x, y {F x|xX, P x}(x XFalse)(¬ P xFalse)(¬ (y = F x)False)False
Axiom. (binunion_asso) We take the following as an axiom:
∀X Y Z : set, X (Y Z) = (X Y) Z
Axiom. (binunion_com) We take the following as an axiom:
∀X Y : set, X Y = Y X
Axiom. (binunion_idl) We take the following as an axiom:
∀X : set, X = X
Axiom. (binunion_idr) We take the following as an axiom:
∀X : set, X = X
Axiom. (binunion_idem) We take the following as an axiom:
∀X : set, X X = X
Axiom. (binunion_Subq_1) We take the following as an axiom:
∀X Y : set, X X Y
Axiom. (binunion_Subq_2) We take the following as an axiom:
∀X Y : set, Y X Y
Axiom. (binunion_Subq_min) We take the following as an axiom:
∀X Y Z : set, X ZY ZX Y Z
Axiom. (Subq_binunion_eq) We take the following as an axiom:
∀X Y, (X Y) = (X Y = Y)
Axiom. (binunion_nIn_I) We take the following as an axiom:
∀X Y z : set, z Xz Yz X Y
Axiom. (binunion_nIn_E) We take the following as an axiom:
∀X Y z : set, z X Yz X z Y
Axiom. (binunion_nIn_E_impred) We take the following as an axiom:
∀X Y z : set, z X Y∀p : prop, (z Xz Yp)p
Axiom. (binintersectI) We take the following as an axiom:
∀X Y z, z Xz Yz X Y
Axiom. (binintersectE) We take the following as an axiom:
∀X Y z, z X Yz X z Y
Axiom. (binintersectE_impred) We take the following as an axiom:
∀X Y z, z X Y∀p : prop, (z Xz Yp)p
Axiom. (binintersectE1) We take the following as an axiom:
∀X Y z, z X Yz X
Axiom. (binintersectE2) We take the following as an axiom:
∀X Y z, z X Yz Y
Axiom. (binintersect_Subq_1) We take the following as an axiom:
∀X Y : set, X Y X
Axiom. (binintersect_Subq_2) We take the following as an axiom:
∀X Y : set, X Y Y
Axiom. (binintersect_Subq_eq_1) We take the following as an axiom:
∀X Y, X YX Y = X
Axiom. (binintersect_Subq_max) We take the following as an axiom:
∀X Y Z : set, Z XZ YZ X Y
Axiom. (binintersect_asso) We take the following as an axiom:
∀X Y Z : set, X (Y Z) = (X Y) Z
Axiom. (binintersect_com) We take the following as an axiom:
∀X Y : set, X Y = Y X
Axiom. (binintersect_annil) We take the following as an axiom:
∀X : set, X =
Axiom. (binintersect_annir) We take the following as an axiom:
∀X : set, X =
Axiom. (binintersect_idem) We take the following as an axiom:
∀X : set, X X = X
Axiom. (binintersect_binunion_distr) We take the following as an axiom:
∀X Y Z : set, X (Y Z) = X Y X Z
Axiom. (binunion_binintersect_distr) We take the following as an axiom:
∀X Y Z : set, X Y Z = (X Y) (X Z)
Axiom. (Subq_binintersection_eq) We take the following as an axiom:
∀X Y : set, (X Y) = (X Y = X)
Axiom. (binintersect_nIn_I1) We take the following as an axiom:
∀X Y z : set, z Xz X Y
Axiom. (binintersect_nIn_I2) We take the following as an axiom:
∀X Y z : set, z Yz X Y
Axiom. (binintersect_nIn_E) We take the following as an axiom:
∀X Y z : set, z X Yz X z Y
Axiom. (binintersect_nIn_E_impred) We take the following as an axiom:
∀X Y z, z X Y∀p : prop, (z Xp)(z Yp)p
Axiom. (tab_pos_binintersect) We take the following as an axiom:
∀X Y x, x X Y(x Xx YFalse)False
Axiom. (tab_neg_binintersect) We take the following as an axiom:
∀X Y x, x X Y(x XFalse)(x YFalse)False
Axiom. (setminusI) We take the following as an axiom:
∀X Y z, (z X)(z Y)z X Y
Axiom. (setminusE) We take the following as an axiom:
∀X Y z, (z X Y)z X z Y
Axiom. (setminusE_impred) We take the following as an axiom:
∀X Y z, (z X Y)∀p : prop, (z Xz Yp)p
Axiom. (setminusE1) We take the following as an axiom:
∀X Y z, (z X Y)z X
Axiom. (setminusE2) We take the following as an axiom:
∀X Y z, (z X Y)z Y
Axiom. (setminus_Subq) We take the following as an axiom:
∀X Y : set, X Y X
Axiom. (setminus_Subq_contra) We take the following as an axiom:
∀X Y Z : set, Z YX Y X Z
Axiom. (setminus_nIn_I1) We take the following as an axiom:
∀X Y z, z Xz X Y
Axiom. (setminus_nIn_I2) We take the following as an axiom:
∀X Y z, z Yz X Y
Axiom. (setminus_nIn_E) We take the following as an axiom:
∀X Y z, z X Yz X z Y
Axiom. (setminus_nIn_E_impred) We take the following as an axiom:
∀X Y z, z X Y∀p : prop, (z Xp)(z Yp)p
Axiom. (setminus_selfannih) We take the following as an axiom:
∀X : set, (X X) =
Axiom. (setminus_binintersect) We take the following as an axiom:
∀X Y Z : set, X Y Z = (X Y) (X Z)
Axiom. (setminus_binunion) We take the following as an axiom:
∀X Y Z : set, X Y Z = (X Y) Z
Axiom. (binintersect_setminus) We take the following as an axiom:
∀X Y Z : set, (X Y) Z = X (Y Z)
Axiom. (binunion_setminus) We take the following as an axiom:
∀X Y Z : set, X Y Z = (X Z) (Y Z)
Axiom. (setminus_setminus) We take the following as an axiom:
∀X Y Z : set, X (Y Z) = (X Y) (X Z)
Axiom. (setminus_annil) We take the following as an axiom:
∀X : set, X =
Axiom. (setminus_idr) We take the following as an axiom:
∀X : set, X = X
Axiom. (tab_pos_setminus) We take the following as an axiom:
∀X Y x, x X Y(x Xx YFalse)False
Axiom. (tab_neg_setminus) We take the following as an axiom:
∀X Y x, x X Y(x XFalse)(x YFalse)False
Axiom. (eq_sym_i) We take the following as an axiom:
∀x y : set, x = yy = x
Axiom. (neq_sym_i) We take the following as an axiom:
∀x y : set, x yy x
Axiom. (In_irref) We take the following as an axiom:
∀x, x x
Axiom. (In_no2cycle) We take the following as an axiom:
∀x y, x yy xFalse
Axiom. (In_no3cycle) We take the following as an axiom:
∀x y z, x yy zz xFalse
Axiom. (ordsuccI1) We take the following as an axiom:
∀x : set, x ordsucc x
Axiom. (ordsuccI1b) We take the following as an axiom:
∀x y : set, y xy ordsucc x
Axiom. (ordsuccI2) We take the following as an axiom:
∀x : set, x ordsucc x
Axiom. (ordsuccE) We take the following as an axiom:
∀x y : set, y ordsucc xy x y = x
Axiom. (ordsuccE_impred) We take the following as an axiom:
∀x y : set, y ordsucc x∀p : prop, (y xp)(y = xp)p
Notation. Natural numbers 0,1,2,... are notation for the terms formed using as 0 and forming successors with ordsucc.
Axiom. (neq_0_ordsucc) We take the following as an axiom:
∀a : set, 0 ordsucc a
Axiom. (neq_ordsucc_0) We take the following as an axiom:
∀a : set, ordsucc a 0
Axiom. (ordsucc_inj) We take the following as an axiom:
∀a b : set, ordsucc a = ordsucc ba = b
Axiom. (ordsucc_inj_contra) We take the following as an axiom:
∀a b : set, a bordsucc a ordsucc b
Axiom. (In_0_1) We take the following as an axiom:
0 1
Axiom. (In_0_2) We take the following as an axiom:
0 2
Axiom. (In_1_2) We take the following as an axiom:
1 2
Axiom. (cases_1) We take the following as an axiom:
∀i1, ∀p : setprop, p 0p i
Axiom. (cases_2) We take the following as an axiom:
∀i2, ∀p : setprop, p 0p 1p i
Axiom. (cases_3) We take the following as an axiom:
∀i3, ∀p : setprop, p 0p 1p 2p i
Axiom. (cases_4) We take the following as an axiom:
∀i4, ∀p : setprop, p 0p 1p 2p 3p i
Axiom. (cases_5) We take the following as an axiom:
∀i5, ∀p : setprop, p 0p 1p 2p 3p 4p i
Axiom. (cases_6) We take the following as an axiom:
∀i6, ∀p : setprop, p 0p 1p 2p 3p 4p 5p i
Axiom. (cases_7) We take the following as an axiom:
∀i7, ∀p : setprop, p 0p 1p 2p 3p 4p 5p 6p i
Axiom. (cases_8) We take the following as an axiom:
∀i8, ∀p : setprop, p 0p 1p 2p 3p 4p 5p 6p 7p i
Axiom. (cases_9) We take the following as an axiom:
∀i9, ∀p : setprop, p 0p 1p 2p 3p 4p 5p 6p 7p 8p i
Axiom. (neq_0_1) We take the following as an axiom:
0 1
Axiom. (neq_1_0) We take the following as an axiom:
1 0
Axiom. (neq_0_2) We take the following as an axiom:
0 2
Axiom. (neq_2_0) We take the following as an axiom:
2 0
Axiom. (neq_1_2) We take the following as an axiom:
1 2
Axiom. (neq_2_1) We take the following as an axiom:
2 1
Axiom. (Subq_0_0) We take the following as an axiom:
0 0
Axiom. (Subq_0_1) We take the following as an axiom:
0 1
Axiom. (Subq_0_2) We take the following as an axiom:
0 2
Axiom. (Subq_1_1) We take the following as an axiom:
1 1
Axiom. (Subq_1_2) We take the following as an axiom:
1 2
Axiom. (Subq_2_2) We take the following as an axiom:
2 2
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. (nat_0) We take the following as an axiom:
nat_p 0
Axiom. (nat_ordsucc) We take the following as an axiom:
∀n : set, nat_p nnat_p (ordsucc n)
Axiom. (nat_1) We take the following as an axiom:
nat_p 1
Axiom. (nat_2) We take the following as an axiom:
nat_p 2
Axiom. (nat_0_in_ordsucc) We take the following as an axiom:
∀n, nat_p n0 ordsucc n
Axiom. (nat_ordsucc_in_ordsucc) We take the following as an axiom:
∀n, nat_p n∀mn, ordsucc m ordsucc n
Axiom. (nat_ind) We take the following as an axiom:
∀p : setprop, p 0(∀n, nat_p np np (ordsucc n))∀n, nat_p np n
Axiom. (nat_inv) We take the following as an axiom:
∀n, nat_p nn = 0 ∃x, nat_p x n = ordsucc x
Axiom. (nat_complete_ind) We take the following as an axiom:
∀p : setprop, (∀n, nat_p n(∀mn, p m)p n)∀n, nat_p np n
Axiom. (nat_p_trans) We take the following as an axiom:
∀n, nat_p n∀mn, nat_p m
Axiom. (nat_trans) We take the following as an axiom:
∀n, nat_p n∀mn, m n
Axiom. (nat_TransSet) We take the following as an axiom:
∀n, nat_p nTransSet n
Axiom. (nat_ordinal) We take the following as an axiom:
∀n, nat_p nordinal n
Axiom. (nat_ordsucc_trans) We take the following as an axiom:
∀n, nat_p n∀mordsucc n, m n
Axiom. (Union_ordsucc_eq) We take the following as an axiom:
∀n, nat_p n (ordsucc n) = n
Axiom. (In_0_3) We take the following as an axiom:
0 3
Axiom. (In_1_3) We take the following as an axiom:
1 3
Axiom. (In_2_3) We take the following as an axiom:
2 3
Axiom. (In_0_4) We take the following as an axiom:
0 4
Axiom. (In_1_4) We take the following as an axiom:
1 4
Axiom. (In_2_4) We take the following as an axiom:
2 4
Axiom. (In_3_4) We take the following as an axiom:
3 4
Axiom. (In_0_5) We take the following as an axiom:
0 5
Axiom. (In_1_5) We take the following as an axiom:
1 5
Axiom. (In_2_5) We take the following as an axiom:
2 5
Axiom. (In_3_5) We take the following as an axiom:
3 5
Axiom. (In_4_5) We take the following as an axiom:
4 5
Axiom. (In_0_6) We take the following as an axiom:
0 6
Axiom. (In_1_6) We take the following as an axiom:
1 6
Axiom. (In_2_6) We take the following as an axiom:
2 6
Axiom. (In_3_6) We take the following as an axiom:
3 6
Axiom. (In_4_6) We take the following as an axiom:
4 6
Axiom. (In_5_6) We take the following as an axiom:
5 6
Axiom. (In_0_7) We take the following as an axiom:
0 7
Axiom. (In_1_7) We take the following as an axiom:
1 7
Axiom. (In_2_7) We take the following as an axiom:
2 7
Axiom. (In_3_7) We take the following as an axiom:
3 7
Axiom. (In_4_7) We take the following as an axiom:
4 7
Axiom. (In_5_7) We take the following as an axiom:
5 7
Axiom. (In_6_7) We take the following as an axiom:
6 7
Axiom. (In_0_8) We take the following as an axiom:
0 8
Axiom. (In_1_8) We take the following as an axiom:
1 8
Axiom. (In_2_8) We take the following as an axiom:
2 8
Axiom. (In_3_8) We take the following as an axiom:
3 8
Axiom. (In_4_8) We take the following as an axiom:
4 8
Axiom. (In_5_8) We take the following as an axiom:
5 8
Axiom. (In_6_8) We take the following as an axiom:
6 8
Axiom. (In_7_8) We take the following as an axiom:
7 8
Axiom. (In_0_9) We take the following as an axiom:
0 9
Axiom. (In_1_9) We take the following as an axiom:
1 9
Axiom. (In_2_9) We take the following as an axiom:
2 9
Axiom. (In_3_9) We take the following as an axiom:
3 9
Axiom. (In_4_9) We take the following as an axiom:
4 9
Axiom. (In_5_9) We take the following as an axiom:
5 9
Axiom. (In_6_9) We take the following as an axiom:
6 9
Axiom. (In_7_9) We take the following as an axiom:
7 9
Axiom. (In_8_9) We take the following as an axiom:
8 9
Axiom. (nIn_0_0) We take the following as an axiom:
0 0
Axiom. (nIn_1_0) We take the following as an axiom:
1 0
Axiom. (nIn_2_0) We take the following as an axiom:
2 0
Axiom. (nIn_1_1) We take the following as an axiom:
1 1
Axiom. (nIn_2_1) We take the following as an axiom:
2 1
Axiom. (nIn_2_2) We take the following as an axiom:
2 2
Axiom. (nSubq_1_0) We take the following as an axiom:
1 0
Axiom. (nSubq_2_0) We take the following as an axiom:
2 0
Axiom. (nSubq_2_1) We take the following as an axiom:
2 1
Axiom. (exandE_ii) We take the following as an axiom:
∀P Q : (setset)prop, (∃x : setset, P x Q x)∀p : prop, (∀x : setset, P xQ xp)p
Axiom. (tab_pos_exactly1of2) We take the following as an axiom:
∀A B : prop, exactly1of2 A B(A¬ BFalse)(¬ ABFalse)False
Axiom. (tab_neg_exactly1of2) We take the following as an axiom:
∀A B : prop, ¬ exactly1of2 A B(ABFalse)(¬ A¬ BFalse)False
Axiom. (tab_pos_exactly1of3) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B C(A¬ B¬ CFalse)(¬ AB¬ CFalse)(¬ A¬ BCFalse)False
Axiom. (tab_neg_exactly1of3) We take the following as an axiom:
∀A B C : prop, ¬ exactly1of3 A B C(¬ A¬ B¬ CFalse)(ABFalse)(ACFalse)(BCFalse)False
Axiom. (Regularity) We take the following as an axiom:
∀X x : set, x X∃Y : set, Y X ¬ ∃z : set, z X z Y
Beginning of Section EpsilonRec
Variable F : set(setset)set
Axiom. (In_rec_G_i_c) We take the following as an axiom:
∀X : set, ∀f : setset, (∀xX, In_rec_G_i F x (f x))In_rec_G_i F X (F X f)
Axiom. (In_rec_G_i_inv) We take the following as an axiom:
∀X : set, ∀Y : set, In_rec_G_i F X Y∃f : setset, (∀xX, In_rec_G_i F x (f x)) Y = F X f
Hypothesis Fr : ∀X : set, ∀g h : setset, (∀xX, g x = h x)F X g = F X h
Axiom. (In_rec_G_i_f) We take the following as an axiom:
∀X : set, ∀Y Z : set, In_rec_G_i F X YIn_rec_G_i F X ZY = Z
Axiom. (In_rec_G_i_In_rec_i) We take the following as an axiom:
∀X : set, In_rec_G_i F X (In_rec_i F X)
Axiom. (In_rec_G_i_In_rec_d) We take the following as an axiom:
∀X : set, In_rec_G_i F X (F X (In_rec_i F))
Axiom. (In_rec_i_eq) We take the following as an axiom:
∀X : set, In_rec_i F X = F X (In_rec_i F)
End of Section EpsilonRec
Notation. Natural numbers 0,1,2,... are notation for the terms formed using as 0 and forming successors with ordsucc.
Axiom. (Inj1_eq) We take the following as an axiom:
∀X : set, Inj1 X = {0} {Inj1 x|xX}
Axiom. (Inj1I1) We take the following as an axiom:
∀X : set, 0 Inj1 X
Axiom. (Inj1I2) We take the following as an axiom:
∀X x : set, x XInj1 x Inj1 X
Axiom. (Inj1E) We take the following as an axiom:
∀X y : set, y Inj1 Xy = 0 ∃xX, y = Inj1 x
Axiom. (Inj1E_impred) We take the following as an axiom:
∀X y : set, y Inj1 X∀p : setprop, p 0(∀xX, p (Inj1 x))p y
Axiom. (Inj1NE1) We take the following as an axiom:
∀x : set, Inj1 x 0
Axiom. (Inj1NE2) We take the following as an axiom:
∀x : set, Inj1 x {0}
Axiom. (Inj0I) We take the following as an axiom:
∀X x : set, x XInj1 x Inj0 X
Axiom. (Inj0E) We take the following as an axiom:
∀X y : set, y Inj0 X∃x : set, x X y = Inj1 x
Axiom. (Inj0E_impred) We take the following as an axiom:
∀X y : set, y Inj0 X∀p : setprop, (∀x, x Xp (Inj1 x))p y
Axiom. (Unj_eq) We take the following as an axiom:
∀X : set, Unj X = {Unj x|xX {0}}
Axiom. (Unj_Inj1_eq) We take the following as an axiom:
∀X : set, Unj (Inj1 X) = X
Axiom. (Inj1_inj) We take the following as an axiom:
∀X Y : set, Inj1 X = Inj1 YX = Y
Axiom. (Unj_Inj0_eq) We take the following as an axiom:
∀X : set, Unj (Inj0 X) = X
Axiom. (Inj0_inj) We take the following as an axiom:
∀X Y : set, Inj0 X = Inj0 YX = Y
Axiom. (Inj0_0) We take the following as an axiom:
Inj0 0 = 0
Axiom. (Inj0_Inj1_neq) We take the following as an axiom:
∀X Y : set, Inj0 X Inj1 Y
Notation. We use + as an infix operator with priority 450 and which associates to the left corresponding to applying term setsum.
Axiom. (Inj0_setsum) We take the following as an axiom:
∀X Y x : set, x XInj0 x X + Y
Axiom. (Inj1_setsum) We take the following as an axiom:
∀X Y y : set, y YInj1 y X + Y
Axiom. (setsum_Inj_inv) We take the following as an axiom:
∀X Y z : set, z X + Y(∃xX, z = Inj0 x) (∃yY, z = Inj1 y)
Axiom. (setsum_Inj_inv_impred) We take the following as an axiom:
∀X Y z : set, z X + Y∀p : setprop, (∀xX, p (Inj0 x))(∀yY, p (Inj1 y))p z
Axiom. (Inj0_setsum_0L) We take the following as an axiom:
∀X : set, 0 + X = Inj0 X
Axiom. (setsum_mon) We take the following as an axiom:
∀X Y W Z, X WY ZX + Y W + Z
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
Axiom. (exandE_iii) We take the following as an axiom:
∀P Q : (setsetset)prop, (∃x : setsetset, P x Q x)∀p : prop, (∀x : setsetset, P xQ xp)p
Axiom. (exandE_iiii) We take the following as an axiom:
∀P Q : (setsetsetset)prop, (∃x : setsetsetset, P x Q x)∀p : prop, (∀x : setsetsetset, P xQ xp)p
Axiom. (exandE_iio) We take the following as an axiom:
∀P Q : (setsetprop)prop, (∃x : setsetprop, P x Q 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 x Q x)∀p : prop, (∀x : setsetsetprop, P xQ xp)p
Primitive. The name Descr_ii is a term of type ((setset)prop)(setset).
Axiom. (Descr_ii_prop) We take the following as an axiom:
∀P : (setset)prop, (∃f : setset, P f)(∀f g : setset, P fP gf = g)P (Descr_ii P)
Primitive. The name Descr_iii is a term of type ((setsetset)prop)(setsetset).
Axiom. (Descr_iii_prop) We take the following as an axiom:
∀P : (setsetset)prop, (∃f : setsetset, P f)(∀f g : setsetset, P fP gf = g)P (Descr_iii P)
Primitive. The name Descr_iio is a term of type ((setsetprop)prop)(setsetprop).
Axiom. (Descr_iio_prop) We take the following as an axiom:
∀P : (setsetprop)prop, (∃f : setsetprop, P f)(∀f g : setsetprop, P fP gf = g)P (Descr_iio P)
Primitive. The name Descr_Vo1 is a term of type (Vo 1prop)Vo 1.
Axiom. (Descr_Vo1_prop) We take the following as an axiom:
∀P : Vo 1prop, (∃f : Vo 1, P f)(∀f g : Vo 1, P fP gf = g)P (Descr_Vo1 P)
Primitive. The name Descr_Vo2 is a term of type (Vo 2prop)Vo 2.
Axiom. (Descr_Vo2_prop) We take the following as an axiom:
∀P : Vo 2prop, (∃f : Vo 2, P f)(∀f g : Vo 2, P fP gf = g)P (Descr_Vo2 P)
Primitive. The name Descr_Vo3 is a term of type (Vo 3prop)Vo 3.
Axiom. (Descr_Vo3_prop) We take the following as an axiom:
∀P : Vo 3prop, (∃f : Vo 3, P f)(∀f g : Vo 3, P fP gf = g)P (Descr_Vo3 P)
Primitive. The name Descr_Vo4 is a term of type (Vo 4prop)Vo 4.
Axiom. (Descr_Vo4_prop) We take the following as an axiom:
∀P : Vo 4prop, (∃f : Vo 4, P f)(∀f g : Vo 4, P fP gf = g)P (Descr_Vo4 P)
Primitive. The name If_ii is a term of type prop(setset)(setset)(setset).
Axiom. (If_ii_1) We take the following as an axiom:
∀p : prop, ∀x y : (setset), pIf_ii p x y = x
Axiom. (If_ii_0) We take the following as an axiom:
∀p : prop, ∀x y : (setset), ¬ pIf_ii p x y = y
Primitive. The name If_iii is a term of type prop(setsetset)(setsetset)(setsetset).
Axiom. (If_iii_1) We take the following as an axiom:
∀p : prop, ∀x y : (setsetset), pIf_iii p x y = x
Axiom. (If_iii_0) We take the following as an axiom:
∀p : prop, ∀x y : (setsetset), ¬ pIf_iii p x y = y
Primitive. The name If_iio is a term of type prop(setsetprop)(setsetprop)(setsetprop).
Axiom. (If_iio_1) We take the following as an axiom:
∀p : prop, ∀x y : (setsetprop), pIf_iio p x y = x
Axiom. (If_iio_0) We take the following as an axiom:
∀p : prop, ∀x y : (setsetprop), ¬ pIf_iio p x y = y
Primitive. The name If_Vo1 is a term of type propVo 1Vo 1Vo 1.
Axiom. (If_Vo1_1) We take the following as an axiom:
∀p : prop, ∀x y : Vo 1, pIf_Vo1 p x y = x
Axiom. (If_Vo1_0) We take the following as an axiom:
∀p : prop, ∀x y : Vo 1, ¬ pIf_Vo1 p x y = y
Primitive. The name If_Vo2 is a term of type propVo 2Vo 2Vo 2.
Axiom. (If_Vo2_1) We take the following as an axiom:
∀p : prop, ∀x y : Vo 2, pIf_Vo2 p x y = x
Axiom. (If_Vo2_0) We take the following as an axiom:
∀p : prop, ∀x y : Vo 2, ¬ pIf_Vo2 p x y = y
Primitive. The name If_Vo3 is a term of type propVo 3Vo 3Vo 3.
Axiom. (If_Vo3_1) We take the following as an axiom:
∀p : prop, ∀x y : Vo 3, pIf_Vo3 p x y = x
Axiom. (If_Vo3_0) We take the following as an axiom:
∀p : prop, ∀x y : Vo 3, ¬ pIf_Vo3 p x y = y
Primitive. The name If_Vo4 is a term of type propVo 4Vo 4Vo 4.
Axiom. (If_Vo4_1) We take the following as an axiom:
∀p : prop, ∀x y : Vo 4, pIf_Vo4 p x y = x
Axiom. (If_Vo4_0) We take the following as an axiom:
∀p : prop, ∀x y : Vo 4, ¬ pIf_Vo4 p x y = y
Primitive. The name In_rec_ii is a term of type (set(set(setset))(setset))set(setset).
Axiom. (In_rec_ii_eq) We take the following as an axiom:
∀F : set(set(setset))(setset), (∀X : set, ∀g h : set(setset), (∀xX, g x = h x)F X g = F X h)∀X : set, In_rec_ii F X = F X (In_rec_ii F)
Primitive. The name In_rec_iii is a term of type (set(set(setsetset))(setsetset))set(setsetset).
Axiom. (In_rec_iii_eq) We take the following as an axiom:
∀F : set(set(setsetset))(setsetset), (∀X : set, ∀g h : set(setsetset), (∀xX, g x = h x)F X g = F X h)∀X : set, In_rec_iii F X = F X (In_rec_iii F)
Primitive. The name In_rec_iio is a term of type (set(set(setsetprop))(setsetprop))set(setsetprop).
Axiom. (In_rec_iio_eq) We take the following as an axiom:
∀F : set(set(setsetprop))(setsetprop), (∀X : set, ∀g h : set(setsetprop), (∀xX, g x = h x)F X g = F X h)∀X : set, In_rec_iio F X = F X (In_rec_iio F)
Primitive. The name In_rec_Vo1 is a term of type (set(setVo 1)Vo 1)setVo 1.
Axiom. (In_rec_Vo1_eq) We take the following as an axiom:
∀F : set(setVo 1)Vo 1, (∀X : set, ∀g h : setVo 1, (∀xX, g x = h x)F X g = F X h)∀X : set, In_rec_Vo1 F X = F X (In_rec_Vo1 F)
Primitive. The name In_rec_Vo2 is a term of type (set(setVo 2)Vo 2)setVo 2.
Axiom. (In_rec_Vo2_eq) We take the following as an axiom:
∀F : set(setVo 2)Vo 2, (∀X : set, ∀g h : setVo 2, (∀xX, g x = h x)F X g = F X h)∀X : set, In_rec_Vo2 F X = F X (In_rec_Vo2 F)
Primitive. The name In_rec_Vo3 is a term of type (set(setVo 3)Vo 3)setVo 3.
Axiom. (In_rec_Vo3_eq) We take the following as an axiom:
∀F : set(setVo 3)Vo 3, (∀X : set, ∀g h : setVo 3, (∀xX, g x = h x)F X g = F X h)∀X : set, In_rec_Vo3 F X = F X (In_rec_Vo3 F)
Primitive. The name In_rec_Vo4 is a term of type (set(setVo 4)Vo 4)setVo 4.
Axiom. (In_rec_Vo4_eq) We take the following as an axiom:
∀F : set(setVo 4)Vo 4, (∀X : set, ∀g h : setVo 4, (∀xX, g x = h x)F X g = F X h)∀X : set, In_rec_Vo4 F X = F X (In_rec_Vo4 F)
Definition. We define incl_0_1 to be λx ⇒ λy ⇒ y x of type Vo 0Vo 1.
Definition. We define In_1 to be λX Y ⇒ ∃x : Vo 0, X = incl_0_1 x Y x of type Vo 1Vo 1prop.
Definition. We define incl_1_2 to be λX ⇒ λY ⇒ In_1 Y X of type Vo 1Vo 2.
Definition. We define In_2 to be λX Y ⇒ ∃x : Vo 1, X = incl_1_2 x Y x of type Vo 2Vo 2prop.
Definition. We define incl_2_3 to be λX ⇒ λY ⇒ In_2 Y X of type Vo 2Vo 3.
Definition. We define In_3 to be λX Y ⇒ ∃x : Vo 2, X = incl_2_3 x Y x of type Vo 3Vo 3prop.
Definition. We define incl_3_4 to be λX ⇒ λY ⇒ In_3 Y X of type Vo 3Vo 4.
Definition. We define In_4 to be λX Y ⇒ ∃x : Vo 3, X = incl_3_4 x Y x of type Vo 4Vo 4prop.
Axiom. (In_1_I) We take the following as an axiom:
∀x, ∀Y : Vo 1, Y xIn_1 (incl_0_1 x) Y
Axiom. (In_1_E) We take the following as an axiom:
∀X Y : Vo 1, In_1 X Y∀p : Vo 1prop, (∀x, Y xp (incl_0_1 x))p X
Axiom. (incl_0_1_inj) We take the following as an axiom:
∀x y, incl_0_1 x = incl_0_1 yx = y
Axiom. (In_1_up) We take the following as an axiom:
∀x y, x yIn_1 (incl_0_1 x) (incl_0_1 y)
Axiom. (In_1_down) We take the following as an axiom:
∀x y, In_1 (incl_0_1 x) (incl_0_1 y)x y
Axiom. (In_2_I) We take the following as an axiom:
∀x : Vo 1, ∀Y : Vo 2, Y xIn_2 (incl_1_2 x) Y
Axiom. (In_2_E) We take the following as an axiom:
∀X Y : Vo 2, In_2 X Y∀p : Vo 2prop, (∀x : Vo 1, Y xp (incl_1_2 x))p X
Axiom. (incl_1_2_inj) We take the following as an axiom:
∀x y : Vo 1, incl_1_2 x = incl_1_2 yx = y
Axiom. (In_2_up) We take the following as an axiom:
∀x y : Vo 1, In_1 x yIn_2 (incl_1_2 x) (incl_1_2 y)
Axiom. (In_2_down) We take the following as an axiom:
∀x y : Vo 1, In_2 (incl_1_2 x) (incl_1_2 y)In_1 x y
Axiom. (In_3_I) We take the following as an axiom:
∀x : Vo 2, ∀Y : Vo 3, Y xIn_3 (incl_2_3 x) Y
Axiom. (In_3_E) We take the following as an axiom:
∀X Y : Vo 3, In_3 X Y∀p : Vo 3prop, (∀x : Vo 2, Y xp (incl_2_3 x))p X
Axiom. (incl_2_3_inj) We take the following as an axiom:
∀x y : Vo 2, incl_2_3 x = incl_2_3 yx = y
Axiom. (In_3_up) We take the following as an axiom:
∀x y : Vo 2, In_2 x yIn_3 (incl_2_3 x) (incl_2_3 y)
Axiom. (In_3_down) We take the following as an axiom:
∀x y : Vo 2, In_3 (incl_2_3 x) (incl_2_3 y)In_2 x y
Axiom. (In_4_I) We take the following as an axiom:
∀x : Vo 3, ∀Y : Vo 4, Y xIn_4 (incl_3_4 x) Y
Axiom. (In_4_E) We take the following as an axiom:
∀X Y : Vo 4, In_4 X Y∀p : Vo 4prop, (∀x : Vo 3, Y xp (incl_3_4 x))p X
Axiom. (incl_3_4_inj) We take the following as an axiom:
∀x y : Vo 3, incl_3_4 x = incl_3_4 yx = y
Axiom. (In_4_up) We take the following as an axiom:
∀x y : Vo 3, In_3 x yIn_4 (incl_3_4 x) (incl_3_4 y)
Axiom. (In_4_down) We take the following as an axiom:
∀x y : Vo 3, In_4 (incl_3_4 x) (incl_3_4 y)In_3 x y
Axiom. (PowerI2) We take the following as an axiom:
∀X Y, (∀yY, y X)Y 𝒫 X
Axiom. (PowerE2) We take the following as an axiom:
∀X Y, Y 𝒫 X∀yY, y 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
Let pair : setsetsetsetsum
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
Axiom. (Inj0_pair_0_eq) We take the following as an axiom:
Inj0 = pair 0
Axiom. (Inj1_pair_1_eq) We take the following as an axiom:
Inj1 = pair 1
Axiom. (pairI0) We take the following as an axiom:
∀X Y x, x Xpair 0 x pair X Y
Axiom. (pairI1) We take the following as an axiom:
∀X Y y, y Ypair 1 y pair X Y
Axiom. (pairE) We take the following as an axiom:
∀X Y z, z pair X Y(∃xX, z = pair 0 x) (∃yY, z = pair 1 y)
Axiom. (pairE_impred) We take the following as an axiom:
∀X Y z, z pair X Y∀p : setprop, (∀xX, p (pair 0 x))(∀yY, p (pair 1 y))p z
Axiom. (pairE0) We take the following as an axiom:
∀X Y x, pair 0 x pair X Yx X
Axiom. (pairE1) We take the following as an axiom:
∀X Y y, pair 1 y pair X Yy Y
Axiom. (pairEq) We take the following as an axiom:
∀X Y z, z pair X Y (∃xX, z = pair 0 x) (∃yY, z = pair 1 y)
Axiom. (pairSubq) We take the following as an axiom:
∀X Y W Z, X WY Zpair X Y pair W Z
Axiom. (proj0I) We take the following as an axiom:
∀w u : set, pair 0 u wu proj0 w
Axiom. (proj0E) We take the following as an axiom:
∀w u : set, u proj0 wpair 0 u w
Axiom. (proj1I) We take the following as an axiom:
∀w u : set, pair 1 u wu proj1 w
Axiom. (proj1E) We take the following as an axiom:
∀w u : set, u proj1 wpair 1 u w
Axiom. (proj0_pair_eq) We take the following as an axiom:
∀X Y : set, proj0 (pair X Y) = X
Axiom. (proj1_pair_eq) We take the following as an axiom:
∀X Y : set, proj1 (pair X Y) = Y
Axiom. (pair_inj) We take the following as an axiom:
∀x y w z : set, pair x y = pair w zx = w y = z
Axiom. (pair_eta_Subq_proj) We take the following as an axiom:
∀w, pair (proj0 w) (proj1 w) w
Let Sigma : set(setset)setlam
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
Axiom. (pair_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀xX, ∀yY x, pair x y xX, Y x
Axiom. (Sigma_eta_proj0_proj1) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z(xX, Y x), pair (proj0 z) (proj1 z) = z proj0 z X proj1 z Y (proj0 z)
Axiom. (proj_Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z(xX, Y x), pair (proj0 z) (proj1 z) = z
Axiom. (proj0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj0 z X
Axiom. (proj1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj1 z Y (proj0 z)
Axiom. (pair_Sigma_E0) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀x y : set, pair x y (xX, Y x)x X
Axiom. (pair_Sigma_E1) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀x y : set, pair x y (xX, Y x)y Y x
Axiom. (Sigma_E) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)∃xX, ∃yY x, z = pair x y
Axiom. (Sigma_Eq) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x) ∃xX, ∃yY x, z = pair x y
Axiom. (Sigma_mon) We take the following as an axiom:
∀X Y : set, X Y∀Z W : setset, (∀xX, Z x W x)(xX, Z x) yY, W y
Axiom. (Sigma_mon0) We take the following as an axiom:
∀X Y : set, X Y∀Z : setset, (xX, Z x) yY, Z y
Axiom. (Sigma_mon1) We take the following as an axiom:
∀X : set, ∀Z W : setset, (∀x, x XZ x W x)(xX, Z x) xX, W x
Axiom. (Sigma_Power_1) We take the following as an axiom:
∀X : set, X 𝒫 1∀Y : setset, (∀xX, Y x 𝒫 1)(xX, Y x) 𝒫 1
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, ∀(xX)(yY), pair x y X Y
Axiom. (proj0_setprod) We take the following as an axiom:
∀X Y : set, ∀zX Y, proj0 z X
Axiom. (proj1_setprod) We take the following as an axiom:
∀X Y : set, ∀zX Y, proj1 z Y
Axiom. (setprod_mon) We take the following as an axiom:
∀X Y : set, X Y∀Z W : set, Z WX Z Y W
Axiom. (setprod_mon0) We take the following as an axiom:
∀X Y : set, X Y∀Z : set, X Z Y Z
Axiom. (setprod_mon1) We take the following as an axiom:
∀X : set, ∀Z W : set, Z WX Z X W
Axiom. (pair_setprod_E0) We take the following as an axiom:
∀X Y x y : set, pair x y X Yx X
Axiom. (pair_setprod_E1) We take the following as an axiom:
∀X Y x y : set, pair x y X Yy Y
Notation. When x is a set, a term x y is notation for ap x y.
Notation. λ xAB is notation for the set lam Ax : set ⇒ B).
Notation. We now use n-tuple notation (a0,...,an-1) for n ≥ 2 for λ i ∈ n . if i = 0 then a0 else ... if i = n-2 then an-2 else an-1.
Axiom. (lamI) We take the following as an axiom:
∀X : set, ∀F : setset, ∀xX, ∀yF x, pair x y λxXF x
Axiom. (lamE) We take the following as an axiom:
∀X : set, ∀F : setset, ∀z : set, z (λxXF x)∃xX, ∃yF x, z = pair x y
Axiom. (lamEq) We take the following as an axiom:
∀X : set, ∀F : setset, ∀z, z (λxXF x) ∃xX, ∃yF x, z = pair x y
Axiom. (apI) We take the following as an axiom:
∀f x y, pair x y fy f x
Axiom. (apE) We take the following as an axiom:
∀f x y, y f xpair x y f
Axiom. (apEq) We take the following as an axiom:
∀f x y, y f x pair x y f
Axiom. (beta) We take the following as an axiom:
∀X : set, ∀F : setset, ∀x : set, x X(λxXF x) x = F x
Axiom. (beta0) We take the following as an axiom:
∀X : set, ∀F : setset, ∀x : set, x X(λxXF x) x = 0
Axiom. (neq_3_0) We take the following as an axiom:
3 0
Axiom. (neq_3_1) We take the following as an axiom:
3 1
Axiom. (neq_3_2) We take the following as an axiom:
3 2
Axiom. (neq_4_0) We take the following as an axiom:
4 0
Axiom. (neq_4_1) We take the following as an axiom:
4 1
Axiom. (neq_4_2) We take the following as an axiom:
4 2
Axiom. (neq_4_3) We take the following as an axiom:
4 3
Axiom. (neq_5_0) We take the following as an axiom:
5 0
Axiom. (neq_5_1) We take the following as an axiom:
5 1
Axiom. (neq_5_2) We take the following as an axiom:
5 2
Axiom. (neq_5_3) We take the following as an axiom:
5 3
Axiom. (neq_5_4) We take the following as an axiom:
5 4
Axiom. (neq_6_0) We take the following as an axiom:
6 0
Axiom. (neq_6_1) We take the following as an axiom:
6 1
Axiom. (neq_6_2) We take the following as an axiom:
6 2
Axiom. (neq_6_3) We take the following as an axiom:
6 3
Axiom. (neq_6_4) We take the following as an axiom:
6 4
Axiom. (neq_6_5) We take the following as an axiom:
6 5
Axiom. (neq_7_0) We take the following as an axiom:
7 0
Axiom. (neq_7_1) We take the following as an axiom:
7 1
Axiom. (neq_7_2) We take the following as an axiom:
7 2
Axiom. (neq_7_3) We take the following as an axiom:
7 3
Axiom. (neq_7_4) We take the following as an axiom:
7 4
Axiom. (neq_7_5) We take the following as an axiom:
7 5
Axiom. (neq_7_6) We take the following as an axiom:
7 6
Axiom. (neq_8_0) We take the following as an axiom:
8 0
Axiom. (neq_8_1) We take the following as an axiom:
8 1
Axiom. (neq_8_2) We take the following as an axiom:
8 2
Axiom. (neq_8_3) We take the following as an axiom:
8 3
Axiom. (neq_8_4) We take the following as an axiom:
8 4
Axiom. (neq_8_5) We take the following as an axiom:
8 5
Axiom. (neq_8_6) We take the following as an axiom:
8 6
Axiom. (neq_8_7) We take the following as an axiom:
8 7
Axiom. (neq_9_0) We take the following as an axiom:
9 0
Axiom. (neq_9_1) We take the following as an axiom:
9 1
Axiom. (neq_9_2) We take the following as an axiom:
9 2
Axiom. (neq_9_3) We take the following as an axiom:
9 3
Axiom. (neq_9_4) We take the following as an axiom:
9 4
Axiom. (neq_9_5) We take the following as an axiom:
9 5
Axiom. (neq_9_6) We take the following as an axiom:
9 6
Axiom. (neq_9_7) We take the following as an axiom:
9 7
Axiom. (neq_9_8) We take the following as an axiom:
9 8
Axiom. (TransSetIb) We take the following as an axiom:
∀X, (∀xX, ∀yx, y X)TransSet X
Axiom. (TransSetEb) We take the following as an axiom:
∀X, TransSet X∀xX, ∀yx, y X
Axiom. (ordinal_TransSet) We take the following as an axiom:
∀alpha, ordinal alphaTransSet alpha
Axiom. (ordinal_TransSet_b) We take the following as an axiom:
∀alpha, ordinal alpha∀betaalpha, ∀gammabeta, gamma alpha
Axiom. (ordinal_In_TransSet) We take the following as an axiom:
∀alpha : set, ordinal alpha∀betaalpha, TransSet beta
Axiom. (ordinal_In_TransSet_b) We take the following as an axiom:
∀alpha : set, ordinal alpha∀betaalpha, ∀gammabeta, ∀deltagamma, delta beta
Axiom. (ordinal_Empty) We take the following as an axiom:
ordinal
Axiom. (ordinal_Hered) We take the following as an axiom:
∀alpha : set, ordinal alpha∀betaalpha, ordinal beta
Axiom. (ordinal_ind) We take the following as an axiom:
∀p : setprop, (∀alpha, ordinal alpha(∀betaalpha, p beta)p alpha)∀alpha, ordinal alphap alpha
Axiom. (least_ordinal_ex) We take the following as an axiom:
∀p : setprop, (∃alpha, ordinal alpha p alpha)∃alpha, ordinal alpha p alpha ∀betaalpha, ¬ p beta
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. (TransSet_ordsucc_In_Subq) We take the following as an axiom:
∀X : set, TransSet X∀xX, ordsucc x X
Axiom. (ordinal_ordsucc_In_Subq) We take the following as an axiom:
∀alpha, ordinal alpha∀betaalpha, ordsucc beta alpha
Axiom. (ordinal_trichotomy_or) We take the following as an axiom:
∀alpha beta : set, ordinal alphaordinal betaalpha beta alpha = beta beta alpha
Axiom. (ordinal_trichotomy_or_impred) We take the following as an axiom:
∀alpha beta : set, ordinal alphaordinal beta∀p : prop, (alpha betap)(alpha = betap)(beta alphap)p
Axiom. (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. (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. (ordinal_trichotomy) We take the following as an axiom:
∀alpha beta : set, ordinal alphaordinal betaexactly1of3 (alpha beta) (alpha = beta) (beta alpha)
Axiom. (ordinal_In_Or_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha beta beta alpha
Axiom. (ordinal_linear) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha beta beta alpha
Axiom. (ordinal_ordsucc_In_eq) We take the following as an axiom:
∀alpha beta, ordinal alphabeta alphaordsucc beta alpha alpha = ordsucc beta
Axiom. (ordinal_lim_or_succ) We take the following as an axiom:
∀alpha, ordinal alpha(∀betaalpha, ordsucc beta alpha) (∃betaalpha, alpha = ordsucc beta)
Axiom. (ordinal_ordsucc_In) We take the following as an axiom:
∀alpha, ordinal alpha∀betaalpha, ordsucc beta ordsucc alpha
Axiom. (ordinal_Union) We take the following as an axiom:
∀X, (∀xX, ordinal x)ordinal ( X)
Axiom. (ordinal_famunion) We take the following as an axiom:
∀X, ∀F : setset, (∀xX, ordinal (F x))ordinal (xXF x)
Axiom. (ordinal_binintersect) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaordinal (alpha beta)
Axiom. (ordinal_binunion) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaordinal (alpha beta)
Axiom. (ordinal_Sep) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, (∀betaalpha, ∀gammabeta, p betap gamma)ordinal {betaalpha|p beta}
Definition. We define down_1_0 to be λX ⇒ Eps_i (λx ⇒ incl_0_1 x = X) of type Vo 1Vo 0.
Definition. We define down_2_1 to be λX ⇒ Descr_Vo1 (λx ⇒ incl_1_2 x = X) of type Vo 2Vo 1.
Definition. We define down_3_2 to be λX ⇒ Descr_Vo2 (λx ⇒ incl_2_3 x = X) of type Vo 3Vo 2.
Definition. We define down_4_3 to be λX ⇒ Descr_Vo3 (λx ⇒ incl_3_4 x = X) of type Vo 4Vo 3.
Definition. We define AC_1 to be ∃C : (Vo 1prop)Vo 1, ∀P : Vo 1prop, ∀x : Vo 1, P xP (C P) of type prop.
Definition. We define AC_2 to be ∃C : (Vo 2prop)Vo 2, ∀P : Vo 2prop, ∀x : Vo 2, P xP (C P) of type prop.
Definition. We define AC_3 to be ∃C : (Vo 3prop)Vo 3, ∀P : Vo 3prop, ∀x : Vo 3, P xP (C P) of type prop.
Axiom. (down_1_0_incl_0_1) We take the following as an axiom:
∀x, down_1_0 (incl_0_1 x) = x
Axiom. (down_2_1_incl_1_2) We take the following as an axiom:
∀x : Vo 1, down_2_1 (incl_1_2 x) = x
Axiom. (down_3_2_incl_2_3) We take the following as an axiom:
∀x : Vo 2, down_3_2 (incl_2_3 x) = x
Axiom. (down_4_3_incl_3_4) We take the following as an axiom:
∀x : Vo 3, down_4_3 (incl_3_4 x) = x
Axiom. (AC_3_imp_AC_2) We take the following as an axiom:
AC_3AC_2
Axiom. (AC_2_imp_AC_1) We take the following as an axiom:
AC_2AC_1
Axiom. (Skolem_0) We take the following as an axiom:
∀r : setsetprop, (∀x, ∃y, r x y)∃f : setset, ∀x, r x (f x)
Axiom. (Skolem_0_bdd) We take the following as an axiom:
∀X : set, ∀r : setsetprop, (∀xX, ∃y, r x y)∃f : setset, ∀xX, r x (f x)
Axiom. (Skolem_1) We take the following as an axiom:
AC_1∀r : Vo 1Vo 1prop, (∀x : Vo 1, ∃y : Vo 1, r x y)∃f : Vo 1Vo 1, ∀x : Vo 1, r x (f x)
Axiom. (Skolem_1_bdd) We take the following as an axiom:
AC_1∀X : Vo 1, ∀r : Vo 1Vo 1prop, (∀x : Vo 1, In_1 x X∃y : Vo 1, r x y)∃f : Vo 1Vo 1, ∀x : Vo 1, In_1 x Xr x (f x)
Axiom. (Skolem_2) We take the following as an axiom:
AC_2∀r : Vo 2Vo 2prop, (∀x : Vo 2, ∃y : Vo 2, r x y)∃f : Vo 2Vo 2, ∀x : Vo 2, r x (f x)
Axiom. (Skolem_2_bdd) We take the following as an axiom:
AC_2∀X : Vo 2, ∀r : Vo 2Vo 2prop, (∀x : Vo 2, In_2 x X∃y : Vo 2, r x y)∃f : Vo 2Vo 2, ∀x : Vo 2, In_2 x Xr x (f x)
Axiom. (Skolem_3) We take the following as an axiom:
AC_3∀r : Vo 3Vo 3prop, (∀x : Vo 3, ∃y : Vo 3, r x y)∃f : Vo 3Vo 3, ∀x : Vo 3, r x (f x)
Axiom. (Skolem_3_bdd) We take the following as an axiom:
AC_3∀X : Vo 3, ∀r : Vo 3Vo 3prop, (∀x : Vo 3, In_3 x X∃y : Vo 3, r x y)∃f : Vo 3Vo 3, ∀x : Vo 3, In_3 x Xr x (f x)
Axiom. (proj0_ap_0) We take the following as an axiom:
∀u, proj0 u = u 0
Axiom. (proj1_ap_1) We take the following as an axiom:
∀u, proj1 u = u 1
Axiom. (pair_ap_0) We take the following as an axiom:
∀x y : set, (pair x y) 0 = x
Axiom. (pair_ap_1) We take the following as an axiom:
∀x y : set, (pair x y) 1 = y
Axiom. (pair_ap_n2) We take the following as an axiom:
∀x y i : set, i 2(pair x y) i = 0
Axiom. (pair_eta_Subq) We take the following as an axiom:
∀w, pair (w 0) (w 1) w
Axiom. (ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 0) X
Axiom. (ap1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 1) (Y (z 0))
Axiom. (Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z(xX, Y x), pair (z 0) (z 1) = z
Axiom. (ReplEq_setprod_ext) We take the following as an axiom:
∀X Y, ∀F G : setsetset, (∀xX, ∀yY, F x y = G x y){F (w 0) (w 1)|wX Y} = {G (w 0) (w 1)|wX Y}
Axiom. (setsum_p_E) We take the following as an axiom:
∀u, setsum_p u∀p : setprop, (∀x y, p (setsum x y))p u
Axiom. (setsum_p_I) We take the following as an axiom:
∀x y, setsum_p (setsum x y)
Axiom. (setsum_p_I2) We take the following as an axiom:
∀w, (∀uw, setsum_p u u 0 2)setsum_p w
Axiom. (setsum_p_In_ap) We take the following as an axiom:
∀w f, setsum_p ww fw 1 ap f (w 0)
Axiom. (pred_ext_i) We take the following as an axiom:
∀p q : setprop, (∀x, p xq x)(∀x, q xp x)p = q
Axiom. (setsum_p_tuple2) We take the following as an axiom:
setsum_p = tuple_p 2
Axiom. (tuple_p_2_tuple) We take the following as an axiom:
∀x y : set, tuple_p 2 (x,y)
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. (tuple_pair) We take the following as an axiom:
∀x y : set, pair x y = (x,y)
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
Axiom. (PiI) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, (∀uf, setsum_p u u 0 X)(∀xX, f x Y x)f xX, Y x
Axiom. (PiE_impred) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, f (xX, Y x)∀p : prop, ((∀uf, setsum_p u u 0 X)(∀xX, f x Y x)p)p
Axiom. (PiE) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, f (xX, Y x)(∀uf, setsum_p u u 0 X) (∀xX, f x Y x)
Axiom. (PiEq) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, f Pi X Y (∀uf, setsum_p u u 0 X) (∀xX, f x Y x)
Axiom. (lam_Pi) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀F : setset, (∀xX, F x Y x)(λxXF x) (xX, Y x)
Axiom. (ap_Pi) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, ∀x : set, f (xX, Y x)x Xf x Y x
Axiom. (Pi_ext_Subq) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f g(xX, Y x), (∀xX, f x g x)f g
Axiom. (Pi_ext) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f g(xX, Y x), (∀xX, f x = g x)f = g
Axiom. (Pi_eta) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, f (xX, Y x)(λxXf x) = f
Axiom. (Pi_Power_1) We take the following as an axiom:
∀X : set, ∀Y : setset, (∀xX, Y x 𝒫 1)(xX, Y x) 𝒫 1
Axiom. (Pi_0_dom_mon) We take the following as an axiom:
∀X Y : set, ∀A : setset, X Y(∀yY, y X0 A y)(xX, A x) yY, A y
Axiom. (Pi_cod_mon) We take the following as an axiom:
∀X : set, ∀A B : setset, (∀xX, A x B x)(xX, A x) xX, B x
Axiom. (Pi_0_mon) We take the following as an axiom:
∀X Y : set, ∀A B : setset, (∀xX, A x B x)X Y(∀yY, y X0 B y)(xX, A x) yY, B y
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
Axiom. (setexp_2_eq) We take the following as an axiom:
∀X : set, X X = X2
Axiom. (setexp_0_dom_mon) We take the following as an axiom:
∀A : set, 0 A∀X Y : set, X YAX AY
Axiom. (setexp_0_mon) We take the following as an axiom:
∀X Y A B : set, 0 BA BX YAX BY
Axiom. (nat_in_setexp_mon) We take the following as an axiom:
∀A : set, 0 A∀n, nat_p n∀mn, Am An
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
Variable 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
End of Section Tuples
Axiom. (pair_tuple_fun) We take the following as an axiom:
pair = (λx y ⇒ (x,y))
Axiom. (tupleI0) We take the following as an axiom:
∀X Y x, x X(0,x) (X,Y)
Axiom. (tupleI1) We take the following as an axiom:
∀X Y y, y Y(1,y) (X,Y)
Axiom. (tupleE) We take the following as an axiom:
∀X Y z, z (X,Y)(∃xX, z = (0,x)) (∃yY, z = (1,y))
Axiom. (tuple_2_inj) We take the following as an axiom:
∀x y w z : set, (x,y) = (w,z)x = w y = z
Axiom. (tuple_2_inj_impred) We take the following as an axiom:
∀x y w z : set, (x,y) = (w,z)∀p : prop, (x = wy = zp)p
Axiom. (tuple_2_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀xX, ∀yY x, (x,y) xX, Y x
Axiom. (tuple_2_setprod) We take the following as an axiom:
∀X : set, ∀Y : set, ∀xX, ∀yY, (x,y) X Y
Axiom. (tuple_Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z(xX, Y x), (z 0,z 1) = z
Axiom. (lamI2) We take the following as an axiom:
∀X, ∀F : setset, ∀xX, ∀yF x, (x,y) λxXF x
Axiom. (lamE2) We take the following as an axiom:
∀X, ∀F : setset, ∀z : set, z (λxXF x)∃xX, ∃yF x, z = (x,y)
Axiom. (lamE_impred) We take the following as an axiom:
∀X, ∀F : setset, ∀z : set, z (λxXF x)∀p : setprop, (∀xX, ∀yF x, p (pair x y))p z
Axiom. (lamE2_impred) We take the following as an axiom:
∀X, ∀F : setset, ∀z : set, z (λxXF x)∀p : setprop, (∀xX, ∀yF x, p (x,y))p z
Axiom. (apI2) We take the following as an axiom:
∀f x y, (x,y) fy f x
Axiom. (apE2) We take the following as an axiom:
∀f x y, y f x(x,y) f
Axiom. (ap_const_0) We take the following as an axiom:
∀x, 0 x = 0
Axiom. (lam_ext_sub) We take the following as an axiom:
∀X, ∀F G : setset, (∀xX, F x = G x)(λxXF x) (λxXG x)
Axiom. (lam_ext) We take the following as an axiom:
∀X, ∀F G : setset, (∀xX, F x = G x)(λxXF x) = (λxXG x)
Axiom. (lam_eta) We take the following as an axiom:
∀X, ∀F : setset, (λxX(λxXF x) x) = (λxXF x)
Axiom. (tuple_2_eta) We take the following as an axiom:
∀x y, (λi2(x,y) i) = (x,y)
Axiom. (tuple_3_eta) We take the following as an axiom:
∀x y z, (λi3(x,y,z) i) = (x,y,z)
Axiom. (tuple_4_eta) We take the following as an axiom:
∀x y z w, (λi4(x,y,z,w) i) = (x,y,z,w)
Axiom. (Sep2I) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀xX, ∀yY x, R x y(x,y) Sep2 X Y R
Axiom. (Sep2E_impred) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀uSep2 X Y R, ∀p : setprop, (∀xX, ∀yY x, R x yp (x,y))p u
Axiom. (Sep2E) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀uSep2 X Y R, ∃xX, ∃yY x, u = (x,y) R x y
Axiom. (Sep2E'_impred) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀x y, (x,y) Sep2 X Y R∀p : prop, (x Xy Y xR x yp)p
Axiom. (Sep2E'1) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀x y, (x,y) Sep2 X Y Rx X
Axiom. (Sep2E'2) We take the following as an axiom:
∀X, ∀Y : setset, ∀R : setsetprop, ∀x y, (x,y) Sep2 X Y Ry Y 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
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, (∀xX, ∀yY x, R x y R' x y)Sep2 X Y R = Sep2 X Y R'
Axiom. (beta2) We take the following as an axiom:
∀X, ∀Y : setset, ∀F : setsetset, ∀xX, ∀yY 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, (∀xX, ∀yY x, F x y = G x y)lam2 X Y F = lam2 X Y G
Axiom. (tuple_2_in_A_2) We take the following as an axiom:
∀x y A, x Ay A(x,y) A2
Axiom. (tuple_3_in_A_3) We take the following as an axiom:
∀x y z A, x Ay Az A(x,y,z) A3
Axiom. (injI) We take the following as an axiom:
∀X Y, ∀f : setset, (∀xX, f x Y)(∀x zX, f x = f zx = z)inj X Y f
Axiom. (injE_impred) We take the following as an axiom:
∀X Y, ∀f : setset, inj X Y f∀p : prop, ((∀xX, f x Y)(∀x zX, f x = f zx = z)p)p
Axiom. (bijI) We take the following as an axiom:
∀X Y, ∀f : setset, inj X Y f(∀yY, ∃xX, f x = y)bij X Y f
Axiom. (bijE_impred) We take the following as an axiom:
∀X Y, ∀f : setset, bij X Y f∀p : prop, (inj X Y f(∀yY, ∃xX, f x = y)p)p
Axiom. (PigeonHole_nat) We take the following as an axiom:
∀n, nat_p n∀f : setset, (∀iordsucc n, f i n)¬ (∀i jordsucc n, f i = f ji = j)
Axiom. (PigeonHole_nat_bij) We take the following as an axiom:
∀n, nat_p n∀f : setset, (∀in, f i n)(∀i jn, f i = f ji = j)bij n n f
Axiom. (tuple_2_bij_2) We take the following as an axiom:
∀x y, x 2y 2x ybij 2 2 (λi ⇒ (x,y) i)
Axiom. (tuple_3_bij_3) We take the following as an axiom:
∀x y z, x 3y 3z 3x yx zy zbij 3 3 (λi ⇒ (x,y,z) i)
Axiom. (In_irref_b) We take the following as an axiom:
∀X, X XFalse
Axiom. (neq_i_E) We take the following as an axiom:
∀x y, x yx = y∀p : prop, p
Axiom. (neq_i_sym_E) We take the following as an axiom:
∀x y, x yy = x∀p : prop, p
Beginning of Section Tuples
Variable x0 x1 x2 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
Axiom. (tuple_4_in_A_4) We take the following as an axiom:
∀x y z w A, x Ay Az Aw A(x,y,z,w) A4
Axiom. (tuple_4_bij_4) We take the following as an axiom:
∀x y z w, x 4y 4z 4w 4x yx zx wy zy wz wbij 4 4 (λi ⇒ (x,y,z,w) i)
Axiom. (V_eq) We take the following as an axiom:
∀X : set, V_ X = xX𝒫 (V_ x)
Axiom. (V_I) We take the following as an axiom:
∀y x X : set, x Xy V_ xy V_ X
Axiom. (V_E) We take the following as an axiom:
∀y X : set, y V_ X∀p : prop, (∀xX, y V_ xp)p
Axiom. (V_Subq) We take the following as an axiom:
∀X : set, X V_ X
Axiom. (V_Subq_2) We take the following as an axiom:
∀X Y : set, X V_ YV_ X V_ Y
Axiom. (V_In) We take the following as an axiom:
∀X Y : set, X V_ YV_ X V_ Y
Axiom. (V_In_or_Subq) We take the following as an axiom:
∀X Y : set, X V_ Y V_ Y V_ X
Axiom. (V_In_or_Subq_2) We take the following as an axiom:
∀X Y : set, V_ X V_ Y V_ Y V_ X
Axiom. (iff_refl) We take the following as an axiom:
∀A : prop, A A
Axiom. (iff_sym) We take the following as an axiom:
∀A B : prop, (A B)(B A)
Axiom. (iff_trans) We take the following as an axiom:
∀A B C : prop, (A B)(B C)(A C)
Axiom. (PNoEq_ref_) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoEq_ alpha p p
Axiom. (PNoEq_sym_) We take the following as an axiom:
∀alpha, ∀p q : setprop, PNoEq_ alpha p qPNoEq_ alpha q p
Axiom. (PNoEq_tra_) We take the following as an axiom:
∀alpha, ∀p q r : setprop, PNoEq_ alpha p qPNoEq_ alpha q rPNoEq_ alpha p r
Axiom. (PNoEq_antimon_) We take the following as an axiom:
∀p q : setprop, ∀alpha, ordinal alpha∀betaalpha, PNoEq_ alpha p qPNoEq_ beta p q
Axiom. (PNoLt_E_) We take the following as an axiom:
∀alpha, ∀p q : setprop, PNoLt_ alpha p q∀R : prop, (∀beta, beta alphaPNoEq_ beta p q¬ p betaq betaR)R
Axiom. (PNoLt_irref_) We take the following as an axiom:
∀alpha, ∀p : setprop, ¬ PNoLt_ alpha p p
Axiom. (PNoLt_irref__b) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoLt_ alpha p pFalse
Axiom. (PNoLt_mon_) We take the following as an axiom:
∀p q : setprop, ∀alpha, ordinal alpha∀betaalpha, PNoLt_ beta p qPNoLt_ alpha p q
Axiom. (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. (PNoLt_trichotomy_or_) We take the following as an axiom:
∀p q : setprop, ∀alpha, ordinal alphaPNoLt_ alpha p q PNoEq_ alpha p q PNoLt_ alpha q p
Axiom. (PNoLt_trichotomy_or__impred) We take the following as an axiom:
∀p q : setprop, ∀alpha, ordinal alpha∀r : prop, (PNoLt_ alpha p qr)(PNoEq_ alpha p qr)(PNoLt_ alpha q pr)r
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
Axiom. (PNoLtI1) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, PNoLt_ (alpha beta) p qPNoLt alpha p beta q
Axiom. (PNoLtI2) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, alpha betaPNoEq_ alpha p qq alphaPNoLt alpha p beta q
Axiom. (PNoLtI3) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, beta alphaPNoEq_ beta p q¬ p betaPNoLt alpha p beta q
Axiom. (PNoLtE) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, PNoLt alpha p beta q∀R : prop, (PNoLt_ (alpha beta) p qR)(alpha betaPNoEq_ alpha p qq alphaR)(beta alphaPNoEq_ beta p q¬ p betaR)R
Axiom. (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_irref_b) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoLt alpha p alpha pFalse
Axiom. (PNoLt_trichotomy_or) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNoLt alpha p beta q alpha = beta PNoEq_ alpha p q PNoLt beta q alpha p
Axiom. (PNoLtEq_tra) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoLt alpha p beta qPNoEq_ beta q rPNoLt alpha p beta r
Axiom. (PNoEqLt_tra) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoEq_ alpha p qPNoLt alpha q beta rPNoLt alpha p beta r
Axiom. (PNoLt_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLt alpha p beta qPNoLt beta q gamma rPNoLt alpha p gamma r
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. (PNoLeE) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, PNoLe alpha p beta q∀r : prop, (PNoLt alpha p beta qr)(alpha = betaPNoEq_ alpha p qr)r
Axiom. (PNoLe_ref) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoLe alpha p alpha p
Axiom. (PNoLe_antisym) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q : setprop, PNoLe alpha p beta qPNoLe beta q alpha palpha = beta PNoEq_ alpha p q
Axiom. (PNoLtLe_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLt alpha p beta qPNoLe beta q gamma rPNoLt alpha p gamma r
Axiom. (PNoLeLt_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLe alpha p beta qPNoLt beta q gamma rPNoLt alpha p gamma r
Axiom. (PNoEqLe_tra) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoEq_ alpha p qPNoLe alpha q beta rPNoLe alpha p beta r
Axiom. (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
Axiom. (exactly1of2_E) We take the following as an axiom:
∀A B : prop, exactly1of2 A B∀p : prop, (A¬ Bp)(¬ ABp)p
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. (exu_i_E1) We take the following as an axiom:
∀P : setprop, (exu_i P)∃x, P x
Axiom. (exu_i_E2) We take the following as an axiom:
∀P : setprop, (exu_i P)∀x y, P xP yx = y
Axiom. (exu_i_I) We take the following as an axiom:
∀P : setprop, (∃x, P x)(∀x y, P xP yx = y)exu_i P
Axiom. (atleastp_I) We take the following as an axiom:
∀X Y, ∀f : setset, inj X Y fatleastp X Y
Axiom. (atleastp_E_impred) We take the following as an axiom:
∀X Y, atleastp X Y∀p : prop, (∀f : setset, inj X Y fp)p
Axiom. (ordinalI) We take the following as an axiom:
∀alpha, TransSet alpha(∀betaalpha, TransSet beta)ordinal alpha
Axiom. (reflexive_i_I) We take the following as an axiom:
∀R : setsetprop, (∀x, R x x)reflexive_i R
Axiom. (reflexive_i_E) We take the following as an axiom:
∀R : setsetprop, reflexive_i R∀x, R x x
Axiom. (irreflexive_i_I) We take the following as an axiom:
∀R : setsetprop, (∀x, ¬ R x x)irreflexive_i R
Axiom. (irreflexive_i_E) We take the following as an axiom:
∀R : setsetprop, irreflexive_i R∀x, ¬ R x x
Axiom. (symmetric_i_I) We take the following as an axiom:
∀R : setsetprop, (∀x y, R x yR y x)symmetric_i R
Axiom. (symmetric_i_E) We take the following as an axiom:
∀R : setsetprop, symmetric_i R∀x y, R x yR y x
Axiom. (antisymmetric_i_I) We take the following as an axiom:
∀R : setsetprop, (∀x y, R x yR y xx = y)antisymmetric_i R
Axiom. (antisymmetric_i_E) We take the following as an axiom:
∀R : setsetprop, antisymmetric_i R∀x y, R x yR y xx = y
Axiom. (transitive_i_I) We take the following as an axiom:
∀R : setsetprop, (∀x y z, R x yR y zR x z)transitive_i R
Axiom. (transitive_i_E) We take the following as an axiom:
∀R : setsetprop, transitive_i R∀x y z, R x yR y zR x z
Axiom. (eqreln_i_I) We take the following as an axiom:
∀R : setsetprop, reflexive_i Rsymmetric_i Rtransitive_i Reqreln_i R
Axiom. (eqreln_i_E) We take the following as an axiom:
∀R : setsetprop, eqreln_i R∀p : prop, (reflexive_i Rsymmetric_i Rtransitive_i Rp)p
Axiom. (per_i_I) We take the following as an axiom:
∀R : setsetprop, symmetric_i Rtransitive_i Rper_i R
Axiom. (per_i_E) We take the following as an axiom:
∀R : setsetprop, per_i R∀p : prop, (symmetric_i Rtransitive_i Rp)p
Axiom. (linear_i_I) We take the following as an axiom:
∀R : setsetprop, (∀x y, R x y R y x)linear_i R
Axiom. (linear_i_E) We take the following as an axiom:
∀R : setsetprop, linear_i R∀x y, R x y R y x
Axiom. (trichotomous_or_i_I) We take the following as an axiom:
∀R : setsetprop, (∀x y, R x y x = y R y x)trichotomous_or_i R
Axiom. (trichotomous_or_i_E) We take the following as an axiom:
∀R : setsetprop, trichotomous_or_i R∀x y, R x y x = y R y x
Axiom. (partialorder_i_I) We take the following as an axiom:
∀R : setsetprop, reflexive_i Rantisymmetric_i Rtransitive_i Rpartialorder_i R
Axiom. (partialorder_i_E) We take the following as an axiom:
∀R : setsetprop, partialorder_i R∀p : prop, (reflexive_i Rantisymmetric_i Rtransitive_i Rp)p
Axiom. (totalorder_i_I) We take the following as an axiom:
∀R : setsetprop, partialorder_i Rlinear_i Rtotalorder_i R
Axiom. (totalorder_i_E) We take the following as an axiom:
∀R : setsetprop, totalorder_i R∀p : prop, (partialorder_i Rlinear_i Rp)p
Axiom. (strictpartialorder_i_I) We take the following as an axiom:
∀R : setsetprop, irreflexive_i Rtransitive_i Rstrictpartialorder_i R
Axiom. (strictpartialorder_i_E) We take the following as an axiom:
∀R : setsetprop, strictpartialorder_i R∀p : prop, (irreflexive_i Rtransitive_i Rp)p
Axiom. (stricttotalorder_i_I) We take the following as an axiom:
∀R : setsetprop, strictpartialorder_i Rtrichotomous_or_i Rstricttotalorder_i R
Axiom. (stricttotalorder_i_E) We take the following as an axiom:
∀R : setsetprop, stricttotalorder_i R∀p : prop, (strictpartialorder_i Rtrichotomous_or_i Rp)p
Axiom. (binrep_I1) We take the following as an axiom:
∀X Y, ∀xX, Inj0 x binrep X Y
Axiom. (binrep_I2) We take the following as an axiom:
∀X Y Z, Z YInj1 Z binrep X Y
Axiom. (binrep_E) We take the following as an axiom:
∀X Y, ∀zbinrep X Y, ∀p : setprop, (∀xX, p (Inj0 x))(∀Z, Z Yp (Inj1 Z))p z
Axiom. (equip_mod_I1) We take the following as an axiom:
∀X Y M Z V, equip (X + Z) Yequip (V Z) Mequip_mod X Y M
Axiom. (equip_mod_I2) We take the following as an axiom:
∀X Y M Z V, equip (Y + Z) Xequip (V Z) Mequip_mod X Y M
Axiom. (equip_mod_E) We take the following as an axiom:
∀X Y M, equip_mod X Y M∀p : prop, (∀Z V, equip (X + Z) Yequip (V Z) Mp)(∀Z V, equip (Y + Z) Xequip (V Z) Mp)p
Axiom. (tuple_p_I) We take the following as an axiom:
∀n x, (∀ux, ∃in, ∃v, u = i + v)tuple_p n x
Axiom. (tuple_p_E) We take the following as an axiom:
∀n x, tuple_p n x∀ux, ∃in, ∃v, u = i + v
Axiom. (setexp_I) We take the following as an axiom:
∀X Y, ∀f(xX, Y), f YX
Axiom. (setexp_E) We take the following as an axiom:
∀X Y, ∀fYX, f xX, Y
Axiom. (lam2_I) We take the following as an axiom:
∀X, ∀Y : setset, ∀F : setsetset, ∀xX, ∀yY x, ∀zF x y, x + (y + z) lam2 X Y F
Axiom. (lam2_E) We take the following as an axiom:
∀X, ∀Y : setset, ∀F : setsetset, ∀wlam2 X Y F, ∃xX, ∃yY x, ∃zF x y, w = x + (y + z)
Axiom. (lam2_E_impred) We take the following as an axiom:
∀X, ∀Y : setset, ∀F : setsetset, ∀wlam2 X Y F, ∀p : setprop, (∀xX, ∀yY x, ∀zF x y, p (x + (y + z)))p w
Axiom. (lam2_I2) We take the following as an axiom:
∀X, ∀Y : setset, ∀F : setsetset, ∀xX, ∀yY x, ∀zF x y, (x,(y,z)) lam2 X Y F
Axiom. (lam2_E2) We take the following as an axiom:
∀X, ∀Y : setset, ∀F : setsetset, ∀wlam2 X Y F, ∃xX, ∃yY x, ∃zF x y, w = (x,(y,z))
Axiom. (lam2_E2_impred) We take the following as an axiom:
∀X, ∀Y : setset, ∀F : setsetset, ∀wlam2 X Y F, ∀p : setprop, (∀xX, ∀yY x, ∀zF x y, p (x,(y,z)))p w
Axiom. (binop_on_I) We take the following as an axiom:
∀X, ∀f : setsetset, (∀x yX, f x y X)binop_on X f
Axiom. (binop_on_E) We take the following as an axiom:
∀X, ∀f : setsetset, binop_on X f∀x yX, f x y X
Beginning of Section NatRec
Variable z : set
Variable f : setsetset
Let F : set(setset)setλn g ⇒ if n n then f ( n) (g ( n)) else z
Axiom. (nat_primrec_r) We take the following as an axiom:
∀X : set, ∀g h : setset, (∀xX, g x = h x)F X g = F X h
Axiom. (nat_primrec_0) We take the following as an axiom:
Axiom. (nat_primrec_S) We take the following as an axiom:
∀n : set, nat_p nnat_primrec z f (ordsucc n) = f n (nat_primrec z f n)
End of Section NatRec
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, ∀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
Axiom. (ordsucc_add_nat_1) We take the following as an axiom:
∀n, ordsucc n = n + 1
Axiom. (add_nat_1_1_2) We take the following as an axiom:
1 + 1 = 2
Axiom. (add_nat_leq) We take the following as an axiom:
∀n m, nat_p mn n + m
Axiom. (add_nat_ltL) We take the following as an axiom:
∀k, nat_p k∀mk, ∀n, nat_p nm + n k + n
Axiom. (add_nat_ltR) We take the following as an axiom:
∀k, nat_p k∀mk, ∀n, nat_p nn + m n + k
Axiom. (add_nat_mem_impred) We take the following as an axiom:
∀m, ∀n, nat_p n∀ym + n, ∀p : prop, (y mp)(∀in, y = m + ip)p
Axiom. (add_nat_cancelR) We take the following as an axiom:
∀i j n, nat_p ni + n = j + ni = j
Axiom. (add_nat_cancelL) We take the following as an axiom:
∀n i j, nat_p nnat_p inat_p jn + i = n + ji = j
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)
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.
Axiom. (exp_nat_0) We take the following as an axiom:
∀n, n ^ 0 = 1
Axiom. (exp_nat_S) We take the following as an axiom:
∀n m, nat_p mn ^ (ordsucc m) = n * n ^ m
Axiom. (equipI) We take the following as an axiom:
∀X Y, ∀f : setset, bij X Y fequip X Y
Axiom. (equipE_impred) We take the following as an axiom:
∀X Y, equip X Y∀p : prop, (∀f : setset, bij X Y fp)p
Axiom. (inj_incl) We take the following as an axiom:
∀X Y, X Yinj X Y (λx ⇒ x)
Axiom. (inj_id) We take the following as an axiom:
∀X, inj X X (λx ⇒ x)
Axiom. (bij_id) We take the following as an axiom:
∀X, bij X X (λx ⇒ x)
Definition. We define inv to be λX f ⇒ λy : setEps_i (λx ⇒ x X f x = y) of type set(setset)setset.
Axiom. (surj_rinv) We take the following as an axiom:
∀X Y, ∀f : setset, (∀wY, ∃uX, f u = w)∀yY, inv X f y X f (inv X f y) = y
Axiom. (inj_linv) We take the following as an axiom:
∀X Y, ∀f : setset, (∀u vX, f u = f vu = v)∀xX, inv X f (f x) = x
Axiom. (bij_inv) We take the following as an axiom:
∀X Y, ∀f : setset, bij X Y fbij Y X (inv X f)
Axiom. (inj_comp) We take the following as an axiom:
∀X Y Z : set, ∀f g : setset, inj X Y finj Y Z ginj X Z (λx ⇒ g (f x))
Axiom. (bij_comp) We take the following as an axiom:
∀X Y Z : set, ∀f g : setset, bij X Y fbij Y Z gbij X Z (λx ⇒ g (f x))
Axiom. (equip_ref) We take the following as an axiom:
∀X, equip X X
Axiom. (equip_sym) We take the following as an axiom:
∀X Y, equip X Yequip Y X
Axiom. (equip_tra) We take the following as an axiom:
∀X Y Z, equip X Yequip Y Zequip X Z
Axiom. (inj_setsum_Inj0) We take the following as an axiom:
∀X Y, inj X (X + Y) Inj0
Axiom. (inj_setsum_Inj1) We take the following as an axiom:
∀X Y, inj Y (X + Y) Inj1
Axiom. (equip_setsum_Empty_R) We take the following as an axiom:
∀X, equip (X + 0) X
Axiom. (setsum_binunion_distrR) We take the following as an axiom:
∀X Y Z, X + (Y Z) = (X + Y) (X + Z)
Axiom. (equip_setsum_add_nat) We take the following as an axiom:
∀n, nat_p n∀m, nat_p mequip (n + m) (n + m)
Axiom. (combine_funcs_fun) We take the following as an axiom:
∀X Y Z, ∀f g : setset, (∀xX, f x Z)(∀yY, g y Z)∀uX + Y, combine_funcs X Y f g u Z
Axiom. (combine_funcs_inj) We take the following as an axiom:
∀X Y Z, ∀f g : setset, inj X Z finj Y Z g(∀xX, ∀yY, f x g y)inj (X + Y) Z (combine_funcs X Y f g)
Axiom. (inj_Inj0) We take the following as an axiom:
∀X Y, inj X (X + Y) Inj0
Axiom. (inj_Inj1) We take the following as an axiom:
∀X Y, inj Y (X + Y) Inj1
Axiom. (equip_setsum_cong) We take the following as an axiom:
∀X Y Z W, equip X Zequip Y Wequip (X + Y) (Z + W)
Axiom. (equip_setsum_add_nat_2) We take the following as an axiom:
∀n, nat_p n∀m, nat_p m∀X Y, equip X nequip Y mequip (X + Y) (n + m)
Axiom. (LoopI) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, binop_on X mbinop_on X bbinop_on X s(∀xX, (m e x = x m x e = x))(∀x yX, (b x (m x y) = y m x (b x y) = y s (m x y) y = x m (s x y) y = x))Loop X m b s e
Axiom. (LoopE) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, Loop X m b s e∀p : prop, (binop_on X mbinop_on X bbinop_on X s(∀xX, (m e x = x m x e = x))(∀x yX, (b x (m x y) = y m x (b x y) = y s (m x y) y = x m (s x y) y = x))p)p
Axiom. (Loop_with_defs_I) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, ∀K : setsetset, ∀a : setsetsetset, ∀T : setsetset, ∀L R : setsetsetset, ∀I1 J1 I2 J2 : setsetset, Loop X m b s e(∀x yX, K x y = b (m y x) (m x y))(∀x y zX, a x y z = b (m x (m y z)) (m (m x y) z))(∀x uX, T x u = b x (m u x) I1 x u = m x (m u (b x e)) J1 x u = m (m (s e x) u) x I2 x u = m (b x u) (b (b x e) e) J2 x u = m (s e (s e x)) (s u x))(∀x y uX, L x y u = b (m y x) (m y (m x u)) R x y u = s (m (m u x) y) (m x y))Loop_with_defs X m b s e K a T L R I1 J1 I2 J2
Axiom. (Loop_with_defs_E) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, ∀K : setsetset, ∀a : setsetsetset, ∀T : setsetset, ∀L R : setsetsetset, ∀I1 J1 I2 J2 : setsetset, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2∀p : prop, (Loop X m b s e(∀x yX, K x y = b (m y x) (m x y))(∀x y zX, a x y z = b (m x (m y z)) (m (m x y) z))(∀x uX, T x u = b x (m u x) I1 x u = m x (m u (b x e)) J1 x u = m (m (s e x) u) x I2 x u = m (b x u) (b (b x e) e) J2 x u = m (s e (s e x)) (s u x))(∀x y uX, L x y u = b (m y x) (m y (m x u)) R x y u = s (m (m u x) y) (m x y))p)p
Axiom. (Loop_with_defs_cex1_I0) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, ∀K : setsetset, ∀a : setsetsetset, ∀T : setsetset, ∀L R : setsetsetset, ∀I1 J1 I2 J2 : setsetset, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2(∃u x y wX, K (m (b (L x y u) e) u) w e)Loop_with_defs_cex1 X m b s e K a T L R I1 J1 I2 J2
Axiom. (Loop_with_defs_cex1_E0) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, ∀K : setsetset, ∀a : setsetsetset, ∀T : setsetset, ∀L R : setsetsetset, ∀I1 J1 I2 J2 : setsetset, Loop_with_defs_cex1 X m b s e K a T L R I1 J1 I2 J2∀p : prop, (Loop_with_defs X m b s e K a T L R I1 J1 I2 J2(∃u x y wX, K (m (b (L x y u) e) u) w e)p)p
Axiom. (Loop_with_defs_cex1_I) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, ∀K : setsetset, ∀a : setsetsetset, ∀T : setsetset, ∀L R : setsetsetset, ∀I1 J1 I2 J2 : setsetset, ∀u x y wX, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2K (m (b (L x y u) e) u) w eLoop_with_defs_cex1 X m b s e K a T L R I1 J1 I2 J2
Axiom. (andE_imp) We take the following as an axiom:
∀A B p : prop, (ABp)(A Bp)
Axiom. (orE_imp) We take the following as an axiom:
∀A B p : prop, (Ap)(Bp)(A Bp)
Axiom. (Loop_with_defs_cex1_E) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, ∀K : setsetset, ∀a : setsetsetset, ∀T : setsetset, ∀L R : setsetsetset, ∀I1 J1 I2 J2 : setsetset, Loop_with_defs_cex1 X m b s e K a T L R I1 J1 I2 J2∀p : prop, (∀u x y wX, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2K (m (b (L x y u) e) u) w ep)p
Axiom. (Loop_with_defs_cex2_I0) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, ∀K : setsetset, ∀a : setsetsetset, ∀T : setsetset, ∀L R : setsetsetset, ∀I1 J1 I2 J2 : setsetset, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2(∃u x y z wX, a w (m (s e u) (R x y u)) z e)Loop_with_defs_cex2 X m b s e K a T L R I1 J1 I2 J2
Axiom. (Loop_with_defs_cex2_E0) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, ∀K : setsetset, ∀a : setsetsetset, ∀T : setsetset, ∀L R : setsetsetset, ∀I1 J1 I2 J2 : setsetset, Loop_with_defs_cex2 X m b s e K a T L R I1 J1 I2 J2∀p : prop, (Loop_with_defs X m b s e K a T L R I1 J1 I2 J2(∃u x y z wX, a w (m (s e u) (R x y u)) z e)p)p
Axiom. (Loop_with_defs_cex2_I) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, ∀K : setsetset, ∀a : setsetsetset, ∀T : setsetset, ∀L R : setsetsetset, ∀I1 J1 I2 J2 : setsetset, ∀u x y z wX, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2a w (m (s e u) (R x y u)) z eLoop_with_defs_cex2 X m b s e K a T L R I1 J1 I2 J2
Axiom. (Loop_with_defs_cex2_E) We take the following as an axiom:
∀X, ∀m b s : setsetset, ∀e : set, ∀K : setsetset, ∀a : setsetsetset, ∀T : setsetset, ∀L R : setsetsetset, ∀I1 J1 I2 J2 : setsetset, Loop_with_defs_cex2 X m b s e K a T L R I1 J1 I2 J2∀p : prop, (∀u x y z wX, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2a w (m (s e u) (R x y u)) z ep)p
Axiom. (binop_on_1) We take the following as an axiom:
binop_on 1 (λx y ⇒ 0)
Axiom. (Trivial_Loop) We take the following as an axiom:
Loop 1 (λx y ⇒ 0) (λx y ⇒ 0) (λx y ⇒ 0) 0
Definition. We define binop_table_2 to be λx_0_0 x_0_1 x_1_0 x_1_1 i j ⇒ ((x_0_0,x_0_1),(x_1_0,x_1_1)) i j of type setsetsetsetsetsetset.
Axiom. (binop_table_2_0_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_1_0 x_1_1, binop_table_2 x_0_0 x_0_1 x_1_0 x_1_1 0 0 = x_0_0
Axiom. (binop_table_2_0_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_1_0 x_1_1, binop_table_2 x_0_0 x_0_1 x_1_0 x_1_1 0 1 = x_0_1
Axiom. (binop_table_2_1_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_1_0 x_1_1, binop_table_2 x_0_0 x_0_1 x_1_0 x_1_1 1 0 = x_1_0
Axiom. (binop_table_2_1_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_1_0 x_1_1, binop_table_2 x_0_0 x_0_1 x_1_0 x_1_1 1 1 = x_1_1
Axiom. (binop_table_on_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_1_0 x_1_12, binop_on 2 (binop_table_2 x_0_0 x_0_1 x_1_0 x_1_1)
Axiom. (Z2_table_binop_on_2) We take the following as an axiom:
binop_on 2 (binop_table_2 0 1 1 0)
Axiom. (Z2_Loop) We take the following as an axiom:
Loop 2 (binop_table_2 0 1 1 0) (binop_table_2 0 1 1 0) (binop_table_2 0 1 1 0) 0
Definition. We define binop_table_3 to be λx_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 i j ⇒ ((x_0_0,x_0_1,x_0_2),(x_1_0,x_1_1,x_1_2),(x_2_0,x_2_1,x_2_2)) i j of type setsetsetsetsetsetsetsetsetsetsetset.
Axiom. (binop_table_3_0_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 0 0 = x_0_0
Axiom. (binop_table_3_0_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 0 1 = x_0_1
Axiom. (binop_table_3_0_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 0 2 = x_0_2
Axiom. (binop_table_3_1_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 1 0 = x_1_0
Axiom. (binop_table_3_1_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 1 1 = x_1_1
Axiom. (binop_table_3_1_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 1 2 = x_1_2
Axiom. (binop_table_3_2_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 2 0 = x_2_0
Axiom. (binop_table_3_2_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 2 1 = x_2_1
Axiom. (binop_table_3_2_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 2 2 = x_2_2
Axiom. (binop_table_on_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_23, binop_on 3 (binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2)
Definition. We define binop_table_4 to be λx_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 i j ⇒ ((x_0_0,x_0_1,x_0_2,x_0_3),(x_1_0,x_1_1,x_1_2,x_1_3),(x_2_0,x_2_1,x_2_2,x_2_3),(x_3_0,x_3_1,x_3_2,x_3_3)) i j of type setsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetset.
Axiom. (binop_table_4_0_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 0 0 = x_0_0
Axiom. (binop_table_4_0_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 0 1 = x_0_1
Axiom. (binop_table_4_0_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 0 2 = x_0_2
Axiom. (binop_table_4_0_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 0 3 = x_0_3
Axiom. (binop_table_4_1_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 1 0 = x_1_0
Axiom. (binop_table_4_1_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 1 1 = x_1_1
Axiom. (binop_table_4_1_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 1 2 = x_1_2
Axiom. (binop_table_4_1_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 1 3 = x_1_3
Axiom. (binop_table_4_2_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 2 0 = x_2_0
Axiom. (binop_table_4_2_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 2 1 = x_2_1
Axiom. (binop_table_4_2_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 2 2 = x_2_2
Axiom. (binop_table_4_2_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 2 3 = x_2_3
Axiom. (binop_table_4_3_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 3 0 = x_3_0
Axiom. (binop_table_4_3_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 3 1 = x_3_1
Axiom. (binop_table_4_3_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 3 2 = x_3_2
Axiom. (binop_table_4_3_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 3 3 = x_3_3
Axiom. (binop_table_on_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_34, binop_on 4 (binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3)
Definition. We define binop_table_5 to be λx_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 i j ⇒ ((x_0_0,x_0_1,x_0_2,x_0_3,x_0_4),(x_1_0,x_1_1,x_1_2,x_1_3,x_1_4),(x_2_0,x_2_1,x_2_2,x_2_3,x_2_4),(x_3_0,x_3_1,x_3_2,x_3_3,x_3_4),(x_4_0,x_4_1,x_4_2,x_4_3,x_4_4)) i j of type setsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetsetset.
Axiom. (binop_table_5_0_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 0 0 = x_0_0
Axiom. (binop_table_5_0_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 0 1 = x_0_1
Axiom. (binop_table_5_0_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 0 2 = x_0_2
Axiom. (binop_table_5_0_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 0 3 = x_0_3
Axiom. (binop_table_5_0_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 0 4 = x_0_4
Axiom. (binop_table_5_1_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 1 0 = x_1_0
Axiom. (binop_table_5_1_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 1 1 = x_1_1
Axiom. (binop_table_5_1_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 1 2 = x_1_2
Axiom. (binop_table_5_1_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 1 3 = x_1_3
Axiom. (binop_table_5_1_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 1 4 = x_1_4
Axiom. (binop_table_5_2_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 2 0 = x_2_0
Axiom. (binop_table_5_2_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 2 1 = x_2_1
Axiom. (binop_table_5_2_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 2 2 = x_2_2
Axiom. (binop_table_5_2_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 2 3 = x_2_3
Axiom. (binop_table_5_2_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 2 4 = x_2_4
Axiom. (binop_table_5_3_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 3 0 = x_3_0
Axiom. (binop_table_5_3_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 3 1 = x_3_1
Axiom. (binop_table_5_3_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 3 2 = x_3_2
Axiom. (binop_table_5_3_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 3 3 = x_3_3
Axiom. (binop_table_5_3_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 3 4 = x_3_4
Axiom. (binop_table_5_4_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 4 0 = x_4_0
Axiom. (binop_table_5_4_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 4 1 = x_4_1
Axiom. (binop_table_5_4_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 4 2 = x_4_2
Axiom. (binop_table_5_4_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 4 3 = x_4_3
Axiom. (binop_table_5_4_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 4 4 = x_4_4
Axiom. (binop_table_on_5) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_45, binop_on 5 (binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4)
Beginning of Section Combinators
Let K : setInj0
Let S : setInj0 (𝒫 )
Let Ap : setsetsetλW Z : setInj1 (W + Z)
Axiom. (combinator_K) We take the following as an axiom:
Axiom. (combinator_S) We take the following as an axiom:
Axiom. (combinator_Ap) We take the following as an axiom:
∀X Y, combinator Xcombinator Ycombinator (Ap X Y)
Axiom. (combinator_ind) We take the following as an axiom:
∀p : setprop, p Kp S(∀X Y, combinator Xp Xcombinator Yp Yp (Ap X Y))∀X, combinator Xp X
Axiom. (combinator_equiv_sym) We take the following as an axiom:
Axiom. (combinator_equiv_tra) We take the following as an axiom:
∀X Y Z, combinator_equiv X Ycombinator_equiv Y Zcombinator_equiv X Z
Axiom. (combinator_equiv_Ap) We take the following as an axiom:
∀X Y Z W, combinator Xcombinator Ycombinator Zcombinator Wcombinator_equiv X Zcombinator_equiv Y Wcombinator_equiv (Ap X Y) (Ap Z W)
Axiom. (combinator_equiv_K) We take the following as an axiom:
∀X Y, combinator_equiv (Ap (Ap K X) Y) X
Axiom. (combinator_equiv_S) We take the following as an axiom:
∀X Y Z, combinator_equiv (Ap (Ap (Ap S X) Y) Z) (Ap (Ap X Z) (Ap Y Z))
Axiom. (combinator_equiv_ref) We take the following as an axiom:
Axiom. (combinator_equiv_ind) We take the following as an axiom:
∀r : setsetprop, per_i r(∀X, combinator Xr X X)(∀X Y Z W, combinator Xcombinator Ycombinator Zcombinator Wcombinator_equiv X Zr X Zcombinator_equiv Y Wr Y Wr (Ap X Y) (Ap Z W))(∀W Z, r (Ap (Ap K W) Z) W)(∀W Z V, r (Ap (Ap (Ap S W) Z) V) (Ap (Ap W V) (Ap Z V)))∀X Y, combinator_equiv X Yr X Y
Axiom. (combinator_SKK) We take the following as an axiom:
∀X, combinator_equiv (Ap (Ap (Ap S K) K) X) X
End of Section Combinators
Axiom. (setprod_I) We take the following as an axiom:
∀X Y, ∀u(λ_XY), u X Y
Axiom. (setprod_E) We take the following as an axiom:
∀X Y, ∀uX Y, u (λ_XY)
Axiom. (ap0_setprod) We take the following as an axiom:
∀X Y, ∀zX Y, z 0 X
Axiom. (ap1_setprod) We take the following as an axiom:
∀X Y, ∀zX Y, z 1 Y
Axiom. (tuple_setprod_eta) We take the following as an axiom:
∀X Y, ∀zX Y, (z 0,z 1) = z
Axiom. (lam_setexp) We take the following as an axiom:
∀X Y, ∀F : setset, (∀xX, F x Y)(λxXF x) YX
Axiom. (ap_setexp) We take the following as an axiom:
∀X Y, ∀fYX, ∀xX, f x Y
Axiom. (setexp_ext) We take the following as an axiom:
∀X Y, ∀f gYX, (∀xX, f x = g x)f = g
Axiom. (setexp_eta) We take the following as an axiom:
∀X Y, ∀fYX, (λxXf x) = f
Axiom. (mul_nat_1R) We take the following as an axiom:
∀n, n * 1 = n
Axiom. (mul_nat_1L) We take the following as an axiom:
∀n, nat_p n1 * n = n
Axiom. (exp_nat_p) We take the following as an axiom:
∀n, nat_p n∀m, nat_p mnat_p (n ^ m)
Axiom. (exp_nat_1) We take the following as an axiom:
∀n, n ^ 1 = n
Axiom. (exp_nat_2_mul_nat) We take the following as an axiom:
∀n, n ^ 2 = n * n
Axiom. (nat_inv_impred) We take the following as an axiom:
∀n, nat_p n∀p : setprop, p 0(∀m, nat_p mn = ordsucc mp (ordsucc m))p n
Axiom. (pos_nat_inv_impred) We take the following as an axiom:
∀n, nat_p n∀in, ∀p : setprop, (∀m, nat_p mn = ordsucc mp (ordsucc m))p n
Axiom. (add_nat_leL) We take the following as an axiom:
∀m k n, nat_p mnat_p km knat_p nm + n k + n
Axiom. (add_nat_leR) We take the following as an axiom:
∀n m k, nat_p nnat_p mnat_p km kn + m n + k
Axiom. (add_nat_leL_2) We take the following as an axiom:
∀n m, nat_p nnat_p mn m + n
Axiom. (add_nat_leR_2) We take the following as an axiom:
∀n m, nat_p nnat_p mn n + m
Axiom. (mul_nat_ltL) We take the following as an axiom:
∀k, nat_p k∀mk, ∀n, nat_p nm * (ordsucc n) k * (ordsucc n)
Axiom. (mul_nat_ltR) We take the following as an axiom:
∀k, nat_p k∀mk, ∀n, nat_p nordsucc n * m ordsucc n * k
Axiom. (mul_nat_leL) We take the following as an axiom:
∀m k, nat_p mnat_p km k∀n, nat_p nm * n k * n
Axiom. (mul_nat_leR) We take the following as an axiom:
∀n m k, nat_p nnat_p mnat_p km kn * m n * k
Axiom. (quot_rem_nat_impred) We take the following as an axiom:
∀m, nat_p m∀n, nat_p n∀ym * n, ∀p : prop, (∀im, ∀jn, y = i + j * m(∀i'm, ∀j'n, y = i' + j' * mi' = i j' = j)p)p
Axiom. (add_mul_nat_lt) We take the following as an axiom:
∀n m, nat_p nnat_p m∀in, ∀jm, i + j * n n * m
Axiom. (equip_setprod_mul_nat) We take the following as an axiom:
∀n m, nat_p nnat_p mequip (n m) (n * m)
Axiom. (equip_setprod_cong) We take the following as an axiom:
∀X Y Z W, equip X Zequip Y Wequip (X Y) (Z W)
Axiom. (equip_setprod_mul_nat_2) We take the following as an axiom:
∀n, nat_p n∀m, nat_p m∀X Y, equip X nequip Y mequip (X Y) (n * m)
Axiom. (equip_setexp_2) We take the following as an axiom:
∀n, nat_p n∀X, equip X nequip (X2) (n * n)
Axiom. (equip_setexp_2b) We take the following as an axiom:
∀n, nat_p n∀X, equip X nequip (X2) (n ^ 2)
Axiom. (equip_setexp_ordsucc_setprod) We take the following as an axiom:
∀n X, equip (Xordsucc n) (X (Xn))
Axiom. (equip_setexp_3) We take the following as an axiom:
∀n, nat_p n∀X, equip X nequip (X3) (n ^ 3)
Axiom. (SetAdjoinI1) We take the following as an axiom:
∀X y, ∀xX, x SetAdjoin X y
Axiom. (SetAdjoinI2) We take the following as an axiom:
∀X y, y SetAdjoin X y
Axiom. (SetAdjoinE) We take the following as an axiom:
∀X y, ∀zSetAdjoin X y, ∀p : prop, (z Xp)(z = yp)p
Axiom. (PNoEq__I) We take the following as an axiom:
∀alpha, ∀p q : setprop, (∀betaalpha, p beta q beta)PNoEq_ alpha p q
Axiom. (PNoEq__E) We take the following as an axiom:
∀alpha, ∀p q : setprop, ∀r : prop, ((∀betaalpha, p beta q beta)r)PNoEq_ alpha p qr
Axiom. (PNoLt__I) We take the following as an axiom:
∀beta alpha, beta alpha∀p q : setprop, PNoEq_ beta p q¬ p betaq betaPNoLt_ alpha p q
Axiom. (PNoLt__E) We take the following as an axiom:
∀alpha, ∀p q : setprop, ∀r : prop, (∀betaalpha, PNoEq_ beta p q¬ p betaq betar)PNoLt_ alpha p qr
Axiom. (PNoLt_trichotomy_or_impred) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, ordinal alphaordinal beta∀r : prop, (PNoLt alpha p beta qr)(alpha = betaPNoEq_ alpha p qr)(PNoLt beta q alpha pr)r
Axiom. (PNoLe_antisym_impred) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q : setprop, PNoLe alpha p beta qPNoLe beta q alpha p∀r : prop, (alpha = betaPNoEq_ alpha p qr)r
Axiom. (PNo_downc_I) We take the following as an axiom:
∀beta, ∀q : setprop, ∀L : set(setprop)prop, ∀alpha, ∀p : setprop, ordinal betaL beta qPNoLe alpha p beta qPNo_downc L alpha p
Axiom. (PNo_downc_E) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ∀p : setprop, ∀r : prop, (∀beta, ordinal beta∀q : setprop, L beta qPNoLe alpha p beta qr)PNo_downc L alpha pr
Axiom. (PNo_upc_I) We take the following as an axiom:
∀beta, ∀q : setprop, ∀R : set(setprop)prop, ∀alpha, ∀p : setprop, ordinal betaR beta qPNoLe beta q alpha pPNo_upc R alpha p
Axiom. (PNo_upc_E) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ∀p : setprop, ∀r : prop, (∀beta, ordinal beta∀q : setprop, R beta qPNoLe beta q alpha pr)PNo_upc R alpha pr
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_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. (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)
Beginning of Section TaggedSets
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Axiom. (not_TransSet_Sing1) We take the following as an axiom:
Axiom. (not_ordinal_Sing1) We take the following as an axiom:
Axiom. (tagged_not_ordinal) We take the following as an axiom:
∀y, ordinal (y ')False
Axiom. (tagged_notin_ordinal) We take the following as an axiom:
∀alpha y, ordinal alpha(y ') alphaFalse
Axiom. (tagged_eqE_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaalpha ' = beta 'alpha beta
Axiom. (tagged_eqE_eq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha ' = beta 'alpha = beta
Axiom. (tagged_ReplE) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betabeta ' {gamma '|gammaalpha}beta alpha
Axiom. (ordinal_notin_tagged_Repl) We take the following as an axiom:
∀alpha Y, ordinal alphaalpha {y '|yY}False
Axiom. (SNoElts__I1) We take the following as an axiom:
∀alpha, ∀betaalpha, beta SNoElts_ alpha
Axiom. (SNoElts__I2) We take the following as an axiom:
∀alpha, ∀betaalpha, beta ' SNoElts_ alpha
Axiom. (SNoElts__E) We take the following as an axiom:
∀alpha, ∀p : setprop, (∀betaalpha, p beta)(∀betaalpha, p (beta '))∀xSNoElts_ alpha, p x
Axiom. (SNoElts_mon) We take the following as an axiom:
∀alpha beta, alpha betaSNoElts_ alpha SNoElts_ beta
Axiom. (SNo__I) We take the following as an axiom:
∀alpha x, x SNoElts_ alpha(∀betaalpha, exactly1of2 (beta ' x) (beta x))SNo_ alpha x
Axiom. (SNo__E) We take the following as an axiom:
∀alpha x, ∀p : prop, (x SNoElts_ alpha(∀betaalpha, exactly1of2 (beta ' x) (beta x))p)SNo_ alpha xp
Axiom. (PSNo_I1) We take the following as an axiom:
∀alpha, ∀p : setprop, ∀betaalpha, p betabeta PSNo alpha p
Axiom. (PSNo_I2) We take the following as an axiom:
∀alpha, ∀p : setprop, ∀betaalpha, ¬ p betabeta ' PSNo alpha p
Axiom. (PSNo_E) We take the following as an axiom:
∀alpha, ∀p q : setprop, (∀betaalpha, p betaq beta)(∀betaalpha, ¬ p betaq (beta '))∀xPSNo alpha p, q x
End of Section TaggedSets
Axiom. (PNoEq_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, PNoEq_ alpha (λbeta ⇒ beta PSNo alpha p) p
Axiom. (SNo_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, SNo_ alpha (PSNo alpha p)
Axiom. (SNo_PSNo_eta_) We take the following as an axiom:
∀alpha x, ordinal alphaSNo_ alpha xx = PSNo alpha (λbeta ⇒ beta x)
Axiom. (SNo_I) We take the following as an axiom:
∀alpha, ordinal alpha∀z, SNo_ alpha zSNo z
Axiom. (SNo_E) We take the following as an axiom:
∀z, SNo z∀p : prop, (∀alpha, ordinal alphaSNo_ alpha zp)p
Axiom. (SNoLev_uniq_Subq) We take the following as an axiom:
∀x alpha beta, ordinal alphaordinal betaSNo_ alpha xSNo_ beta xalpha beta
Axiom. (SNoLev_uniq) We take the following as an axiom:
∀x alpha beta, ordinal alphaordinal betaSNo_ alpha xSNo_ beta xalpha = beta
Axiom. (SNoLev_prop) We take the following as an axiom:
∀x, SNo xordinal (SNoLev x) SNo_ (SNoLev x) x
Axiom. (SNoLev_prop_impred) We take the following as an axiom:
∀x, SNo x∀p : prop, (ordinal (SNoLev x)SNo_ (SNoLev x) xp)p
Axiom. (SNoLev_ordinal) We take the following as an axiom:
∀x, SNo xordinal (SNoLev x)
Axiom. (SNoLev_) We take the following as an axiom:
∀x, SNo xSNo_ (SNoLev x) x
Axiom. (SNo_PSNo_eta) We take the following as an axiom:
∀x, SNo xx = PSNo (SNoLev x) (λbeta ⇒ beta x)
Axiom. (SNoLev_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, SNoLev (PSNo alpha p) = alpha
Axiom. (SNo_Subq) We take the following as an axiom:
∀x y, SNo xSNo ySNoLev x SNoLev y(∀alphaSNoLev x, alpha x alpha y)x y
Axiom. (SNoEq_I) We take the following as an axiom:
∀alpha x y, PNoEq_ alpha (λbeta ⇒ beta x) (λbeta ⇒ beta y)SNoEq_ alpha x y
Axiom. (SNoEq_E) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x yPNoEq_ alpha (λbeta ⇒ beta x) (λbeta ⇒ beta y)
Axiom. (SNoEq_E') We take the following as an axiom:
∀alpha x y, ∀p : prop, (PNoEq_ alpha (λbeta ⇒ beta x) (λbeta ⇒ beta y)p)SNoEq_ alpha x yp
Axiom. (SNoEq_E1) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x y∀betaalpha, beta xbeta y
Axiom. (SNoEq_E2) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x y∀betaalpha, beta ybeta x
Axiom. (SNoEq_antimon_) We take the following as an axiom:
∀alpha, ordinal alpha∀betaalpha, ∀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
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Axiom. (SNoLtI) We take the following as an axiom:
∀x y, PNoLt (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y)x < y
Axiom. (SNoLtE) We take the following as an axiom:
∀x y, x < yPNoLt (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y)
Axiom. (SNoLtE') We take the following as an axiom:
∀x y, ∀p : prop, (PNoLt (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y)p)x < yp
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Axiom. (SNoLeI) We take the following as an axiom:
∀x y, PNoLe (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y)x y
Axiom. (SNoLeE) We take the following as an axiom:
∀x y, x yPNoLe (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y)
Axiom. (SNoLeE') We take the following as an axiom:
∀x y, ∀p : prop, (PNoLe (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y)p)x yp
Axiom. (SNoLtLe) We take the following as an axiom:
∀x y, x < yx y
Axiom. (SNoLeE_or) We take the following as an axiom:
∀x y, SNo xSNo yx yx < y x = 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. (SNoLtE3) We take the following as an axiom:
∀x y, SNo xSNo yx < y∀p : prop, (∀z, SNo zSNoLev z SNoLev x SNoLev ySNoEq_ (SNoLev z) z xSNoEq_ (SNoLev z) z yx < zz < ySNoLev z xSNoLev z yp)(SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yp)(SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev y xp)p
Axiom. (SNoLtI2) We take the following as an axiom:
∀x y, SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yx < y
Axiom. (SNoLtI3) We take the following as an axiom:
∀x y, SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev y xx < y
Axiom. (SNoLt_irref) We take the following as an axiom:
∀x, ¬ SNoLt x x
Axiom. (SNoLt_trichotomy_or) We take the following as an axiom:
∀x y, SNo xSNo yx < y x = y y < x
Axiom. (SNoLt_trichotomy_or_impred) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (x < yp)(x = yp)(y < xp)p
Axiom. (SNoLt_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < yy < zx < z
Axiom. (SNoLe_ref) We take the following as an axiom:
∀x, SNoLe x x
Axiom. (SNoLe_antisym) We take the following as an axiom:
∀x y, SNo xSNo yx yy xx = y
Axiom. (SNoLtLe_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < yy zx < z
Axiom. (SNoLeLt_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx yy < zx < z
Axiom. (SNoLe_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx yy zx z
Axiom. (SNoLtLe_or) We take the following as an axiom:
∀x y, SNo xSNo yx < y y x
Axiom. (SNoLtLe_or_impred) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (x < yp)(y xp)p
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