Prev: Theory of groups with functions - Help on a question
Next: SCI.MATH POLL - uncountable infinity
From: zuhair on 2 Jun 2010 18:00
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

From: zuhair on 2 Jun 2010 18:02
On Jun 2, 5:00 pm, zuhair <zaljo...(a)gmail.com> wrote:
> 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

This notational system looks better when fixed font is used.

Zuhair
From: zuhair on 4 Jun 2010 17:22
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

From: zuhair on 4 Jun 2010 17:25
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

From: zuhair on 5 Jun 2010 05:05
On Jun 4, 4:25 pm, zuhair <zaljo...(a)gmail.com> wrote:
> 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

This notation appears clearer on fixed text.

Zuhair
First  |  Prev  | 
Pages: 1 2
Prev: Theory of groups with functions - Help on a question
Next: SCI.MATH POLL - uncountable infinity