Re: [mizar] Urelements?

[trybulec@math.uwb.edu.pl]

Cytowanie 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".

We have a regular mechanism to prevent an object defined as \tau with the type
\theta to be processed as \theta. If we define

          func F(...) -> \theta_1
             equals \tau

F(...) is processed as an object with the type \theta_1 that may be 
less specific than the type \theta. Also 'qua' is used to force 
widenning of the term type. The problem is only with the type 'set', we 
cannot say "forget that x is a set, process it as an object that has no 
specific properties". And
with more and more automation related to sets it may cause more and 
more troubles.

I agree that it covers only some problems related. We have to look for
other solutions.

A. maybe definitions should be classified as 'good' definitions and 
'bad' definitions like in the case of quaternions. And 'bad' 
definitions should be encapsulated.

B. maybe we need more specific constructions in the Environment Declaration.

Greetings,
Andrzej