Abbreviating FOL with identity and membership2
in [Math]
|
From: zuhair on 1 May 2010 19:37 > > 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, No dot notation is used at all.
From: zuhair on 1 May 2010 20:32 On May 1, 11:42 am, zuhair <zaljo...(a)gmail.com> wrote: > This is the continuation of the same topic that I've lastly posted to > this Usenet. > > Seeing the dot system I would like to make some modification on the > system that I proposed in the previous post. > > Alternative Notation of FOL(=,membership) > > (1) Logical connectives > > Negation ~ > > Disjunction | > > Implication > > > Bi-conditional <> > > Conjunction No symbol, jusxtapositionning the formulae. > > so QP stands for Q and P. > > (2) Quantifiers > > Existential quantifier _ > > so _x stands for 'there exist x'. > > Unique Existential quantifier ! > > !x stands for 'there exist only one x'. > > Universal quantifier no symbol only write the quantified variable. > > Example: > > x _y is read as: for all x there exist y > > 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) > > The order of the quantifiers > > if x is written to the left of y for example > then the order of quantification is the same > > For example > > _x ~yx > > this is the Empty set axiom, it is read as > > There exist x for all y not y in x. > > We don't need to write > > _x y ~yx > > because the y in the middle add nothing to the meaning > of the sentence, so it is redundant. > > However this method is tricky, for example > > ~yx alone would be read as for all y for all x not y in x. > > also > > _y yx > > is read as, there exist y for all x y in x. > > While > > x _y ~yx is read as: > > For all x there exist y not y in x. > > (3) Quantification strings > > To write for example > > Exist x0, Exist x1,...,Exist xn > > which is usually written as > > Exist x0,...,xn > > We write it here as: > > _x0,,,xn > > while, for all x0, for all x1,..., for all xn > > is written as > > x0,,,xn > > while Exist x0 for all x1, for all x2,...,for all xn > > is written as: > > _x0; x1,,,xn > > so a semi-colon separates x0 from x1. > > (4) Primitives: > > Membership No symbol > > only juxtapositioning the two symbols. > > Example: xy mean x is a member of y > > Identity = > > (4) Functions: the same traditional way of symbolization > > F(x1,,,xn) > > The ordered pair is written as (x,y). > > f: A -> B means f is a function from the domain A to the > co-domain B. > > (5) Predicates: written in the usual manner. > > (6) The class builder notation { : } or { | } > is to remain as it is. > > (7) Dots notations, these serve to determine the sequence of > processing the formulas in a certain formula, so they > replace brackets in performing that function. > > Generally the flow is from the smaller power dot notations > to the larger ones. > > A dot notation is to be placed always on the left of a connective. > > we have different powers of dot notations:- > > . is a unit power dot notation > > : is a double power dot notation > > :. is a triple power dot notation > > :: is a quadruple power dot notation > > ::. is a five unit power dot notation > > and so on, the power of a dot notation is determined directly > by the number of dots in it. > > of course the first connectives to be processed are > those who do not have any dot notation on the left of them. > > Examples: > > P|Q.|Q:>D.S<>K > > this would be ( (P|Q) | Q ) > (D and (S<>K)) > > so instead of 8 brackets, we only have three controller symbols. > > Another example: > > P|Q:.|Q:>D.S<>K > > this would be > > (P|Q) | (Q>(D and (S<>K))) > > 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 > > 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)). > > As one can see, there is a great difference in the size, and > clarity of the two formulas. > > As a last example, I shall re-write the formulas of the axioms > of ZF set theory: > > _______________________________________________ > > Extensionality: zx<>zy > x=y > > Foundation: x _yx > _yx _cy cx > > Empty: _x ~yx > > Pairing: a,b _x yx.<> y=a|y=b > > Union: a _x yx <> _z yza > > Power: a _x yx<> zy>za > > Separation: a _x yx.<> yaQ > > Replacement: x!yQ> a _b zb <>_xaQ(x,z) > _______________________________________________ > > This technique greatly abbreviate fol(=,membership), and it is > clearer, more neat and do not have strange looking symbols in them. > > Isn't it? > > Zuhair Three rules must be mentioned though (1)The rule of Exhaustive quantification, Quantification ends when the symbols quantified upon do not further appear in the formula, unless there are symbols still appearing that are quantified after, or dot notation clarify otherwise. So for example: zx<>zy > y=x clearly z seize to appear after the implication symbol, and since there is no dot notation appearing in the formula, then what is expected is that this mean the following for all z (z e x <-> zey) -> y=x it is clear that y and x have an order in quantification that precedes z since they appear on both sides of implication while z don't. However suppose we wrote the following formula zx<>zy. > y=x here it is clear from the dot after zy that the quantification over z do not end before the implication so the above is read as for all z (( z e x <-> z e y ) -> y=x). that's why the dot is placed, other wise if left without a dot then we can't discriminate it from for all z(zex <-> (zey -> y=x)) which is written as zx. <> zy>y=x On the other hand take the following formula x!yQ> a _b zb<>_xaQ(x,z) Now the symbol b seize to appear after the bi-conditional, but yet that doesn't mean that the quantification over b ended i.e. that doesn't mean x!yQ> a exist b for z (zeb) <> exist x in a Q(x,z) the reason is because z is quantified "after" b, so since z appear on the right of the bi-conditional then the quantification over b extends as far as that over z. This complete the understanding of rule 1. (2) the Rule of minimal requirement for unique readability. a formula is acceptable using this system only if it leads to one interpretation, now the minimal amount of symbols that renders the formula uniquely interpretable is what is needed, so extra dot notations are deemed redundant and not acceptable. (3) Quantification can obviates the need for do notation. Example Extensional. so for all z ( z e y <-> z e x) is considered as one block. zy<>zx>y=x do not lead to any bi-interpret-ability because zy<>zx here refers to for all z ( z e y <-> z e x), which is one statement. Zuhair
From: Jesse F. Hughes on 2 May 2010 08:51 zuhair <zaljohar(a)gmail.com> writes: > 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. Oh? Then how do you write Az((zex <-> zey) -> x=y)? Is the difference merely in the number of spaces? > 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! Yes, number of characters is the most accurate way to indicate readability. Good job! -- "Mathematicians are rather important in the infrastructures of many organizations that protect civilization. I've determined that they are a consistent security risk, and seem to have other agendas, other loyalties beyond loyalty to their respective nations." -- James Harris
From: zuhair on 2 May 2010 09:21 On May 2, 7:51 am, "Jesse F. Hughes" <je...(a)phiwumbda.org> wrote: > zuhair <zaljo...(a)gmail.com> writes: > > 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. > > Oh? Then how do you write > > Az((zex <-> zey) -> x=y)? If you read my reply to Moe, then you'd seen the answer. Az((zex <-> zey) -> x=y) is written in the following way: zx<>zy.>x=y you must place the dot after zy, otherwise you will end up with a statement that is not uniquely interpretable (that is if you take it to represent z being quantified upon over both sides). the only way zx<>zy > x=y, would make sense in this notation is if quantification over z ends before the implication since zx<>zy would by then represent a closed sentence, and not confusion as to its interpret-ability would rise. So in short, if quantification over z closes after x=y, then in order to avoid bi-interpretability, you must place a dot after zy; while if quantification over z closes after zy, then you don't need to place a dot after zy, since the issue of bi-interpretability disappears by then. > > Is the difference merely in the number of spaces? No, the approach here do not use space. I think for further reading, its better to refer to my last post on that matter it has the same title with number 3 instad of 2. > > > 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! > > Yes, number of characters is the most accurate way to indicate > readability. Good job! No, I didn't say that, I said abbreviation is measured by the number of characters, and it was abbreviation that is the main concern behind writing this notation. Of course with this extreme version of abbreviation readability would be somewhat harder, this is expected, see my reply Elliot in my last post. However in addition to abbreviation, I claim that this notation is not crowded doesn't contain odd looking symbols like an upside-down A, or a turnaround E, or and an upside-down large V, etc..., also it contains less repeatable symbols in them. I assume that all these properties would make the formulae written here neater, and nicer looking. The problem with readability of this syntax, rises from the abbreviation power of it and from having many rules in it (please see the last post I referred to above). Zuhair > -- > "Mathematicians are rather important in the infrastructures of many > organizations that protect civilization. I've determined that they > are a consistent security risk, and seem to have other agendas, other > loyalties beyond loyalty to their respective nations." -- James Harris
From: Daryl McCullough on 2 May 2010 09:59
Jesse F. Hughes says... >Yes, number of characters is the most accurate way to indicate >readability. Good job! When I was in college, one of my classmates liked to program in APL, whose claim to fame was the ability to write incredibly powerful programs in just one line of code. Some examples are in Wikipedia: http://en.wikipedia.org/wiki/APL_%28programming_language%29 The following expression sorts a word list stored in matrix X according to word length: X[⍋X+.≠' ';] This following immediate-mode expression generates a typical set of Pick 6 lottery numbers: six pseudo-random integers ranging from 1 through 40, guaranteed non-repeating, and displays them sorted in ascending order: x[⍋x←6?40] -- Daryl McCullough Ithaca, NY |