[FOM] Mizar's type system

[Freek Wiedijk]

Dear Artur,

Thanks for the reaction!  Still this does not make me
completely happy.  This way you still cannot get the type
of the elements of a given set to behave in the appropriate
way, i.e., such that "x has type element of the set X"
means the same as "x is an element of X".  In other words,
you won't be able to have a type that corresponds to _the_
basic relation of set theory, elementhood.

Also, because of this, you hardwire the axiom of choice
in the first order predicate logic that is really the
foundations of Mizar.  That is unsatisfactory.  I might
want to work in a set theory without choice (for instance,
to make sure that some theorem does not need choice),
and Mizar does not give me that.

Freek