[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] 'element'
On Wed, Aug 22, 2012 at 6:53 AM, Adam Naumowicz <adamn@math.uwb.edu.pl> 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: adamn@mizar.org
> Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
> =======================================================================
>