Acta Mathematica Sinica, New Series 1990, Vol. 6, No. 2, pp. 189- 192
An og-Hierarchy of Axiom System ZF Zhang Jinwen ( ~:q~ ~ ) The Institute of Software, Academia Sinica Received July 23, 1988 Abstract. In this paper we develop a sequence Z0,'",Zn,"-(nc-(.o)ofaxiom systems for set theory, such that (1) the consistency of any system within the sequence is provable in its succeeding systems, (2) the first system in the sequence is Zermelo's system Z and the union of all systems in the sequence is just ZF.
1. Introduction From investigations by GSdel, Tarski, we know that given a system St , we can construct some stronger system S~, such that there is a criterion of soundness for St according to which all the theorems of SI are sound in S~. In this way one obtains a consistency proof for St in $2 9 The consistency so obtained can be of use in studying the interconnection and relative strength of different systems. If a consistency proof for $1 can be formalized in Sv then, according to Grdel's second incompleteness theorem such a proof cannot be formalized in 5'1 itself, and its arguments must be formalized in $2_but not in St 9 Since $1 and S_, may be very strong systems, similar questions and arguments as in [ 1,2] have arisen. A system S~ is an extension of St if every theorem of St is a theorem ofSv A conservative extension of S, is an extension of $2 such that a formula of St which is a theorem of $2 is also a theorem of S,. A nonconservative extension of St is an extension of S, and there exists a formula A of St such that A is a theorem of $2 but not of S~. The consistent problems and relative strength of Zermelo's system which is denoted by Z have been extensively discussed in the literature, for example, References [2, 3]. 'In this paper, our objectives are to investigate the consistent problems and relative strength of Zermelo-Fraenkel system in analogous forms.
2. Basic Definitions Definition 1. Let St and S~ be two systems. By S~< &__ we mean that St is a subsystem of $2, and Sz is a non-conservative extension of St 9 Definition 2. Let St and $2 be two systems. By St << $2 we mean that St < $2 and $2 F con S t , where con St is in a sentence which is to say the system St is consistent. Definition 3. In the language of set theory, by A 0 we mean the set E 0. If ~o(x) is a A; formula,then 9 xcp(x)and Vx~0(x)are all A ,+t-formulas [4,5]. Let R(n+ 1 )be an axiom schema of replacement about A ; formula:
V x 3 !y~o(x, y)--~Vx 3z Vy (yez--,. 3uex~o(u, y) ), where q~(x,y)is a A; formula. The axiom schema says that if any A ; formula q)(x,y) defines uniquely as a function of x, say y=f(x), then for each x the range o f f on x is a set.
190
Zhang Jinwen Definition 4. By recursion, we can define the axiom systems as follows: A0:=Z
,
A,+~ : =A0+ R (~) , A:=[.)
A,
nEr
It is easy to show that the system obtained from A, by deleting the axioms of separation which are not contained in R(0)is just Kripke-Platek system KP TM . Definition 5. By recursion, we can define the axiom systems as follows: Z 0 " =Z
Z.§
,
= A.+conZ.,
zo.=Uz.. #I E r
Proposition 1. For any given nature number n, we have TM Z F ~- con A, . 3. Main Theorems Theorem 1. Z0 << Z~. Proof. Obviously, Z0 is a subsystem of Zt by Definition 5. According to G~del's second incompleteness theorem, the consistency of Z0 (i. e., the formula con Zo) cannot be proved in Z. Since the formula conZ0 is in ZI , the Zo is a proper subsystem of Z0 and Zt 1- conZ0 ,as required. Theorem 2. Zt << Z2. Proof. From Definition 5, Z~ is Z0+conZ0 and Z2 is At+ conZ~. Moreover, Z0 is a subsystem of A t by Definition 4. Thus, the consistency of Zt derives from the consistency of Zo. That is, conZl--,-conZ0, so Zt < Z2 9 On the other hand, by Definition 5, t h e Z z ~ c o n Z . So we have ZI < Z2,as required. Theorem 3. For any. natural number n>2, we have Z. << Z.+ t 9 Proof. From Definitions 3 and 4, for any natural number n > 2 , we have A._~ << A. ,and Z. is A.+ conZ._t ,Z.+~ is A.+ conZ.. By mathematical induction, it is easy to see that if the system Z.+ ~is consistent, then the system Z. is consistent, i.e., con Z.+ t ~ c o n Z . . T h u s we have Z. < Z.+ v On the other hand, from Definition 5, Z.+ t- conZ0. So Zt << Z2,as required. Theorem 4. In the system sequence o f Definition 5, any system is a subsystem o f its succeeding system, and the consistency o f any system within the sequence can be proved in its succeeding system. That is to say, for any two natural numbers m and n, if n< m, then
Z.<< Zm. Proof. Since n < m, there exists a natural number k such that m = k + 1 and n < k. Thus Z, << Z.,. According to the transitivity of the subsystem and the consistency of the system Z,., the system Z. is consistent. Thus Z. << Zm 9 From Theorems 1 - 4 , we have the following relationship among the systems: Zo << Z~ << Z2 << - "
<< Z . << . . . .
An ~o-Hierarchy of Axiom System ZF
191
Because of the relationship above and the definition of the system Zoo in Definition 5, we can get at once: for any natural number n, Z. << Zo, 9 Theorem 5. Z . ~---~ZF. Proof. We have U. ~oA. c Z~, by Definition 5. Again, using Definitions 2 and 4, it is not difficult to get Z F = Un E r A. Thus w e h a v e ZFcZo~, so Zo,r---ZF. On the other hand, using Proposition 1, conA. can be proved in the system ZF. Because conA. is a sentence in the language of the system ZF, there is a natural number m such that conA. is a sentence in A.. Using again Proposition 1, we can get the consistency ofA.+ conZo(by induction on n), as required. 4. Epilogue
As is known to all, according to GSdel's second incompleteness theorem, for any system rich enough, if it is consistent, then there is no consistency proof for it by method formalizable in the system. Of course, there is no consistency proof for it in a system weaker than the system. That'is to say, there is consistency proof for it in a system stronger than the system. The consistency of Peano's arithmetic system P is provable in a system which contains an infinite process (i.e. ZF or Z). The consistency of the system ZF is provable in the ZF*~and QM (see [1] ). And one gets a sequence To, TL,..., T, ,... (new) of axiom systems such that the consistency of any system within the sequence is provable in its succeeding systems, and To is P; and for any nsco, T, is provable in Z(See [ 3] ). Thus when we hope to prove the consistency of the system P we need not prove it in a very strong system, but need only to prove it in the system TI, strong enough. In this paper, we get that the axiom system ZF fails into the following Hierarchy: Z0, ZI, "--, Z, ,---(nso9 )such that Z0 is just Zermelo's system Z, and the union of all systems in the sequence is just ZF. The consistency of any system within the sequence is provalble in its succeeding systems. Every theorem of any system within the sequence is also a theorem of its succeeding systems. The result is that not only the consistency of the system Z is provable in the system Z~ which is much weaker than the system ZF, but also the system ZF falls into a sequence such that the consistency of those systems is all provable in the system ZF, and the union of them is just ZF. This result expresses that the consistency of Z.F is provable in the system ZF in a certain sense. Here by "in a certain sense" we mean that the proof is done at a certain stage in the hierar chy of ZF. That is to say, for any n~o, the consistency of the system Z, is provable in the system ZF. If we get the consitency of every system Z,(n~o9 ), then we getthe consistency of ZF, because the union of these systems is just ZF. On the contrary, if Z F is inconsistent, then there exists a formula A such that A and ~ A are all provable in the system ZF. By induction on the construction and the complexity of A, we can get a natural number n such that A and -7 A are provable in the system Z; so Z is inconsistent. References [ 1] Fraenkel A.A., Bar-Hillel, Y. and Levy, A., Foundations of Set Theory, North-Holland Publishing Company,
192
[2] [ 3] [ 4] [5] [6] [ 7]
Zhang Jinwen
Amsterdam, London, 1973. Wang Hao, A Survey of Mathematical Logic, Science Press, Peking, 1962. Wang Hao, et R. McNaughton, Les systems aniomatigues de la theofie des ensembles, Paris, 1953. Enderton, H. B., Elements of Set Theorey, Academic P re.ss,New York,San Francisco, London, 1977. Levy, A., A hierarchy of formulas in set theorey, Mem. Arner.Math. Soc., 57(1974). Devilin, K.J., Construcyibility, Springer Veflag, Berlin,Heidelberg, New York, Tokyo, 1984. Zhao Xishun,A consistent result of the system A+ the replacement axiom schema off:n-formulas, Science gul" letin, 54 (1989).