Talk:Kleene–Rosser paradox

Resolution by Curry?

I don't know, but I presume that it was Haskell Curry, with his "don't run away from the paradox" attitude, that resolved the paradox by proposing its equivalence to recursion. linas 16:13, 15 November 2007 (UTC)

To answer my own question, it seems to be implied in the Stanford encyclopedia of philosophy that Curry did this in 1941 or 1942 in one or more essays, but no reference is given. linas 16:39, 15 November 2007 (UTC)

Comments

I had a very hard time following this; I think it's because of some notational and terminological issues. On one hand, the lambda calculus is not inconsistent; what Kleene and Rosser showed inconsistent was a formal logic the Church had proposed. This logic was not what is now called lambda calculus; $\lambda x(\lnot xx)$ is not an expression in pure lambda calculus.

I looked up the original paper by Kleene and Rosser and redid the article to match what I could find there and in the Stanford entry linked in the article. This resulted in this version which, while more clear to me has none of the flavor of the orignal.

This made me think that maybe there is some other source that is actually being used here, or maybe some other phenomenon than Kleene and Rosser's proof is being discussed. So I reverted my edits for the time being. But after reworking it, I still don't have a good sense of what the original version is trying to say. — Carl (CBM · talk) 19:16, 15 November 2007 (UTC)

I think this should be deleted, I think it's started by someone who doesn't really understand λc. As far as I know '¬' is not even an object in Λc. ¬ applies to truth values, lambda expressions aren't truth values. Sure, it's a convention to interpret Λyx.x as 'false', but that's just a convention and it's simply 'the constant function which returns the identity function for any input.', if '¬' here is defined as the standard NOT in lambda calculus then it's just infinite regress. Which is mainly the fault of defining a ridiculous function. Also, even if we could define a function in Λ which would lead to strange behaviour in λc, that doesn't make λc inconsistent, it just means we can define a function that does strange things. Saying 'Let 3 be 4...' doesn't make arithmetics inconsistent. Unless of course an axiom of lambda calculus is that no lambda expression equals its own negation. But to think of it, that can't even be so, because lambda expressions have no truth values to begin with. That a certain expression IS a lambda expression has a truth value.

I vote for removing this article and adjusting the other articles that claim that untyped lambda is inconsistent. Rajakhr (talk) 20:29, 24 December 2009 (UTC)

It doesn't compute

The article does no make any sense to me. What is " λ.x(¬xx)" supposed to mean? Is the intention λ x. ¬ x x? But this is a denotation for a function; if f is a function, what is the meaning of f ⇔ ¬ f supposed to be? Also, I don't see how one is "deduced" from the other. If Y is the paradoxical combinator, which is expressible in the untyped lambda calculus, then Y ¬ is interconvertible with ¬(Y ¬) – which, if ¬ is interpreted semantically as negation and interconvertibility as material equivalence, shows an inconsistency. I don't know, though, if this is the paradox found by Kleene & Rosser.  --Lambiam 19:29, 15 November 2007 (UTC)

I am also confused (see above). The original paper of Kleene and Rosser doesn't appear to explicitly use a fixed point, so this must be referring to something else. — Carl (CBM · talk) 19:55, 15 November 2007 (UTC)

Sorry, writing articles while waking up, while staring at scribbled notes made late at night when one is tired, is perhaps a bad idea. Especially when ones grasp of the subject matter is shaky and general knowledge superficial. Yes, its a combinator-ish thing. According to my notes, I should have written $K=(\lambda x.\neg xx)$ and so $KK=(\lambda x.\neg xx)K=\neg KK$. Since Church's attempts were to lay a foundation for mathematics and logic, the collection of valid symbols included negation, for-all, there-exists, etc in addition to just-plain lambda-binding of free variables. Rather than using equals signs, I should have written "implies", or "if and only if", thus the use of the double-sided arrow in the earlier draft. Yes, Y ¬ is essentially the same thing, where interconversion is interpreted to mean "if ... then ..." so that "if Y ¬ then ¬(Y ¬)" is the paradox. I presume, then, that this is Curry's true contribution to elucidating the connection to recursive functions. I did not get the impression that this was ever written up in a paper; rather Kleene and Rosser were both grad students of his, and that this simply came up during thier studies. I don't know. There were appearently various repairs made to the original system to avoid this paradox, including the elimination of some of the axioms; supposedly this was disheartening enough that Church abandoned further attempts to formalize mathematics. I'm skimming the surface of a topic I'm mostly unfamiliar with. linas 05:43, 16 November 2007 (UTC)

