Abbreviating FOL with identity and membership2
in [Math]
|
From: zuhair on 1 May 2010 15:10 On May 1, 1:58 pm, "Jesse F. Hughes" <je...(a)phiwumbda.org> wrote: > zuhair <zaljo...(a)gmail.com> writes: > > On May 1, 12:22 pm, MoeBlee <jazzm...(a)hotmail.com> wrote: > >> On May 1, 9:42 am, zuhair <zaljo...(a)gmail.com> wrote: > > >> > The quantifiers need not be actually written if writing them > >> > makes no difference to the meaning of the formula > > >> > Example: writing the Extensionality axiom (see below) > > >> [...] > > >> > Extensionality: zx<>zy > x=y > > >> WRONG > > >> Az(zex <-> zey) -> x=y > > >> is NOT equivalent with > > >> Az((zex <-> zey) -> x=y) > > >> Please get a book on the basics of this subject. > > >> MoeBlee > > > hmmm...., > > > it seems that we must apply the dot notation to be sometimes > > on the right of quantifiers also. > > > like: > > > z.zx<>zy:> y=x > > Boy, that's *much* more readable than > > Az(zex <-> zey) -> x=y > > Kudos! > > -- > Jesse F. Hughes > "[M]oving towards development meetings for new release class viewer 5.0 > and since [I]'m the only developer, easy to schedule." > --James S. Harris tweets on code development No Jesse, you came late. The correct way to write Az(zex <-> zey) -> x=y using this system is zx<>zy > x=y I was correct really. Sorry for the confusion. And I do think that zx<>zy > x=y is by far more neat and nicer than the clumsy Az(zex <-> zey) -> x=y this have 18 characters while the above have only 10, almost a half size reduction! Zuhair
From: zuhair on 1 May 2010 18:49 On May 1, 1:51 pm, zuhair <zaljo...(a)gmail.com> wrote: > On May 1, 1:40 pm, zuhair <zaljo...(a)gmail.com> wrote: > > > > > > > On May 1, 12:22 pm, MoeBlee <jazzm...(a)hotmail.com> wrote: > > > > On May 1, 9:42 am, zuhair <zaljo...(a)gmail.com> wrote: > > > > > The quantifiers need not be actually written if writing them > > > > makes no difference to the meaning of the formula > > > > > Example: writing the Extensionality axiom (see below) > > > > [...] > > > > > Extensionality: zx<>zy > x=y > > > > WRONG > > > > Az(zex <-> zey) -> x=y > > > > is NOT equivalent with > > > > Az((zex <-> zey) -> x=y) > > > > Please get a book on the basics of this subject. > > > > MoeBlee > > > Ok Moe, sorry for the above replies, the following is the correct one: > > > All right, my way of writing it was correct, actually, but I myself > > had forgotten the rational behind it. > > > zx<>zy>y=x > > > this is read as for all z ( z in x iff z in y ) -> x=y, which is > > Extensionality. > > > there is nothing wrong with the notation. > > > The reason here is because I am using quantification itself as a flow > > controller. > > > To make matters clearer zx<>zy>y=x CANNOT be used to symbolize > > > for all z (( z in x iff z in y) -> x=y) as you thought! > > > this is actually written as zx<>zy.>x=y > > > the reason is as you see there is no dot notation whatsoever in > > zx<>zy>y=x > > > so if we say that this is taken to represent > > for all z (( z in x iff z in y) -> x=y), then the question wold > > be:which connective we work first? is it the bi-conditional or the > > implication? > > as you see this would be "undetermined" because there is no dot > > notation > > on the left of any connective! > > > The only way zx<>zy>y=x would make sense is if the quantification by z > > would end before the implication, since by then zx<>zy would be > > considered > > as one block, therefore obviating the need for dot notation. > > > I agree that this is complex somehow though. > > > Zuhair > > To add to that, still the idea of Exhaustive quantification holds > also. > I thought it want work but actually it works. > > To correct some earlier errors: > > Example: > > t _x yt::.<> w _k uw::<> u is a wiener ordered pair > i _s,r isru > i subset k: > j _p,q jpqu 0eq. > j=x:. > > yw Really old habits die hard! the formula is t _x yt::.<> w _k uw::<> u is a wiener ordered pair i _s,r isru > i subset k: j _p,q jpqu 0q. > j=x:. > yw Regards > > is the abbreviation of > > for all t Exist x for all y ( y e t <-> for all w > ( Exist k for all u ( u e w <-> > (u is a wiener ordered pair & > for all i (Exist sr iesereu -> i subset k)& > for all j (Exist pq (jepeqeu & 0eq) -> j=x))) > -> yew)). > > so we have 5 dot notations, abbreviating 14 bracket! > > Zuhair
From: zuhair on 1 May 2010 19:02 > > Really old habits die hard! > > the formula is > > t _x yt::.<> w _k uw::<> u is a wiener ordered pair > i _s,r isru > i subset k: > j _p,q jpqu 0q. > j=x:. > > yw > Actually using the principle of exhaustive quantification this can be written as: _x yt:.<> w _k uw:<> u is a wiener ordered pair i _s,r isru > i subset k j _p,q jpqu 0q > j=x. > yw so instead of 14 brackets, only 3 dot notations is used which only consume four characters.
From: zuhair on 1 May 2010 19:04 > > > Example: > > > t _x yt::.<> w _k uw::<> u is a wiener ordered pair > > i _s,r isru > i subset k: > > j _p,q jpqu 0eq. > j=x:. > > > yw > Actually using the principle of exhaustive quantification this can be written as: _x yt:.<> w _k uw:<> u is a wiener ordered pair i _s,r isru > i subset k j _p,q jpqu 0q > j=x. > yw so instead of 14 brackets, only 3 dot notations is used which only consume four characters.
From: zuhair on 1 May 2010 19:07
> > Really old habits die hard! > > the formula is > > t _x yt::.<> w _k uw::<> u is a wiener ordered pair > i _s,r isru > i subset k: > j _p,q jpqu 0q. > j=x:. > > yw > > Regards > Actually using the principle of exhaustive quantification this can be written as: _x yt:.<> w _k uw:<> u is a wiener ordered pair i _s,r isru > i subset k j _p,q jpqu 0q > j=x. > yw so instead of 14 brackets, only 3 dot notations is used which only consume four characters. |