Urelements?

Hi;

I would like to start with Polish "Nie przesadzajmy, jak mawiał leniwy 
ogrodnik", I do not know how to translate it. I wonder what Google does 
with it.
It seems that we exaggerated with the statement that everything is a set.
Actually numbers and structures behave rather like urelements (I am 
aware  that
elements of structures are supposed to be urelements, not the 
structures themselves).

In old Mizar the root type (and mode) was 'Any'. The type 'set' was a 
subtype of 'Any', the first axiom in TARSKI said that 'everything is a 
set'. One of the reason was that we planned to develop other 
repositories based e.g. on arithmetics, in which probably the first 
axiom would be 'everything is a natural number'. Then we decided that 
it is enough trouble with one MML, and keeping two different types with 
the same denotation is useless.

Recently Artur started to experiment with definitional expansion of 
atomic sentences in the Inference Checker (CHECKER in the Mizar jargon) 
and the results are disgusting. Verifying some articles becomes longer 
by more than two orders. One of the reason was the lack of the type 
discipline. If e.g. 'x <> y' is among premises the poor thing will 
append to premises both 'not x c= y' and 'not y c= x' even when x and y 
are real numbers and such inclusions are (almost) meaningless.

Therefore it is necessary to recover the old root type, under the new 
name 'element'. When identifying 'Any' and 'set' was easy, going back 
is a little bit harder. The first obvious step was done (by Czeslaw and 
Artur):

i. in HIDDEN the mode 'element' is introduced and it is the mother type 
of the mode 'set'. The equality is introduced for elements, but the 
membership needs the second argument to be a set.
ii. default types for numerals and structures are put to 'set' (temporarily)
iii. when in the functor or mode definition qualification was empty, it 
was by default set, it was necessary, again for a while, to insert the 
qualification '-> set'.

We should now discuss what should be a set, and what should not. E.g. 
ordered pairs are probably elements, not sets?

Regards,
Andrzej