Logical relationはなぜlogicalなのか

かなり前にも触れましたが、ATTAPL (Advanced Topics in Types and Programming Languages)の234ページにある

Such a relation is called "logical" because it respects the actions of the logical operators (in this case implication) that correspond to the language's type constructors.

という記述は、（命名者自身によれば）歴史的経緯としては事実ではないそうです。
http://www.seas.upenn.edu/~sweirich/types/archive/1989/msg00047.html (強調筆者)

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.

まあ、そもそもATTAPLのこの章(6章)の著者は（以下検閲削除

P.S. 上でreferされているmemorandumはオンラインにないと思うので、もしほしい方がいらしたら私にメールしてください。（Typesメーリングリストで質問したときにPlotkinが郵送してくれたのでスキャンしてあります。）　Curry Festschriftの"Lambda-Definability in the Full Type Hierarchy"とは別の論文です（内容は近いですが）。

P.P.S. 私も決して専門家ではないのですが門外漢なりに一応の解説をすると、並列論理和の件で触れた通り、CPOなど古典的な表示的意味論は普通の型付きλ計算の正確なモデルにならないのですが、論理関係を使うとfully abstractなモデルが作れる、という話だと思います。モデル化している「対象」が「論理的」（型付きλ計算）なのであって、そのモデル自身(logical relation)が論理的なわけではない、という（命名者本人による）説明↑です。あくまで「歴史的経緯」というだけで、実際の結果としてはまさに「論理的な関係」になっていますが。