The paradox requires 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, who wrote about it in 1942.
First, common natural-language proof techniques can be used to prove that the example sentence is true [steps 1–4 below].
Second, the truth of the sentence can be used to prove that Germany borders China [steps 5–6]: Because Germany does not border China, this suggests that there has been an error in one of the proof steps.
[3] 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".
in the usual way, by assuming the hypothesis and deriving the conclusion.
The example in the previous section used unformalized, natural-language reasoning.
Curry's paradox also occurs in some varieties of formal logic.
This together with Peirce's law ((X → Y) → X) → X and modus ponens implies X and subsequently Y (as in above proof).
The above derivation shows that, if Y is an unprovable statement in a formal system, then there is no statement X in that system such that X is equivalent to the implication (X → Y).
In other words, step 1 of the previous proof fails.
Even if the underlying mathematical logic does not admit any self-referential sentences, certain forms of naive set theory are still vulnerable to Curry's paradox.
In set theories that allow unrestricted comprehension, we can prove any logical statement Y by examining the set
Some proposals for set theory have attempted to deal with Russell's paradox not by restricting the rule of comprehension, but by restricting the rules of logic so that it tolerates the contradictory nature of the set of all sets that are not members of themselves.
Curry's paradox may be expressed in untyped lambda calculus, enriched by implicational propositional calculus.
To cope with the lambda calculus's syntactic restrictions,
shall denote the implication function taking two parameters, that is, the lambda term
, hence the above sentential logic proof can be duplicated in the calculus:[4][5][6]
Curry's paradox may also be expressed in combinatory logic, which has equivalent expressive power to lambda calculus.
Any lambda expression may be translated into combinatory logic, so a translation of the implementation of Curry's paradox in lambda calculus would suffice.
Curry's paradox can be formulated in any language supporting basic logic operations that also allows a self-recursive function to be constructed as an expression.
Two mechanisms that support the construction of the paradox are self-reference (the ability to refer to "this sentence" from within a sentence) and unrestricted comprehension in naive set theory.
Usually, the addition of metaprogramming capabilities to a language will add the features needed.
Mathematical logic generally does not allow explicit reference to its own sentences; however, the heart of Gödel's incompleteness theorems is the observation that a different form of self-reference can be added—see Gödel number.
In the 1930s, Curry's paradox and the related Kleene–Rosser paradox, from which Curry's paradox was developed,[8][1] played a major role in showing that various formal logic systems allowing self-recursive expressions are inconsistent.
The axiom of unrestricted comprehension is not supported by modern set theory, and Curry's paradox is thus avoided.