Re: [mizar] Re: Urelements?

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

2012/3/12  <trybulec@math.uwb.edu.pl>:
> Cytowanie Jesse Alama <jesse.alama@gmail.com>:
>
>> trybulec@math.uwb.edu.pl writes:
>>
>
>>> We should now discuss what should be a set, and what should
>>> not. E.g. ordered pairs are probably elements, not sets?
>>
>>
>> Of course, ordered pairs are sets (and robustly so: one can choose
>> from various notions of "ordered pair" and still get the same
>> conclusion).
>>
>
> The problem is 'robustly so'. If we can use different definitions, we do not
> care what they actually are. Even if we agree that it is the Kuratowski
> definition
>
>          func [x,y] equals {{x,y},{x}}
>
> we are not really interested in the definition.
> Somebody, I believe Elliott Mendelson, wrote that "it has no intrinsic
> value'.
> Once we proved injectivity
>        [a,b] = [c,d] implies a = c & b = d
>
> we are rarely interested in the definition.

If this is just an interesting remark, and we only want to hide the
definition for efficiency reasons, then it is just a matter of
automation discussed before.

If we want to actually re-use for differently defined pairs (most of)
the theory developed for Kuratowski pairs, then mechanisms like little
theories (or their set-theory versions) are needed. For "big objects"
(like an arbitrary pairing functor) it has to be developed on
universes (this is what higher-order systems basically do), or using
limited second-order matching like in ACL2: extending scheme
mechanisms, to be able to develop a theory with a schematic (Skolem
:-) variable standing for the pairing functor.

Or it can also be the case that we just want to "see" that a lot of
theorems depend only on injectivity, and think about an action
(generalizing, copy/replace, or nothing) later. This can be done by
dependency analysis.

Best,
Josef



>When we are, e.g. when proving
> that if x and y belong to a universal class the [x,y] belongs, too, we may
> use the definition.
>
>     [x,y] = {{x,y},{x}};
>     then [x,y] is set;
>
> should be obvious. As Josef wrote it does not cover preventing us from using
> useless definitions, but it helps.
>
> Regards,
> Andrzej