[isabelle] Sets



Elsa L Gunter's answer means:
   "if we take I = B and A i = {0,1}  then the
direct product has the cardinality strictly
larger than that of B and we have contradiction."
 Is it?

  This is the key point I am worrying. But, I 
am still thinking that it is possible to express
such set B as type 'b in Isabelle/HOL. Because of
the set theory, we see there is a set isomorphic
to the direct product, we have only to put type
'b to the set B, I think.
  It seems that Isabelle polymorphic type has no
restriction to instantiate. (My impression, I am 
not sure, is that a type of a set with higher cardinality
shouldn't take a type of lower 
cardinality in some cases.)
   Therefore, if we carefully avoid such a wrong 
instantiation, we can obtain correct formalization,
isn't it? Is it OK?

 
Best

Kobayashi, Hidetsune
  
--- Elsa L Gunter <egunter at cs.uiuc.edu> :
> No, it would have to be a polymorphic type
> constructor (which => is)
> because of cardinality constraints. Suppose there
> were such a fixed
> non-polymorphic type a123. If I understand your
> question correctly, you
> want a123 to be isomorphic to 'i => 'a for all 'i
> and 'a. Then you could
> instantiate 'i and 'a with a123 getting the a123 is
> isomorphic to a123
> => a123, thus falling afoul of Cantor's paradox.
> ---Elsa Gunter

--------------------------------------
TSUKAME EIKOU! KAGAYAKE EGAO!
Yahoo! JAPAN JPC OFFICIAL PARTNER INTERNET PORTAL SITE
http://pr.mail.yahoo.co.jp/wintergames/





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.