From: zuhair on
On Apr 27, 12:13 pm, zuhair <zaljo...(a)gmail.com> wrote:
> On Apr 27, 10:43 am, MoeBlee <jazzm...(a)hotmail.com> wrote:
>
> > On Apr 27, 10:41 am, MoeBlee <jazzm...(a)hotmail.com> wrote:
>
> > > But you've not given an unambiguous machine-checkable spacing RULE.
>
> > Oops, sorry, to be fair, you did just mention that you're not
> > proposing a rigorous syntax but rather informal notational
> > conventions. Okay, that is a different context for the discussion.
> > Yet, still, I personally don't find your notations helpful.
>
> > MoeBlee
>
> Well to me (a personal opinion) they are helpful, they definitely
> abbreviate
> writing these long formulas, in a matter that makes sense and even
> simplify reading these formulas, that's in addition they don't contain
> what I consider
> as clumsy notation.
>
> Regarding promoting that technique to be as what you say an:
>
> "unambiguous machine-check-able spacing RULE"
>
> I say this can be done really, but of course it will involve a lot of
> specifications
> of spacing between characters, but it is generally workable.
>
> just an "incomplete" example is to say that
>
> Rule(1):The space between any two terms and a connective between them
> must be equal.
>
> Rule(2):The lesser the space between a term and a connective, the
> first that
> connective be undone and vise verse,
>
> so for example  P  |  Q>S
>
> Now the space between Q and > is lesser than that separating Q from |
> so we must undo "implication" before disjunction, so the above would
> mean:
>
> P or (Q ->S)
>
> While  P|Q > S would mean (P or Q) -> S.
>
> Rule(3): spaces between a term c and two adjacent connectives (i.e.
> connective in which there is no intervening terms between c and
> these two connectives) Must be different iff the sequence
> of undoing the connectives makes a difference.


One can actually use comas and semi-colons as spacers:

so for example: in P|Q , the space between each formula
and the connective | is zero.

we can use the following spacers:

, single spacing (=unit spacing)

; double spacing

;, triple spacing

;; quadruple spacing

;;, five unit spacing

continue in same manner until ;;;;; which 10 unit spacing.

so for example the formula

(((A or B) and (P>S)) or (K<>C)) > (D or (K or S))


this would be abbreviated to:

A|B,P>S;| K<>S;, > D,| D|S

so instead of 14 brackets, we use only five spacer symbols.

Zuhair

















>
> Now suppose one wrote P|Q>S
>
> Now this notation is not acceptable, because
> it might make a difference to say (P or Q)->S
> from saying P or (Q->S), so the spaces between
> the variables in the above formula and the connectives must be
> different.
>
> However I think Rule(3) must be extended to cover up more complex
> formulas, in which double triple or even quadruple spacing are needed.
>
> On the other hand when the sequence of undoing connectives
> is immaterial then one can use equal spacing between formulas.
>
> For example we can write
>
> Q|S|P
>
> Also we can write
>
> QSP
>
> However to make a detailed algorithm governing that, in such a manner
> that we avoid non unique readability of all formulas, is a big job,
> which
> is something that is suitable only for computers to do, but of course
> it can be done.
>
> However my main interest was not that really, because if I do that I
> will end up
> with rules of spacing that are more or less as complex (or perhaps
> even more) as what I tried to avoid, although the net result would be
> more neat than these clumsy brackets.
>
> I wanted spacing to be left to the visual imaginative power of the
> writer, such that the writer must use spacing in such an artistic way
> that makes no two readers differ as to the interpretation of what he
> is writing.
>
> I see it as a nice short-handing of FOL formulas, and that's the main
> purpose behind developing them.
>
> However One thing to be mentioned here, is that although the syntax
> that I introduced is not an unambiguous machine-checking rule syntax,
>
> But it is meant to be written is such a way that it must avoid
> non unique readability, It is largely meant for Human minds to grasp
> it
> and not for machines to check it; it permits flexibility
> to the human mind of the writer to use his artistic capabilities
> to present the formulas in a non disputable manner.
>
> So the net reading of the formulas written in this way must be
> indisputable, although we are using a flexible syntax.
>
> Zuhair

