[TYPES] logical relations

[Jeffrey Sarnat]

A little bit of further digging reveals this message, which seems to 
confirm the "Gordon Plotkin coined the term" hypothesis:

http://www.seas.upenn.edu/~sweirich/types/archive/1989/msg00047.html

I've never seen the technical report he's referring to either, but you can 
count me among the people who would love to get their hands on a copy of 
it.

Also, Statman's 1985 Information and Control paper makes use of the term 
"fundamental theorem of logical relations," although I can't say if he's 
the first to give it a name. His notation is somewhat nonstandard (for me 
at least), but it's a fun paper nonetheless.

As far as I can tell, the first use of the concept of a logical relation 
is usually attributed to Tait's 1967 JSL paper "Intensional interpretation 
of functionals of finite type I." You can actually get an electronic copy 
of this paper (and pretty much every other JSL paper, as far as I know) 
through jstor, but the writing is pretty dense. There are numerous other 
papers that make essential use of logical relations (including Girard's 
original reducibility candidates proof) in the "Proceedings of the Second 
Scandinavian Logic Symposium" (published in 1971), but as far as I can 
remember they all use terminology to the effect of "computability 
predicate" and "reducibility candidate" and do not give a special name for 
the main/fundamental/basic lemma/theorem.

 	Jeff

On Thu, 26 Jan 2006, Eijiro Sumii wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> Thank you very much for all the replies (both private and public).
> Many of them have pointed out the lambda-definability papers by
> Plotkin.  I managed to get a copy of the one in Curry Festschrift
> (thanks to my colleagues).
>
> HOWEVER, according to my quick "eye grep" of this paper, it does not
> seem to contain the words "logical relations" nor
> "main/basic/fundamental lemma/theorem" anywhere, so I still do not
> know the answer to the "for what reason" part of my question.  Perhaps
> I should try harder to get the 1973 tech report (as well as other
> original papers by Tait and Statman).
>
> By the way, there was also a similar question back in 1988 in Types
>
>  http://www.seas.upenn.edu/~sweirich/types/archive/1988/msg00052.html
>
> and a reply by Prof. John Mitchell
>
>  http://www.seas.upenn.edu/~sweirich/types/archive/1988/msg00061.html
>
> but even he does not seem to have known a clear answer...!
>
>        Eijiro
>
> P.S.  A few people asked me why I am asking.  The primary reason is my
> own curiosity, but this time my question was also inpired by a student
> who loves to know.
>