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". 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.^[1] It has also been called Löb's paradox after Martin Hugo Löb,^[2] due to its relationship to Löb's theorem.

In natural language

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:

If this sentence is true, then Germany borders China.

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 [steps 1–4 below]. Second, the truth of the sentence can be used to prove that Germany borders China [steps 5–6]:

The sentence reads "If this sentence is true, then Germany borders China" [repeat definition to get step numbering compatible to the formal proof]
If the sentence is true, then it is true. [obvious, i.e., a tautology]
If the sentence is true, then: if the sentence is true, then Germany borders China. [replace "it is true" by the sentence's definition]
If the sentence is true, then Germany borders China. [contract repeated condition]
But 4. is what the sentence says, so it is indeed true.
The sentence is true [by 5.], and [by 4.]: if it is true, then Germany borders China.
So, Germany borders China. [modus ponens]

Because Germany does not border China, this suggests that there has been an error in one of the proof steps. 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.^[3]

Informal proof

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". Here A, "this sentence is true", refers to the overall sentence, while B is "Germany borders China". So, assuming A is the same as assuming "If A, then B". Therefore, in assuming A, we have assumed both A and "If A, then B". Therefore, B is true, by modus ponens, and we have proven "If this sentence is true, then 'Germany borders China' is true." in the usual way, by assuming the hypothesis and deriving the conclusion.

Now, because we have proved "If this sentence is true, then 'Germany borders China' is true", then we can again apply modus ponens, because we know that the claim "this sentence is true" is correct. In this way, we can deduce that Germany borders China.

In formal logics

Sentential logic

The example in the previous section used unformalized, natural-language reasoning. Curry's paradox also occurs in some varieties of formal logic. In this context, it shows that if we assume there is a formal sentence (X → Y), where X itself is equivalent to (X → Y), then we can prove Y with a formal proof. One example of such a formal proof is as follows. For an explanation of the logic notation used in this section, refer to the list of logic symbols.

X := (X → Y)
assumption, the starting point, equivalent to "If this sentence is true, then Y"
X → X
law of identity
X → (X → Y)
substitute right side of 2, since X is equivalent to X → Y by 1
X → Y
from 3 by contraction
X
substitute 4, by 1
Y
from 5 and 4 by modus ponens

An alternative proof is via Peirce's law. If X = X → Y, then (X → Y) → X. 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. By contrast, the previous section shows that in natural (unformalized) language, for every natural language statement Y there is a natural language statement Z such that Z is equivalent to (Z → Y) in natural language. Namely, Z is "If this sentence is true then Y".

Naive set theory

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 $X\ {\stackrel {\mathrm {def} }{=}}\ \left\{x\mid (x\in x)\to Y\right\}.$ One then shows easily that the statement $X\in X$ is equivalent to $(X\in X)\to Y$ . From this, $Y$ may be deduced, similarly to the proofs shown above. (" $X\in X$ " stands for "this sentence".)

Therefore, in a consistent set theory, the set $\left\{x\mid (x\in x)\to Y\right\}$ does not exist for false Y. This can be seen as a variant on Russell's paradox, but is not identical. 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. The existence of proofs like the one above shows that such a task is not so simple, because at least one of the deduction rules used in the proof above must be omitted or restricted.

Lambda calculus with restricted minimal logic

Curry's paradox may be expressed in untyped lambda calculus, enriched by implicational propositional calculus. To cope with the lambda calculus's syntactic restrictions, $m$ shall denote the implication function taking two parameters, that is, the lambda term $((mA)B)$ shall be equivalent to the usual infix notation $A\to B$ .

An arbitrary formula $Z$ can be proved by defining a lambda function $N:=\lambda p.((mp)Z)$ , and $X:=({\textsf {Y}}N)$ , where ${\textsf {Y}}$ denotes Curry's fixed-point combinator. Then $X=(NX)=((mX)Z)$ by definition of ${\textsf {Y}}$ and $N$ , hence the above sentential logic proof can be duplicated in the calculus:^[4]^[5]^[6]

${\begin{array}{cll}\vdash &((mX)X)&{\mbox{ by the minimal logic axiom }}A\to A\\\vdash &((mX)((mX)Z))&{\mbox{ since }}X=((mX)Z)\\\vdash &((mX)Z)&{\mbox{ by the theorem }}(A\to (A\to B))\vdash (A\to B){\mbox{ of minimal logic }}\\\vdash &X&{\mbox{ since }}X=((mX)Z)\\\vdash &Z&{\mbox{ by modus ponens }}A,(A\to B)\vdash B{\mbox{ from }}X{\mbox{ and }}((mX)Z)\\\end{array}}$

In simply typed lambda calculus, fixed-point combinators cannot be typed and hence are not admitted.

Combinatory logic

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.

The above term $X$ translates to $(r\ r)$ in combinatory logic, where $r={\textsf {S}}\ ({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))\ ({\textsf {K}}Z);$ hence^[7] $(r\ r)=((m(rr))\ Z).$

Discussion

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. Natural languages nearly always contain many features that could be used to construct the paradox, as do many other languages. 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.

The rules used in the construction of the proof are the rule of assumption for conditional proof, the rule of contraction, and modus ponens. These are included in most common logical systems, such as first-order logic.

Consequences for some formal logic

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.

References

^ ^a ^b Curry, Haskell B. (Sep 1942). "The Inconsistency of Certain Formal Logics". The Journal of Symbolic Logic. 7 (3): 115–117. doi:10.2307/2269292. JSTOR 2269292. S2CID 121991184.
^ Barwise, Jon; Etchemendy, John (1987). The Liar: An Essay on Truth and Circularity. New York: Oxford University Press. p. 23. ISBN 0195059441. Retrieved 24 January 2013.
^ A parallel example is explained in the Stanford Encyclopedia of Philosophy. See Shapiro, Lionel; Beall, Jc (2018). "Curry's Paradox". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
^ The naming here follows the sentential logic proof, except that "Z" is used instead of "Y" to avoid confusion with Curry's fixed-point combinator ${\textsf {Y}}$ .
^ Gérard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Marktoberdorf. Archived from the original on 2014-07-14.{{cite book}}: CS1 maint: location missing publisher (link) Here: p.125
^ Haskell B. Curry; Robert Feys (1958). Combinatory Logic I. Studies in Logic and the Foundations of Mathematics. Vol. 22. Amsterdem: North Holland.^{[page needed]}
^ $(rr)$ $=$ $({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))$ $\to$ $({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}})({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {K}}Z({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))$ $\to$ $({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}})({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))Z)$ $\to$ $({\textsf {K}}m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $\to$ $(m({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $\to$ $(m({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))Z)$ $\to$ $(m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))Z)$ $\to$ $(m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $=$ $((m(rr))\ Z)$
^ Curry, Haskell B. (Jun 1942). "The Combinatory Foundations of Mathematical Logic". Journal of Symbolic Logic. 7 (2): 49–64. doi:10.2307/2266302. JSTOR 2266302. S2CID 36344702.