Re: '0' replacement

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Josef Urban wrote:

> > So maybe we should place
> > it in HIDDEN ? Or maybe some other existing vocabulary, or a new one?
> > Any comments and suggestions will be appreciated,

It is Czeslaw Bylinski that argued against HIDDEN. Let him make his point.

The real problem is the identification of the empty set and 0. Not the
representation. I would propose first to substituted for d238 '{}' (as a
functor symbol, not functor brackets). Some people claim that it looks a bit
childish. ? Then it should be put on the BOOLE vocabulary, if course. And '0'
may be introduced later as a synonym for '{}'.

One can prove in MML that
    0 = {}
(CARD_1:51, also CARD_2:20)

Freek Wiedijk had some doubts about typing of  the empty set and the zero
number, if they are identified. Me too, even if I do not see any example. Let
us be secure. Typing is sensitive to the notation, then introducing '0' as a
synonym is more secure.

Regards,
Andrzej Trybulec