Re: [mizar] weak types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Sun, 16 Nov 2003, Andrzej Trybulec wrote:

> > Actually we have (at least) two kinds of "permissive" definitions:
> > (1) Those with assumptions (like above)
> > (2) "per cases" definitions, like that of "Element of X":
> >     "it in X if X is non empty otherwise it is empty;"
> 
> No, we have not. 
....

OK, you set the terminology, I just wanted to compare those two, giving 
some reasons why (2) seems to be better, and why a weak type might be 
even better than (2).

> > The weak types (or clusters) could deal with this, are more intuitive
> > (things are what they should be, or do not exist at all, not some strange
> > default or a whole science of managing strange defaults),
> > and could thus possibly also reduce the need for using the Global Choice.
> 
> I do not believe that talking about "square circles" is intuitive. 

I believe that most mathematicians understand talking about "square 
circles" as talking about nothing (empty domain). Making Mizar respect 
that opinion is what I call "intuitive". 

The current state in Mizar is that (1)-like definition of "square circle" 
is just some unknown circle, and (2)-like definition of it is some chosen 
default circle (e.g. unit circle, or whatever the author thinks to be 
clever). Both these things are heavily used now in Mizar - isomorphisms of 
nonisomorphic sets, elements of empty set, etc. Sometimes you have to do a 
long recursive traversal of definitions, to discover the deeply buried 
default, that makes some theorem true. I am far from calling that 
intuitive.

We can make a fair poll among normal mathematicians, and I will gladly bet 
you 9:1 Bialystok beers, that majority will share my opinion.

Except from "intuitiveness", the other question is "utility" of these 
approaches. The example with multiple inheritence IMHO shows, that you can 
do more with weak types (or rather clusters), than any default allows.

Josef