Re: [mizar] I am trying to figure out...

[trybulec@math.uwb.edu.pl]

Hi:

Cytowanie freek <freek@cs.ru.nl>:

> If Mizar's type system wasn't broken (in the sense that
> it doesn't allow types to be empty; well, maybe "broken"
> is too strong a word, but the Mizar type system _is_
> severly limited because of this) then one could define
> "Element of" in the natural way.  And then this would be
> a provable theorem (and then in fact it would be automatic
> when one has requirement SUBSET, I guess.)

Mizar does not allow for meaningless types like

    an empty non empty set
    an element of the empty set
    a function from a non empty set into the empty set

Does it means that it is "broken"? I may agree that it is more limited;
I would rather say that it is more demanding. Then suspending the 
requirement might be exciting: the life becomes easier (and the quality 
of work done becomes lower: some questions are left unanswered).

If a meaningless type \theta is allowed that           for x being 
\theta holds ...

is understood as

    for x st x is \theta holds ...

so actulally the type is eliminated by a predicate and the whole type 
system becomes syntactic sugar. And why we need two predicates

       x is element of A

and     x in A?

I do not argue that the solution adopted by Mizar is the only good solution
or the best one. However we need arguments to change it, not to keep it 
as it is. I do not claim that it is not possible that we eventually 
find such arguments. The problem is that it is difficult to anticipate 
the consequences of changing the approach.

Regards,
Andrzej