Re: [isabelle] Limit cardinals



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.