Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Fri, 12 Feb 1993 09:33:51 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28074;
          Fri, 12 Feb 93 01:23:10 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from relay.pipex.net by ted.cs.uidaho.edu (16.6/1.34) id AA28069;
          Fri, 12 Feb 93 01:23:03 -0800
X400-Received: by mta relay.pipex.net in /PRMD=pipex/ADMD=cwmail/C=GB/; Relayed;
               Fri, 12 Feb 1993 09:21:28 +0000
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2));
               Relayed; Fri, 12 Feb 1993 09:18:35 +0000
Date: Fri, 12 Feb 1993 09:18:35 +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 0000012600002259]
Original-Encoded-Information-Types: undefined (0)
X400-Content-Type: P2-1984 (2)
Content-Identifier: 2259
From: R.B.Jones@uk.co.icl.wins.win0109
Message-Id: <"2259*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.uidaho.cs.ted
Subject: power of HOL







         Power of HOL
         
         Computationally HOL is Turing Complete.  This isn't saying much.
         
         The logical (proof theoretic) strength of HOL is a logical matter, 
         I would not have thought it a problem in "advanced computation", 
         and the answer is well known.
         
         Logically its strength is similar to Zermelo set theory. It is 
         extremely easy to increase the strength (you just add more axioms, 
         and its not difficult to find safe extensions), but for most 
         applications this is unnecessary.  Since its intended 
         interpretation admits the construction of the natural numbers, the 
         logic is bound to be incomplete relative to that interpretation 
         (because arithmetic truths are not even semi-decidable, and 
         "theoremhood" must be).
         
         A more interesting topic to computer scientists and engineers 
         concerns the quality of the support which the various HOL 
         implementations provide for constructing and checking proofs.  
         Unfortunately I don't think there are any good metrics in this 
         area.
         
         
         Roger Jones
         International Computers Limited
         R.B.Jones@win0109.wins.icl.co.uk