Completeness, invariance and λ-definability

In [4] Gordon Plotkin considers the problem of characterizing the λ -definable functionals in full type structures. A plausible, but, as we shall see, quite false, conjecture is that a functional is λ -definable ⇔ it is invariant in the sense of Fraenkel and Mostowski. A better guess might be that the set of λ -definable functionals of type σ has a uniform (in σ ) definition in type theory over all full type structures (Plotkin explicitly considers a certain sort of definition by means of “logical relations”). More or less generally, one may ask if the following question is decidable. Given: a functional F in a full type structure over a finite ground domain. Question: is F λ -definable? We call the statement that this question is decidable Plotkin's λ -definability conjecture. We do not know if Plotkin's conjecture is true. In this note we consider several questions which quickly arise from Plotkin's conjecture. In § 1, we ask which type structures satisfy λ -definability = invariance. We construct for each consistent set of equations a model satisfying this equality. From consideration of these models we obtain a number of syntactic corollaries including a reduction of βη -conversion to βη -conversion at a single type (Theorem 3), an “ ω -rule” for βη -conversion (Proposition 6) and consistency with βη -conversion (Proposition 8), definability and indefinability results for versions of Kronecker's δ (Propositions 10 and 11), and a decidability result for the problem of inter-definability among combinators.