From: zuhair on
On May 2, 11:16 am, zuhair <zaljo...(a)gmail.com> wrote:
> On May 1, 12:22 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
>
>
>
>
>
> > On May 1, 9:42 am, zuhair <zaljo...(a)gmail.com> wrote:
>
> > > 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)
>
> > [...]
>
> > > Extensionality:   zx<>zy > x=y
>
> > WRONG
>
> > Az(zex <-> zey) -> x=y
>
> > is NOT equivalent with
>
> > Az((zex <-> zey) -> x=y)
>
> > Please get a book on the basics of this subject.
>
> > MoeBlee
>
> I admit my weakness about the basics.
>
> A question regarding the basics of this subject,
>
> is the following a well formed formula in FOL(e,=):
>
> For all x ( For all y ( For all z ((z e x iff z e y) -> x=y) ) ).
>
> z is only appearing on the left of the implication, and all variables
> other than
> z are quantified *before* z, so is that acceptable?
>
> I might accept the following formula
>
> For all z ( For all x ( For all y ((z e x iff z e y) -> x=y) ) ) .
>
> since x and y are quantified *after* z, so quantification over z can
> extend as
> far as variables x and y appear in the formula, so it doesn't matter
> if
> z seize to appear after the implication.
>
> I just thought that quantification over a variable z closes after the
> last formula
> z or the last variable quantified *after* z appears in.
>
> If the answer is yes, which mean that it is a well formed formula,
> then
> in these circumstances we must modify the notation to accommodate for
> that, so
> we either extend the dot notation to cover such cases of
> quantification, or we simply keep the rule of exhaustive
> quantification (as a notation) and always wright the formula z=z on
> the other side to indicate that quantification extend over to the
> other size.


To clarify the last statement, we can for example wright

Axyz(zex -> y=x)

the is written as: xy zx>y=x z=z

so putting the formula z=z on the other side, will ensure
that quantification is extending over the implication
( this is the consequence of the rule of Exhaustive quantification
which is adopted in this notation system, which states that:-

"quantification over a variable z closes after the
last formula in which z or the last variable quantified *after* z
appears in").

however lets take the statement

Axyz((zex<->zey)->x=y)

now this is written as: xy zx<>zy.>x=y

we don't need to write: xy zx<>zy.>x=y z=z

since this would be redundant.

because from the dot after zy , it is clear that
the scope of quantification over z is extending beyond
the implication, otherwise we don't need to place a dot
after zy.

Zuhair

From: zuhair on
On May 2, 4:26 pm, zuhair <zaljo...(a)gmail.com> wrote:
> On May 2, 11:16 am, zuhair <zaljo...(a)gmail.com> wrote:
>
>
>
> > On May 1, 12:22 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
>
> > > On May 1, 9:42 am, zuhair <zaljo...(a)gmail.com> wrote:
>
> > > > 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)
>
> > > [...]
>
> > > > Extensionality:   zx<>zy > x=y
>
> > > WRONG
>
> > > Az(zex <-> zey) -> x=y
>
> > > is NOT equivalent with
>
> > > Az((zex <-> zey) -> x=y)
>
> > > Please get a book on the basics of this subject.
>
> > > MoeBlee
>
> > I admit my weakness about the basics.
>
> > A question regarding the basics of this subject,
>
> > is the following a well formed formula in FOL(e,=):
>
> > For all x ( For all y ( For all z ((z e x iff z e y) -> x=y) ) ).
>
> > z is only appearing on the left of the implication, and all variables
> > other than
> > z are quantified *before* z, so is that acceptable?
>
> > I might accept the following formula
>
> > For all z ( For all x ( For all y ((z e x iff z e y) -> x=y) ) ) .
>
> > since x and y are quantified *after* z, so quantification over z can
> > extend as
> > far as variables x and y appear in the formula, so it doesn't matter
> > if
> > z seize to appear after the implication.
>
> > I just thought that quantification over a variable z closes after the
> > last formula
> > z or the last variable quantified *after* z appears in.
>
> > If the answer is yes, which mean that it is a well formed formula,
> > then
> > in these circumstances we must modify the notation to accommodate for
> > that, so
> > we either extend the dot notation to cover such cases of
> > quantification, or we simply keep the rule of exhaustive
> > quantification (as a notation) and always wright the formula z=z on
> > the other side to indicate that quantification extend over to the
> > other size.
>
> To clarify the last statement, we can for example wright
>
> Axyz(zex -> y=x)
>
> the is written as:  xy zx>y=x z=z
>
> so putting the formula z=z on the other side, will ensure
> that quantification is extending over the implication
> ( this is the consequence of the rule of Exhaustive quantification
> which is adopted in this notation system, which states that:-
>
>  "quantification over a variable z closes after the
> last formula in which z or the last variable quantified *after* z
> appears in").

More thoroughly:

rule of Exhaustive quantification:

"quantification over a variable z closes after the
last formula in which z or the last variable quantified *after* z
appears in; or by the appearance of another quantification over z").


As an example of the last statement, referring to the appearance of
another quantification over z is axiom of Foundation

x _yx > _yx _cy cx

as one can see y is quantified over twice, so the first quantification
over y
closes just before the implication, while the second quantification
over y
extends to the end of the formula since c is quantified after y
and c appears in the last formula which is cx.

so the above formula abbreviates the following:

Ax (Ey (y e x) -> Ey (y e x & Ec (c e y & c e x)))

so 13 characters instead of 32 characters, almost one third of a
reduction!

isn't spectacular!

Zuhair








>
> however lets take the statement
>
> Axyz((zex<->zey)->x=y)
>
> now this is written as: xy zx<>zy.>x=y
>
> we don't need to write:  xy zx<>zy.>x=y z=z
>
> since this would be redundant.
>
> because from the dot after zy , it is clear that
> the scope of quantification over z is extending beyond
> the implication, otherwise we don't need to place a dot
> after zy.
>
> Zuhair