[isabelle] Limit cardinals



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.