From: zuhair on
On Apr 27, 12:16 am, zuhair <zaljo...(a)yahoo.com> wrote:
> Abbreviating FOL with identity and membership FOL(=,e)
>
> Criticism: The customary way of writing FOL(=,e) is
> ridiculous, for the following reasons
>
> (1) It contains strange symbols like for example
> the symbols used for universal quantification
> which looks like an upside-down A , and
> the symbol used for Existential quantification
> which look like a turnaround E.
>
> This gives the impression of a scribble made by
> mentally ill patients, rather than a way of writing
> a rigorous formal language.
>
> (2) It contains a lot of repeated symbols, for
> example the brackets, and the symbols for
> membership relation and the symbol of conjunction,
> now these symbols are the most repeated symbols
> and they need not be actually symbolized.
>
> (3) it can contain long sentences that are virtually
> incomprehensible, and better be broken down into
> smaller components.
>
> (4) The symbols are pretty much complex symbols
> while at the same time they are supposed to be
> denoting simple concepts, for example the symbol
> given to disjunction which is a Large V (clumsy looking actually)
> so is the symbol given for conjunction which is an upside-down V
> ,also the symbol given to implication which is virtually
> composed of three smaller symbols, which is very complex, so
> are the symbols of the quantifiers, they are too complex symbols.
>
> Alternative Notation of FOL(=,e)
>
> (1) Logical connectives
>
> Negation   ~
>
> Disjunction  |
>
> Implication  >
>
> Biconditional  <>
>
> Conjunction   No symbol, only spacing.
>
> so the formula Q and P is written as QP, no need for any symbol
> between them.
>
> Spacing will act to differentiate between different formulas
>
> Examples: for the formulas Q,P,S
>
> Q|P S  denote (Q or P) and S
>
> Q| PS denotes Q or (P and S).
>
> so by spacing technique one can differentiate between different
> formulas.
>
> So spacing technique would replace the need for brackets.
>
> (2) Quantifiers
>
> Existential quantifier    .
>
> Unique Existential quantifier   !
>
> 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 not y in x.
>
> While
>
> x .y ~yx is read as:
>
> For all x there exist y not y in x.
>
> Quantification strings
>
> To write for example
>
> Exist x0, Exist x1,...,Exist xn
>
> or usually written as
>
> Exist x0,...,xn
>
> We write
>
> .x0...xn
>
> However this must be differentiated from for example
>
> .x0,,,xn
>
> which actually means
>
> there exist x0 for all x1, for all x2,..., for all xn.
>
> However when we wright for all x0,...,xn
>
> we must wright it as
>
> x0,,,xn .
>
> (3) Primitives:
>
> Membership  No symbol
>
> only juxtapositioning the two symbols.
>
> Example:  xy  mean x is a member of y
>
> Identity  =
>
> Now lets go to examples of writing FOL(=,e) using this
> technique:
>
> Let’s write the axioms of ZF
>
> _______________________________________________
> 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(x,y) >  a .b zb<>.xaQ(x,z)
> _______________________________________________
>
> Using this technique greatly abbreviate FOL(=,e)
>
> See the following formula:
>
> Exist meR For all i Exist k,l,p,q ((0el <-> 0eq) &
> ((iekeley)<-> Exist j (jepeqem & for all z (zei<->z=j))))).
>
> Look how this is shortened to:
>
> .mR i .k.l.p.q  0l<>0q  ikly<>.jpqm zi<>z=j
>
> As one can see, this method affords a clearer way
> of writing matters, no need for clumsy brackets
> or repetitions of the membership symbol and
> the conjunction symbol
> no clumsy notation at all.
>
> Breaking down complex formulas:
>
> Complex formulas that require more than one line to write
> must be actually decomposed to smaller formulas enough
> to reduced the whole formula in one line.
>
> Example:
>
> 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))))
>
>   -> y e w)) ".
>
> Now this is a long formula, so it is better to break it to
>
> Q(u) <> u is a wiener ordered pair
>
> P(u,k) <> i .s.r isru > i subset k
>
> S(u,x) <> j .p.q jpqu 0eq  > j=x
>
> Now the above formula can be written as:
>
>  yt <>  w .k uw<>Q(u)P(u,k)S(u,x) > yw
>
> Representing relations from Domains to Co domains
>
> the symbol "to" is shortened to -> instead of -->.
>
> so R: A -> B
>
> means
>
> R is a relation from the domain A to the co domain B.
>
> I think that the above technique serve as a good abbreviation
> of writing FOL with identity and membership.
>
> Zuhair

Also one can add the colon to represent the multiple existential
quantifier

so:

:x is read as, there exist more than one x

while !x is read as, there exist a unique x

and of course

..x is read as, there exist x

