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

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

Dear Andrzej,

>The empty set has quite precise meaning. And what is
>
>  the empty non empty set?

Ah yes, this new "the" thing won't work with empty types.
And the same holds for permissive definitions (that's the
name right, when there's an assumption in a func definition?)
If you would define

  definition
    assume contradiction;
    func foo -> A means ...
  end;

then A has better be a non empty type, right?  So one should
have Mizar requiring something like a "cluster" for _those_
two cases.  But I really would like the non-emptiness of a
type to be a _registration_ then, instead of it being part
of the definition.

>>In Coq I can do
>
>Why we should mimic Coq?

I just was trying to argue that it's unproblematic.
Because it's unproblematic there.

>You can always use a permissive definition.

What does this exactly mean in this case?  To do

definition
  let X be non empty set;
  mode Element of X means ...
end;

or to do

definition
  let X be set;
  assume X <> {};
  mode Element of X means ...
end;

?

However in both cases you won't be able to prove that

for x,X being set holds (x in X iff x is Element of X)

right?  So then it still is _wrong._

>So, actually it is a technicality.

You can work around the problems with the non-emptiness of
types, sure.  But you can do arithmetic in Roman numerals
too.  My claim is that the non-emptiness of types in Mizar
is like Roman numerals for arithmetic.   III + IV = VII!
What's the problem?

>If we allow for types with the empty denotation, then
>we should additionally check if all free variables have
>non empty types. Quite unnnatural, isn't it?

So if you make CHECKER first replace

  for x being A holds ...

by

  for x st x is A holds ...

(and similar for ex) in the cases that it cannot establish
the non-emptiness of A by way of a cluster, before running
its usual algorithms, _that_ wouldn't be so big a change,
maybe?  So then you wouldn't need to change your algorithms.
And maybe it still might behave reasonably?

>In general we cannot infer
>
>      for x being theta holds alfa
>      -------------------------------
>            alfa
>
>when x does not occur in alfa
>
>I guess that in Coq such inferences are not allowed in general.

Exactly.  In Coq need to exhibit an element of theta
for that.  And "the theta" doesn't exist :-)

Freek