Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <00852-0@swan.cl.cam.ac.uk>; Thu, 6 Feb 1992 22:45:49 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17579;
          Thu, 6 Feb 92 14:24:26 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from goedel.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA17567;
          Thu, 6 Feb 92 14:23:43 -0800
Date: Thu, 6 Feb 92 17:24:45 EST
From: davidg@com.oracorp.goedel
Received: by goedel.oracorp.com (4.1/1.3-ORA Corporation) id AA02069;
          Thu, 6 Feb 92 17:24:45 EST
Message-Id: <9202062224.AA02069@goedel.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Interpolation theorem


Is it known whether the logic of HOL satisfies some kind of
interpolation theorem?

- David Guaspari
  davidg@oracorp.com

(Note: I am not a member of this mailing list, so I would appreciate
having replies mailed directly to me.)