The "other sources" are multiple library books. I have access to a very good library. I have a goal of reading and understanding the first five pages of every book in there :-) Which explains my scattered contributions on WP. linas 05:49, 16 November 2007 (UTC)

Yes, and although Russell's paradox is strictly about set theory, I'd also been recently reading about topology and lattices and heyting algebras and order theory, where there are a lot of similar concepts and constructions, and so when I saw this, I had a big a-ha moment, vaguely naively along the lines of "for every non-halting turing machine there exists an equivalent paradox in naive set theory, and v.v.". I suppose that's just naive unprovable speculation/inspiration, but it still seems to somehow hook up order theory notions e.g. from ontology, to computable things. OK, that's poetry, I guess. Goodnight. linas 06:12, 16 November 2007 (UTC)

I think my comments above got missed. Kleene and Rosser did write a paper, and their actual result is not similar to what is here. I wrote up a stub about their result here. I would appreciate it if you could add some sources to this stub, because I can't clean it up until I find some reference that says what this "paradox" is supposed to be. — Carl (CBM · talk) 12:55, 16 November 2007 (UTC)

OK. I'll hit the library this weekend or early next week. What I saw was rather thin, a short discussion in an intro chapter. Googling reveals two different things called Kleene-Rosser paradox, one of the form kk=~kk and another being the 1935 paper which is summarized as "a demonstraction that Richard's paradox applies to Churches logic". Google is very thin on this. Some urls:

In support of "KR paradox is kk=~kk":

• http://nnw.berlios.de/docs.php/introftk44 -- someone's class notes
• http://www.cs.uvm.edu/~skalka/skalka-pubs/pres-paradox.pdf -- Skalka, math prof, lecture charts

In support of "KR paradox is thier 1935 paper":

• http://de.scientificcommons.org/932226 -- Bunder, throughly opaque.

Other:

• http://www3.unifi.it/dpfilo/upload/sub/Didattica/Minari/History_2.pdf -- calls ~Y=~Y~ "curry's paradox", and the enumeration over naturals "richards paradox".

linas 16:01, 16 November 2007 (UTC)

Thanks for finding some references; I would really like to clean this up, since if Lambiam and I are confused then probably the intended reader is even more confused. We also need to distinguish between lambda calculus, which is consistent, and Church's formal system, which is inconsistent. Church's system is a formal logic that includes some aspects of lambda calculus along with other aspects of logic.

In 1935, Kleene and Rosser just showed that Church's particular formal system is inconsistent. Since there are lots of inconsistent formal systems it's not surprising to find some occasionally. So I don't see that there is any actual 'paradox'. I hope that the references will clarify exactly what is supposed to be paradoxical about their result. — Carl (CBM · talk) 16:08, 16 November 2007 (UTC)

I guess I don't understand what you want. I've now seen Y called the paradoxical combinator in several texts. I got the impression that perhaps Curry himself called it that. I've seen several books and articles now that make it clear that Curry was drawn to the paradoxes. The result Y~=~Y~ seems paradoxical, don't you agree? The Bunder reference above explicitly calls the results of the 1935 KR paper "the KR paradox", and does so in the title. All I'd seen was a breif discussion about formal systems in the intro/preface, with a presentation no deeper than this article, (surely with a different and more elegant nuance), with the words "kleen-rosser", "paradox" and kk=~kk in proximity. Perhaps there was a deeper discussion further in the book, perhaps not. A few minutes in the library leafing through indexes will solve this. But given that kk=~kk is extremely similar to Russell's paradox, I can't much carry on if you don't think there's anything much "paradoxical" about it. linas (talk) 13:54, 17 November 2007 (UTC)

