[FOM] theory of cardinals in HOL?

[Andrej Bauer]

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,

Andrej

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
>