Re: [mizar] Re: Urelements?

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

2012/3/13  <trybulec@math.uwb.edu.pl>:
> Just for the record, we know that strict structures are equal, if they
> fields
> are equal.
>
> The question set/element arose a couple of months ago in completely
> different context. The sentence
>
>     1 in 1-sorted(#A#);
>
> is grammatically correct, but as you wrote we know nothing about its logical
> value. Actually, if somebody writes
>
>     1 in 1-sorted(#A#)
>
> then he probably uses the overloaded definition
>
>  let S be 1-sorted;
>  let x be set;
>  pred x in S means
> :: STRUCT_0:def 5
>  x in the carrier of S;
>
> That is a general phenomenon. It is simple for expandable type because they
> are expanded, so we freely use such overloading. In the case of predicates,
> attributes and functors situation is different, because such definition as
>
>  let S be 1-sorted;
>  func id S -> Function of S,S equals
> :: STRUCT_0:def 4
>  id the carrier of S;
>
> or the "membership" defined above, will cause necessity to refer to them.
>
> The general rule is: if a locus in a definition is really a set (it is
> treated as set), the when we substitute 1-sorted structure for it we get
> something undefined, so it is reasonable to overload it taking substituting
> not a structure but its carrier instead. Intuitively we know what it means
> that
> 'a locus is "really" a set'. In the membership
>
>         let x,X be set;
>         pred x in X;
>
> X is "really" a set, not so x. So a coercion was proposed:
>
> if locus is 'really' a set, and somebody attempted to substitute a 1-sorted
> S for it, then let Mizar coerce it to 'the carrier of S'.
>
> We either need a definition of "real" set, or allow to specify it by hand.
> If we distinguish 'set' and 'element', Mizar will know when to use the
> coercion.

Why not use the type info that you already have? If a
functor/predicate takes a structural argument, use it. If not, use the
structure's carrier.

It might be better to have a general syntactic mechanism ("use t(X)
instead of X if X has some type/shape in context c") for this than an
ad-hoc implementation for structures. One advantage would be that you
could choose to use them or not in particular articles.

Best,
Josef




>
>
>
> Regards,
> Andrzej
>
>
>
>
>
>
> Cytowanie Jesse Alama <jesse.alama@gmail.com>:
>
>
>> As for structures, the status quo seems to be that structures are in
>> fact sets, but we don't know any of their elements (or, at least no
>> membership statement is obvious for the Mizar checker) and thus
>> (accepting extensionality as globally valid) we don't know their
>> identities:
>>
>>  {} in 1-sorted (# {} #)
>>  ::>                   *4
>>  ::> 4: This inference is not accepted
>>
>>  not {} in 1-sorted (# {} #)
>>  ::>                       *4
>>  ::> 4: This inference is not accepted
>>
>>  1-sorted (# 1 #) = 1-sorted (# 2 #);
>>  ::>                               *4
>>
>> This seems fine to me as an approximation of the idea that they are
>> urelements.  A stricter approach would be to say reject as malformed
>> a membership statement whose right-hand side is a structure:
>>
>>  {} in 1-sorted (# {} #)
>>  ::> *143,321
>>  ::> 143: No implicit qualification
>>  ::> 321: Predicate symbol or "is" expected
>>
>