8
$\begingroup$

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.)

$\endgroup$
8
  • $\begingroup$ Are there any base types? What is known about them? $\endgroup$ Aug 6, 2021 at 22:49
  • $\begingroup$ Oops, I meant to specify that the base types were infinite. Thanks! $\endgroup$ Aug 6, 2021 at 23:19
  • $\begingroup$ Just to make sure, you're more or less (because there are no products) describing a sub-ccc of $\mathsf{Set}$? $\endgroup$ Aug 7, 2021 at 8:28
  • $\begingroup$ 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). $\endgroup$ Aug 7, 2021 at 17:45
  • $\begingroup$ Ah yes, of course, the exponential objects are different. Thanks. $\endgroup$ Aug 7, 2021 at 20:25

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.