Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <m0nOtLr-0000cBC@moa.pmms.cam.ac.uk>
Date: Wed, 17 Feb 93 18:18 GMT
From: Thomas Forster <T.Forster@uk.ac.cam.pmms>
To: info-hol@edu.uidaho.cs.ted

From T.Forster Wed Feb 17 18:13:09 1993
Received: by moa.pmms.cam.ac.uk (UK-Smail 3.1.25.1/1); Wed, 17 Feb 93 18:13 GMT
Message-Id: <m0nOtGb-0000aAC@moa.pmms.cam.ac.uk>
Date: Wed, 17 Feb 93 18:13 GMT
From: Thomas Forster <T.Forster>
To: T.Forster@pmms.cam.ac.uk, rda@win.icl.co.uk
Subject: Re: power of HOL
Status: R

The reason why it is not obvious that Z can be interpreted in HOL is
that there is no bound on the number of quantifiers allowed in
instances of the comprehension scheme of Z.  If we restrict ourselves
to $\Delta_0$ formul{\ae} we get a theory called MacLane set theory
(The Man is on record as believing that all of useful mathematics
can be done in it) which can certainly be interpreted in HOL. However
it is known that MacLane set theory is strictly weaker than Z since
it is equiconsistent with Ramsey's version of Russell's set theory
and it is a *very* old result (it's in John Kemeny's Ph.D. thesis,
but never published as far as i know) that Z proves the consistency
of Ramsey's type theory.  I would have tho'rt that HOL is 
equiconsistent with Ramsey's type theory (a typed set theory with
one base type and only one type constructor, namely power set)
so that it could not be equiconsistent with Z. In fact the more I
think about it the more obvious it seems to me that HOL must be
equiconsistent with (i) Ramsey-style type theory (ii) MacLane
set theory and therefore is (iii) strictly weaker than Z.

     I am at present sitting on a two-year-old paper on these
systems (and related systems) and coincidentally my co-author
will be in Cambridge this weekend.  This may give us the
impetus to finally dust it off and get the damned thing ready
for publication.
      Thomas Forster