Re: axioms and requirements

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

Hello Freek,

thanks for reaction, the biggest problem with such posting seems to be
that I do not know if someone is really interested. 

> Isn't it possible to "factor" everything through an "axioms"
> article, which just copies the statements that you allow
> yourself to use?  
It is possible, probably in case of Euclid's axioms it is a good choice,
but you probably do not use there theorems from other library articles,
nor want some other "applied" articles to profit from your work.

But imagine that someone wants to do nonstandard ZF, without regularity,
and introduces some additional axiom contradictiong regularity. 
Then he may want to use that large amount of theorems that are now in the
library and regularity is not necessary for them. 
And there also might be some general theorems that he had to prove, but
just in ZF, without regularity or its contradiction. And there is no
reason why other people could not use such theorems.

That's why I wrote about keeping track of the axioms used for theorems.
I think getting now such information from the MMl is almost for free (not
much work) and it would be also quite unique (and sometimes also useful)
achievement of the Mizar formalization to know even for very applied
theorems, if they needed AC, regularity, infinity, etc.
The necessary work for such mechanism would be also making the built-in
things (AC, irreflexivity of epsilon, etc.) explicit by creating some
(probably requirement) directive for them.
 
Josef