Re: [mizar] Private DB

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Michael,

>empty types?
>But what about the following:
>
>reserve x for SomePossibleEmptyType;
>
>(*)   (forall x holds P(X))  implies (ex x st P(x))
>
>Obviously, this is not true in empty domain.

So it shouldn't be accepted :-)

>Hence, if empty types will be 
>allowed, the rules of the game must be more complicated.

Yes.  Andrzej claims it will be much more complicated, and _I_
claim that it's worth it.  Now I _don't_ know who of the two
is right (maybe both? :-))

>Or I am missing something here?

No.

I guess I want Mizar to "know" for each type whether it might
be empty or not.  And in both cases do the sensible thing: if
it knows it not to be empty behave like it already is doing,
but if it might be empty still reason correctly about it.

Coq allows empty types.  PVS allows empty types.  So it is
possible to allow empty types and still have a moderately
useful system.  Or do you think that those systems are not
sound? :-)

Freek