<p>I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it.</p>
<p>Some prelimary definitions.</p>
<p>A Henkin structure <span class="math-container">$A = (A^\cdot, ⟦\cdot⟧_A)$</span> for the simply typed <span class="math-container">$\lambda$</span>-calculus with a single base type <span class="math-container">$o$</span> consists of a set <span class="math-container">$A^\sigma$</span> for each type <span class="math-container">$\sigma$</span> such that <span class="math-container">$A^{\sigma\to\tau}\subseteq (A^\tau)^{A^\sigma}$</span>, <span class="math-container">$⟦\cdot⟧$</span> is a function mapping assignments and simply typed <span class="math-container">$\lambda$</span>-term to elements of the appropriate domains satisfying the usual clauses: <span class="math-container">$⟦x⟧^g=g(x)$</span>, <span class="math-container">$⟦\lambda x.M⟧^g = a \mapsto ⟦M⟧^{g[a/x]}$</span>, <span class="math-container">$⟦MN⟧=⟦M⟧⟦N⟧)$</span>.</p>
<p>A homomorphism between structures <span class="math-container">$A$</span> and <span class="math-container">$B$</span> is a type-indexed family  of functions <span class="math-container">$h^\sigma:A^\sigma \to B^\sigma$</span>, such that <span class="math-container">$h^\sigma(⟦ M⟧_A^g)=⟦ M⟧_B^{h\circ g}$</span> for every term <span class="math-container">$M$</span> of type <span class="math-container">$\sigma$</span>.</p>
<p>An element <span class="math-container">$d\in A^\sigma$</span> is <span class="math-container">$\lambda$</span>-definable iff <span class="math-container">$d = ⟦M⟧_A$</span> for some closed term <span class="math-container">$M$</span>, and is <span class="math-container">$\lambda$</span>-definable from elements <span class="math-container">$a_1...a_n$</span> of the structure if <span class="math-container">$d = ⟦M⟧(a_1)...(a_n)$</span> for some closed term <span class="math-container">$M$</span>.</p>
<p>QUESTION: is it true that if <span class="math-container">$A$</span> is a Henkin model with <span class="math-container">$A^o$</span> infinite, and <span class="math-container">$d\in A^\sigma$</span> is an element of that is preserved by homomorphisms, in the sense that for every <span class="math-container">$h,h':A\to B$</span>, <span class="math-container">$h^\sigma(d)=h'^\sigma(d)$</span>, then <span class="math-container">$d$</span> is <span class="math-container">$\lambda$</span>-definable?</p>
<p>(There are analogous questions for more general classes of models of the simply typed <span class="math-container">$\lambda$</span>-calculus, that I would also be interested to know about if the answer depends on the type of model.)</p>

CC BY-SA 4.0
2021-08-06T22:49:31.513Z
Are there any base types? What is known about them?
Andrej Bauer
CC BY-SA 4.0
2021-08-06T23:19:55.547Z
Oops, I meant to specify that the base types were infinite. Thanks!
Andrew Bacon
CC BY-SA 4.0
2021-08-07T08:28:33.267Z
Just to make sure, you're more or less (because there are no products) describing a sub-ccc of $\mathsf{Set}$?
Andrej Bauer
CC BY-SA 4.0
2021-08-07T17:45:16.770Z
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).
Andrew Bacon
CC BY-SA 4.0
2021-08-07T20:25:42.830Z
Ah yes, of course, the exponential objects are different. Thanks.
Andrej Bauer
CC BY-SA 4.0
2021-08-08T09:33:24.117Z
If you take the elements that are preseved by all homomorphisms (they need a name), do they also form a Henkin structure? And if so, what if you then repeat the process, does it stop?
Andrej Bauer
CC BY-SA 4.0
2021-08-08T16:52:34.383Z
Strictly speaking, no. If your new (shrunk) domain $B^\sigma$ is a proper subset of  $A^\sigma$, and $B^{\sigma\to\tau}$ is a subset of $A^{\sigma\to\tau}$ the new structure is not Henkin, since $B^{\sigma\to\tau}$ is not a set of functions with domain $B^\sigma$.
Andrew Bacon
CC BY-SA 4.0
2021-08-08T16:58:40.117Z
But it also seems unlikely to me that the applicative structure consisting of "invariant" elements will even be isomorphic to a Henkin structure. For instance, the substructure of $A$ consisting of $\lambda$-definable elements is not extensional since the Church numerals of type $(o\to o)\to o\to o$ are distinct (since the base types are infinite), but there is only one element in the domain $o\to o$, identity.

That said, there is a variant of my question for the wider class of (possibly non-functional) applicative structures that are models of the simply typed $\lambda$-calculus.
Andrew Bacon
<type-theory><lambda-calculus><typed-lambda-calculus>
$\lambda$-definability and structure preserved by homomorphisms
Andrew Bacon
# $\lambda$-definability and structure preserved by homomorphisms

(Asked by: username_0 on 2021-08-06)

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

**Tags:** type-theory, lambda-calculus, typed-lambda-calculus
> **Comments:**
> **username_1**: Are there any base types? What is known about them?  
> **username_0**: Oops, I meant to specify that the base types were infinite. Thanks!  
> **username_1**: Just to make sure, you're more or less (because there are no products) describing a sub-ccc of $\mathsf{Set}$?  
> **username_0**: 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).  
> **username_1**: Ah yes, of course, the exponential objects are different. Thanks.  
> **username_1**: If you take the elements that are preseved by all homomorphisms (they need a name), do they also form a Henkin structure? And if so, what if you then repeat the process, does it stop?  
> **username_0**: Strictly speaking, no. If your new (shrunk) domain $B^\sigma$ is a proper subset of  $A^\sigma$, and $B^{\sigma\to\tau}$ is a subset of $A^{\sigma\to\tau}$ the new structure is not Henkin, since $B^{\sigma\to\tau}$ is not a set of functions with domain $B^\sigma$.  
> **username_0**: But it also seems unlikely to me that the applicative structure consisting of "invariant" elements will even be isomorphic to a Henkin structure. For instance, the substructure of $A$ consisting of $\lambda$-definable elements is not extensional since the Church numerals of type $(o\to o)\to o\to o$ are distinct (since the base types are infinite), but there is only one element in the domain $o\to o$, identity.  That said, there is a variant of my question for the wider class of (possibly non-functional) applicative structures that are models of the simply typed $\lambda$-calculus.  

---

## 0 answers

