Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Fri, 7 Feb 92 15:42:31 EST
From: davidg@com.oracorp.goedel
Message-Id: <9202072042.AA02645@goedel.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Interpolation theorem (again)
Cc: shb@com.oracorp


An addendum to my question about the existence of interpolation
theorems for the logic of HOL:

My co-worker, Steve Brackin, pointed out that with a naive definition
of "interpolant" (which is more or less the one I had in mind), the
interpolation theorem is immediate for any reasonable higher order
logic.  For example (and excusing, please, any non-HOL notation), if
f: T1 -> T2 is the only non-logical symbol contained in formula A but
not in B, and if

  A |- B,

then

  A |- exists f:T1 -> T2. A

and

  exists f:T1 -> T2. A |- B

And "exists f:T1 -> T2. A" could be regarded as an interpolant of A
and B, since the only constants it contains occur in both formulas.

Presumably one must restrict the notion of "interpolant" to something
like this: an interpolant may refer only to the types occurring in
both A and B.  Possibly there are various kinds of interpolation
theorems.  I'm not quite sure what I'm after, but I'd still like to
know what answers are out there.

- David Guaspari
  davidg@oracorp.com