Let $H$ be the complete hierarchy of functionals over $\mathbb{N}$. To be precise: let the set $T$ of 'simple types' be the smallest set such that '0' $\in T$ and $(α→β) \in T$ whenever $α, β \in T$. $H$ is a function defined on $T$ by the condition that $H(0)$ = $\mathbb{N}$ and $H(α→β) = {H(\beta)}^{H(\alpha)}$, i.e. the set of all functions from $H(α)$ to $H(β)$. Let a "typed subfamily" of $H$ be a function $\Sigma$ on $T$ such that $\Sigma(α)⊂H(α)$ for all $α$. Say that a typed subfamily $\Sigma$ is extensional just in case, for any distinct $f, g ∈ \Sigma(\alpha→\beta)$, there is some $x ∈ \Sigma(\alpha)$ such that $f(x) \ne g(x)$.
For any typed subfamily $\Sigma$, let $\Sigma^*$ — the "combinatory closure" of $\Sigma$ — be the typed subfamily consisting of members of $H$ definable by closed, typed $λ$-terms built up from constants in $\Sigma$. (For those who want a precise definition, here goes. Let Var map each $α \in T$ to an infinite set of variables, with no overlap. $\mathcal{L}_\Sigma$ will assign each type $α$ in $T$ to a collection $\mathcal{L}_Σ(α)$ of 'terms of type $α$' as follows.
- Var$(α) ⊂ \mathcal{L}_Σ(α)$ and $\Sigma(α) ⊂ \mathcal{L}_Σ(α)$.
- $(XY) \in \mathcal{L}_Σ(β)$ whenever $X \in \mathcal{L}_Σ(α→β)$ and $Y \in \mathcal{L}_Σ(α)$.
- $(λv.X) \in \mathcal{L}_Σ(α→β)$ whenever $v \in $Var($α$) and $X \in \mathcal{L}_Σ(β)$.
These are the only terms: $\mathcal{L}_Σ$ is the smallest family meeting these conditions. When $g$ is any 'assignment function' mapping each $Var(α)$ to $H(α)$, let $|\cdot|_g$ be the 'denotation function' that maps each $\mathcal{L}_Σ(α)$ to $H(α)$ according to the following rules:
- $|v|_g = g(v)$ when $v \in Var(α)$
- $|X|_g$ = $X$ when $X \in \Sigma(α)$
- $|(XY)|_g$ = $|X|_g(|Y|_g)$
- $|(λv.X)|_g(y)$ = $|X|_{g^{v→y}}$, where $g^{v→y}$ is the function that agrees with $g$ except for mapping $v$ to $y$.
$|X|_g$ is independent of $g$ when $X$ contains no free variables (is closed) - in that case we write $|X|$. $\Sigma^+(α)$ = $\{|X|: X$ a closed $\mathcal{L}_Σ$-term of type $α\}$.)
Specific question: let $P$ be the typed subfamily of $H$ consisting in all members of $\mathbb{N}$ together with the addition function. That is:
- $P(0) = H(0) = \mathbb{N}$
- $P(0→(0→0)) = \{f\}$ where $f(n)(m) = n+m$
- $P(α) = \emptyset$ for all other $\alpha$.
Is $P^*$ extensional?
More general question: is there a useful general condition for $\Sigma^*$ to be extensional?