[mizar] Syntax

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Robert Solovay wrote:

>  Last night I uncovered a strange Mizar
> bug/feature: If say k is reserved to be Nat, then
> Mizar thinks
>
> k is;
>
> is a perfectly clear and acceptable assertion. As a
> result, I got some strange error messages when I said
>
> k is prime;
>
> without having "prime" in the vocabulary. [I think
> FILTER_0 is what's needed, but I'm just going by
> memory here.]

We have corrected it. (Version 6.1.12). It was well known feature of the
Mizar syntax. We kept it because:

 a Multi Adjective Formula Expression, i.e. Atomic Formula Expression of
the form

      /tau is /alpha_1 ... /alpha_k

 means actually

    /tau is /alpha_1 & ... & /tau is /alpha_k

E.g.
  x is non empty non trivial finite

means

  x is non empty & x is non trivial & x is finite

and because VERUM is a conjunction of the length 0 (in the realm of
Mizar semantic correlates) we believed that

allowing for

 x is

with the meaning

not contradiction

has a didactic value. The only protest as yet was that if the sentence
"/tau is" occurs in the inference one is tempted to believe that the
(ground) term "/tau' occurs, too. It is not true, so such recording is
misleading.

The Bob argument is critical, if the attribute symbol /alpha_1 is not in
the lexical environment of the article that
the formula

  /tau is /alpha_1 ... /alpha_k

is cut to

 /tau is

that causes misleading error messages.

In new syntax if you try to use "/tau is" you will get the error:

 consider x being set;

 x is;
::>  *309
::>
::> 309: Type or attribute expected

Actually the construction has been used in MML (the article YELLOW20 by
Grzegorz Bancerek). The library committee changed it to "not
contradiction" and it is O.K. now.

Regards,
Andrzej Trybulec