Kleene–Rosser paradox

This article may be more technical than it needs to be. It may require attention from an expert. Please make this article accessible to the widest possible audience. WikiProject Computer science or the Computer science Portal may be able to help recruit an expert on this topic. (August 2009)

In mathematics, the Kleene–Rosser paradox is a paradox that shows Church's original lambda calculus is inconsistent. It is similar to Russell's paradox, in that it is a statement that asserts its own falsehood if and only if it is true; that is, it is a self-negating statement. The paradox was developed by Stephen Kleene and J. B. Rosser in 1935, to show that the lambda calculus was inconsistent. The resolution of the paradox is the recognition that recursion is central and fundamental to the notion of computation. See self-reference (especially the sentences sub-section of the examples section there) for some examples about how recursion (which is an instance of, or an example of, self-reference) can lead to paradoxes.

The paradox

First we define the function ; this function applies its argument x to itself and then negates the result. For example, if one had a program P that converted arbitrary text to the output words "good" or "bad", the function k would first feed P to itself so that P would declare P itself "good" or "bad", and then negate this to the other value. If one applies this metafunction to itself, one then may deduce

and so this function, when combined with itself, negates itself.

Several solutions to avoid the paradox were proposed, including type theory or typed lambda calculus. However, most typed lambda calculi are not very expressive, indeed, are not Turing complete^{[citation needed]}. An alternate solution is to re-interpret lambda calculus not as a theory of logical assertions, but rather as a means of expressing computation. In this way, the paradox can be "solved" by reinterpreting it as a recursive statement, that is, the infinite recursion implying

where p = kk is the paradox. In this way, the inconsistency of lambda calculus is revealed to be a central and essential property of computation.^{[citation needed]}

See also

• Richard paradox
• Curry's paradox
• Liar paradox
• Girard's paradox

References

• Andrea Cantini, "The inconsistency of certain formal logics", in the Paradoxes and Contemporary Logic entry of Stanford Encyclopedia of Philosophy (2007)
• S.C. Kleene and J. B. Rosser, "The inconsistency of certain formal logics." Ann. of Math., 36:630–636, 1935.

This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.