# Relationship between lambda-definability, specification and definability in model theory

I am new to lambda calculus and definability theory, and I am trying to clarify my understanding of the relationship among the following concepts:

1. An element $a$ in the domain of a type $A_\sigma$ is $\lambda$-definable if it is the denotation of a closed lambda-term
2. A subset $X$ is definable, in the model-theoretic sense, if it is the denotation of some formulas in the background language
3. Let $L^+$ be an extension of a ground langauge $L$ with a new signature term $r$. We say $r$ is explicitly definable in $L$ if it is extensionally equivalent to a formula in $L$, i.e.~there is $\varphi(x)$ in $L$ such that $\forall x(r(x)\leftrightarrow \varphi(x))$ (if $r$ is a constant, then $r(x)$ stands for $x=r$).
4. The axiom of restricted comprehension/specification says, roughly, for every formula and a given set, there is a subset of that set specified by that formula.

Is it right to think that 1. comprehension and $\lambda$-definability are inversions of each other: the former says, given a description there is a denotation of that description, whereas the latter asks, given a term is it denotated by some description (I have also read somewhere that $\lambda$-abstraction is tantamount to comprehension principles-is it correct?) 2. model-theoretic explicit definability and $\lambda$-definability are largely orthogonal to each other. The former is strictly a question about the relative expressiveness of two languagues, whereas the latter concerns the syntax-semantic interface. On this note, I am also wondering if there has been any work on the relationship between explicit definability in the model-theoretic sense, and definability by $\lambda$-abstraction. For instance, assuming $\beta$-conversion, if $X\equiv\lambda x:\sigma. \varphi(x)$, then $\varphi(x)$ is automatically an explicit definition for $X$ (assuming, of course that we have $\forall^\sigma$ in our language). But we also know that explicit and implicit definability come apart in higher-order logic. Is there a precise definition of implicit definability in type-theoretic terms?