A Reformulation of Z-Reg.2
in [Math]
|
Prev: 24 is gorgeous
Next: MGW: Retiring from the fray
From: zuhair on 16 Jun 2010 15:32 On Jun 15, 8:39 pm, zuhair <zaljo...(a)gmail.com> wrote: > Theory A is the set of all sentences(entailed from FOL with identity > and membership) by the following non logical axioms: > > (1) Comprehension: for n=0,1,2,3,...; if phi(y,w1,...,wn) > is a formula in which y,w1,...,wn *are* its sole free variables > and in which x is not free,then > > Aw1...wn Ar As E!x Ay > ( y e x <-> (( y c r \/ y c s ) /\ phi(y,w1,...,wn))) > > were c is the subset relation. > > (2) Union: Ar Ex Ayer(ycx) > > were c is the subset relation. > > (3) Infinity: as in Z. > > / > > Theorem schema of unique separation: > > for n=1,2,3,...., if pi(y,w1,...,wn) is a formula in which > y,w1,...,wn *are* its sole free variables, and in which x is not free, > then > > Aw1...wn E!x Ay ( y e x <-> ( y e w1 & pi(y,w1,...,wn) ) ). > > Proof: > > Let s=r in the comprehension schema, then for the same specifications > in comprehension we get: > > Aw1...wn Ar E!x Ay > ( y e x <-> (y c r /\ phi(y,w1,...,wn))) > > Let phi(y,w1,...,wn)<-> [y e w1 /\ pi(y,w1,...,wn)] > > were pi(y,w1,...,wn) is a formula in which y,w1,...,wn *are* its sole > free variables and in which x is not free. > > substitute in the above formula and we get: > > Aw1...wn Ar E!x Ay > ( y e x <-> (y c r /\ y e w1 /\ pi(y,w1,...,wn))) > > From union we have > > Aw1 Ew* Ayew1(ycw*) > > now w* is not unique, but we know that for every w1, at least one > w* must exist such that all members of w1 are subsets of w*. > > Now instantiate any one of the w* sets for r in the above formula, we > get: > > Aw1...wn E!x Ay > ( y e x <-> (y c w* /\ y e w1 /\ pi(y,w1,...,wn))) > > Now since every member of w1 is subset of w* (by definition of w* > sets). then we have > > (y c w* /\ y e w1) -> y e w1 > > thus the above formula would be reduced to: > > Aw1...wn E!x Ay > ( y e x <-> (y e w1 /\ pi(y,w1,...,wn))) > > Theorem schema of unique separation proved. > > Zuhair Moe Blee in a previous post asked me to show the following: For ARBITRARY formula Phi (except we know x not free in Phi): all closures of ExAy(yex <-> (yez & Phi)). / I say the above statement is actually equivalent to the unique separation schema mentioned above. Zuhair
From: MoeBlee on 16 Jun 2010 17:15 On Jun 16, 2:32 pm, zuhair <zaljo...(a)gmail.com> wrote: > Moe Blee in a previous post asked me to show the following: > > For ARBITRARY formula Phi (except we know x not free in Phi): > > all closures of > > ExAy(yex <-> (yez & Phi)). > > / > > I say the above statement is actually equivalent to the unique > separation schema mentioned above. I haven't looked over your new formulations, but last night I did figure out a way to formulate your compression schema so that it and your union axiom entail the separation(with built in extensionality) schema, while the separation schema (with built in extensionality) entails your compression schema. However, then it can't be the case that your compression schema, union schema, and infinity entail pairing and power set (did I understand correctly that you claim they do entail pairing and power set?), for then they would not be independent in Z set theory, though it has been proven that they are independent in Z set theory. MoeBlee
From: zuhair on 16 Jun 2010 17:50 On Jun 16, 4:15 pm, MoeBlee <jazzm...(a)hotmail.com> wrote: > On Jun 16, 2:32 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > Moe Blee in a previous post asked me to show the following: > > > For ARBITRARY formula Phi (except we know x not free in Phi): > > > all closures of > > > ExAy(yex <-> (yez & Phi)). > > > / > > > I say the above statement is actually equivalent to the unique > > separation schema mentioned above. > > I haven't looked over your new formulations, but last night I did > figure out a way to formulate your compression schema so that it and > your union axiom entail the separation(with built in extensionality) > schema, while the separation schema (with built in extensionality) > entails your compression schema. > > However, then it can't be the case that your compression schema, union > schema, and infinity entail pairing and power set (did I understand > correctly that you claim they do entail pairing and power set?), for > then they would not be independent in Z set theory, though it has been > proven that they are independent in Z set theory. > > MoeBlee Well I don't know what is your formulation yet. But I think we need to look at what I wrote here. Since there might be a mistake then. Anyhow let see the proof of pairing and power. (1)The proof of power: The formula in comprehension schema reads: Aw1...wn Ar As E!x Ay (y e x <-> (( y c r \/ y c s ) /\ phi(y,w1,...,wn))) Now let r=s and let n=0, then we'll have: Ar E!x Ay (y e x <-> ( y c r /\ phi(y))) Let phi(y)<->y=y thus we'll end up with Ar E!x Ay (y e x <-> y c r) It is clear that x is the power-set of r. Thus power is proved. (2)The proof of pairing: from comprehension with n=2 ,we have: Aw1 Aw2 Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ phi(y,w1,w2))) let phi(y,w1,w2)<->(y=w1 \/ y=w2) then: Aw1 Aw2 Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ phi(y,w1,w2))) let phi(y,w1,w2)<-> (y=w1 \/ y=w2) then: Aw1 Aw2 Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ (y=w1 \/ y=w2))) take r=w1, s=w2 then: Aw1 Aw2 E!x Ay (y e x <-> ((y c w1 \/ y c w2) /\ (y=w1 \/ y=w2))) which is reduced to: Aw1 Aw2 E!x Ay (y e x <-> (y=w1 \/ y=w2)) which is pairing. I don't know what you meant about the issue with the independence of these axioms in Z, and how that can be affected if they spring from the same comprehension and union axioms. To me I don't see that this would affect their independence at all. Zuhair
From: zuhair on 16 Jun 2010 17:53 On Jun 16, 4:15 pm, MoeBlee <jazzm...(a)hotmail.com> wrote: > On Jun 16, 2:32 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > Moe Blee in a previous post asked me to show the following: > > > For ARBITRARY formula Phi (except we know x not free in Phi): > > > all closures of > > > ExAy(yex <-> (yez & Phi)). > > > / > > > I say the above statement is actually equivalent to the unique > > separation schema mentioned above. > > I haven't looked over your new formulations, but last night I did > figure out a way to formulate your compression schema so that it and > your union axiom entail the separation(with built in extensionality) > schema, while the separation schema (with built in extensionality) > entails your compression schema. > > However, then it can't be the case that your compression schema, union > schema, and infinity entail pairing and power set (did I understand > correctly that you claim they do entail pairing and power set?), for > then they would not be independent in Z set theory, though it has been > proven that they are independent in Z set theory. > > MoeBlee Well I don't know what is your formulation yet. But I think we need to look at what I wrote here. Since there might be a mistake then. Anyhow let see the proof of pairing and power. (1)The proof of power: The formula in comprehension schema reads: Aw1...wn Ar As E!x Ay (y e x <-> (( y c r \/ y c s ) /\ phi(y,w1,...,wn))) Now let r=s and let n=0, then we'll have: Ar E!x Ay (y e x <-> ( y c r /\ phi(y))) Let phi(y)<->y=y thus we'll end up with Ar E!x Ay (y e x <-> y c r) It is clear that x is the power-set of r. Thus power is proved. (2)The proof of pairing: from comprehension with n=2 ,we have: Aw1 Aw2 Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ phi(y,w1,w2))) let phi(y,w1,w2)<->(y=w1 \/ y=w2) then: Aw1 Aw2 Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ (y=w1 \/ y=w2))) take r=w1, s=w2 then: Aw1 Aw2 E!x Ay (y e x <-> ((y c w1 \/ y c w2) /\ (y=w1 \/ y=w2))) which is reduced to: Aw1 Aw2 E!x Ay (y e x <-> (y=w1 \/ y=w2)) which is pairing. I don't know what you meant about the issue with the independence of these axioms in Z, and how that can be affected if they spring from comprehension and union. To me I don't see that this would affect their independence at all. Zuhair
From: zuhair on 16 Jun 2010 17:58
On Jun 16, 4:15 pm, MoeBlee <jazzm...(a)hotmail.com> wrote: > On Jun 16, 2:32 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > Moe Blee in a previous post asked me to show the following: > > > For ARBITRARY formula Phi (except we know x not free in Phi): > > > all closures of > > > ExAy(yex <-> (yez & Phi)). > > > / > > > I say the above statement is actually equivalent to the unique > > separation schema mentioned above. > > I haven't looked over your new formulations, but last night I did > figure out a way to formulate your compression schema so that it and > your union axiom entail the separation(with built in extensionality) > schema, while the separation schema (with built in extensionality) > entails your compression schema. > > However, then it can't be the case that your compression schema, union > schema, and infinity entail pairing and power set (did I understand > correctly that you claim they do entail pairing and power set?), for > then they would not be independent in Z set theory, though it has been > proven that they are independent in Z set theory. > > MoeBlee Well I don't know what is your formulation yet. But I think we need to look at what I wrote here. Since there might be a mistake then. Anyhow let see the proof of pairing and power. (1)The proof of power: The formula in comprehension schema reads: Aw1...wn Ar As E!x Ay (y e x <-> (( y c r \/ y c s ) /\ phi(y,w1,...,wn))) Now let r=s and let n=0, then we'll have: Ar E!x Ay (y e x <-> ( y c r /\ phi(y))) Let phi(y)<->y=y thus we'll end up with Ar E!x Ay (y e x <-> y c r) QED. (2)The proof of pairing: from comprehension with n=0 ,we have: Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ phi(y))) let phi(y)<-> y=y then: Ar As E!x Ay (y e x <-> (y c r \/ y c s)) since Ar As ( r c r /\ s c s ) then r and s are members of x thus pairing proved! (axiom of pairing is Ar As Ex ( r e x /\ s e x ). QED I don't know what you meant about the issue with the independence of these axioms in Z, and how that can be affected if they spring from comprehension and union. To me I don't see that this would affect their independence at all. Zuhair |