Re: [mizar] 'element'

[trybulec@math.uwb.edu.pl]

Cytowanie Jesse Alama <jesse.alama@gmail.com>:

> Can we please change the name of new 'element' subtype of 'set'?

It is the other way around: 'set' is a subtype of 'element'.
> To my mind, calling the new subtype 'element' misleadingly suggests  
> that Mizar is making a foundational distinction between sets and  
> urelements.  But that's not the case because TARSKI:1 effectively  
> identifies 'set' and 'element'.

An this is the reason that we use 'element' not 'urelement'. On the other hand
'elements' sometimes mimick 'urelements'. The crucial revision, still  
pending, is:
      mode Element of X -> element

also in the case od X being 1-sorted.

> How about 'thing', 'object', or 'item'?

I see no strong arguments for changing notation. I do not see strong  
arguments for 'element', either.

Regards,
Andrzej