[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Re: Urelements?

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