Re: [mizar] Once more: empty types

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

Hi Jesse,

>I would love MIZAR even more if types were allowed to
>be empty because it would make some formalizations more
>natural.

Most.  (At least: most formalization involving "Element
of" :-))

>What, though, are the costs?

Well, you lose two (dual) inference rules:

	reserve x in SomePossiblyEmptyType of argh;

	for x holds A[]; then A[];

and

	A[]; then ex x st A[];

(In this x does not occur free in the formula A[].)
You would also need "ex x st x is SomePossiblyEmptyType of
argh" for these inferences to be allowed.  Which I guess is
a property of argh.  However you would need that knowledge
only for _these inferences_ to go through.  Most other
inferences would also work perfectly without that knowledge.

>I suppose that the developers would have to edit a good
>deal of code.

I would expect that only CHECKER would be affected?  So it
would be quite localized.  However I guess that CHECKER
really would need quite some rethinking.

Freek