MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
I asked a related question here, which may be of use. – day Feb 11 '14 at 10:56

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.