Re: [mizar] Re: Urelements?

[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.


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