In S.C. Kleene's 1935 paper "$\lambda$-definability and recursiveness," he proves that all $\lambda$-definable functions are general recursive in the Herbrand-Godel sense and vice-versa. However, the exact choice of definition for $\lambda$-definable is a bit confusing for me. He differentiates between well-formed formulas (wff) and properly formed formulas (pff). Wffs are pffs where in each properly formed part $\lambda x[M]$, $x$ must appear as a free symbol in $M$. For example, $\lambda x \cdot x$ is both a wff and a pff, but $\lambda x \cdot y$ is only a pff. He then goes on to define $\lambda$-definable functions using a Church encoding.
All modern sources that I've found on the $\lambda$-calculus are only concerned with properly formed formulas. Kleene himself notes in a footnote that by only considering pffs,
...simplifications are afforded in the proofs of many theorems, but unfortunately difficulties are introduced in the formal logics in which this theory is used. Rosser has shown that the formal definition ($\lambda$-K-definition) under this program is equivalent to $\lambda$-definition, when the range of the independent variable is the set of natural numbers, and all the values have the same free symbols. For functions over all well-formed formulas, $\lambda$-K-definition is not equivalent to $\lambda$-definition, but we conjecture that the equivalence holds for many other significant ranges...
I would like to know more about this. It seems that what we today call the untyped $\lambda$-calculus was the $\lambda$-K-calculus to Kleene and Church. I can see why many of the proofs are much simpler in the $\lambda$-K-calculus. My questions are:
What do we gain by only considering the well-formed formulas ("difficulties are introduced in the formal logics...")?
Does the equivalence still hold between $\lambda$-K-definable functions and Herbrand-Godel general recursive functions?
If so, is there a more modern paper or textbook that shows this using simpler proofs?