Zuhair
From: Tegiri Nenashi on
On Apr 26, 10:16 pm, zuhair <zaljo...(a)yahoo.com> wrote:
> Abbreviating FOL with identity and membership FOL(=,e)
>
> Criticism: The customary way of writing FOL(=,e) is
> ridiculous, for the following reasons
>
> (1) It contains strange symbols like for example
> the symbols used for universal quantification
> which looks like an upside-down A , and
> the symbol used for Existential quantification
> which look like a turnaround E.
>
> This gives the impression of a scribble made by
> mentally ill patients, rather than a way of writing
> a rigorous formal language.

The problem is deeper than just a notation. Paul Halmos summarized it
pretty well in his essay "Autobiograohy of Polyadic Algebras"
http://www.google.com/url?sa=D&q=http://citeseerx.ist.psu.edu/viewdoc/download%3Fdoi%3D10.1.1.25.768%26rep%3Drep1%26type%3Dpdf&usg=AFQjCNFaTeC-h2vSaPnhPoVHgf5ppwBXYA
Algebraization of the first order logic is the answer. There were
several attempts, with none being convincingly sucessful.
From: zuhair on
On Apr 27, 12:16 am, zuhair <zaljo...(a)yahoo.com> wrote:
> Abbreviating FOL with identity and membership FOL(=,e)
>
> Criticism: The customary way of writing FOL(=,e) is
> ridiculous, for the following reasons
>
> (1) It contains strange symbols like for example
> the symbols used for universal quantification
> which looks like an upside-down A , and
> the symbol used for Existential quantification
> which look like a turnaround E.
>
> This gives the impression of a scribble made by
> mentally ill patients, rather than a way of writing
> a rigorous formal language.
>
> (2) It contains a lot of repeated symbols, for
> example the brackets, and the symbols for
> membership relation and the symbol of conjunction,
> now these symbols are the most repeated symbols
> and they need not be actually symbolized.
>
> (3) it can contain long sentences that are virtually
> incomprehensible, and better be broken down into
> smaller components.
>
> (4) The symbols are pretty much complex symbols
> while at the same time they are supposed to be
> denoting simple concepts, for example the symbol
> given to disjunction which is a Large V (clumsy looking actually)
> so is the symbol given for conjunction which is an upside-down V
> ,also the symbol given to implication which is virtually
> composed of three smaller symbols, which is very complex, so
> are the symbols of the quantifiers, they are too complex symbols.
>
> Alternative Notation of FOL(=,e)
>
> (1) Logical connectives
>
> Negation   ~
>
> Disjunction  |
>
> Implication  >
>
> Biconditional  <>
>
> Conjunction   No symbol, only spacing.
>
> so the formula Q and P is written as QP, no need for any symbol
> between them.
>
> Spacing will act to differentiate between different formulas
>
> Examples: for the formulas Q,P,S
>
> Q|P S  denote (Q or P) and S
>
> Q| PS denotes Q or (P and S).
>
> so by spacing technique one can differentiate between different
> formulas.
>
> So spacing technique would replace the need for brackets.
>
> (2) Quantifiers
>
> Existential quantifier    .
>
> Unique Existential quantifier   !
>
> 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 not y in x.
>
> While
>
> x .y ~yx is read as:
>
> For all x there exist y not y in x.
>
> Quantification strings
>
> To write for example
>
> Exist x0, Exist x1,...,Exist xn
>
> or usually written as
>
> Exist x0,...,xn
>
> We write
>
> .x0...xn
>
> However this must be differentiated from for example
>
> .x0,,,xn
>
> which actually means
>
> there exist x0 for all x1, for all x2,..., for all xn.
>
> However when we wright for all x0,...,xn
>
> we must wright it as
>
> x0,,,xn .
>
> (3) Primitives:
>
> Membership  No symbol
>
> only juxtapositioning the two symbols.
>
> Example:  xy  mean x is a member of y
>
> Identity  =
>
> Now lets go to examples of writing FOL(=,e) using this
> technique:
>
> Let’s write the axioms of ZF
>
> _______________________________________________
> 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(x,y) >  a .b zb<>.xaQ(x,z)
> _______________________________________________
>
> Using this technique greatly abbreviate FOL(=,e)
>
> See the following formula:
>
> Exist meR For all i Exist k,l,p,q ((0el <-> 0eq) &
> ((iekeley)<-> Exist j (jepeqem & for all z (zei<->z=j))))).
>
> Look how this is shortened to:
>
> .mR i .k.l.p.q  0l<>0q  ikly<>.jpqm zi<>z=j
>
> As one can see, this method affords a clearer way
> of writing matters, no need for clumsy brackets
> or repetitions of the membership symbol and
> the conjunction symbol
> no clumsy notation at all.
>
> Breaking down complex formulas:
>
> Complex formulas that require more than one line to write
> must be actually decomposed to smaller formulas enough
> to reduced the whole formula in one line.
>
> Example:
>
> 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))))
>
>   -> y e w)) ".
>
> Now this is a long formula, so it is better to break it to
>
> Q(u) <> u is a wiener ordered pair
>
> P(u,k) <> i .s.r isru > i subset k
>
> S(u,x) <> j .p.q jpqu 0eq  > j=x
>
> Now the above formula can be written as:
>
>  yt <>  w .k uw<>Q(u)P(u,k)S(u,x) > yw
>
> Representing relations from Domains to Co domains
>
> the symbol "to" is shortened to -> instead of -->.
>
> so R: A -> B
>
> means
>
> R is a relation from the domain A to the co domain B.
>
> I think that the above technique serve as a good abbreviation
> of writing FOL with identity and membership.
>
> Zuhair

