Re: [mizar] Why do Mizar types have to be non-empty?

[Andrzej Trybulec <trybulec@cs.shinshu-u.ac.jp>]

You should rather use a predicate
     s is_a_normal_form_of t
maybe
     s is Normal_form of t
looks nice, but without "existence" condition it is the same (almost).

The main reason is that in CHECKER fictitious variables (that not occur
in the scope) are not instantiated. If types may be empty, we have to
instatiate them.Also it is nice, that if I need an arbitrary object of
type \theta, I can write
     consider x being \theta;
(it happens quite often) and I do not look for a justification.

If I rather like the solution adopted (it is the main reason that it is
:-) ), maybe we should discuss the empty types again.

Andrzej

Freek Wiedijk wrote:

> Hello,
>
> Can someone explain to me _why_ Mizar types have to be
> non-empty?  It's very inconvenient!  Often there are things
> that I would like to write as a type, but I cannot do so,
> because that type might be non-empty.  (For instance, in
> rewriting, one would like to have a type "Normal_form of t",
> but some terms t don't have a normal form!)  I mean, if Mizar
> doesn't exclude the empty set from its set theory, why does
> it exclude empty types from its type theory?  Of course I'm
> used to Coq in which non empty types are nothing special.
>
> Also, if Mizar allowed empty types, one wouldn't need to
> prove all those tiresome "existence" correctness conditions,
> and there wouldn't need to be existential clusters.  So
> what's the use of all that, except as a sanity check on the
> definitions?  There is no _mathematical_ reason for them, is
> there?
>
> Also, I think that because of this, there are more "non
> empty" adjectives in the MML than it would else be the case.
>
> Freek