Hi Jeremy,
| 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.
I'm pretty sure you're right that the two systems can be modelled by
V_{omega+omega}. Andy Pitts's semantics in the HOL manuals says as
much on page 10:
http://softlayer.dl.sourceforge.net/project/hol/hol/kananaskis-5/kananaskis-5-logic.pdf
This is effectively what I assumed in my "HOL in HOL" proof as a
type V in which to interpret HOL. I must admit that I used HOL
function spaces built up from V to model polymorphism, but this
was really just laziness, and I think these could be replaced by
set-theoretic functions inside V.
http://www.cl.cam.ac.uk/~jrh13/papers/holhol.html
As for the precise strength, I'm not quite sure either, but Thomas
Forster's invited talk "Weak systems of set theory related to HOL" at
the HOL conference in 1994 addressed the relationship between HOL and
various set theories. You can find the paper in various places online,
e.g. here on Springerlink:
http://www.springerlink.com/content/p74255u102410847/
As I understood from a quick skim, HOL seems to be equivalent to a
weakened version of Zermelo called Mac (after Mac Lane). However, I'm
not quite sure whether this HOL includes polymorphism, or whether
the presence of Choice in both systems alters the picture.
John.
------------------------------------------------------------------------------
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
