A Mistake in Church’s Paper

Published 2011-01-23 in sections English, Mathe.

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

why do you say omega reduces to itself?

clearly omega.omega does, but just omega?

#1 anon am 2011-01-23

We have Ω=(λx.xx)(λx.xx), so if we apply the left lambda, we substitute the variable x in xx with the term (λx.xx) and end up at (λx.xx)(λx.xx) which is Ω, so yes, Ω does reduce to itself.

#2 Joachim Breitner (Homepage) am 2011-01-23

Perhaps they would not consider KIΩ to have a normal form? Although, there's no indication in the first paper that this is the case, given what is written about normal forms (the second just points to a book (?) by Kleene, and the paper I found didn't have a bibliography).

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.

#3 Dan Doel am 2011-01-23

Here, the link http://www.jstor.org/stable/1989762 directly takes you to the paper, but maybe that is because I am on a university network (or I am misunderstanding your there).

#4 Joachim Breitner (Homepage) am 2011-01-23

Yes. I only get to view the first page of the paper as far as I can tell. To view more, I'd have to buy a subscription, or find some place that already has.

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

#5 Dan Doel am 2011-01-24

In your summary's section on Hilbert and Gödel, you write that "any consistent system has propositions which are neither true nor false within this system."

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.

#6 Benedict Eastaugh (Homepage) am 2011-01-23

Thanks for your suggestions, I made small some adjustments accordingly.

#7 Joachim Breitner (Homepage) am 2011-01-24

You missed one part of the definition of well-formed. K is not well-formed:

"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)

#8 Christian von Essen am 2011-01-23

Well spottet, and interesting. So in that system, the K combinator can not be defined as (λxy.x), and probably not at all. Thanks, I guess that clears it up.

#9 Joachim Breitner (Homepage) am 2011-01-23

That's right. It seems impossible to "forget" a term in their system. But I would consider both K and \Omega dirty bastards anyway :)

#10 Christian von Essen am 2011-01-23

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.

Go up