Concept

Curry's paradox

Curry's paradox is a paradox in which an arbitrary claim F is proved from the mere existence of a sentence C that says of itself "If C, then F", requiring only a few apparently innocuous logical deduction rules. Since F is arbitrary, any logic having these rules allows one to prove everything. The paradox may be expressed in natural language and in various logics, including certain forms of set theory, lambda calculus, and combinatory logic. The paradox is named after the logician Haskell Curry. It has also been called Löb's paradox after Martin Hugo Löb, due to its relationship to Löb's theorem. Claims of the form "if A, then B" are called conditional claims. Curry's paradox uses a particular kind of self-referential conditional sentence, as demonstrated in this example: Even though Germany does not border China, the example sentence certainly is a natural-language sentence, and so the truth of that sentence can be analyzed. The paradox follows from this analysis. The analysis consists of two steps. First, common natural-language proof techniques can be used to prove that the example sentence is true. Second, the truth of the example sentence can be used to prove that Germany borders China. Because Germany does not border China, this suggests that there has been an error in one of the proofs. The claim "Germany borders China" could be replaced by any other claim, and the sentence would still be provable. Thus every sentence appears to be provable. Because the proof uses only well-accepted methods of deduction, and because none of these methods appears to be incorrect, this situation is paradoxical. The standard method for proving conditional sentences (sentences of the form "if A, then B") is called "conditional proof". In this method, in order to prove "if A, then B", first A is assumed and then with that assumption B is shown to be true. To produce Curry's paradox, as described in the two steps above, apply this method to the sentence "if this sentence is true, then Germany borders China".

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Related lectures (1)
Philosophy of Mathematics: Ontology and Structures
Explores the existence of mathematical objects, truth of propositions, and knowledge about them, covering Platonism, Intuitionism, Structuralism, Nominalism, Logicism, and Formalism.
Related concepts (7)
Fixed-point combinator
In mathematics and computer science in general, a fixed point of a function is a value that is mapped to itself by the function. In combinatory logic for computer science, a fixed-point combinator (or fixpoint combinator) is a higher-order function that returns some fixed point of its argument function, if one exists. Formally, if the function f has one or more fixed points, then and hence, by repeated application, In the classical untyped lambda calculus, every function has a fixed point.
Lambda lifting
Lambda lifting is a meta-process that restructures a computer program so that functions are defined independently of each other in a global scope. An individual "lift" transforms a local function into a global function. It is a two step process, consisting of; Eliminating free variables in the function by adding parameters. Moving functions from a restricted scope to broader or global scope. The term "lambda lifting" was first introduced by Thomas Johnsson around 1982 and was historically considered as a mechanism for implementing functional programming languages.
Let expression
In computer science, a "let" expression associates a function definition with a restricted scope. The "let" expression may also be defined in mathematics, where it associates a Boolean condition with a restricted scope. The "let" expression may be considered as a lambda abstraction applied to a value. Within mathematics, a let expression may also be considered as a conjunction of expressions, within an existential quantifier which restricts the scope of the variable.
Show more

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.