Re: [mizar] Re: Urelements?

[Josef Urban <josef.urban@gmail.com>]

2012/3/14  <trybulec@math.uwb.edu.pl>:
> Cytowanie Josef Urban <josef.urban@gmail.com>:
>
>> 2012/3/14  <trybulec@math.uwb.edu.pl>:
>>>
>>> Cytowanie Josef Urban <josef.urban@gmail.com>:
>>>
>>>
>>>
>>> It does not matter that it is a new mechanism. It still does not work.
>>>
>>> Let be more precise: what yopu want to do with membership:
>>>
>>>
>>>         let x,X be set;
>>>         pred x in X;
>>>
>>> The membership takes structural arguments, so what Mizar is supposed to
>>> do?
>>
>>
>> No, there is no structural argument in that definition.
>>
>
> So, by "takes a structural argument" you mean that the type of locus is
> structural, do you?

Yes.

> But then, if we write
>
>     G in X
> (G - a group) it would be coerced to
>
>     the carrier of G in X,
>
> But if G is a family of groups, and we write
>
>          G in X
> we mean exactly what it means without any coercion.

Yes. (Or: in most cases. I can imagine an ugly theory of cyclic groups.)

So the context for the coercion needs to be specified. Using "element"
in the constructor declaration is indeed one way how to do it. But I
am not sure where it will lead. I'd perhaps prefer to deal with
syntactic problems by purely syntactic mechanisms.

>
> x = y
>
> is not coerced at all, G1 = G2 means that the group are equal

Prove it via extensionality :-).

>
> x c= y
>
> both arguments are coreced, G1 c= G2 means     the carrier of G1 c= the
> carrier of G2

I wonder what T1 c= T2 typically means for topological spaces. Or for
structures with more carriers.

>
> For the membership only the second argument is coerced. There are still some
> minor problems e.g. how to cope with the redefinition of the equality for
> sets
>
>    redefine pred A = B means A c= B & B c= A

I think there is a general problem. Structures are an experiment in
marrying abstract/axiomatic approach with concrete set theory. If we
ever specify them extensionally, the "elements" will disappear, and
the right parsing will become even more context-dependent. And already
now the "element" introduction does not solve some of the above
issues.

Best,
Josef


>
> Regards,
> Andrzej
>
>
>
>