Re: [mizar] I am trying to figure out...

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

Hi Andrzej,

>Mizar does not allow for meaningless types like
>
>    an empty non empty set
>    an element of the empty set
>    a function from a non empty set into the empty set

I disagree that they're meaningless!  They're just empty.
Is the empty _set_ a meaningless _set?_  No, of course it
isn't.  And likewise an empty type is not a meaningless type.

In Coq I can do

     Coq < Check unit->Empty_set.
     unit -> Empty_set
          : Set

     Coq < 

and there is no problem there at all.  ("Empty_set" is an
empty type, and "unit" is a type with exactly one inhabitant,
called "tt":

     Coq < Check tt.
     tt
          : unit
     
     Coq < 

.)

>If a meaningless type \theta is allowed that
>
>    for x being \theta holds ...
>
>is understood as
>
>    for x st x is \theta holds ...
>
>so actulally the type is eliminated by a predicate and the
>whole type system becomes syntactic sugar. And why we need
>two predicates
>
>       x is element of A
>
>and    x in A?

For the same reasons that one now has types in Mizar:

     1. to have the system automatically infer that certain
        predicates hold (using the types in definitions
        and registrations)

     2. to disambiguate overloaded syntax

>However we need arguments to change it, not to keep it
>as it is. I do not claim that it is not possible that we
>eventually find such arguments.

For me the argument is that the types can have much more
natural defintions.  Now, often when I want to define a
type, Mizar won't allow me to write what should be there,
and then I just give up.

In the HOL systems, one doesn't get empty types either,
but there one doesn't have dependent types, so there it
doesn't hurt.  But Mizar, rightly so, _has_ dependent types,
and there often one gets specific parameters for which the
type naturally becomes empty.

>The problem is that it is difficult to anticipate the
>consequences of changing the approach.

You are right that no one will prove "existence" correctness
conditions anymore, and that for that reason there might
be more mistakes in definitions.  But that is balanced for
me by the fact that finally types can be defined in the
natural way.  In the _right_ way.  Like "Element of", yes.

We've had this discussion before, I'm sure.  My excuses
for being triggered.

Freek