[FOM] theory of cardinals in HOL?
uuomul at yahoo.com
Fri Dec 11 21:46:49 EST 2009
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,
More information about the FOM