On Thu, 20 Nov 2003, Andrzej Trybulec 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.
OK.
> > > 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.
Being lazy, I just MMLQueried this last one. NATTRA_1:mode 2 is
"natural_transformation" and NATTRA_1:pred 2 is
"is_naturally_transformable_to":
at least(NATTRA_1:mode 2,NATTRA_1:pred 2) | [th or def]
46 element(s)
at least(NATTRA_1:mode 2) butnot(NATTRA_1:pred 2) | [th or def]
11 element(s)
I did not explore the possibility, that the guard may be buried deeper in
other notions.
> Of course I would like to have better argument than just claiming that it is only
> for "consider", what about
> generalization ("let"),
(not F1 is_naturally_transformable_to F2) implies
for t being natural_transformation of F1,F2 holds t <> t
proof
assume A1: not F1 is_naturally_transformable_to F2;
let t be natural_transformation of F1,F2;
F1 is_naturally_transformable_to F2; :: by the new def of natural_transformation
then contradiction by A1;
hence thesis;
end;
I don't see a problem with "let". If the type is empty, and you have local
constant of that type, you just get contradiction. That's why we
have to avoid "consider". Already now you can write things like
"assume c is circular & c is square".
The question is whether to allow "reconsidering" into weak types, and I
would be for that.
> widening the type (Czeslaw pointed to it),
Could you be more specific?
> and ,what is
> somewhat related to the widening, proving by the definitional expansion a
> qualifying sentence (the mother type might be non empty),
It is the same as e.g. for attributes or predicates, what should be the
problem?
> removing or ignoring the
> fictitious quantifiers.
We discussed that.
> And what about problems that I cannot anticipate just now.
If you cannot, then they are really hard to anticipate just now :-).
> A proof starting with
> let X be empty infinite set
> looks pretty nice.
How about:
let X be empty Element of {};
I hope my simple algorithm for producing answers to question of this kind
is already apparent.
> I guess you want to neglect the existential registration of
> clusters as well.
No, existential registration is important for "consider" at least, maybe
also for removing of fictitious variables. I just want to be allowed to
work with unregistered clusters (generally types), if it is useful.
I find it both more useful and more intuitive than permissive or "default"
type definitions.
I think I understand your real worry here:
It is now quite painful to work with permissive types, and almost
impossible to work with unregistered clusters, and it pushes the authors
to prove the existence condition, even if the effort is not worth it.
So this way, you are increasing the chance, that what is in MML, is not
complete nonsense.
I agree to some extent. But as I wrote, if someone wants to write garbage,
you will not prevent him by any means, e.g. the "is" suggested by Freek
can be trivially used instead. Being a victim of such restrictive
measures, which both make it hard to establish good type mechanism in some
cases, and distort the normal mathematical understanding in others, I find
it hard to support them.
Formalized mathematics is a sort of censorship, but if it is unreasonable,
you will only loose the real enthusiasts. Garbage producers will stay :-).
Josef