チャーチ数と λ 定義可能性

$n\in\mathbb{N}$ のチャーチ数を $\overline n\equiv\lambda fx.f^nx$ とする。ここで $f^0x\equiv x$、$f^{n+1}x\equiv f(f^nx)$。全関数 $\varphi:\mathbb{N}^k\to\mathbb{N}$ が λ 定義可能であるとは、閉項 $F$ が存在して、すべての $n_1,\ldots,n_k$ について

となることをいう。