We shall present various results and open questions on the
F-completeness of various classes af models of untyped lambda-calculus.
We recall that if M' included in M are two classes of lambda-models,
and F is a class of formulae, M' is F-complete w.r.t. M
if, for every formula Phi in F, whenever all the models in M'
satisfy Phi, all the models in M satisfy Phi too.
If time permits, we shall present some elementary uses
of pre-logical relations to models of polymorphism.
öaut;