Re: Zero or empty set

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

How about promoting all numerals to functors?  

With this one would be able to register clusters for them and some of
them are quite useful, eg.  2 -> even.

> A numeral is defined (in Mizar) as
>  either 
>   a. a string of digits starting with a non zero digit
>  or
>   b. the string "0".
> 
> I think that maybe we should rather introduce "0" as a functor symbol
> and simplify the definition of a numeral;
> The 0 equals the empty set (the von Neuman construction of natural
> numbers
> is used in Mizar) and if it was a functor symbol, it could be used as
> the symbol of the empty set (and d237 eliminated).
> 
> Then a functor registration of clusters would be for 0 allowed. It is
> important because 0, actually empty set, has a lot of properties
> (represented by adjective, of course) that better be used automatically.
> E.g. it is a function, a relation, a function-yielding function and so
> on.
> 
> Comments are appreciated.
> 
> Andrzej Trybulec
> 


-- 
Piotr Rudnicki