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; Mon, 15 Feb 1993 16:53:30 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15182;
          Mon, 15 Feb 93 06:21:04 -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 AA15177;
          Mon, 15 Feb 93 06:20:58 -0800
Received: from Q.icl.co.uk by relay.pipex.net with SMTP (PP) 
          id <07154-0@relay.pipex.net>; Mon, 15 Feb 1993 14:20:00 +0000
Received: from eccles.dsbc.icl.co.uk by Q.icl.co.uk id AA14713;
          Mon, 15 Feb 93 14:21:34 GMT
Received: from ozz.oasis.icl.co.uk on eccles.dsbc.icl.co.uk id AA26502;
          Mon, 15 Feb 93 14:19:50 GMT
Received: on ozz.oasis.icl.co.uk over UUCP id AA13377;
          Mon, 15 Feb 93 14:21:13 GMT
Received: from wilfrid by iclbra.oasis.icl.co.uk (4.14/) id AA02816;
          Mon, 15 Feb 93 14:20:34 gmt
From: Rob Arthan <rda@uk.co.icl.win>
Date: Mon, 15 Feb 93 14:14:46 GMT
Message-Id: <9302151414.3441.0@win.icl.co.uk>
To: T.Forster@uk.ac.cam.pmms
Subject: Re: power of HOL
Cc: c@uk.co.icl.win, info-hol@edu.uidaho.cs.ted

Thomas Forster writes:

	Roger has just made the point that HOL is similar in strength to
	Zermelo Set Theory.  I am pretty sure it is *exactly* equivalent.
	At least i cannot see any obvious holes in the obvious proof.

What is the ``obvious proof''?

Rob Arthan. (rda@win.icl.co.uk)			ICL Secure Systems,
						Eskdale Rd.	
						Winnersh,	
						Wokingham	
						Berks. RG11 5TT