ON AXIOMS OF CONDITIONAL SET EXISTENCE1) by HAO WANU in Cambridge, Mass. (U.S.A.)
1. Outline of arguments
I n what follows, the (restricted) predicate calculus with equality is assumed throughout. Let ( U ! u ) H u be short for (w) ( u ) ((Hw A H u ) 13 w = u ) , ( E ! y ) H y be short for (Ey) H y A (U!y) H y , FuncH be short for (v) ( U ! u ) Huv. The convention is to think of Huv as u = f ( v ) , so that a one-many relation defines a function. The basic axioms of the extended ZERMELO set theory, commonly referred to as ZF, are given as:
Briefly, B3. The power set axiom. (By) (u) (u E y = u 2 z). Briefly, (Ey) (y = Pz). B4. The axiom (schema) of replacement. Func B 3 (Ey) (u E y = (Ev) (v E I(: A Guv)) .
(EY) (Y = {a > 6 ) ) .
(Ey) (9 = Uz).
Briefly, F a m B 3 (Ey) (y = G"z).
C. Axiom of infinity (unconditional set existence).
The other axioms (regularity and choice) are generally regarded as more specialized.
The purpose of this note is t o discuss the possibility of combining Bl-B4 into a n organic single schema. This is in part motivated by a wish to supply an analogue of the three axioms of type theory: extensionality, (the axiom of) comprehension, and infinity. The search is not completely successful because in each case the axiom of unit set is required as an auxiliary. It is not clear whether this is a natural need to answer to the notational distinction of different types.
The axiom of unit set is:
Two axiom schemata are considered : K. Func H 2 ( E y ) (y = U (HI' (Px)) , or briefly, F u w H 2 (Ey) (y = U H"Pz) .
L. F u ~c H 3 (Ey) (y = H"P U 2).