Re: [mizar] HIDDEN

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

Piotr Rudnicki wrote:

> Hi:
>
> There is this definition in HIDDEN
>
> definition let x,X be set;
>  pred x in X;
>   antisymmetry;
> end;
>
> Aside of the problem that the meant property be better named asymmetry,
> there is also some redundance here.  Namely, that x in X is
> asymmetric follows from the regularity axiom and thus we should have
> x in X defined as
>
> definition let x,X be set;
>  pred x in X;
> end;
>

The gain seems to be very small.

>
> or to be faceciuos even as
>
> definition let x,X be set;
>  pred x in X means
>  not contradiction;
> end;
>

This would be good! One can prove using this definition reflexivity for the
membership predicate :-)

>
> and then, only after regularity we should
>
> definition let x,X be set;
>  redefine pred x in X;
>   antisymmetry;
> end;
>

The problem is that this redefinition introduces a new redefinitional variant,
that makes processing a bit more
complicated.

It is true that it should not be a new redefinitional variant, the
identification of properties in the CHECKER module could be better, so we may
discuss it again when (if) the system is modified.

Andrzej Trybulec