Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET
          with NIFTP to fgate (PP) id <4622-0@swan.cl.cam.ac.uk>;
          Thu, 20 Jun 1991 01:30:23 +0100
Received: from edu.ucdavis.eecs.iris by sun2.nsfnet-relay.ac.uk
          with SMTP inbound id <21191-0@sun2.nsfnet-relay.ac.uk>;
          Thu, 20 Jun 1991 00:33:37 +0100
Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.7.0) id AA07511;
          Tue, 18 Jun 91 13:06:36 -0700
Received: from iris.eecs.ucdavis.edu
          by clover.eecs.ucdavis.edu (5.59/UCD.EECS.5.0) id AA28433;
          Mon, 17 Jun 91 16:13:12 PDT
Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.7.0) id AA08319;
          Mon, 17 Jun 91 10:41:49 -0700
Date: Mon, 17 Jun 91 13:39:21 EDT
From: garrel@com.oracorp.achilles
Received: by achilles.oracorp.com (4.1/1.3-ORA Corporation) id AA10520;
          Mon, 17 Jun 91 13:39:21 EDT
Message-Id: <9106171739.AA10520@achilles.oracorp.com>
To: info-hol@edu.ucdavis.clover
Subject: Questions about the HOL logic

1.  Completeness and compactness

Has anybody looked into adapting the techniques of Henkin, "Completeness
in the Theory of Types", Journal of Symbolic Logic, vol. 15 (1950),
pp. 81--91, to prove completeness and compactness for the HOL logic?

2.  Adding axioms

There are several warnings in the Tutorial and System Description to
the effect that adding axioms to the HOL logic is very likely to lead
to inconsistency.  It appears to me that this is only a worry if the
axioms involve polymorphic types.  For example, I don't think adding
a type of reals and postulating that it is a complete ordered field
would cause any trouble.  Am I right about this, or have I missed
something?

Garrel Pottinger
garrel@oracorp.com