Kleene-Rosser paradox

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.Fact|date=January 2008 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

Defining the function $k\; =\; (lambda\; x.\; eg\; x\; x)$, one then may deduce

:$kk\; =\; (lambda\; x.\; eg\; x\; x)\; k\; =\; eg\; kk$

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. 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

:$p\; ightarrow\; eg\; p\; ightarrow\; eg\; eg\; p\; ightarrow\; eg\; eg\; eg\; p\; ightarrow\; cdots$

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.Fact|date=January 2008

ee also

* Richard paradox
* Curry's paradox
* Liar paradox

References

* Andrea Cantini, " [http://plato.stanford.edu/entries/paradoxes-contemporary-logic/ Paradoxes and Contemporary Logic] ", "Stanford Encyclopedia of Philosophy" (2007)