# Joachim Breitner's Homepage

## A Mistake in Church’s Paper

For a course at the IIT Bombay on functional programing, I was preparing a presentation on Alonzo Church’s theorem, based on his original 1936 paper “An Unsolvable Problem of Elementary Number Theory” where he first showed that the Entscheidungsproblem is not solvable. In that paper, he states a theorem (Theorem II) “If a formula has a normal form […] any sequence of reductions of the formula must (if continued) terminate in the normal form”. This seems to be wrong. Consider the lambda expression KIΩ, where K=(λxy.x), I=(λx.x) and Ω=(λx.xx)(λx.xx). This has a normal form I. But because Ω reduces to Ω, there is a non-terminating sequence KIΩ → KIΩ → ⋯, in contradiction to Church’s claim. The same example contradicts his Theorem III: “If a formula has a normal form, every well-formed part of it has a normal form.”, which is used in the very proof of his main result, Theorem XVIII.

There is no proof for Theorem II in this paper. He cites it from the then forthcoming paper “Some properties of Conversion” by him and J. B. Rosser. There, proofs are given (see Theorem 2 and its Corollary) but they are quite impenetrable to me. So I was searching for some correction paper, or any other discussion of this issue, but could not find any. Does any reader of this blog know more? What happened in that times when a paper had an error in some proof? What would happen now? Or is this not an error after all, but just a subtle difference between the definitions of λ-calculus as we know and as they introduced it?

Unrelated to this question: The professor asked me to write down a summary of (my interpretation of) the importance and impact of Church’s paper with regard to Gödel and Hilbert’s program, and how that relates to Böhm’s theorem. In the spirit of sharing, I have uploaded my thoughts on Church and Böhm, comments are welcome.

**Update**: Christian von Essen solved the riddle in a comment to this post: Church only considers lambda abstractions as well-formed when the bound variable actually occurs (freely) in the abstracted term. This does not allow for the K combinator and thus there is no problem.

## Comments

If you replace 'has a normal form' with 'is strongly normalizing,' the theorems become true, but they're more or less trivial. So I don't know what they were thinking.

Remarkably, though, as old as these papers are, google actually turns up freely available copies.

Firstly, I would replace "propositions" with "sentences", "statements" or "formulae", since generally a proposition is taken to be the meaning of a sentence, while the sentence or formula is a string of symbols in a formal language.

Secondly, Gödel's first incompleteness theorem shows that there are true but unprovable statements in any sufficiently strong theory (where 'true' here just means that the Gödel sentence assets its own unprovability, and is indeed unprovable). It's unclear whether your locution "true ... within this system" means truth, or just provability. Tarski's undefinability theorem shows that arithmetical truth cannot be defined within arithmetic, so presumably you mean the latter, but it would be better to be precise.

"If the formula M is well-formed and

_contains an occurence of $x$ as a free variable in M_, then \lambda x [M] is well-formed" (page 3, 5th line from below)

Have something to say? You can post a comment by sending an e-Mail to me at <mail@joachim-breitner.de>, and I will include it here.

clearly omega.omega does, but just omega?