Re: Urelements?
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
Cytowanie Josef Urban <[email protected]>: > 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 <[email protected]>: >> 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 >> >> >> >> >