Curry's paradox
Encyclopedia
Curry's paradox is a paradox
that occurs in naive set theory
or naive logic
s, and allows the derivation of an arbitrary sentence from a self-referring sentence and some apparently innocuous logical deduction rules. It is named after the logician Haskell Curry
.
It has also been called Löb's paradox after Martin Hugo Löb.
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. 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. Worse, 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.
Assume A is true. Because A refers to the overall sentence, therefore assuming A is true is the same as assuming that the statement "If A then B" is also true. Because A is true, therefore B is true. Assuming A is true is therefore enough to guarantee that B is true regardless of the truth of statement B.
to show that B is true; but this is impossible, because B is "Germany borders China", which is false.
. 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.
1. X → X
2. X → (X → Y)
3. X → Y
4. X
5. Y
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".
, we can nevertheless prove any logical statement Y by examining the set
The proof proceeds as follows:
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 in 1941 recognized the implication of the paradox as implying that, without restrictions, the following properties of a combinatory logic are incompatible:
(i) 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.
(ii) 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.
Various other sets of conditions are also possible. Natural languages nearly always contain all these features. Mathematical logic, on the other hand, generally does not countenance explicit reference to its own sentences, although the heart of Gödel's incompleteness theorems
is the observation that usually this can be done anyway; see Gödel number
. The truth-predicate is generally not available, but in naive set theory, this is arrived at through the unrestricted rule of comprehension. The rule of contraction is generally accepted, although linear logic
(more precisely, linear logic without the exponential operators) does not admit the reasoning required for this paradox.
Note that unlike the liar paradox or Russell's paradox, this 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, even if they are immune to the liar paradox.
The resolution of Curry's paradox is a contentious issue because resolutions (apart from trivial ones such as disallowing X directly) are difficult and not intuitive. Logicians are undecided whether such sentences are somehow impermissible (and if so, how to banish them), or meaningless, or whether they are correct and reveal problems with the concept of truth itself (and if so, whether we should reject the concept of truth, or change it), or whether they can be rendered benign by a suitable account of their meanings.
Linear logic
disallows contraction and so does not admit this paradox directly, but one must remove its exponential operators, or else the paradox reappears in a modal form.
Paradox
Similar to Circular reasoning, A paradox is a seemingly true statement or group of statements that lead to a contradiction or a situation which seems to defy logic or intuition...
that occurs in naive set theory
Naive set theory
Naive set theory is one of several theories of sets used in the discussion of the foundations of mathematics. The informal content of this naive set theory supports both the aspects of mathematical sets familiar in discrete mathematics , and the everyday usage of set theory concepts in most...
or naive logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
s, and allows the derivation of an arbitrary sentence from a self-referring sentence and some apparently innocuous logical deduction rules. It is named after the logician Haskell Curry
Haskell Curry
Haskell Brooks Curry was an American mathematician and logician. Curry is best known for his work in combinatory logic; while the initial concept of combinatory logic was based on a single paper by Moses Schönfinkel, much of the development was done by Curry. Curry is also known for Curry's...
.
It has also been called Löb's paradox after Martin Hugo Löb.
Natural language
Claims of the form "if A, then B" are called conditionalIndicative conditional
In natural languages, an indicative conditional is the logical operation given by statements of the form "If A then B". Unlike the material conditional, an indicative conditional does not have a stipulated definition...
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. 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. Worse, 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.
Proof that the sentence is true
The following analysis is used to show that the sentence "If this sentence is true, then Germany borders China" is itself true. The quoted sentence is of the form "If A then B" where A refers to the sentence itself and B refers to "Germany borders China". Within the naïve logic that Curry was working on, the method for proving a conditional sentence is to assume that the hypothesis (A) is true, and then prove from that assumption that the conclusion (B) is true.Assume A is true. Because A refers to the overall sentence, therefore assuming A is true is the same as assuming that the statement "If A then B" is also true. Because A is true, therefore B is true. Assuming A is true is therefore enough to guarantee that B is true regardless of the truth of statement B.
The paradox
In a naïve logic, the sentence itself, denoted A, is true. The sentence is of the form "If A then B". Since A is true, therefore "If A then B" is true. We then apply modus ponensModus ponens
In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
to show that B is true; but this is impossible, because B is "Germany borders China", which is false.
Formal logic
The example in the previous section used unformalized, natural-language reasoning. Curry's paradox also occurs in formal logicFormal logic
Classical or traditional system of determining the validity or invalidity of a conclusion deduced from two or more statements...
. 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.
1. X → X
- rule of assumptionNatural deductionIn logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
, also called restatement of premise or of hypothesis
2. X → (X → Y)
- substitute right side of 1, since X is equivalent to X → Y by assumption
3. X → Y
- from 2 by contraction
4. X
- substitute 3, since X = X → Y
5. Y
- from 4 and 3 by modus ponensModus ponensIn classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
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".
Naive set theory
Even if the underlying mathematical logic does not admit any self-referential sentence, in set theories which allow unrestricted comprehensionAxiom schema of specification
In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom schema of specification, axiom schema of separation, subset axiom scheme or axiom schema of restricted comprehension, is a schema of axioms in Zermelo-Fraenkel set theory...
, we can nevertheless prove any logical statement Y by examining the set
The proof proceeds as follows:
-
- Definition of X
-
- from 1
-
- from 2, contraction
-
- from 1
-
- from 3 and 4, modus ponens
-
- from 3 and 5, modus ponens
Therefore, in a consistent set theory, the set
does not exist for false Y. This can be seen as a variant on Russell's paradoxRussell's paradox
In the foundations of mathematics, Russell's paradox , discovered by Bertrand Russell in 1901, showed that the naive set theory created by Georg Cantor leads to a contradiction...
, but is not identical. Some proposals for set theory have attempted to deal with Russell's paradox
Russell's paradox
In the foundations of mathematics, Russell's paradox , discovered by Bertrand Russell in 1901, showed that the naive set theory created by Georg Cantor leads to a contradiction...
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.
Combinatory logic
In the study of illative combinatory logicCombinatory logic
Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...
, Curry in 1941 recognized the implication of the paradox as implying that, without restrictions, the following properties of a combinatory logic are incompatible:
(i) 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.
(ii) 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.
Discussion
Curry's paradox can be formulated in any language meeting certain conditions:- The language must contain an apparatus which lets it refer to, and talk about, its own sentences (such as quotation marks, names, or expressions like "this sentence");
- The language must contain its own truthTruthTruth has a variety of meanings, such as the state of being in accord with fact or reality. It can also mean having fidelity to an original or to a standard or ideal. In a common usage, it also means constancy or sincerity in action or character...
-predicate: that is, the language, call it "L", must contain a predicate meaning "true-in-L", and the ability to ascribe this predicate to any sentences; - The language must admit the rule of contraction, which roughly speaking means that a relevant hypothesis may be reused as many times as necessary; and
- The language must admit the rules of identityLaw of identityIn logic, the law of identity is the first of the so-called three classic laws of thought. It states that an object is the same as itself: A → A ; While this can also be listed as A ≡ A this is redundant Any reflexive relation upholds the law of identity...
(if A, then A) and modus ponensModus ponensIn classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
(from A, and if A then B, conclude B).
Various other sets of conditions are also possible. Natural languages nearly always contain all these features. Mathematical logic, on the other hand, generally does not countenance explicit reference to its own sentences, although the heart of Gödel's incompleteness theorems
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
is the observation that usually this can be done anyway; see Gödel number
Gödel number
In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. The concept was famously used by Kurt Gödel for the proof of his incompleteness theorems...
. The truth-predicate is generally not available, but in naive set theory, this is arrived at through the unrestricted rule of comprehension. The rule of contraction is generally accepted, although linear logic
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
(more precisely, linear logic without the exponential operators) does not admit the reasoning required for this paradox.
Note that unlike the liar paradox or Russell's paradox, this 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, even if they are immune to the liar paradox.
The resolution of Curry's paradox is a contentious issue because resolutions (apart from trivial ones such as disallowing X directly) are difficult and not intuitive. Logicians are undecided whether such sentences are somehow impermissible (and if so, how to banish them), or meaningless, or whether they are correct and reveal problems with the concept of truth itself (and if so, whether we should reject the concept of truth, or change it), or whether they can be rendered benign by a suitable account of their meanings.
Linear logic
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
disallows contraction and so does not admit this paradox directly, but one must remove its exponential operators, or else the paradox reappears in a modal form.
See also
- Richard's paradoxRichard's paradoxIn logic, Richard's paradox is a semantical antinomy in set theory and natural language first described by the French mathematician Jules Richard in 1905. Today, the paradox is ordinarily used in order to motivate the importance of carefully distinguishing between mathematics and metamathematics...
- Kleene–Rosser paradox
- Girard's paradox
- List of paradoxes
External links
- Grossman, Jason, Australian National University: A Proof that Penguins Rule the Universe. A brief and entertaining discussion of Curry's paradox.
- Relevant First-Order Logic LP# and Curry's Paradox