Set-valued set theory. II.
E. William Chapin · Notre Dame Journal of Formal Logic · 1975
Development of the Elementary Theory First note that the following concepts were defined in section 2 in the process of developing the axioms: subset, null set, strong pair, weak pair, strong unit set, weak unit set, ordered pair, function, domain, range, into, onto, standard union, union, strong power set, power set, strong Cartesian product, and Cartesian product.In addition, the two concepts degree and standard, which have no classical counterparts, were introduced.In this section, we first need to define the other concepts common in elementary classical set theory and then to verify that the sets given by the various definitions have the usual properties, including existence.(The reader is reminded that 3\y means that there exists a unique y: there is such a y and any two are equal.)Thm.6: (VΛΓ) [Std (ΛΓ) ^ (3\y)(Vz)(Vw)(e(z,y,w) = (Vt)(3έ r )(e{t,x, t r ) Λ ~(t r = 0)) Ώ € (z,t,w))].Def.25: The set y of Theorem 6 is denoted by I \ s x. (Strong Intersection) Proof of Thm.6: The uniqueness of the strong intersection of a given standard x follows by the usual extensionality argument, since membership in that intersection is defined by an equivalence.The existence of the strong intersection follows from the Axiom of Separation (listed in section 2 as a consequence of the Axiom of Replacement) and the Axiom of Unions, since the intersection is that subset of the union v) s x = \Jx satisfying the condition given on the right hand side of the equivalence sign in the statement of Theorem 6. QEQ Thm.7: (Vx)te\y)((Vυ)(Vw)[e(υ,y,w) = (W)[(3f) (e(t,x, t') A |~(f =0)) D (e(t,x,w)Λe(v,t,w))]]).Def. 26: The set y of Theorem 7 is denoted by \\y.(Intersection)