Re: [mizar] MML duplications

[freek <freek@cs.ru.nl>]

Dear Piotr,

>Maintaining the numbering of theorems stable (if this
>is the case) leeds to fossilization of MML.  What is the
>problem in renumbering theorems after moving them around?

I would have to edit
<http://www.cs.ru.nl/~freek/100/mizar.html> all the time?

Seriously, I think it would be nice to have _some_ stable
way of referencing theorems in the MML.  That you can write
(in a paper, for instance) "this has been formalized as
lemma so-and-so in MML", instead of just being able to
give the statement and then say "well, try to find it,
I'm sure it's there _somewhere!"_

Of course, if you think the results in MML are not
interesting enough for referencing, then this objection
doesn't apply :-)

>Renumbering all theorems and references in MML after a
>revision seems like a mundane editorial job.

_If_ you start to change the numbers on a bigger scale,
then _please_ also move the theorems between articles on
a much bigger scale, so articles will no longer contain
theorems that really should have been somewhere else.

>One argument that I see in support for avoiding renumbering
>theorems is that authors get used to numbers of frequently
>referenced theorems.  This does not apply to me;

Not to me either.  The only one I that I used to know was
AXIOMS:22 (however I don't remember anymore what that was),
and I don't think _that_ one exists anymore.

On the other hand, I _still_ use the old webpage version
of the JFM (now long obsolete) to look up stuff sometimes.
If you start changing numbers, that would not be useful
anymore.

And if one had been working on an article, got distracted,
but then tried to pick it up half a year or so later,
one would have a bit of a problem, wouldn't you?  To get
it working again would take much more work then it takes now.

So I don't know.

Freek