Re: [mizar] Private DB

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

On Thu, 21 Sep 2006 03:37 pm, Freek Wiedijk wrote:
> But!  In the case of Isabelle and HOL Light (or for instance
> Andrea Asperti's Matita as a "divergence" from Coq), those
> really are not branches of an older system!  Those are totally
> new systems, very much inspired by the old one, yes, but _not_
> a derivative.
>
> If you would go, and build a system that very much resembles
> Mizar but is a "new" system really, then I wouldn't complain
> about it at all.  (And if you do this, _please_ allow empty
> types: Mizar is _evil_ that it doesn't allow empty types :-))
>
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. Hence, if empty types will be 
allowed, the rules of the game must be more complicated. Or I am missing 
something here?

Michael