axioms and requirements

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

I am now writing an article on large cardinals, which is a field, where
quite often declarations like "We are now working in pure ZF (without AC)"
occur (because sometimes a principle directly contradicting e.g. AC or
V=L, etc. is discussed).

This leads to thinking about the strength and implementation of Mizar
axiomatic system. E.g. proving now that Axiom of Determinacy (AD) implies
something (and there is a whole chapter about AD in my book on large
cardinals) would be really easy in Mizar, because AD contradicts AC (and
with AC as proved theorem in MML you can get all the theorems by
contradiction).

One way out is to use Mizar just as a metatheory, pushing all such things
to some kind of model theory. I don't think it is good, first because
writing proofs from whole chapters as objects of some model theory
formalized in Mizar means that you lose all advantages of Mizar language
over a formal proof language (unless you want to define fomalized Mizar
language ;-)) ), and the second reason is that even having some strong
principles just in the metatheory could sometimes influence the object
theory (but I do not have some good example for this).    

I think the right way is to have some modularity of axiomatic systems for
such cases. Only I fear that the body of mathematics needing this feature
is so small, that the benefits would be quite small in comparison with the
amount of work needed to do it, and the module overhead for all the
"normal" parts of mathematics. I don't know, this is probably a topic for
discussion.
Maybe, it is not so difficult to do it, using more extensively the current
"requirements" directive ( I suppose it just adds some theorems as obvious
to the checker). The problem begins if we wanted to use theorems from
articles with different requirements (they would not have to be
compatible). One solution would be to keep for each theorem a list of
axioms which it (recursively) requires, and during the stage of importing
things from MML, check these lists against the requirements of current
article. Maybe, it would not enlarge the library too much, adding e.g. one
file for each article to the "prel" directory. Maybe there is a better
solution, or this problem is in practice so marginal, that it is not worth
of solving :-)). 
It depends on what people currently write in Mizar, and
if it could be an incentive for someone to write some article, where such
feature is needed (some nonstandard theory for ZF, etc.).  

Josef Urban