Re: [mizar] non necessarily non empty types

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

Dear Andrzej,

>(In fact I would like to stratify MML into the part
>depending on ZFC and needing TG, maybe we should use even
>finer stratification)

I think that Raph Levien (see
<http://www.advogato.org/person/raph/diary.html>) wants a
stratification that distinguishes the part that only needs
second order arithmetic, the part that only needs higher
order logic, and the full ZFC.

Also I think that in the Metamath system (see
<http://www.metamath.org/>) you can for _any_ theorem exactly
what axioms it uses.  This is the content of Appendix 5 in
<http://us.metamath.org/mpegif/mmset.html#assume>.

Now a Mizar to Metamath compiler, that would be a very
interesting and very useless thing :-)

Freek