Re: [mizar] Urelements?

[Josef Urban <josef.urban@gmail.com>]

Calling the basic object of set theory an "element" and preventing its
automated typing as "set" feels foundationally inventive.

It seems that you want additional ad-hoc type/definitional-expansion
machinery for some particular sets. I would not do it ad-hoc for two
kinds of objects, but rather have a standard mechanism that allows to
mark a definition as something that should not be automatically
expanded by default (or in an environment). We faced a similar
situation some time ago with quaternions, and that had nothing to do
with foundations - just with having proper mechanisms for "knowledge
expansion".

Josef

2012/3/12  <trybulec@math.uwb.edu.pl>:
> Let me make one thing clear:
>
> we do not propose to chang the foundations of MML. The chang eis rather
> related to type handling.
>
> The (quite old/brand new) TARSKI:1 will be
>
> for x being element holds x is set
>
>
> It now obvious that 2 is a set, I mean
>
>     2 is set;
>
> is accepted without any references. In new approach it will need
> justification:
>
>     2 is set by TARSKI:1;
>
> I used many times (and it must be revised)
>
>     1-sorted(#1, ... #)
>
> for 1-element 1-sorted. I even wanted to do a revision :-). With new
> approach
> one must write
>
>     1-sorted(#{0}, ...#)
>
> that means the same and it less tricky.
>
> Regards,
> Andrzej
>
>
>
>