https://lawrencecpaulson.github.io/2024/01/31/Russells_Paradox.html

[utterances-bot]

Russell's Paradox: Myth and Fact

https://lawrencecpaulson.github.io/2024/01/31/Russells_Paradox.html

[Ian-Grant]

Hi Larry, I haven't read this in detail, but I'm sure it's all right.

I want you to see this blog post of mine and read it all carefully, and watch all of the videos, and then respond to the question at the end. This message is just to let you know that I mean this in all seriousness. I cannot do all this on my own on unemployment benefit, living ina studio in Harrow. I would be more than happy to come up to Cambridge and talk to you and anyone else in person and in confidence.

https://eternaldoorman.blogspot.com/2024/02/david-turner-obituary-by-sarah-nicholas.html

Best wishes Ian Grant

PS You can also contact me on fastmail if you prefer, Markus Kuhn has my e-mail address.

[phlegmaticprogrammer]

That is a very nice and concise description of why Church's lambda calculus is inconsistent, when considered as a logic. Do you have a pointer to a paper or book where it is described like that? I have seen the various original papers, but they use old-fashioned notation and are generally hard to read.

[lawrencecpaulson]

I'm afraid I no longer recall where I learned about this. But I bet there's something about it in Barendregt's volume The Lambda Calculus: Its Syntax and Semantics.

[Ian-Grant]

I'm afraid I no longer recall where I learned about this. But I bet there's something about it in Barendregt's volume The Lambda Calculus: Its Syntax and Semantics.

From: The Impact of the Lambda Calculus in Logic and Computer Science in The Bulletin of Symbolic Logic, Vol. 3, No. 2 (Jun., 1997), pp. 181-215 (35 pages) by Henk Barendregt. [https://www.jstor.org/stable/421013]

From Section 2 on page 185:

Church introduced a formal theory, let us call it T, based on the notion of function. This system was intended to be a foundation of mathematics. Predicates were represented by characteristic functions. There were many axioms to deal with logical notions.

The system T turned out to be inconsistent, as was shown by Church's students Kleene and Rosser in [71] using a tour de force argument involving all the techniques needed to prove Godel's incompleteness theorem.

Then Church [28] isolated the lambda calculus from the system T by deleting the part dealing with logic and keeping the essence of the part dealing with functions. This was proved consistent by Church and Rosser [31], who showed the confluence of beta-reductions. Curry, who also wanted to build a foundation for mathematics based on functions (in his case in the form of combinators that do not mention free or bound variables), found a paradox for a system with a similar aim as T, that is very easy to derive, see e.g., [6, Appendix B]

Reference 31 is to: A. Church and J. B. Rosser, Some properties of conversion, Transactions of the American Mathematical Society, vol. 39 (1936), pp. 472-482.

Reference 71 is to: The Inconsistency of Certain Formal Logics by S. C. Kleene, J. B. Rosser. Annals of Mathematics, Vol. 36, No. 3 (Jul., 1935), pp. 630-636 (7 pages) [https://www.jstor.org/stable/1968646]

Reference 28 ia to An Unsolvable Problem of Elementary Number Theory by Alonzo Church [https://www.jstor.org/stable/2371045]

Footnote 19 If this interpretation or some similar one is not allowed, it is difficult to see how the notion of an algorithm can be given any exact meaning at all.

Reference 6 is to: H. P. Barendregt, The lambda calculus: its syntax and semantics, revised ed., North- Holland, Amsterdam, 1984.

Hope this helps!

[Ian-Grant]

I don't have immediate access to a copy of Barendregt's encyclopedia, but Appendix B is on Illitiave Combinatory Logic: https://encyclopediaofmath.org/wiki/Illative_combinatory_logic