Email Gateway (Aug 19 2022 at 15:56): Email Gateway (Aug 19 2022 at 15:56):From: Eddy Westbrook <westbrook@kestrel.edu>
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
Email Gateway (Aug 19 2022 at 15:56):From: Lawrence Paulson <lp15@cam.ac.uk>
If you want to do cardinals properly, there’s always Isabelle/ZF…
Larry Paulson
Email Gateway (Aug 19 2022 at 15:56):From: Brian Huffman <huffman.brian.c@gmail.com>
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.
Email Gateway (Aug 19 2022 at 15:56):From: Eddy Westbrook <westbrook@kestrel.edu>
Brian,
Ah, ok, this makes sense. Thanks for your response.
-Eddy
Email Gateway (Aug 19 2022 at 15:56):From: Andrei Popescu <uuomul@yahoo.com>
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
Email Gateway (Aug 19 2022 at 15:56):From: Lawrence Paulson <lp15@cam.ac.uk>
Set theory version here:
http://www.cl.cam.ac.uk/~lp15/papers/Sets/AC.pdf
--lcp
Email Gateway (Aug 19 2022 at 15:56):From: Andrei Popescu <uuomul@yahoo.com>
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
Last updated: Apr 19 2024 at 12:27 UTC