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

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

Freek Wiedijk wrote:

> >You may use a permissive definition, say
> >
> >definition let R be redunction-relation such that
> >Z:  R has_normal_forms;
> >  mode Normal_form of R means
> >   it is_normal_form;
> >  existence by Z;
> >end;
>
> I didn't know you could have "assume" in a mode definition
> too!
>
> So what is the meaning of "n is Normal_form of R" when this
> "Z" condition fails?  Is it an "unknown" statement, just like
> sqrt(-1) is an "unknown real number" (where I mean the "sqrt"
> from SQUARE_1:def 4).  Or is it just equivalent to
> "contradiction"? (which seems appropriate in this case, if R
> doesn't have normal forms, then n should not have type
> "normal form" :-))

To answer this I need to know the mother type of the mode 'Normal_form
of ...'. Let it be 'theta of R', i.e. actually the definition has the
form of

       mode Normal_form of R -> theta of R means
  .....

Then if the 'Z' condition fails, it equals to the fixed (in the game
theoretic setting - fixed by the opponent, not the proponent) element
of  (the denotation of) 'theta of R'. So one does not know if
    n is Normal_form of R
is true or not. With one exception. If the (denotation of the) type
'theta of R' is a singleton, then the fixed 'theta of R' must be the
only element of the denotation, then
     n is Normal_form of R
is true.
And the proposition
   ex n being theta or R st n is Normal_form of R
is always true
On the other side the proposition
    n is_normal_form_of R
is false, if the condition 'Z' fails. I presume of course that n has the
type 'theta of R'

Andrzej