We looked into this kind of thing about seven or eight years ago. See @inproceedings( mmms87, author="A. R. Meyer and J. C. Mitchell and E. Moggi and R. Statman", Key="MMMS 87", Title="Empty types in polymorphic lambda calculus", Booktitle="Proc. 14th ACM Symp. on Principles of Programming Languages", Month="January",Year="1987", pages="253-262", Note="Reprinted with minor revisions in {\it Logical Foundations of Functional Programming,} ed. G. Huet, Addison-Wesley (1990) 273--284.") @article( mm87, author="Mitchell, J.C. and Moggi, E.", Title="Kripke-style models for typed lambda calculus", Journal="Ann. Pure and Applied Logic", Volume="51",Year="1991", pages="99--124", Note="Preliminary version in {\it Proc. IEEE Symp. on Logic in Computer Science,} 1987, pages 303--314.") @incollection( MitchScott,Author="Mitchell, J.C. and Scott, P.J.", Title="Typed lambda calculus and cartesian closed categories", Booktitle="Categories in Computer Science and Logic, Proc. Summer Research Conference, Boulder, Colorado, June, 1987", Series="Contemporary Mathematics", volume="92", publisher="Amer. Math. Society", editors="J.W. Gray and A. Scedrov", Year="1989", pages="301-316") Friedman's completeness theorem is completeness of beta,eta for full classical model (i.e., Set). Deductive completeness fails for Set and for models (interpretations into categories) where every type (every object named by a type expression) is required to be non-empty (have a global element). I tried to clarify this in my book (still to appear). If anyone is seriously interested, I could email the appropriate sections of the book. John Mitchell