[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] '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: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
=======================================================================