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