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

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

Dear Freek,

It is a working semantics, but one cannot prove that n=n'. Actually, one
may suppose that
   for x being theta of R holds x is Normal_form of R
as well. The problem is that to use the definition of 'Normal_form' one
have first to prove, that
   R has_normal_forms

By working semantics, maybe the name is no good, I mean a model, or a
class of models
that is used to ensure that Mizar is inconsistent (to our best believes).

Regards,
Andrzej


Freek Wiedijk wrote:

> Dear Andrzej,
>
> >> So what is the meaning of "n is Normal_form of R" when this
> >> "Z" condition fails?
>
> >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'.
>
> I see.  Does this mean that if R fails the "Z" condition, and
> if both n is Normal_form of R and n' is Normal_form of R, that then
> n = n'?
>
> Freek