I'm not familiar with the literature about the "Kleene-Church paradox" so I need to review it to learn about the issue. If the standard terminology is 'paradox', I'll go with it in the article, but I can explain what I meant.

On its own, "kk = ~kk" is just a string of 8 symbols. Only when you try to apply some semantics can it appear paradoxical. The problem is that the semantics that Church developed are inconsistent. If I use an invalid algebraic method and derive "0 = 1", that doesn't make the equation a paradox, it just shows that I used an invalid method. So I prefer to limit the word 'paradox' to actual paradoxes in natural language, for example the question about the set of all sets that don't contain themselves, or Curry's paradox in natural language. When natural language paradoxes are formalized, invariably one of two things happens: (1) the formal system is inconsistent, in which case it's hard to claim the result is paradoxical or (2) the paradox no longer arises. Classic examples of this are the paradoxes of naive set theory and Lowenheim's 'paradox' about countable models.

In short, I like to be more conservative with the word 'paradox' than other authors. — Carl (CBM · talk) 14:26, 17 November 2007 (UTC)

The thing is not reviewed in Barendregt's book "Lambda calculus", or, at least, its not in the index.

The paradox, to me, is precisely that the thing is so minimal: "kk=~kk" requires two "axioms" (I'm not sure if the word "axiom" is appropriate here), and a linguistic gloss or two: the axiom of "apply" (lambda application), linguisticaly interpreted as "if the previous formula is true, then the result of apply is true". A second axiom is that formulas can be either true or false, and a third axiom is the admission of ~ as a valid symbol, denoting "not". So the ingredients to the paradox are quite minimal -- In particular, note that there is no appeal to "there exists", "for each", "is an element of", "and", "or", etc. The vocabulary is very small. The paradox lies in the linguistic gloss: The statement "kk" is neither true, nor is it false. Its indeterminate. Thus, since "kk" was neither true nor false, then "~kk" is neither false nor true, and so "kk=~kk" isn't really a contradication of any sort at all. It just looks like one, if one makes the mental slip, the mental error of beleiving that "kk" evaluates to T or F. It does not. This is why the rephrasing as a recursive function is the "solution" to the paradox: the recursion provides a semantics for the thing which is "consistent". (Similar remark apply to Y~=~Y~ : because Y does not (cannot) evaluate to T or F, there is nothing "wrong" with Y~=~Y~; it is only the erroneous use of natural language that makes it seem contradictory. The correct use is to say that "Y implies recursion".)

The thing that has me stumped is this: is there any way of "axiomatizing" or "formalizing" the statement "Y implies recursion"? Perhaps Barendregt's book will inform ... linas (talk) 15:55, 19 November 2007 (UTC)

It can only be a paradox if there is a notion of semantics and truth involved. If I say "@@", there is no paradox. If this is a theorem in some formal system, there is still no paradox. If you additionally know that the semantic interpretation of "@F", where the interpretation F of "F" is a predicate, is the same as of what is more conventionally written as ∀x:F(x), with α-conversion as needed, we get that the interpretation of "@@" is ∀P:@(P) = ∀P:∀x:P(x). This is an inconsistency, not a paradox. Only when it is agreed that the axioms and inference rules of the formal system appear quite sound when interpreted semantically do we get a paradox. Most of the ingredients needed to make the rewriting of "kk" to "~kk" a paradox are missing (in the sense of not having been supplied).

In many programming languages you can give a definition like "define f(x) = not(f(x))". This is really similar to adding an axiom to a possibly consistent system for a new symbol "f", stating that ∀x:(f(x)⇔¬f(x)). This obviously makes the system inconsistent, but does not create a paradox. Under any reasonable semantics for such programming languages the "definition" does not actually define "f", except possibly as the everywhere undefined function.

Our article on fixed point combinators assumes, unfortunately and without justification, immediately a computational interpretation of the lambda calculus. It is not a coincidence that I used the section title "It doesn't compute". If you use a computational interpretation, then guaranteed termination is related to the normalization property, which a lambda calculus may or may not have. If it has the property (like the simply-typed lambda calculus), you cannot express any of the fixed-point combinators, and also not your "k".

In summary, without a logical system that appeared sound – but wasn't – there is no paradox. It is possible that K & R first gave a complicated construction exhibiting an inconsistency, while Church later found a much simpler construction using "k".  --Lambiam 20:11, 19 November 2007 (UTC)

OK, point taken, I don't really have a semantic interpretation for what k is supposed to be. I'll try to dig up stronger material for all this, but I do not have high hopes; what I've seen was cursory, and I don't particularly want to engage in original research in the history of mathematics. Again, I have only a shallow acquaintance with the field, I presume that @@ is a standard textbook example, but its refreshingly new to me :-) Perhaps Prof. Skalka, author cited above, can be recruited to sort out the muddle. linas (talk) 05:27, 20 November 2007 (UTC)

