Re: [mizar] weak types

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

Josef Urban wrote:

> > >  definition let G,H be Group such that
> > > A: G,H are_isomorphic;
> > >    mode Isomorphism of G,H means
> > >     .....;
> > >    existence by A;
> > >  end;

> Actually we have (at least) two kinds of "permissive" definitions:
> (1) Those with assumptions (like above)
> (2) "per cases" definitions, like that of "Element of X":
>     "it in X if X is non empty otherwise it is empty;"

No, we have not. At least, if you use Mizar terminology (originally it was
introduced by St. Turski - "permissive specification" meant "(possibly)
incomplete specification". Turski complained that when we used "incomplete
specification" referees tried to reject his papers, with "permissive
specification" they intended to accept :-)

Yes, we have. If the otherwise is not specified. So it is not the case with the
definition (2). It is a regular definition.
So, we have to distinguish carefully two things:
-   using non standard definitions for well known concepts (such as 'Element of
A' )
-   using permissiveness that means basically using some form of Choice
To make thing clear: even if we make selectors in Mizar to be natural  numbers
(as an obligatory semantics) we would like probably to have this choice
permissive - we do not want to care which selector corresponds to which number.

It is even more general, when Rudnicki's students modeled the system of
reservation of air plane places, they made it permissive, the system takes the
first free place, it does not mean they they use a specific ordering.


> The weak types (or clusters) could deal with this, are more intuitive
> (things are what they should be, or do not exist at all, not some strange
> default or a whole science of managing strange defaults),
> and could thus possibly also reduce the need for using the Global Choice.

I do not believe that talking about "square circles" is intuitive. But it maybe
be a matter of taste, so
   de gustibus non est disputandum


Andrzej