Thanks for a good answer to a sloppy question.
There appears to be a free, newer version of "Weak Systems of Set theory
Related to HOL" at http://www.dpmms.cam.ac.uk/~tf/maltapaper.ps. I also
found Mathias's paper on "The Strength of Mac Lane Set Theory", at
http://www.dpmms.cam.ac.uk/~ardm/maclane.pdf, to be informative.
After asking my question, I realized that it's a lot clearer to me how one
might translate a HOL development into ZC than vice versa, so with
hindsight, it makes sense to me that HOL is weaker than ZC. (I'm still
being sloppy. I mean that HOL can be interpreted in ZC, not that the latter
can prove the former's consistency. And I suppose I haven't actually
defined what it means to interpret a type theory in a set theory or vice
versa.)
Maybe it's not hard to translate a HOL development into ZC? Type parameters
become unbounded quantifiers, free variables become bounded quantifiers,
instances of "new_basic_type_definition" become instances of comprehension,
etc. But in the reverse direction, arbitrary instances of comprehension
can't be translated, because they might contain unbounded quantifiers. This
consideration yields the restriction that comprehension can only be applied
to delta-0 predicates, which is Mac.
-Jeremy
On Tue, Nov 3, 2009 at 9:43 AM, John Harrison <[email protected]>wrote:
>
> 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<http://www.cl.cam.ac.uk/%7Ejrh13/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.
>
------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now. http://p.sf.net/sfu/bobj-july
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
