Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
X400-Received: by mta relay.pipex.net in /PRMD=pipex/ADMD=cwmail/C=GB/; Relayed;
               Thu, 18 Feb 1993 08:45:51 +0000
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2));
               Relayed; Thu, 18 Feb 1993 08:43:34 +0000
Date: Thu, 18 Feb 1993 08:43:34 +0000
X400-Originator: R.B.Jones@uk.co.icl.wins.win0109
X400-Recipients: info-hol@edu.uidaho.cs.ted
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600002273]
Original-Encoded-Information-Types: undefined (0)
X400-Content-Type: P2-1984 (2)
Content-Identifier: 2273
From: R.B.Jones@uk.co.icl.wins.win0109
Message-Id: <"2273*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: Strength of HOL


         I think the interesting question concerns the relative strength of 
         the HOL logic (as in HOL88/90 & ProofPower) and Zermelo + choice 
         (if the choice makes any difference).  ZF or ZFC are clearly (!) 
         stronger than either.
         
         To demonstrate that they have the same strength does not require 
         that you have to construct something in HOL which serves as the 
         universe of ZC (as suggested by Ching Tsun).  If you could do that 
         then you would prove that HOL was strictly stronger than ZC.
         
         A crude argument for equivalence refers to the alternative 
         definition of "Proof Theoretic Strength" (also in Beeson), which 
         states that the ordering by proof theoretic strength is the same 
         as the ordering by supremum of the well orderings provable in each 
         system (A is stronger than B if the supremum of the well-ordering 
         provable in A is larger than the supremum of the well-orderings 
         provable in B).  In terms of sizes of sets, there are no larger 
         sets in ZC than there are in HOL (and vice versa), so maybe that 
         holds for well-orderings too.
         
         Thomas Forster has moved on from thinking they are the same in 
         strength to thinking that they are different, but the quality of 
         his arguments (at least the ones presented to info-hol) havn't 
         moved on much, we still don't know much more than that he thinks 
         its "obvious".  How would you go about the proof Thomas?  The 
         naive approach, viz: constructing a set in ZC which is the natural 
         model for HOL doesn't work (because you can't), so how do you do 
         it?
         
         Incidentally, Feferman claims in a paper in the Handbook of 
         Mathematical Logic (Barwise) that Higher Order Logic is the same 
         strength as Zermelo set theory.  But evidently he also thinks this 
         obvious, since he doesn't offer an arguments in support of this 
         claim.
         
         I THINK they are the same, but I KNOW I can't prove it!
         
         Roger Jones
         International Computers Limited
         R.B.Jones@win0109.wins.icl.co.uk