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 14 Jun 2010 12:50 On Jun 12, 3:42 pm, zuhair <zaljo...(a)gmail.com> wrote: > (1)Comprehension: If phi is a formula in which at least y is free, and > in which x is not free, then all closures of > > Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ phi)) > > are axioms. > > were c refers to the subset relation defined in the standard manner. > > (2) Union: written in the standard manner. > (3) Infinity: written in the standard manner. > > Proof: > > first we prove what I call *unique Separation*, were for the same > specifications of phi listed in comprehension above, we have all > closures of > > Ar E!x Ay (y e x <-> (y e r /\ phi)) > > are axioms. > > Proof: form union for any set r, we have at least one set r" such that > every member of r is a subset of r". Yes, we have Axer r subset Ur. So Er* Axer r subset r*. So, existentially instantiate to get: Axer r subset r*. > take phi <-> (y e r /\ pi) I think I know what you're doing here, but it's possibly confusing. We need to prove for a given phi, which we can't switch to pi. So, instead I'd say: Let x not be free in phi (we only need to prove for phi in which x is not free, so whether y is free in phi doesn't matter for this step, because you have a free y in "yer" for purposes of your comprehension schema). So comprehension gives: E!xAy(yex <-> ((y subset r* or y subset s) & yer* & phi[r* | r])) Notice, now that we lost phi, and instead have phi[r* | r]. I.e., phi except all free occurrences of r replaced by r*. I don't see how you can avoid that, That is, if you use r* instead of r in the comprehension schema, then it has to be r* in your "phi" formula too (which is now "yer & Phi", which with the substitution becomes "yer* & phi[r* | r]. You can't just swap SOME of the variables when restating comprehension in terms of r* instead of r. And you can't stipulate that r does not occur free in phi anyway; the reason you can't stipulate that is that phi is ANY formula in which x does not occur free, and that includes those phi in which r occurs free. If I am confused on this point, or have overlooked a workaround, then someone may correct me. So now you need to prove E!xAy(yex <-> (yez /\ phi)) And you can't let z be r*, since r* came from existential instantiation and thus is not arbitrary any longer. MoeBlee
From: zuhair on 14 Jun 2010 21:55 On Jun 14, 11:50 am, MoeBlee <jazzm...(a)hotmail.com> wrote: > On Jun 12, 3:42 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > > > (1)Comprehension: If phi is a formula in which at least y is free, and > > in which x is not free, then all closures of > > > Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ phi)) > > > are axioms. > > > were c refers to the subset relation defined in the standard manner. > > > (2) Union: written in the standard manner. > > (3) Infinity: written in the standard manner. > > > Proof: > > > first we prove what I call *unique Separation*, were for the same > > specifications of phi listed in comprehension above, we have all > > closures of > > > Ar E!x Ay (y e x <-> (y e r /\ phi)) > > > are axioms. > > > Proof: form union for any set r, we have at least one set r" such that > > every member of r is a subset of r". > > Yes, we have Axer r subset Ur. > > So Er* Axer r subset r*. > > So, existentially instantiate to get: > > Axer r subset r*. > > > take phi <-> (y e r /\ pi) > > I think I know what you're doing here, but it's possibly confusing. > > We need to prove for a given phi, which we can't switch to pi. > > So, instead I'd say: > > Let x not be free in phi (we only need to prove for phi in which x is > not free, so whether y is free in phi doesn't matter for this step, > because you have a free y in "yer" for purposes of your comprehension > schema). > > So comprehension gives: > > E!xAy(yex <-> ((y subset r* or y subset s) & yer* & phi[r* | r])) > > Notice, now that we lost phi, and instead have phi[r* | r]. I.e., phi > except all free occurrences of r replaced by r*. I don't see how you > can avoid that, That is, if you use r* instead of r in the > comprehension schema, then it has to be r* in your "phi" formula too > (which is now "yer & Phi", which with the substitution becomes "yer* & > phi[r* | r]. You can't just swap SOME of the variables when restating > comprehension in terms of r* instead of r. And you can't stipulate > that r does not occur free in phi anyway; the reason you can't > stipulate that is that phi is ANY formula in which x does not occur > free, and that includes those phi in which r occurs free. > > If I am confused on this point, or have overlooked a workaround, then > someone may correct me. > > So now you need to prove > > E!xAy(yex <-> (yez /\ phi)) > > And you can't let z be r*, since r* came from existential > instantiation and thus is not arbitrary any longer. > > MoeBlee 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. / 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)) ). 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* Now let Phi(y,w1)<-> (y e w1 /\ pi(y,w1)) so we have Aw1 Aw* E!x Ay ( y e x <-> ( y c w* /\ y e w1 /\ pi(y,w1) ) ) Now since it is true that for every w1 and w* all y (y e w1 -> y c w*) therefore we can eliminate w* to have Aw1 E!x Ay ( y e x <-> (y e w1 /\ pi ) ) QED.
From: zuhair on 14 Jun 2010 22:23 On Jun 14, 11:50 am, MoeBlee <jazzm...(a)hotmail.com> wrote: > On Jun 12, 3:42 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > > > (1)Comprehension: If phi is a formula in which at least y is free, and > > in which x is not free, then all closures of > > > Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ phi)) > > > are axioms. > > > were c refers to the subset relation defined in the standard manner. > > > (2) Union: written in the standard manner. > > (3) Infinity: written in the standard manner. > > > Proof: > > > first we prove what I call *unique Separation*, were for the same > > specifications of phi listed in comprehension above, we have all > > closures of > > > Ar E!x Ay (y e x <-> (y e r /\ phi)) > > > are axioms. > > > Proof: form union for any set r, we have at least one set r" such that > > every member of r is a subset of r". > > Yes, we have Axer r subset Ur. > > So Er* Axer r subset r*. > > So, existentially instantiate to get: > > Axer r subset r*. > > > take phi <-> (y e r /\ pi) > > I think I know what you're doing here, but it's possibly confusing. > > We need to prove for a given phi, which we can't switch to pi. > > So, instead I'd say: > > Let x not be free in phi (we only need to prove for phi in which x is > not free, so whether y is free in phi doesn't matter for this step, > because you have a free y in "yer" for purposes of your comprehension > schema). > > So comprehension gives: > > E!xAy(yex <-> ((y subset r* or y subset s) & yer* & phi[r* | r])) > > Notice, now that we lost phi, and instead have phi[r* | r]. I.e., phi > except all free occurrences of r replaced by r*. I don't see how you > can avoid that, That is, if you use r* instead of r in the > comprehension schema, then it has to be r* in your "phi" formula too > (which is now "yer & Phi", which with the substitution becomes "yer* & > phi[r* | r]. You can't just swap SOME of the variables when restating > comprehension in terms of r* instead of r. And you can't stipulate > that r does not occur free in phi anyway; the reason you can't > stipulate that is that phi is ANY formula in which x does not occur > free, and that includes those phi in which r occurs free. > > If I am confused on this point, or have overlooked a workaround, then > someone may correct me. > > So now you need to prove > > E!xAy(yex <-> (yez /\ phi)) > > And you can't let z be r*, since r* came from existential > instantiation and thus is not arbitrary any longer. > > MoeBlee Also one can present matters in a more general manner. Comprehension officially 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. / Now what we need to prove is: 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 Ar E!x Ay (y e x <-> ( y e r /\ Phi(y,w1,...,wn))) is an axiom. Now the first step is to let r=s then from comprehension we'll have: 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 any formula in fOL with identity and membership that has y,w1,...,wn as its sole free variables. Now take r when r is a set such that every member of w1 is a subset of r, the proof that such a set r must exist comes directly from axiom of union. substitute in comprehension above: Aw1...wn Ar E!x Ay (y e x <-> (y c r /\ y e w1 /\ pi (y,w1,...,wn))) since y e w1 -> y c r then we can remove r and we'll have Aw1...wn E!x Ay (y e x <-> (y e w1 /\ pi (y,w1,...,wn))) which is what we want.
From: zuhair on 14 Jun 2010 22:41 On Jun 14, 9:23 pm, zuhair <zaljo...(a)gmail.com> wrote: > On Jun 14, 11:50 am, MoeBlee <jazzm...(a)hotmail.com> wrote: > > > > > On Jun 12, 3:42 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > > (1)Comprehension: If phi is a formula in which at least y is free, and > > > in which x is not free, then all closures of > > > > Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ phi)) > > > > are axioms. > > > > were c refers to the subset relation defined in the standard manner. > > > > (2) Union: written in the standard manner. > > > (3) Infinity: written in the standard manner. > > > > Proof: > > > > first we prove what I call *unique Separation*, were for the same > > > specifications of phi listed in comprehension above, we have all > > > closures of > > > > Ar E!x Ay (y e x <-> (y e r /\ phi)) > > > > are axioms. > > > > Proof: form union for any set r, we have at least one set r" such that > > > every member of r is a subset of r". > > > Yes, we have Axer r subset Ur. > > > So Er* Axer r subset r*. > > > So, existentially instantiate to get: > > > Axer r subset r*. > > > > take phi <-> (y e r /\ pi) > > > I think I know what you're doing here, but it's possibly confusing. > > > We need to prove for a given phi, which we can't switch to pi. > > > So, instead I'd say: > > > Let x not be free in phi (we only need to prove for phi in which x is > > not free, so whether y is free in phi doesn't matter for this step, > > because you have a free y in "yer" for purposes of your comprehension > > schema). > > > So comprehension gives: > > > E!xAy(yex <-> ((y subset r* or y subset s) & yer* & phi[r* | r])) > > > Notice, now that we lost phi, and instead have phi[r* | r]. I.e., phi > > except all free occurrences of r replaced by r*. I don't see how you > > can avoid that, That is, if you use r* instead of r in the > > comprehension schema, then it has to be r* in your "phi" formula too > > (which is now "yer & Phi", which with the substitution becomes "yer* & > > phi[r* | r]. You can't just swap SOME of the variables when restating > > comprehension in terms of r* instead of r. And you can't stipulate > > that r does not occur free in phi anyway; the reason you can't > > stipulate that is that phi is ANY formula in which x does not occur > > free, and that includes those phi in which r occurs free. > > > If I am confused on this point, or have overlooked a workaround, then > > someone may correct me. > > > So now you need to prove > > > E!xAy(yex <-> (yez /\ phi)) > > > And you can't let z be r*, since r* came from existential > > instantiation and thus is not arbitrary any longer. > > > MoeBlee > > Also one can present matters in a more general manner. > > Comprehension officially 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. > / > > Now what we need to prove is: > > 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 Ar E!x Ay (y e x <-> ( y e r /\ Phi(y,w1,...,wn))) > > is an axiom. > > Now the first step is to let r=s then from comprehension we'll have: > > 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 any formula in fOL with identity and > membership > that has y,w1,...,wn as its sole free variables. > > Now take r when r is a set such that every member of w1 is a subset of > r, the proof that such a set r must exist comes directly from axiom of > union. > > substitute in comprehension above: > > Aw1...wn Ar E!x Ay (y e x <-> (y c r /\ y e w1 /\ pi (y,w1,...,wn))) > > since y e w1 -> y c r > > then we can remove r and we'll have > > Aw1...wn E!x Ay (y e x <-> (y e w1 /\ pi (y,w1,...,wn))) The only thing that I am noticing here is that w1 is present in pi as a free variable, while unique separation must read as: Aw1...wn Ar E!x Ay (y e x <-> (y e r /\ pi (y,w1,...,wn))) I need to look into that. Zuhair
From: zuhair on 14 Jun 2010 22:56
On Jun 14, 9:41 pm, zuhair <zaljo...(a)gmail.com> wrote: > On Jun 14, 9:23 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > > > On Jun 14, 11:50 am, MoeBlee <jazzm...(a)hotmail.com> wrote: > > > > On Jun 12, 3:42 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > > > (1)Comprehension: If phi is a formula in which at least y is free, and > > > > in which x is not free, then all closures of > > > > > Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ phi)) > > > > > are axioms. > > > > > were c refers to the subset relation defined in the standard manner.. > > > > > (2) Union: written in the standard manner. > > > > (3) Infinity: written in the standard manner. > > > > > Proof: > > > > > first we prove what I call *unique Separation*, were for the same > > > > specifications of phi listed in comprehension above, we have all > > > > closures of > > > > > Ar E!x Ay (y e x <-> (y e r /\ phi)) > > > > > are axioms. > > > > > Proof: form union for any set r, we have at least one set r" such that > > > > every member of r is a subset of r". > > > > Yes, we have Axer r subset Ur. > > > > So Er* Axer r subset r*. > > > > So, existentially instantiate to get: > > > > Axer r subset r*. > > > > > take phi <-> (y e r /\ pi) > > > > I think I know what you're doing here, but it's possibly confusing. > > > > We need to prove for a given phi, which we can't switch to pi. > > > > So, instead I'd say: > > > > Let x not be free in phi (we only need to prove for phi in which x is > > > not free, so whether y is free in phi doesn't matter for this step, > > > because you have a free y in "yer" for purposes of your comprehension > > > schema). > > > > So comprehension gives: > > > > E!xAy(yex <-> ((y subset r* or y subset s) & yer* & phi[r* | r])) > > > > Notice, now that we lost phi, and instead have phi[r* | r]. I.e., phi > > > except all free occurrences of r replaced by r*. I don't see how you > > > can avoid that, That is, if you use r* instead of r in the > > > comprehension schema, then it has to be r* in your "phi" formula too > > > (which is now "yer & Phi", which with the substitution becomes "yer* & > > > phi[r* | r]. You can't just swap SOME of the variables when restating > > > comprehension in terms of r* instead of r. And you can't stipulate > > > that r does not occur free in phi anyway; the reason you can't > > > stipulate that is that phi is ANY formula in which x does not occur > > > free, and that includes those phi in which r occurs free. > > > > If I am confused on this point, or have overlooked a workaround, then > > > someone may correct me. > > > > So now you need to prove > > > > E!xAy(yex <-> (yez /\ phi)) > > > > And you can't let z be r*, since r* came from existential > > > instantiation and thus is not arbitrary any longer. > > > > MoeBlee > > > Also one can present matters in a more general manner. > > > Comprehension officially 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. > > / > > > Now what we need to prove is: > > > 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 Ar E!x Ay (y e x <-> ( y e r /\ Phi(y,w1,...,wn))) > > > is an axiom. > > > Now the first step is to let r=s then from comprehension we'll have: > > > 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 any formula in fOL with identity and > > membership > > that has y,w1,...,wn as its sole free variables. > > > Now take r when r is a set such that every member of w1 is a subset of > > r, the proof that such a set r must exist comes directly from axiom of > > union. > > > substitute in comprehension above: > > > Aw1...wn Ar E!x Ay (y e x <-> (y c r /\ y e w1 /\ pi (y,w1,...,wn))) > > > since y e w1 -> y c r > > > then we can remove r and we'll have > > > Aw1...wn E!x Ay (y e x <-> (y e w1 /\ pi (y,w1,...,wn))) > > The only thing that I am noticing here is that w1 is present in pi > as a free variable, while unique separation must read as: > > Aw1...wn Ar E!x Ay (y e x <-> (y e r /\ pi (y,w1,...,wn))) > > I need to look into that. > > Zuhair after a close look, I see both formulations of unique separation equivalent to each other. Axiom of unique separation can be stated in the following manner: For n=1,2,3,..., if phi(y,w1,...,wn) is a formula in which y,w1,...,wn are its sole free variables, then Aw1...wn E!x Ay ( y e x <-> ( y e w1 & phi (y,w1,...,wn) ) ) is an axiom. this would turn to be equivalent to for all n=0,1,2,3,...,if phi(y,w1,...,wn) is a formula in which y,w1,...,wn are its sole free variables, then Aw1...wn Ar E!x Ay ( y e x <-> ( y e r & phi (y,w1,...,wn) ) ) is an axiom. Although for the first glance r looks independent from the list of free variables in phi, while w1 is not, but yet both will turn to be equivalent formulations. one can easily make a formula of phi(y,w1) to be equivalent to a formula of phi(y) take Q(y) we can have phi(y,w1)<-> Q(y) /\ w1=w1 So both formulations are equivalent. then unique separation is proved. Thus this theory is equal to Z-Reg. Zuhair |