Re: 'element'

Hi Jesse,

On Mon, 20 Aug 2012, Jesse Alama wrote:

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

Thanks for raising this topic, because I also don't feel comfortable with 
this new name. If there is a better name, it would be best to change it 
before it sticks for good.

> 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'.

Apart from that, the distinction between 'element' and 'Element' can be 
even more confusing, especially for new users.

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

To me 'thing' would be a bit too colloquial. If I were to choose 
the name, I would select 'object'. Looking at the English dictionary, many 
formal definitions refer to 'object' as something most general. However, 
the term has some connotations (like in grammar, category theory, or 
programming) that might interfere here.

'object' is already used in MML, so replacing the new 'element' with it 
might require some library revision. 'item' has not been used in MML yet, 
so that would be easiest to implement. Similarly, 'entity' could also be 
used without much of a problem. It seems similar to 'item' and tends to be 
used in some formal environments to mean something which is independent, 
separate or self-contained.

Best regards,

Adam

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================