Re: [isabelle] Limit cardinals



Set theory version here:

http://www.cl.cam.ac.uk/~lp15/papers/Sets/AC.pdf

--lcp

> 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.