Actually we can make a rigorous syntactical system, by adopting
a simpler version of the dot system instead of the spacing technique.

So instead of dots I shall use the coma and semi-colon

Now the coma and semi-colons are to be considered like valves
deciding the order of processing the formulae in a given formula.

I shall call these comas and semi-colons as "controllers"

Now these controllers occur always on the left of a connsective.

They are of different strengths as below:

One coma , is a single strength controller (=unit strength
controller)
Semi-colon ; is a double strength controller

Higher order strength controllers are combinations of the above two
so

;, represent triple strength controller
;; represent quadruple strength controller
;;, is five unit strength controller

and so on.


Now the follow of processing of formulas is directed from the lesser
strength
controller to the higher one.

So for example

P|Q,>D

this would be written using the bracketing system as (P|Q)>D

while P,|Q>D is written using brackets as P|(Q>D).

Another example:

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)))

so one would work the connectives that has the lesser strength
controllers
on their left side, before working connectives having the higher
strength controllers, so the lesser strength controllers are similar
to the inner brackets and the higher
controllers as somewhat similar to the outer brackets.


So I think using this simple technique with these controllers we can
write FOL(=,membership) in a rigorous manner and also greatly
abbreviates the formulas
and makes them clearer to read.

so to right the axioms of ZF again:

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)


Now as see how this system greatly abbreviates the formulae:

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

56 characters.

is the abbreviattion for:

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)).

95 characters.

with only 4 controllers instead of 14 brackets.

39 character difference,and the formula is reduced to almost 60% of
its size, which is a significant reduction, that is besides the
formula is much clearer
and much more neat.

Zuhair









