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

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

Freek Wiedijk wrote:

> Dear Andrzej,
>
> >The main reason is that in CHECKER fictitious variables
> >(that not occur in the scope) are not instantiated. If types
> >may be empty, we have to instatiate them.
>
> I do not understand, sorry.  Can you give an example?

If the type 'theta' is empty, the sentence
E:     for x being theta holds alpha(x)
is true. Let us suppose that 'x' actually does not occur in 'alpha'. The
instantiation in CHECKER is steered by pattern matching with the
auxiliary premises. let 'alpha' be
     for y being natural number holds y = 0
so one can infer that 1 = 0.

Step by step. We have to refute
     for y being natural number holds y = 0, 1 <> 0
after substituting 1 for 'y' we got contradiction.

To prevent it we have to check, that the sentence E is true only because
the type 'theta' is empty. To enable to use it, the simplest thing is to
look which 'variables' are not substituted and provide example. Now it
gets nasty, because not only fictitious variables might be not
substituted. E.g. in

      for x,y,z being theta st P[x,y] or P[y,z] holds P[x,z]
        --------------------------------------------
           P[a,b] implies P[a,c]
y is not substituted (while checking). What to do ?
 1. to remember that the variable is "legally" not substituted
      or
 2. try to instatiate it anyway. In this particular case we can use 'a',
but if the type of 'y' is not 'theta', let say
  for x,z being theta, y being theta_1 st P[x,y] or P[y,z] holds P[x,z]
and in l'universe de discourse there is no ground term with the types
theta_1?

I understand that the arguments are not conclusive, I just try to
explain why we choose such a solution. On the other hand why systems
that allow for empty types are consistent, that I do not know :-)

Regards,
Andrzej