Hi,
So, are the HOL systems basically equivalent to ZC (Zermelo set theory plus
the axiom of choice)? I kind of have that impression, but haven't found an
explicit statement. In particular, it sounds like both can be modeled by
V_{omega+omega}, with or without the empty set.
See for example
http://sourceforge.net/projects/hol/files/hol/kananaskis-5-logic.pdf
<http://sourceforge.net/projects/hol/files/hol/kananaskis-5-logic.pdf/download>(last
paragraph of the introduction), together with Wikipedia articles such as
"Von Neumann universe", "ordinary mathematics", and "Zermelo set theory".
-Jeremy
------------------------------------------------------------------------------
Come build with us! The BlackBerry(R) Developer Conference in SF, CA
is the only developer event you need to attend this year. Jumpstart your
developing skills, take BlackBerry mobile applications to market and stay
ahead of the curve. Join us from November 9 - 12, 2009. Register now!
http://p.sf.net/sfu/devconference
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
