RE: Plotkin-Statman conjecture

To: types@theory.LCS.MIT.EDU
Subject: RE: Plotkin-Statman conjecture
From: GDP%ECSVAX.ED.AC.UK@MITVMA.MIT.EDU (Gordon Plotkin)
Date: Wed, 29 Mar 89 19:56:00 EST
Sender: meyer@theory.LCS.MIT.EDU

Date:       28 Mar 89 14:57:03 BST

	A while ago I claimed to have proved that
Statman's conjecture (he called it mine, I call it his)
was true. Unfortunately the proposed proof relied
on my faulty recall of a theorem in my Curry paper.
This  was Theorem 2:

	"Suppose D is infinite. Then an element of the
finite type-hierarchy over D is lambda-definable iff
it  I-satisfies every I-relation ( in the terminology
of the paper)."


I forgot the restriction on D, and then proved the
truth of the  conjecture! If (as may well be) the
theorem is true without  restriction, the conjecture
is established.

First Thierry Coquand and them Henk Barendregt
pointed out the problem to  me.

Gordon Plotkin


PS Another thing I meant to post was on
terminology. Someone was wondering where the
terminology "logical relations" comes from. As far as
I know I was the first to use it in an unpublished
memorandum "Lambda-definability and logical
relations" ( part of that appeared as the Curry
volume paper). The idea is not that the relations are
in any sense logical themselves, but rather they can
be used to characterise those elements in the finite
type hierarchy which are logical in the sense that
they can be defined by logical means, i.e. just using
the typed lambda calculus. Richard Statman did
look at some of their logical properties, closure
under various operations. It may well not be good
practice to name things by what they are for, but
on the other hand, something like "hereditarily
definable" is a bit lifeless.