Re: [isabelle] Limit cardinals



>> Set theory version here:
>>  http://www.cl.cam.ac.uk/~lp15/papers/Sets/AC.pdf
>> --lcp

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

http://www4.in.tum.de/~popescua/pdf/card.pdf

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:

http://afp.sourceforge.net/entries/Ordinal.shtml

Andrei 





On 26 Sep 2014, at 19:46, Andrei Popescu <uuomul at yahoo.com> 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.
>
>Cheers, 
> Andrei 
>
>Date: Fri, 26 Sep 2014 09:21:13 -0700
>From: Eddy Westbrook <westbrook at kestrel.edu>
>Subject: [isabelle] Limit cardinals
>To: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
>Message-ID: <3C17F81F-FA7C-43A9-9909-1C03BB1773EF at kestrel.edu>
>Content-Type: text/plain; charset=us-ascii
>
>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
>
>
>End of Cl-isabelle-users Digest, Vol 111, Issue 25
>**************************************************
>
>





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