[FOM] theory of cardinals in HOL?

Andrej Bauer andrej.bauer at andrej.com
Sun Dec 13 04:33:15 EST 2009

I would suggest looking at Paul Taylor's paper

"Intutionistic Sets and Ordinals", Journal of Symbolic Logic, 61
(1996) 705-744.

available for download from http://www.paultaylor.eu/ordinals/

It focuses on the intuitionistic case but is of course compatible with
excluded middle and choice. It should be useful for your purposes
because it does not assume a single-sorted theory with a global
membership relation. The sets are considered "type-theoretically" so
to speak. I am pretty sure the basic definitions can be translated
easily enough into HOL, and some will simplify under classical logic
and choice.

With kind regards,


On Sat, Dec 12, 2009 at 3:46 AM, Andrei Popescu <uuomul at yahoo.com> wrote:
> Hello,
> If I am not mistaking, cardinals are usually presented in textbooks in a set-theoretic (typically ZF) setting and their theory is constructed basing on ordinals, in turn based on the membership relation.   On the other hand, for my work I needed to employ cardinals within Higher-Order Logic with Infinity and Choice -- some of the theory does seem to go through without using ordinals (and their proper class), but appealing to well-orders instead.  However, I could not find references  to a development of the basic theory of cardinals in this (or a similar) setting.
> Thank you in advance for any such references,
>   Andrei Popescu
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

More information about the FOM mailing list