Re: [mizar] non necessarily non empty types

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

On Mon, 17 Nov 2003, Freek Wiedijk wrote:

> >(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>) 

Reading there about Mizar is not exatly flattering, maybe SUM should keep 
an official statistics of the number of people distracted from Mizar by 
the closed-source policy. Raph is the third one I know about so far, plus 
the two reverse hackers to Java - any guesses how many yet?

> 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.

I think we would also have to allow alternative proofs of theorems in 
MML. If you work in ZFC, you do not exactly want to read 
complicated finitary proofs of things obtained trivially by Choice.

> 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>.

There were some statistical programs for MML doing similar things, it 
would not be too hard to adapt them. If you prefer a quick Prolog hack, 
get the file references.db from MPTP, but schemes are not handled there, 
amd e.g. proofs of correctness conditions for definitions neither.

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

Unfortunately yes, the suggestion about absolute notation was 
also about making things more stable.
Mizar is very advanced when it comes to revision tools (and ideas :-), 
and makes full use of them, so one day you do the translation, and one 
year after that it is outdated. If people are producing new stuff over 
the translated library, there will be a fork.
At the moment, it is quite hard to imagine any cooperation on the level of 
library between MML and some other system. Already working with older MML 
is discouraged. I think the only feasible option for new stuff done e.g. 
by provers on MML translation, is to incorporate it in MML as quickly as 
possible (if it is worth it).

Josef