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 20:04:51 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02259;
          Fri, 12 Feb 93 11:38:26 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA02252;
          Fri, 12 Feb 93 11:38:09 -0800
Received: by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA03560;
          Fri, 12 Feb 93 11:36:35 -0800
Date: Fri, 12 Feb 93 11:36:35 -0800
From: chou@edu.ucla.cs (Ching-Tsun Chou)
Message-Id: <9302121936.AA03560@maui.cs.ucla.edu>
To: R.B.Jones@uk.co.icl.wins.win0109, T.Forster@uk.ac.cam.pmms, 
    info-hol@edu.uidaho.cs.ted
Subject: Re: power of HOL


Thomas Forster wrote:

> Roger has just made the point that HOL is similar in strength to
> Zermelo Set Theory.  

I've seen this statement a lot, but never understood what exactly
it means.  Could someone enlighten me?  How does one compare two
formal theories?

- Ching Tsun