[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,

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
>



More information about the FOM mailing list