Dot FOL

Prev: Theory of groups with functions - Help on a question
Next: SCI.MATH POLL - uncountable infinity

From: zuhair on 2 Jun 2010 06:23

---

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 06:33

---

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<->(,)(u),:i.s.r_isru..->i subset:,:j.p.q_jpqu,0q..-
>j=x::.->yw::.:

is the following formula:

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 06:37

---

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 06:39

---

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 06:45

---

On Jun 2, 5:39 am, 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 when one uses fixed font instead of
proportional text.

Zuhair

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