From: zuhair on
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

From: Frederick Williams on
zuhair wrote:

> This technique greatly abbreviate fol(=,membership), and it is
> clearer, more neat and do not have strange looking symbols in them.
>
> Isn't it?

No.

--
I can't go on, I'll go on.
From: MoeBlee on
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





From: zuhair on
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)

Infinity: _x 0x yx > U(y,{y})x

were z=U(y,{y}):<> uz.<> uy|u=y
> _______________________________________________
>
> 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

From: zuhair on
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

Zuhair