[mizar] Urelements?

[trybulec@math.uwb.edu.pl]

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