Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 25 May 1994 06:52:12 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA10712;
          Tue, 24 May 1994 23:45:53 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from diamond.idbsu.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA10708;
          Tue, 24 May 1994 23:45:48 -0600
Received: by diamond.idbsu.edu (1.37.109.4/16.2) id AA25487;
          Tue, 24 May 94 23:47:17 -0600
Date: Tue, 24 May 94 23:47:17 -0600
From: Randall Holmes <holmes@diamond.idbsu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Decidability
Message-ID: <"swan.cl.cam.:290840:940525055324"@cl.cam.ac.uk>


HOL is certainly not decidable; it has the strength of the theory 
of types of Russell, slightly weaker than the original set theory of
Zermelo.  This means that it is considerably stronger than arithmetic,
so G\"odel's theorems apply.

The opinions expressed		|     --Sincerely,
above are not the "official"	|     M. Randall Holmes
opinions of any person		|     Math. Dept., Boise State Univ.
or institution.			|     holmes@math.idbsu.edu