Extended ASCII in Mizar

[Mariusz Zynel <mariuszz@math.uw.bialystok.pl>]

Extended ASCII, or rather IBM set II, used in Mizar articles causes
many problems:
  1. Authors are forced to use DOS based systems. Unix systems
     require special hardware and software. Even Windows systems
     causes troubles, particularly their local versions.
  2. It is hard to give a Mizar text good HTML representation.
  3. Articles, or their parts, can not be transmitted via email without
     special encoding.

Of course, some characters like "membership relation", "empty set",
"intersection", "less (grater) than or equal", "orthogonal",
or "parallel", so common in mathematical papers, are very convenient
and make the natation shorter. It seems however, that most of the 
others are extraneous to mathematics. There is a lot of symbols
in Mizar vocabularies that contain such characters. Most of them
are not reasonable and irrelevant.

In most cases Extended ASCII characters can be eliminated fairly
easy. For example, instead of U - "union" and "intersection"
symbols 'cup' and 'cap' (or maybe well known for TeX users - '\cup' 
and '\cap') can be used. The "membership relation" could be 
exchanged for 'in' (or '\in'). Unfortunately, writing 'parallel'
or 'orthogonal' in place of symbols may be annoying. I have also
no idea for an equivalent to "empty set". The characters 
"less than or equal" and "greater than or equal" could be written
as '<=' and '>=' according to some programming languages.

I think that there is more disadvantages of using Extended ASCII
then advantages, so it should be prohibited.

What is your opinion about applying TeX conventions to denote 
some Mizar symbols?

-- 
        .
Mariusz Zynel
Institute of Mathematics
University in Bialystok

mailto:mariuszz@math.uw.bialystok.pl

http://math.uw.bialystok.pl/~mariuszz/