I just came up with @@ on the spot to illustrate the point.  --Lambiam 14:16, 20 November 2007 (UTC)

Skalka is an associate professor of computer science, and has no specific background in logic that I can discern. You might consider asking assistance from Wikipedians who are professional mathematical logicians, such as User:Hans Adler.  --Lambiam 15:34, 20 November 2007 (UTC)

There's also Trovatore, Arthur Rubin, me, and others. The problem is that this is a relatively obscure topic in contemporary mathematical logic. So it might take some luck to find a person with an immediate working knowledge of it. The original paper by Kleene and Rosser is easy enough to read but doesn't contain the info being presented here. — Carl (CBM · talk) 16:06, 20 November 2007 (UTC)

Um... Since when are computer scientists specializing in theory of computation and programming languages not qualified to discuss the Lambda calculus? Ever heard of the Curry-Howard isomorphism (to quote Wikipedia's article: "the direct relationship between computer programs and mathematical proofs")?!! 65.183.135.231 (talk) 19:51, 4 February 2009 (UTC)

My understanding of this is that k is to be interpreted as a propositional function, or equivalently as the set of terms that it is true for. With this interpretation, \x.-(x x) is essentially interpreted as "the set of all sets that don't contain themselves," which is Russell's Paradox in this system. k k is interpreted as "k contains itself" and -(k k) is interpreted as "k does not contain itself," which is the paradox. —Preceding unsigned comment added by 69.120.140.170 (talk) 20:56, 14 July 2008 (UTC)

I don't understand the problem here. It is an infinite function. When you ask a question and get infinity, it's because you asked the wrong question.. You can't just evaluate kk because it is infinity recursive. —Preceding unsigned comment added by 207.207.126.249 (talk) 05:30, 11 February 2009 (UTC)

Explanation

If you read this, and know how to explain this paradox, please edit this page and help others understand it, because it is using symbols which go without a prepared explanation of use. Please avoid symbols altogether in an explanation, unless they are specifically explained themselves. —Preceding unsigned comment added by 70.171.37.195 (talk) 13:28, 20 March 2009 (UTC)

ugly!

I am not a dumb in mathematics, but I do not know nothing about \lambda-calculus. The written "kk+ etc..." sounds incomprehensible... why x and double x? why the point? I think the author of the page should reconsider rewritting it. —Preceding unsigned comment added by 160.103.2.224 (talk) 17:25, 25 November 2009 (UTC)

Clarify Syntax

The symbols in "k = (lambda x . not(xx))" need to be clarified.

What does lambda mean?

What does dot mean?

What does xx mean? It's obviously not x squared in this context.

—Preceding unsigned comment added by 129.174.190.101 (talk) 02:07, 2 March 2011 (UTC)