Re: [isabelle] Limit cardinals


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


On Sep 26, 2014, at 9:56 AM, Brian Huffman <huffman.brian.c at> 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> 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.