From: zuhair on
On Apr 27, 12:16 am, zuhair <zaljo...(a)yahoo.com> wrote:
> Abbreviating FOL with identity and membership FOL(=,e)
>
> Criticism: The customary way of writing FOL(=,e) is
> ridiculous, for the following reasons
>
> (1) It contains strange symbols like for example
> the symbols used for universal quantification
> which looks like an upside-down A , and
> the symbol used for Existential quantification
> which look like a turnaround E.
>
> This gives the impression of a scribble made by
> mentally ill patients, rather than a way of writing
> a rigorous formal language.
>
> (2) It contains a lot of repeated symbols, for
> example the brackets, and the symbols for
> membership relation and the symbol of conjunction,
> now these symbols are the most repeated symbols
> and they need not be actually symbolized.
>
> (3) it can contain long sentences that are virtually
> incomprehensible, and better be broken down into
> smaller components.
>
> (4) The symbols are pretty much complex symbols
> while at the same time they are supposed to be
> denoting simple concepts, for example the symbol
> given to disjunction which is a Large V (clumsy looking actually)
> so is the symbol given for conjunction which is an upside-down V
> ,also the symbol given to implication which is virtually
> composed of three smaller symbols, which is very complex, so
> are the symbols of the quantifiers, they are too complex symbols.
>
> Alternative Notation of FOL(=,e)
>
> (1) Logical connectives
>
> Negation   ~
>
> Disjunction  |
>
> Implication  >
>
> Biconditional  <>
>
> Conjunction   No symbol, only spacing.
>
> so the formula Q and P is written as QP, no need for any symbol
> between them.
>
> Spacing will act to differentiate between different formulas
>
> Examples: for the formulas Q,P,S
>
> Q|P S  denote (Q or P) and S
>
> Q| PS denotes Q or (P and S).
>
> so by spacing technique one can differentiate between different
> formulas.
>
> So spacing technique would replace the need for brackets.
>
> (2) Quantifiers
>
> Existential quantifier    .
>
> Unique Existential quantifier   !
>
> 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 not y in x.
>
> While
>
> x .y ~yx is read as:
>
> For all x there exist y not y in x.
>
> Quantification strings
>
> To write for example
>
> Exist x0, Exist x1,...,Exist xn
>
> or usually written as
>
> Exist x0,...,xn
>
> We write
>
> .x0...xn
>
> However this must be differentiated from for example
>
> .x0,,,xn
>
> which actually means
>
> there exist x0 for all x1, for all x2,..., for all xn.
>
> However when we wright for all x0,...,xn
>
> we must wright it as
>
> x0,,,xn .
>
> (3) Primitives:
>
> Membership  No symbol
>
> only juxtapositioning the two symbols.
>
> Example:  xy  mean x is a member of y
>
> Identity  =
>
> Now lets go to examples of writing FOL(=,e) using this
> technique:
>
> Let’s write the axioms of ZF
>
> _______________________________________________
> 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(x,y) >  a .b zb<>.xaQ(x,z)
> _______________________________________________
>
> Using this technique greatly abbreviate FOL(=,e)
>
> See the following formula:
>
> Exist meR For all i Exist k,l,p,q ((0el <-> 0eq) &
> ((iekeley)<-> Exist j (jepeqem & for all z (zei<->z=j))))).
>
> Look how this is shortened to:
>
> .mR i .k.l.p.q  0l<>0q  ikly<>.jpqm zi<>z=j
>
> As one can see, this method affords a clearer way
> of writing matters, no need for clumsy brackets
> or repetitions of the membership symbol and
> the conjunction symbol
> no clumsy notation at all.
>
> Breaking down complex formulas:
>
> Complex formulas that require more than one line to write
> must be actually decomposed to smaller formulas enough
> to reduced the whole formula in one line.
>
> Example:
>
> 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))))
>
>   -> y e w)) ".
>
> Now this is a long formula, so it is better to break it to
>
> Q(u) <> u is a wiener ordered pair
>
> P(u,k) <> i .s.r isru > i subset k
>
> S(u,x) <> j .p.q jpqu 0eq  > j=x
>
> Now the above formula can be written as:
>
>  yt <>  w .k uw<>Q(u)P(u,k)S(u,x) > yw
>
> Representing relations from Domains to Co domains
>
> the symbol "to" is shortened to -> instead of -->.
>
> so R: A -> B
>
> means
>
> R is a relation from the domain A to the co domain B.
>
> I think that the above technique serve as a good abbreviation
> of writing FOL with identity and membership.
>
> Zuhair

Actually we can make a rigorous syntactical system, by adopting
a simpler version of the dot system instead of the spacing technique.

So instead of dots I shall use the coma and semi-colon

Now the coma and semi-colons are to be considered like valves
deciding the order of processing the formulae in a given formula.

I shall call these comas and semi-colons as "controllers"

Now these controllers occur always on the left of a connsective.

They are of different strengths as below:

One coma , is a single strength controller
(=unit strength controller)

Semi-colon ; is a double strength controller

Higher order strength controllers are combinations of the above two
so

;, represent triple strength controller
;; represent quadruple strength controller
;;, is five unit strength controller

and so on.

Now the follow of processing of formulas is directed from the lesser
strength
controller to the higher one.

So for example

P|Q,>D

this would be written using the bracketing system as (P|Q)>D

while P,|Q>D is written using brackets as P|(Q>D).

Another example:

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)))

so one would work the connectives that has the lesser strength
controllers on their left side, before working connectives having the
higher
strength controllers, so the lesser strength controllers are similar
to the inner brackets and the higher controllers as somewhat similar
to the outer brackets.

So I think using this simple technique with these controllers we can
write FOL(=,membership) in a rigorous manner and also greatly
abbreviates the formulas
and makes them clearer to read.

so to right the axioms of ZF again:

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)

Now as see how this system greatly abbreviates the formulae:

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

56 characters.

is the abbreviattion for:

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)).

95 characters.

with only 4 controllers instead of 14 brackets.

39 character difference,and the formula is reduced to almost 60% of
its size, which is a significant reduction, that is besides the
formula is much clearer
and much more neat.

Zuhair