# [isabelle] Sets

• To: isabelle-users at cl.cam.ac.uk
• Subject: [isabelle] Sets
• From: "Kobayashi, Hidetsune" <hd_coba at yahoo.co.jp>
• Date: Sun, 12 Mar 2006 11:43:36 +0900 (JST)
• Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=yj20050223; d=yahoo.co.jp; h=Message-ID:Received:Date:From:Subject:To:MIME-Version:Content-Type; b=Q2RJlhO2YuauKhQalJNUQnrXBEIAfF5F3q/+wca30M8q7OXN0QKe1S3mLLxNvkykroHXZZiLq1h6I8aAiIl4Ej2aFn7jJAudw+sFYBAO/VI3WyKfqNCZmyn/LACV8Ld6 ;

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