Re: [mizar] Once more: empty types

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi Freek,

On Wed, Nov 07, 2007 at 10:43:52PM +0100, Freek Wiedijk wrote:
> Hi Piotr,
> 
> Thanks for answering my mail.  So I _was_ right that _only_
> me and Josef seem to think that the non-emptiness is a
> real problem...
> 
> > - I have never run into a situtation when a possibly
> >   empty type would make a formalization more natural.
> 
> Really!  The "Element of" weirdness doesn't bother you?
> And, for instance, you don't think that "Function of A,B"
> should be an empty type when B is empty but A is not?  Or,  
> ...

(Now I regret using the word 'never.')  Thanks for the examples though.

I have trouble imagining  the consequences of allowing Mizar types
to be possibly empty.  I agree that p.e. types allow some formulations
to look more natural.  If someone shows that using p.e. causes no logical
problems then I guess everyone will use them.  Before this happens,
my lack of experience with p.e. types makes me look at them as not 'natural'.

> ...
> I can imagine, though, trying to figure out what needs to
> be changed in CHECKER (the way I understand how it works,
> from Andrzej's explanations) without actually implementing
> it in the system.  It still might be a small step in the
> right direction.

I would like to encourage you to do this as it seems the right way
to sort out the worth of p.e. types.

Cheers, PR

-- 
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr