Thanks. This is all very helpful. I'm trying to understand foundations
generally. I'm actually not so interested in ZFC, as the definition of the
Von Neumann universe never seemed like valid mathematics to me. In
contrast, V_{omega+omega} does, so I'm more interested in ZC and Mac.
Bringing in the category-theoretic perspective, it seems like we have four
equivalent systems:
(1) Mac - bounded Zermelo with choice
(2) TST - typed set theory a la Russell-Whitehead
(3) HOL
(4) ETCS - the elementary theory of the category of sets, i.e. the internal
language of a Boolean topos with natural numbers object and choice
Would it be reasonable to say that there is a circularity in the equivalence
proofs? From a distance, it seems like Forster covers 1<->2<->3, Lambek and
Scott cover 3<->4, and Mac Lane and Moerdijk cover 4<->1.
-Jeremy
On Wed, Nov 4, 2009 at 2:41 AM, <[email protected]> wrote:
> Grant,
>
> Thanks for sending me this! Dear John, Jeremy.. the definitive version of
> my TPHOL94 talk is the one linked from my homepage. I have one question and
> one answer. the queation is; why is JRH using a .cam.ac.uk address..?
> Could it be that he is in Blighty as we speak..? And the answer is that, yes
> HOL is indeed equivalent in strength to Mac Lane set theory, also to to the
> simply typed theory of sets (a la russell-whitehead) with infinity. I can
> supply more details if you like, but i suspect what you want confirmed is
> that HOL is vastly weaker than ZF(C). Friedmannology can supply lots of
> combinatorial facts about naturals that ZF(C) can prove but which HOL can't.
>
> John - where are you??
>
>
>
>
>
> On Nov 4 2009, Grant Olney Passmore wrote:
>
> hi, Thomas --
>>
>> I hope this finds you well! FYI, in case you're not on the HOL mailing
>> list, I forward a discussion going on between John Harrison
>> and Jeremy Bem which includes discussion of your work.
>>
>> very best wishes,
>> Grant
>>
>>
>> -------- Original Message --------
>> Subject: Re: [Hol-info] Is HOL equivalent to ZC?
>> Date: Tue, 3 Nov 2009 17:39:13 -0800
>> From: Jeremy Bem <[email protected]>
>> To: John Harrison <[email protected]>
>> CC: [email protected]
>> References: <[email protected]>
>> <[email protected]>
>>
>>
>>
>> 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<http://www.dpmms.cam.ac.uk/%7Etf/maltapaper.ps><
>> http://www.dpmms.cam.ac.uk/%7Etf/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<http://www.dpmms.cam.ac.uk/%7Eardm/maclane.pdf><
>> http://www.dpmms.cam.ac.uk/%7Eardm/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]<mailto:
>> [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>
>> <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
