Re: [isabelle] Limit cardinals

>> Set theory version here:
>> --lcp

We also formalized some bits and pieces of cardinal theory in Isabelle/HOL:

No limit cardinals in our formalization, of course. Just like in Larry's paper 18 years earlier, our main motivation was the construction of more flexible (co)datatypes.  

Of a different flavor is Brian's prior formalization of a rich theory of countable ordinals in Isabelle/HOL:


On 26 Sep 2014, at 19:46, Andrei Popescu <uuomul at> wrote:

Hi Eddy, 
>I don't think you can do such a construction in HOL, otherwise you would be able to use it for giving (in HOL) a model-theoretic proof of HOL's consistency.
> Andrei 
>Date: Fri, 26 Sep 2014 09:21:13 -0700
>From: Eddy Westbrook <westbrook at>
>Subject: [isabelle] Limit cardinals
>To: USR Isabelle Mailinglist <isabelle-users at>
>Message-ID: <3C17F81F-FA7C-43A9-9909-1C03BB1773EF at>
>Content-Type: text/plain; charset=us-ascii
>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?
>End of Cl-isabelle-users Digest, Vol 111, Issue 25

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