# Re: [isabelle] Limit cardinals

Brian,

Ah, ok, this makes sense. Thanks for your response.

-Eddy

On Sep 26, 2014, at 9:56 AM, Brian Huffman <huffman.brian.c at gmail.com> wrote:

> This is not possible in HOL, at least not without adding new axioms.
>
> The standard set-theoretic model for HOL maps everything into the Von
> Neumann universe V_{\omega + \omega}, which does not contain any sets
> with cardinalities as big as the one you are trying to construct.
>
> - Brian
>
> On Fri, Sep 26, 2014 at 9:21 AM, Eddy Westbrook <westbrook at kestrel.edu> wrote:
>> Hi,
>>
>> How does one build a limit cardinal in Isabelle from an ascending sequence of cardinals?
>>
>> For example, if I start from the types nat, nat -> bool, (nat -> bool) -> bool, etc., is it possible to create a type into which I can embed all of these types?
>>
>> Thanks,
>> -Eddy



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