How strong is equivalence of lambda expressions?

Consider two lambda expressions $\mu$, $\nu$ representing computable functions $f_{\mu,\nu}:\mathbb{N} \rightarrow \mathbb{N}$. If $\mu$ and $\nu$ are equivalent under the combination of $\beta$-reductions, $\alpha$-conversions and $\eta$-conversions then $f_\mu=f_\nu$.


Under what conditions does the converse hold? In particular, if it is possible to prove in Peano arithmetic that $f_\mu=f_\nu$, does it follow $\mu$, $\nu$ are equivalent in the above sense?

In general, there is always an infinite number of "computationally different" functions that are extensionally equal: take for instance the "$3n+1$-function" $g$, and for any function $f$ define $G_f$ to be:

$$ G_f(n)=\begin{cases} f(n) & \mbox{if }g(n)\mbox{ cycles at }1 \\ 0 & \mbox{otherwise}\end{cases}$$

This function is (probably) extensionally equal to $f$ for every $f$, but this is (possibly) not provable in $\mathrm{PA}$, or indeed in the weak framework of $\beta\eta\alpha$-conversion.

More pragmatically, the identity function $\lambda x.x$ and the "stupid identity"
$$ \lambda n.n\ (\lambda x\ f.x)\ (\lambda m\ x\ f.f(m\ x \ f))$$

Denote the same function $\mathrm{id}:\mathbb{N}\rightarrow \mathbb{N}$, under the usual church encoding, but are not $\beta\eta$-equal, as can easily be seen (they are both in normal form).

StackExchange Computer Science Q#20052, answer score: 3