Re: [mizar] weak types

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

Josef Urban wrote:

> > Removing the fictitious variables is a comparatively new feature, and I hope that
> > we remove the removing.
>
> Which one? :-)
>

I meant that I do not want the fictitious variables to be removed, I would rather have
them ignored like it was before implementing the distributivity of universal quantifier
wrt. conjunction.

> > So, the quantifiers are ignored. If you have as a premise
> >        for x being S, y be T holds P[x]
> > you may infer P[a]. If T was empty, the sentence above would be true for any P[.].
>
> 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 :-)

> 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;


> 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.

Andrzej