| Newsgroups |
gmane.comp.mathematics.mizar |
| Message-ID |
<[email protected]> |
Cytowanie Jesse Alama <[email protected]>:
> [email protected] 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. 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