Re: axioms and requirements

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Josef,

>I think the right way is to have some modularity of
>axiomatic systems for such cases.

Isn't it possible to "factor" everything through an "axioms"
article, which just copies the statements that you allow
yourself to use?  If you then only have that article (and
ones decending from it) in the environ, you'd be sure that
you wouldn't use statements that you think should not be
permitted (like AC.)

I had a similar problem: I'd like to translate Euclid's
Elements into Mizar, which would mean that I'd only be
allowed to refer to Euclid's axioms instead of to all of
ZF++.  The approach I'd imagined would be to prove that
Euclid's axioms hold in a "model" (the plane) and then force
myself to use only those axioms by restricting the environ.
I think that in that case you _would_ be using model theory,
in a sense.

A difficulty for you would be that Mizar has AC "built in" to
its logic, because of the way Mizar treats partial functions
(which I think is a hack, although a very practical one.)  So
you can prove AC without using the corresponding Mizar axiom
from Mizar's list of set theoretical axioms (TARSKI:9, I
guess.)  I don't think there's such an easy way around that.

Freek