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