# $\lambda$-definability and structure preserved by homomorphisms

I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it.

Some prelimary definitions.

A Henkin structure $$A = (A^\cdot, ⟦\cdot⟧_A)$$ for the simply typed $$\lambda$$-calculus with a single base type $$o$$ consists of a set $$A^\sigma$$ for each type $$\sigma$$ such that $$A^{\sigma\to\tau}\subseteq (A^\tau)^{A^\sigma}$$, $$⟦\cdot⟧$$ is a function mapping assignments and simply typed $$\lambda$$-term to elements of the appropriate domains satisfying the usual clauses: $$⟦x⟧^g=g(x)$$, $$⟦\lambda x.M⟧^g = a \mapsto ⟦M⟧^{g[a/x]}$$, $$⟦MN⟧=⟦M⟧⟦N⟧)$$.

A homomorphism between structures $$A$$ and $$B$$ is a type-indexed family of functions $$h^\sigma:A^\sigma \to B^\sigma$$, such that $$h^\sigma(⟦ M⟧_A^g)=⟦ M⟧_B^{h\circ g}$$ for every term $$M$$ of type $$\sigma$$.

An element $$d\in A^\sigma$$ is $$\lambda$$-definable iff $$d = ⟦M⟧_A$$ for some closed term $$M$$, and is $$\lambda$$-definable from elements $$a_1...a_n$$ of the structure if $$d = ⟦M⟧(a_1)...(a_n)$$ for some closed term $$M$$.

QUESTION: is it true that if $$A$$ is a Henkin model with $$A^o$$ infinite, and $$d\in A^\sigma$$ is an element of that is preserved by homomorphisms, in the sense that for every $$h,h':A\to B$$, $$h^\sigma(d)=h'^\sigma(d)$$, then $$d$$ is $$\lambda$$-definable?

(There are analogous questions for more general classes of models of the simply typed $$\lambda$$-calculus, that I would also be interested to know about if the answer depends on the type of model.)

• Are there any base types? What is known about them? Aug 6, 2021 at 22:49
• Oops, I meant to specify that the base types were infinite. Thanks! Aug 6, 2021 at 23:19
• Just to make sure, you're more or less (because there are no products) describing a sub-ccc of $\mathsf{Set}$? Aug 7, 2021 at 8:28
• I'm not sure how to define "sub-CCC", but if you add products and treat the domains $A^\sigma$ as objects with $Hom(A^\sigma,A^\tau)=A^{\sigma\to\tau}$, a Henkin model is a CCC that is also a subcategory of set (but, potentially, with different exponential objects). Aug 7, 2021 at 17:45
• Ah yes, of course, the exponential objects are different. Thanks. Aug 7, 2021 at 20:25