Wishes for Mizar

Freek Wiedijk

                          freek@cs.kun.nl

University of Nijmegen

Abstract. Here is a list of the things I desire for the Mizar system.

0

In an e-mail to Grzegorz Bancerek I mentioned that there were some things I’d like to see different in Mizar. He asked for a description. So here are some things I would like to be different.

These are listed in order of importance (most important first). The first three wishes are easy, the last two wishes are hard.

1 Manual

Mizar has no proper documentation. This is unacceptable. Please write something.

It should at least consist of a hundred page reference manual and a thirty page tutorial. It should be in English.

Once you do this: keep it up to date. So if a requirement is added to the language then add it to the manual, if the type of real numbers becomes real number instead of Real then modify the tutorial, etc.

2 Weird characters

The ‘mathematical’ characters look nice if you have the right fonts installed, but they make everything complicated. The fonts often are not available, these characters are hard to type, these characters make the MML web pages ugly because of the GIFs.

I know these characters are already gradually being phased out. I’d prefer to see this problem solved in one big substitution operation.

I don’t consider going to full Unicode an improvement. On the contrary. Please only use ASCII characters with codes between 32 and 126.

3 Modules

The environ part of a Mizar article is difficult to get right. I would like to see three changes to the Mizar module system.

3.1 Vocabulary names versus article names

Vocabulary names and article names are similar but different. For instance one vocabulary is called PFUNC1 but the article is called PARTFUN1.

Make them really the same name space. So have each vocabulary ‘belong’ to an article.

3.2 Vocabulary files versus article files

Vocabulary files are separate from the article files. It is not very practical to have to have a small ‘satelite file’ when developing an article.

I’d like to see the two kinds of files merged. Put the vocabulary files as a ‘vocabulary section’ at the top of the article file. Or have ‘vocabulary definitions’ among the other kinds of definition.

3.3 Separate directives

There are a several ‘library directives’:

 – vocabulary
 – notation
 – constructors
 – clusters
 – definitions
 – theorems
 – schemes

In practice the same article name generally occurs in all of them.

I’d like to see this simplified. Just have one import directive which imports all the features of the article at the same time.

This will make things a bit slower. This is not important.

4 Not only Intel

Mizar only runs on computers with an Intel processor. I don’t own one. This means I can’t run Mizar properly.

Please port Mizar to a language that can be run on most processors.

5 Partial functors

The semantics of functors in Mizar treats typing and predicates differently (sqrt -1 doesn’t satisfy the defining predicate of sqrt, but it has type Real). This hardwires the axiom of choice (in fact something stronger: a choice operator) into the first order logic.

I’d like to have something different from the way it is now.

This probably would make the system harder to use (you might have to prove being allowed to use a functor before being able to use it) but it would make things more elegant mathematically.