[mizar] Weak types

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

Michael Nedzelsky wrote:

> reserve x for SomePossibleEmptyType;
>
> (*)   (forall x holds P(X))  implies (ex x st P(x))
>
> Obviously, this is not true in empty domain. Hence, if empty types will be 
> allowed, the rules of the game must be more complicated. Or I am missing 
> something here?
>
>  
Let us try to prove it :-)

  (for x holds P(x)) implies ex x st P(x)
    proof
      assume
Z:      for x holds P(x);

      take a;
      thus P(a) by Z;
     end;

So, to complete proof we need at least one term 'a' with the type 
'SomePossibleEmptyType'. We cannot of course introduce 'a' by a Choice 
Statement (Josef was once laughing on me, that I need nonemptiness of 
types to be able to write 'consider a;'). But it is much more: we cannot 
allow for a ground term, even in a relaxed meaning - with local 
constants in it - with the type 'SomePossibleEmptyType'. Am I wrong?

So, what is that we need weak types for?

Greetings,
Andrzej