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.
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:
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 a "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.
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
- X → (X → Y)substitute right side of 2, since X is equivalent to X → Y by 1
- X → Yfrom 3 by contraction
- Xsubstitute 4, by 1
- Yfrom 5 and 4 by modus ponens
Therefore, if Y is an unprovable statement in a formal system, there is no statement X in that system such that X is equivalent to the implication (X → Y). 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".
In specific cases where the classification of Y is already known, few steps are needed to reveal the contradiction. For example, when Y is "Germany borders China," it is known that Y is false.
- X = (X → Y)assumption
- X = (X → false)substitute known value of Y
- X = (¬X ∨ false)
- X = ¬Xidentity
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 nevertheless prove any logical statement Y by examining the set
Assuming that takes precedence over both and , the proof proceeds as follows:
- Definition of X
- Substitution of equal sets in membership
- Addition of a consequent to both sides of a biconditional (from 2)
- Law of concretion (from 1 and 3)
- Biconditional elimination (from 4)
- Contraction (from 5)
- Biconditional elimination (from 4)
- Modus ponens (from 6 and 7)
- Modus ponens (from 8 and 6)
Step 4 is the only step invalid in a consistent set theory. In Zermelo–Fraenkel set theory, an extra hypothesis stating X is a set would be required, which is not provable in ZF or in its extension ZFC (with the axiom of choice).
Therefore, in a consistent set theory, the set 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.
Curry's paradox may be expressed in untyped lambda calculus, enriched by restricted minimal logic. To cope with the lambda calculus's syntactic restrictions, shall denote the implication function taking two parameters, that is, the lambda term shall be equivalent to the usual infix notation .
An arbitrary formula can be proved by defining a lambda function , and , where denotes Curry's fixed-point combinator. Then by definition of and , hence the above sentential logic proof can be duplicated in the calculus:
In simply typed lambda calculus, fixed-point combinators cannot be typed and hence are not admitted.
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 translates to in combinatory logic, where
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 of features that could be used to construct the paradox, as do many other languages. Usually the addition of meta programming 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 axiom of unrestricted comprehension adds the ability to construct a recursive definition in set theory. This axiom is not supported by modern set theory.
The logic rules used in the construction of the proof are rule of assumption for conditional proof, the rule of contraction, and modus ponens. These are included in the 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 played a major role in showing that formal logic systems based on self-recursive expressions are inconsistent. These include some versions of lambda calculus and combinatory logic.
Curry began with the Kleene–Rosser paradox and deduced that the core problem could be expressed in this simpler Curry's paradox. His conclusion may be stated as saying that combinatory logic and lambda calculus cannot be made consistent as deductive languages, while still allowing recursion.
In the study of illative (deductive) combinatory logic, Curry in 1941 recognized the implication of the paradox as implying that, without restrictions, the following properties of a combinatory logic are incompatible:
- Combinatorial completeness. This means that an abstraction operator is definable (or primitive) in the system, which is a requirement on the expressive power of the system.
- Deductive completeness. This is a requirement on derivability, namely, the principle that in a formal system with material implication and modus ponens, if Y is provable from the hypothesis X, then there is also a proof of X → Y.
This section does not cite any sources. (August 2019) (Learn how and when to remove this template message)
This section's factual accuracy is disputed. (August 2019) (Learn how and when to remove this template message)
Note that unlike the liar paradox or Russell's paradox, Curry's paradox does not depend on what model of negation is used, as it is completely negation-free. Thus paraconsistent logics can still be vulnerable to this paradox, even if they are immune to the liar paradox.
No resolution in lambda calculus
This definition is valid if there is one and only one function that satisfies the equation , but invalid otherwise. This is the core of the problem that Stephen Cole Kleene and then Haskell Curry discovered with combinatory logic and Lambda calculus.
The situation may be compared to defining
This definition is fine as long as only positive values are allowed for the square root. In mathematics an existentially quantified variable may represent multiple values, but only one at a time. Existential quantification is the disjunction of many instances of an equation. In each equation is one value for the variable.
However, in mathematics, an expression with no free variables must have one and only one value. So can only represent . However there is no convenient way to restrict the lambda abstraction to one value or to assure that there is a value.
Lambda calculus allows recursion by passing the same function that is called as a parameter. This allows situations where has multiple or no solutions for .
Lambda calculus may be considered as part of mathematics if only lambda abstractions that represent a single solution to an equation are allowed. Other lambda abstractions are incorrect in mathematics.
Domain of lambda calculus terms
Lambda calculus is a consistent theory in its own domain. However, it is not consistent to add the lambda abstraction definition to general mathematics. Lambda terms describe values from the lambda calculus domain. Each lambda term has a value in that domain.
When translating expressions from mathematics to lambda calculus, the domain of lambda calculus terms is not always isomorphic to the domain of the mathematical expressions. This lack of isomorphism is the source of the apparent contradictions.
Resolution in unrestricted languages
There are many language constructs that implicitly invoke an equation that may have none or many solutions. The sound resolution to this problem is to syntactically link these expressions to an existentially quantified variable. The variable represents the multiple values in a way that is meaningful in common human reasoning, but is also valid in mathematics.
For example, a natural language that allows the Eval function is not mathematically consistent. But each call to Eval in that natural language may be translated into mathematics in a way that is consistent. The translation of Eval(s) into mathematics is
So where s = "Eval(s) → y",
If y is false, then the x = x → y is false, but this is a falsehood, not a paradox.
The existence of the variable x was implicit in the natural language. The variable x is created when the natural language is translated into mathematics. This allows us to use natural language, with natural semantics, while maintaining mathematical integrity.
Resolution in formal logic
The argument in formal logic starts with assuming the validity of naming (X → Y) as X. However, this is not a valid starting point. First we must deduce the validity of the naming. The following theorem is easily proved and represents such a naming:
In the above statement the formula A is named as X. Now attempt to instantiate the formula with (X → Y) for A. However, this is not possible, as the scope of is inside the scope of . The order of the quantifiers may be reversed using Skolemization:
However, now instantiation gives
which is not the starting point for the proof and does not lead to a contradiction. There are no other instantiations for A that lead to the starting point of the paradox.
Resolution in set theory
In Zermelo–Fraenkel set theory (ZFC), the axiom of unrestricted comprehension is replaced with a group of axioms that allow construction of sets. So Curry's paradox cannot be stated in ZFC. ZFC evolved in response to Russell's paradox.
- Russell's paradox
- Girard's paradox
- Kleene–Rosser paradox
- Liar paradox
- List of paradoxes
- Richard's paradox
- Zermelo–Fraenkel set theory
- Fixed-point combinator
- Deductive lambda calculus
- Let expression
- 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 .
- Gérard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Marktoberdorf. Here: p.125
- Haskell B. Curry; Robert Feys (1958). Combinatory Logic I. Studies in Logic and the Foundations of Mathematics. 22. Amsterdem: North Holland.[page needed]
- Kleene, S. C. & Rosser, J. B. (1935). "The inconsistency of certain formal logics". Annals of Mathematics. 36 (3): 630–636. doi:10.2307/1968646.
- Curry, Haskell B. (Jun 1942). "The Combinatory Foundations of Mathematical Logic". Journal of Symbolic Logic. 7 (2): 49–64. JSTOR 2266302.
- 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.
- Curry, Haskell B. (1941). "The Paradox of Kleene and Rosser". Transactions of the American Mathematical Society. 50 (3): 454–516. doi:10.1090/S0002-9947-1941-0005275-6. MR 0005275. Retrieved 24 January 2013.
- Stenlund, Sören (1972). Combinators, λ-terms, and Proof Theory. Dordrecht: D. Reidel. p. 71. ISBN 978-9027703057.
- Beall, J. C. "Curry's paradox". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
- Cantini, Andrea. "Paradoxes and Contemporary Logic". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
- Penguins Rule the Universe: A Proof that Penguins Rule the Universe, a brief and entertaining discussion of Curry's paradox.