Re: [mizar] weak types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Sun, 16 Nov 2003, Andrzej Trybulec wrote:

> > So we would have to force the instantiation in such cases, either
> > explicitly in the "Unifier", or by Freek's encoding as implication.
> > It almost seems to me that the result would be the same now.
> 
> If it is an implication, why not to write an implication?
> And the first solution means that we have
> 
> 1. to make list of quantifiers with the type possibly empty
> 2. to press an instantiation for the variables bound by them
>     (maybe only in the scope of them ?)
> 
> It seems very ugly. If it had practical values, then maybe. But it seems that as yet the
> arguments for weak type are very weak :-)

I agree that as a quick hack, the implication is less ugly. What I 
probably do not like is, that here is some nontrivial assumption, 
hardwired in an unknown number of places in Mizar. I would prefer to be 
able to switch such additions on and off, e.g. with something like 
requirements, or at least have some transparent control over them in the 
code. 
Especially now that I found the arguments for weak types stronger and 
stronger (see the previous posting and the example here) :-). 


> > But that does not apply to clusters, and clusters are more
> > frequent and usually preferable to modes (especially now, when the
> > nonclusterable attributes are gone). It fixes the type hierarchy, but
> >
> 
> Could you given an example for clusters, or I have to look to your previous messages?
> 
> Is it so that you want the conditional registration like
> 
> registration
>  cluster measurable -> inaccessible (cardinal number);
>   ......
> end;

Yes. Other example:

surjective Function of A,B -> non empty Function of A,B;

(maybe A,B being non empty, I have just started enjoying ignoring
the defaults for nonexistant cases :-)


> > the price is that you have to drag along the assumptions, if you need the
> > definiens. So you can end up with funny implications like:
> >
> > ex M being Cardinal st M is_measurable implies
> > for N being MeasurableCardinal holds N is inaccessible.
> 
> Maybe you need:
> 
>   pred ZFM means ex M being Cardinal st M is_measurable
> 
> and then to use it as antecedent of the implication.

Giving a funny thing a nice name does not make it less funny, 
provided one understands what is going on (and that should be the case).

Josef