Re: 'element'
Josef Urban <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAFP4q15hpeM=Nb2rFd7UCbYgiGwiC-n5W-kgLkT6Y5MZW2-pdQ@mail.gmail.com> |
On Wed, Aug 22, 2012 at 6:53 AM, Adam Naumowicz <[email protected]> wrote: > 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'. I don't have a strong opinion (apart from the one expressed here: http://mizar.uwb.edu.pl/forum/archive/1203/msg00010.html), but Bolzano seems to be using "Ding" (thing) in Paradoxen der Unendlichen (http://books.google.nl/books?id=RT84AAAAMAAJ&dq=Paradoxien+des+Unendlichen&pg=PR3&hl=en#v=onepage&q&f=false). Josef > 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/ > ======================================================================= >