Re: [mizar] Was this supposed to be so?

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

Piotr Rudnicki wrote:
> 
> Hi:
> 
> I have expected an error in the following
> 
>         for X, Y, Z being set st X = Y holds Y = X
>         proof let X, Y be set;
>           thus thesis;
>         end;
> 
> but did not get any.  Such theorem would look pretty silly in an abstract.

Hi,

There is no error "It is silly".  But in that case the checker does
nothing because equality is symmetric
 (see http://mizar.org/JFM/Axiomatics/hidden.abs.html).
Library Committee removes such and even more advanced theorems,
so you haven't to wary.

If you mean it is silly because it includes a redundant variable,
you are partially right.  Such statements are sometimes required
when proving with scheme justification. In that case a structure
of a instantiation of scheme premises and scheme thesis must be
exactly the same as in the scheme declaration, so you must follow
all quantifiers (even redundant in your instantiation).
Redundad variables as well as redundant assumptions in theorems
sould be eliminated.

Grzegorz