[TYPES] logical relations

[Thomas Streicher]

I don't know who used which term first. But a logical relations technique
was first used by W.Tait in his proof for strong normalisation for the
typed \lambda-calculus. It was a unary logical relation, i.e. a 
"logical predicate". I guess this this the source for the term "logical".

Another source is Laeuchli's paper from 1970 who proved for Set^Z (i.e. sets
with an iso and equivariant maps between them) that all interpretations of
proofs are premutation invariant. He used this for showing that all 
interpretations of a type are inhabited iff there is a proof for the
corresponding proposition.

As I heard by rumour Lauchli's result inspired Gordon Plotkin to introduce
an appropriate generalisation of permutation-invariance, namely logical
realtions, for characterising \lambda definability. He din't f ully succeed.
Much later there was a paper by Jung & Tiuryn (TLCA 1993) where using Kripke
logical relations they finally arrived at this goal.

I think the "fundamental lemma" is called the  "fundamental lemma" because
it tells you the fundamental fact about logical relations namely that
syntactically definable elements are invariant under every logical relation
under which that constants are invariant. "Invariance Lemma" might be a more
telling name but history decided otherwise.

Thomas Streicher