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: zuhair on 12 Jun 2010 16:42 I think that Z-Reg. is equal to the following theory in FOL(=,e) with the following axiom schemes: (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". take phi <-> (y e r /\ pi) were y is free in pi and x do not occur in pi. substitute in comprehension we have: Ar" E!x Ay (y e x <-> (y c r" /\ y e r /\ pi)) this would entail that Ar E!x Ay (yex <-> (y e r /\ pi)). QED. Now this would prove Extensionality. Pairing is easily proved from comprehension by letting phi <-> ( y=r \/ y=s ) Power is easily proved from comprehension by letting phi <-> y=y and let r=s. Thus all axioms of Z-Reg. are proved in this theory, thus Z-Reg is a sub-theory of this theory. On the other hand it is clear that the comprehension scheme of this theory is a sub-theory of Z, since (y c r \/ y c s) <-> y e P(r) U P(s) Now P(r) U P(s) is a set , thus the formula in Comprehension schema would mount to: Ar As E!x Ay (y e x <-> (y e P(r) U P(s) /\ phi)) which is a sub-theory of Z-Reg. Thus the following theory is equal to Z-Reg. However the nice thing about this Reformulation of Z-Reg. is that it is shorter than the standard one. Zuhair
From: George Greene on 12 Jun 2010 16:51 On Jun 12, 4:42 pm, zuhair <zaljo...(a)gmail.com> wrote: > I think that Z-Reg. is equal to the following theory in > FOL(=,e) with the following axiom schemes: > > (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. You cannot claim to be simplifying anything while adding a whole new kind of quantifier.
From: zuhair on 12 Jun 2010 16:59 On Jun 12, 3:51 pm, George Greene <gree...(a)email.unc.edu> wrote: > On Jun 12, 4:42 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > I think that Z-Reg. is equal to the following theory in > > FOL(=,e) with the following axiom schemes: > > > (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. > > You cannot claim to be simplifying anything while adding a whole new > kind of quantifier. There is no new quantifier here, although I am speaking here of Z, but yet the uniqueness quantifier is used in the language of ZF, review axiom of Replacement. We can dispense altogether with writing the uniqueness symbol. see the following: Ar As Ez Ax ( Ay(y e x <-> ((y c r \/ y c s) /\ phi)) <-> x=z ). which is equivalent to the formula in comprehension written above. Still the formulation is shorter than written Extensionality as an axiom. We write the uniqueness symbol for simplicity only, but we can dispense with it altogether as I showed above. Zuhair
From: zuhair on 12 Jun 2010 18:11 On Jun 12, 3:59 pm, zuhair <zaljo...(a)gmail.com> wrote: > On Jun 12, 3:51 pm, George Greene <gree...(a)email.unc.edu> wrote: > > > On Jun 12, 4:42 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > > I think that Z-Reg. is equal to the following theory in > > > FOL(=,e) with the following axiom schemes: > > > > (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. > > > You cannot claim to be simplifying anything while adding a whole new > > kind of quantifier. > There is no new quantifier here, although I am speaking here of Z, but yet the uniqueness quantifier is used in the language of ZF, review axiom of Replacement. We can dispense altogether with writing the uniqueness symbol. see the following: Ar As Ez Ax ( Ay(y e x <-> ((y c r \/ y c s) /\ phi)) <-> x=z ). which is equivalent to the formula in comprehension written above. Still the formulation is shorter than writing Extensionality as an axiom. We write the uniqueness symbol for simplicity only, but we can dispense with it altogether as I showed above. Zuhair
From: zuhair on 12 Jun 2010 18:13
On Jun 12, 3:51 pm, George Greene <gree...(a)email.unc.edu> wrote: > On Jun 12, 4:42 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > I think that Z-Reg. is equal to the following theory in > > FOL(=,e) with the following axiom schemes: > > > (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. > > You cannot claim to be simplifying anything while adding a whole new > kind of quantifier. There is no new quantifier here, although I am speaking here of Z, but yet the uniqueness quantifier is used in the language of ZF, review axiom of Replacement, also we use it as a shorthand to write many theorems in Z, for example the theorem E!x Ay (~ y e x), etc.. We can dispense altogether with writing the uniqueness symbol. see the following: Ar As Ez Ax ( Ay(y e x <-> ((y c r \/ y c s) /\ phi)) <-> x=z ). which is equivalent to the formula in comprehension written above. Still the formulation is shorter than writing Extensionality as an axiom. We write the uniqueness symbol for simplicity only, but we can dispense with it altogether as I showed above. Zuhair |