Return-Path: 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 09:21:37 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA12025; Wed, 25 May 1994 02:14:46 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from irafs1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA12021; Wed, 25 May 1994 02:14:42 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Wed, 25 May 1994 10:10:27 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <03314-0@i80fs2.ira.uka.de>; Wed, 25 May 1994 10:16:46 +0200 To: info-hol@leopard.cs.byu.edu Subject: Decidability Date: Wed, 25 May 1994 10:16:45 +0200 From: schneide Message-Id: <"i80fs2.ira.316:25.04.94.08.16.48"@ira.uka.de> As it has already been pointed out: HOL is certainly not decidable. And even worse, there is no algorithm which could list all theorems of the logic. HOL means "higher order logic", not the calculus of the HOL system. The proveable formulae of the HOL system are recursively enumerable, but I they are also not decidable, since number theory has been formalized in the HOL system (Goedels theorems). Klaus.