A Reformulation of Z-Reg.
in [Logic]
|
Prev: Download new programs and english courses
Next: All you have to do is c o m p r e h e n d this statement anddiagonalisation falls apart
From: MoeBlee on 15 Jun 2010 12:32 On Jun 14, 8:55 pm, zuhair <zaljo...(a)yahoo.com> wrote: > The complete statement of axiom schema of comprehension reads: > > For n=0,1,2,..., if Phi(y,w1,...,wn) is a formula in which > y,w1,...,wn are all the free variables occurring in it, then > > Aw1...wn As Ar E!x Ay > (y e x <-> ((y c s \/ y c r) /\ Phi(y,w1,...,wn))) > > is an axiom. You don't want to exclude x from being a free variable in Phi? > Now let s=r and let n=1 this would be reduced to > > Aw1 Ar E!x Ay ( y e x <-> (y c r /\ Phi(y,w1)) ). Okay. ArE!xAy(yex <-> (y subset r & Phi)) where the free variables in Phi are at most y and w1 > Now According to axiom of union, there must exist at least one set > r such that all members of w are subsets of r. so this r shall be > denoted as w* Okay, existential instantiation to r and also to w*. But, as far as I can tell, you might as well just consider Uw itself: Axew x subset Uw. > Now let Phi(y,w1)<-> (y e w1 /\ pi(y,w1)) y e w1 & Pi where the only free variables in Pi are at most y and w1. But you end up with Pi as the formula we prove for schema of sepration. So Pi must be ARBITRARY (except we know x does not occur free in it). Therefore, you cannot assume that the only free variables in Pi are at most y and w1. What you can do is assume that the only free variables in Pi are at most y, w1, ... , wn for ARBITRARY n. (But I don't know whether you even use the property of Pi having only at most y and w1 as its free variables, so we'll see...) > so we have > > Aw1 Aw* E!x Ay ( y e x <-> ( y c w* /\ y e w1 /\ pi(y,w1) ) ) Aw1Aw*E!xAy(yex <-> (y subset w* & y e w1 & Pi)) where the free variables in Pi are at most y and w1 Yes, by exchange of bound variables, that follows from your compression schema. > Now since it is true that for every w1 and w* > > all y (y e w1 -> y c w*) Where did you get that? Where did you get such a statement about w1 and ALL w*. What we DO have: For all w1 there exists a w* such that Ay(y e w1 -> y subset of w*). Also we have: Aw1Ay(y e w1 -> y subset Uw1) We do NOT have: Aw1Aw*Ay(y e w1 -> y subset of w*) > therefore we can eliminate w* to have > > Aw1 E!x Ay ( y e x <-> (y e w1 /\ pi ) ) Go back to my previous comment that we do not have Aw1Aw*Ay(y e w1 -> y subset of w*) but instead we have Aw1Ew*Ay(y e w1 -> y subset w*) So show me the quantifer logic by which you get from Aw1Aw*E!xAy(yex <-> (y subset w* & y e w1 & Pi)) and Aw1Ew*Ay(y e w1 -> y subset w*) to Aw1E!xAy (yex <-> (y e w1 /\ Pi )) What I see is this: (1) Aw1Aw*E!xAy(yex <-> (y subset w* & y e w1 & Pi)) (2) Aw1Ew*Ay(y e w1 -> y subset w*) From (2), by universal, then existential, instantiation let Ay(y e w1 - > y subset w*) From (1), by universal instantiation E!xAy(yex <-> (y subset w* & y e w1 & Pi)) So (I think) E!xAy (yex <-> (y e w1 /\ Pi)) But w* may not leave the argument with w* free in Phi, as that would violate the rule of existential instantion (you can't existentially instantiate to w* and then CONCLUDE with w* left dangling free, which would leave w* available to universally generalize, though we can't universally generalize w* since by existentially instantiating it, we ASSUMED CERTAIN PROPERTIES about it). And it seems this is what came back to bite you when you earlier incorrectly stated: For ALL w* Ay(y e w1 -> y subset w*) instead of EXISTS w* (Ay y e w1 -> y subset w*) So if w* is free in Phi, then your argument breaks down. But, of course, you want to be able to have w* free in Phi and then close the axiom with w* as one of the universal quantifiers. It's a tricky situation, and I didn't take the time to doublecheck it by the literal rules, but I'm pretty sure I'm right. I would ask other people who are sensitve to such details in predicate logic. Remember, you can't use any property of Pi other than x is not free in it. You can't assume that the free variables in Pi are at most y and w1. To prove the separation schema, you have to START with an ARBITRARY formula Pi that does not have x free in it. THEN derive Aw1E!xAy (y e x <-> (y e w1 /\ Pi )) Throughout your argument, this Pi must be ARBITRARY except that we know x does not occur free in it. MoeBlee
From: zuhair on 15 Jun 2010 19:10 On Jun 15, 11:32 am, MoeBlee <jazzm...(a)hotmail.com> wrote: > On Jun 14, 8:55 pm, zuhair <zaljo...(a)yahoo.com> wrote: > > > The complete statement of axiom schema of comprehension reads: > > > For n=0,1,2,..., if Phi(y,w1,...,wn) is a formula in which > > y,w1,...,wn are all the free variables occurring in it, then > > > Aw1...wn As Ar E!x Ay > > (y e x <-> ((y c s \/ y c r) /\ Phi(y,w1,...,wn))) > > > is an axiom. > > You don't want to exclude x from being a free variable in Phi? Yes of course. > > > Now let s=r and let n=1 this would be reduced to > > > Aw1 Ar E!x Ay ( y e x <-> (y c r /\ Phi(y,w1)) ). > > Okay. > > ArE!xAy(yex <-> (y subset r & Phi)) > > where the free variables in Phi are at most y and w1 > > > Now According to axiom of union, there must exist at least one set > > r such that all members of w are subsets of r. so this r shall be > > denoted as w* > > Okay, existential instantiation to r and also to w*. But, as far as I > can tell, you might as well just consider Uw itself: > > Axew x subset Uw. Yea I know, but we didn't prove the uniqueness of Uw yet. We need extensionality, for it we need unique separation to be proved first. What we have from axiom of union is that for every set w there exist a set w* such that all members of w are subsets of w*. Notice that w* is not a unique set, it might be any set in which all members of w are subsets of. > > > Now let Phi(y,w1)<-> (y e w1 /\ pi(y,w1)) > > y e w1 & Pi > > where the only free variables in Pi are at most y and w1. > > But you end up with Pi as the formula we prove for schema of > sepration. So Pi must be ARBITRARY (except we know x does not occur > free in it). No the formula in unique separation is not arbitrary, it has two conditions, first y must be free in it, also w1 and x must not occur free in it. Therefore, you cannot assume that the only free variables > in Pi are at most y and w1. Of course I can, because that is what we need to prove. What you can do is assume that the only > free variables in Pi are at most y, w1, ... , wn for ARBITRARY n. (But > I don't know whether you even use the property of Pi having only at > most y and w1 as its free variables, so we'll see...) ah this is another argument, see my next post which would clarify this point. > > > so we have > > > Aw1 Aw* E!x Ay ( y e x <-> ( y c w* /\ y e w1 /\ pi(y,w1) ) ) Notice that w* is by definition a set in which every member of w is a subset of it w*, so w* is not any set. Possibly this can be re-written as Aw1 Aw* ( Ayew1(y c w*) -> E!x Ay ( y e x <-> ( y c w* /\ y e w1 /\ pi(y,w1) ) )). this might be easier to write. Now from the above it is clear that y c w* /\ y e w1 would be redundant, since this would be equivalent to y e w1. That was my basis to get rid of w* all together. anyhow this seems to be complicated approach somehow. Let's take the most obvious approach. From comprehension we have Aw1,...,wn Ar E!x Ay ( y e x <-> ( y c r /\ y e w1 /\ pi(y,w1,...,wn) ) Let name this formula as : formula 1. pi(y,w1,...,wn) mean a formula that has y w1,...,wn as its sole free variables, and x is not among them. I don't think we have any problem here, because phi(y,w1,...,wn) is characterised as *any* formula in which y,w1,...,wn are its sole free variables and in which x is not free. so the formula ( y e w1 /\ pi(y,w1,...,wn)) were pi(y,w1,...,wn) is any formula in which y,w1,...,wn are its sole free variables, and in which x is not free. so it is clear that the formula ( y e w1 /\ pi(y,w1,...,wn)) *is* a formula that satisfy phi(y,w1,...,wn). is there any problem with that? Now from union we know that Aw1 Ew* ( Ayew1(ycw*) ) Of course w* is not a unique set, it is any set that has the property Ayew1(ycw*) . Now lets instantiate *any one* of w* sets , for r in formula 1. so we end up with for n=1,2,3,..... Aw1...wn E!x Ay ( y e x <-> ( y e w1 /\ pi(y,w1,...,wn) ) ). and this is what we want to prove. Now it is not difficult to prove that this is equivalent to the following: for n=0,1,2,3,...,if phi(y,w1,...,wn) is a formula in which y,w1,...,wn are its sole free variables, in which x do not occur, then Aw1...wn Ar E!x Ay ( y e x <-> ( y e r & phi (y,w1,...,wn) ) ) is an axiom. this two formulas are equivalent. simply take pi to be the following Let pi(y,w1,...,wn) <-> [ Q(y,w2,...,wn) /\ w1=w1 ] so we simply got around w1 is a smart way, although w1 is their, but yet we know that [ Q(y,w2,...,wn) /\ w1=w1 ] <-> Q(y,w2,...,wn) so we can have: for n=1,2,3,..... Aw1...wn E!x Ay ( y e x <-> ( y e w1 /\ Q(y,w2,...,wn)) ). which is exactly the same as: for n=0,1,2,3,...,if phi(y,w1,...,wn) is a formula in which y,w1,...,wn are its sole free variables, in which x do not occur, then Aw1...wn Ar E!x Ay ( y e x <-> ( y e r & phi (y,w1,...,wn) ) ) is an axiom. Zuhair > > Aw1Aw*E!xAy(yex <-> (y subset w* & y e w1 & Pi)) > > where the free variables in Pi are at most y and w1 > > Yes, by exchange of bound variables, that follows from your > compression schema. > > > Now since it is true that for every w1 and w* > > > all y (y e w1 -> y c w*) > > Where did you get that? Where did you get such a statement about w1 > and ALL w*. I got that from the definition of w*. (this notation is confusing somehow I must admit that). > > What we DO have: > > For all w1 there exists a w* such that Ay(y e w1 -> y subset of w*). > > Also we have: > > Aw1Ay(y e w1 -> y subset Uw1) > > We do NOT have: > > Aw1Aw*Ay(y e w1 -> y subset of w*) > > > therefore we can eliminate w* to have > > > Aw1 E!x Ay ( y e x <-> (y e w1 /\ pi ) ) > > Go back to my previous comment that we do not have > > Aw1Aw*Ay(y e w1 -> y subset of w*) > > but instead we have > > Aw1Ew*Ay(y e w1 -> y subset w*) > > So show me the quantifer logic by which you get from > > Aw1Aw*E!xAy(yex <-> (y subset w* & y e w1 & Pi)) > and > Aw1Ew*Ay(y e w1 -> y subset w*) > > to > > Aw1E!xAy (yex <-> (y e w1 /\ Pi )) > > What I see is this: > > (1) Aw1Aw*E!xAy(yex <-> (y subset w* & y e w1 & Pi)) > (2) Aw1Ew*Ay(y e w1 -> y subset w*) > From (2), by universal, then existential, instantiation let Ay(y e w1 -> y subset w*) > > From (1), by universal instantiation E!xAy(yex <-> (y subset w* & y e > w1 & Pi)) > So (I think) E!xAy (yex <-> (y e w1 /\ Pi)) > > But w* may not leave the argument with w* free in Phi, as that would > violate the rule of existential instantion (you can't existentially > instantiate to w* and then CONCLUDE with w* left dangling free, which > would leave w* available to universally generalize, though we can't > universally generalize w* since by existentially instantiating it, we > ASSUMED CERTAIN PROPERTIES about it). > > And it seems this is what came back to bite you when you earlier > incorrectly stated: > > For ALL w* Ay(y e w1 -> y subset w*) > instead of > EXISTS w* (Ay y e w1 -> y subset w*) > > So if w* is free in Phi, then your argument breaks down. But, of > course, you want to be able to have w* free in Phi and then close the > axiom with w* as one of the universal quantifiers. > > It's a tricky situation, and I didn't take the time to doublecheck it > by the literal rules, but I'm pretty sure I'm right. I would ask other > people who are sensitve to such details in predicate logic. > > Remember, you can't use any property of Pi other than x is not free in > it. You can't assume that the free variables in Pi are at most y and > w1. > > To prove the separation schema, you have to START with an ARBITRARY > formula Pi that does not have x free in it. THEN derive > > Aw1E!xAy (y e x <-> (y e w1 /\ Pi )) > > Throughout your argument, this Pi must be ARBITRARY except that we > know x does not occur free in it. > > MoeBlee
From: MoeBlee on 15 Jun 2010 20:03
(1) You mean 'x' does not occur free in Pi or in Phi, right? (2) When you say "a formula that has y w1,...,wn as its sole free variables", you mean that AT MOST y, w1, ... wn occur free while it might be that none or only some of them occur free, right? (3) There's too much clutter now in all our back and forth. Please write a post all by itself in which you purport to show: For ARBITRARY formula Phi (except we know x not free in Phi): all closures of ExAy(yex <-> (yez & Phi)). Leave out all the old quotes conversation. Please just let me see your argument in a post by itself. MoeBlee |