This is another way of writing FOL(membership and identity)
using a dot system, but not for punctuation.
Punctuation here is done by using the bracket system on need,
i.e. only when we have unexpected order of connectives.
Logical connectives in Ascending order of power:
Negation ~
Conjunction ,
Disjunction ;
Implication ->
Bi-conditional <->
Primitives
Membership juxtaposing
Identity =
Quantifiers
Universal :
Existential .
Unique Existential !
Syntax of quantification:
Quantifier x_Q quantifier
There is no need for the underscore if Q begins with a quantifier.
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.
Brackets ( ): used in n-arity functions and predicates; for
punctuation: ONLY used to delineate *unexpected* order
of connectives.
Examples:
:t.x:yt<->:w.k:uw<->Wiener pair(u),:i.s.r_isru..->i subset k:,
:j.p.q_jpqu,0q..->j=x::.->yw::.:
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)).
Extensionality :x:y:zx<->zy:->x=y::
Foundation :x.yx.->.zx,~.cz,cx..:
Empty .x:y_~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:.:
Infinity .x_0x,:yx->:z:uz<->uy;u=y:->zx::.
Zuhair
