Prev: A A
Next: How can the MMx math be corrected?
From: zuhair on 20 May 2010 09:56
This notational system only has some abbreviation power, it is neat,
elegant and easy to read.

Logical connectives:

Negation ~
Conjunction .
Disjunction |
Exclusive Disjunction ||
Implication >
Bi-conditional <>

Quantification

for all x Q x:Q

Exist x Q _x:Q

Exist only one x Q _!x:Q

Exist many x Q _^^x:Q

Multiple quantification is represented as

x1,...,xn: stands for: for all x1,...,for all xn
_x1,...,xn: stands for: exist x1,...,exist xn

if there is a change in the type of quantification then
the colon should demarcate that change

example: x1:_x2,...,xn stands for
for all x1 there exist x2,...,there exist xn

the end of quantification is demarcated by a semi-colon
if the formula in the scope of quantification is not a sentence(i.e
contain a free variable), or by a period if the formula
is a sentence.

Examples:

x,y,z: Q(x,y);;

x,y,z: Q(x,y,z).

The period at the end of a formula signify that this
formula is a sentence, i.e. all variables in that formula
are bound.

Hiding Quantifiers:

Quantifiers can be hidden if their appearance would be
consecutive otherwise; or in case of universal
quantification the detail of which is totally
decidable without their appearance".


Primitives:

Identity =

Membership Juxtaposing the two terms.

Example: xy stands for x is a member of y

The order of connectives and the use of brackets.

<> , > , |, ., ~

so bi-conditional has higher scope power than implication, which in
turn has higher scope power than disjunction which is higher than
conjunction which is higher than negation.

Of course the scope of any connective is limited by the scope
of quantification over the variables in the formulas that connective
is connecting.

So actually the scope of quantification has higher power than
all the above connectives.

Brackets are only used to delineate an unexpected order
of connectives:-

Examples:

P.(Q>R)
(Q<>R)>P
~(P.Q)
P.(Q|R)


The notation of functions, predicates, ordered pairs, class builders,
all are as in the standard manner.

Examples of using this notation:

Writing ZF set theory axioms:

Extensionality zx<>zy;>x=y.

Foundation _yx;>_zx.~_cz.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<>ya.Q.

Replacement x:_!y:Q(x,y);;>a:_b:yb<>_xa.Q(x,y).

Infinity _x:0x.yx>z:uz<>uy|u=y;>zx.



t:_x:yt<>w:_k:uw<>Wiener pair(u).
i:_s,r:isru;;>i subset k;.
j:_p,q:jpqu.0q;;>j=x;;;
> yw.

Abbreviates:

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


This system doesn't have the dot notations as the previous one that
I've introduced to this Usenet, also it does not have the complex
visual rules of exhaustive quantification, so it is simpler, and
easier to read than the previous one, and it looks neater than the
standard one.

Zuhair

 | 
Pages: 1
Prev: A A
Next: How can the MMx math be corrected?