Re: [mizar] weak types

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

Josef Urban wrote:

> Just repeating the argument from previous post, this seems to me pretty
> unnatural :-). If we defined predicate
> "t is_natural_transformation_of F1,F2"  in the corresponding way, your
> definition just says:
>
> assume A1: ex t st t is_natural_transformation_of F1,F2;
> mode natural_transformation of F1,F2 -> transformation of F1,F2 means
>      it is_natural_transformation_of F1,F2;
> existence by A1;
>

Yeah, but it is a special case. If you look to the definition of transformation
the guarding predicate is a bit simpler.

>
> > when one proves that a transformation is a natural transformation, then one
> > has to prove first the guard (the assumption in the definition)
>
> So before I am allowed to prove, that t is natural, I have to prove that
> there is something natural. Thanks.

It was shortcut of course. If I prove by the definitional expansion, then I should
to state the guard. This does not
means that I must to prove it, if you meant a Mizar proof. Sometimes the
justification is quite obvious.
And, after the theory is developed, we are not pressed to prove by the
definitional expansion.

>
> The permissiveness might be good for functions like sqrt, I am not sure.
> But for types, the only "advantage" of permissive over weak is, that
> you can "consider" them even in cases when they "are empty", knowing
> exactly nothing in such cases. For weak types, if you find out that you
> are in the empty case, you can trivially prove anything right away, which
> (I repeat myself) is the common mathematical understanding.

It is an argument, but then the mathematical jargon is so sloppy.

Of course I would like to have better argument than just claiming that it is only
for "consider", what about
generalization ("let"), widening the type (Czeslaw pointed to it), and ,what is
somewhat related to the widening, proving by the definitional expansion a
qualifying sentence (the mother type might be non empty), removing or ignoring the
fictitious quantifiers. And what about problems that I cannot anticipate just now.

A proof starting with
    let X be empty infinite set
looks pretty nice. I guess you want to neglect the existential registration of
clusters as well.

Andrzej