Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-5.6) id <19675-0@swan.cl.cam.ac.uk>; Wed, 20 Nov 1991 19:36:50 +0000 Received: by ted.cs.uidaho.edu (15.11/1.34) id AA06916; Wed, 20 Nov 91 11:22:02 pst Reply-To: info-hol@ted Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from electra.oracorp.com by ted.cs.uidaho.edu (15.11/1.34) id AA06912; Wed, 20 Nov 91 11:21:48 pst Date: Wed, 20 Nov 91 14:16:54 EST From: garrel@com.oracorp.electra Received: by electra.oracorp.com (4.1/1.3-ORA Corporation) id AA09802; Wed, 20 Nov 91 14:16:54 EST Message-Id: <9111201916.AA09802@electra.oracorp.com> To: info-hol@edu.uidaho.cs.ted, andrews@EDU.CMU.CS, rc@edu.cornell.cs, bret@com.oracorp, hook@edu.ogi.cse, anil@edu.cornell.msi.mssun7, richard@com.oracorp, coquand@fr.inria.margaux, majrh@uk.ac.swan.pyr, henkin@edu.berkeley.math, seldin@ca.concordia.alcor Subject: Completeness for the HOL logic I have extended Henkin's completeness theorem for Church's type theory to cover the HOL logic. I will send a report giving some of the details in a few days, after I rest a bit and take care of some mundane, but pressing business. Garrel Pottinger garrel@oracorp.com