Curry's paradox

For Paul Curry's optical illusion and dissection puzzle, see Missing square puzzle.

Curry's paradox is a paradox that occurs in naive set theory or naive logics, 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. While naive set theory fails to identify it, a more rigorous examination reveals that the sentence is self-contradictory.

It has also been called Löb's paradox after Martin Hugo Löb.

Statement of Curry's paradox

The Paradox may be expressed in natural language and in various mathematical languages;

• Natural language
• Formal logic
• Set theory
• Logic with a string Eval function
• Lambda calculus
• Combinatory logic

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. 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". The usual method for proving a conditional sentence is to show that by assuming that hypothesis (A) is true, then the conclusion (B ) can be proven from that assumption. Therefore, for the purpose of the proof, assume A. Because A refers to the overall sentence, this means that 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". From these, we can obtain B by modus ponens. Therefore, A implies B and we have proved "If this sentence is true then Germany borders China" is true. Therefore "Germany borders China", but we know that is false, which is a paradox.

Brief statement

In a naïve logic, the sentence itself, denoted A, is true. The sentence is of the form "If A then B". Then "A = (if A then B)" is true. But this contracts to "If A then B" is true. So A is true. We then apply modus ponens 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 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 explanation of the logic notation used in this section, refer to the list of logic symbols.

1. X → X

rule of assumption, 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 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.

1. X = X → Y

assumption

2. X = X → false

substitute known value of Y

3. X = ¬X ∨ false

implication

4. X = ¬X

identity

Naive set theory

Even if the underlying mathematical logic does not admit any self-referential sentence, in set theories which allow unrestricted comprehension, we can nevertheless prove any logical statement Y by examining the set

$X\ {\stackrel {\mathrm {def} }{=}}\ \left\{x\mid (x\in x)\to Y\right\}.$

The proof proceeds as follows:

1. $(X\in X)\iff ((X\in X)\to Y)$

   Definition of X

2. $(X\in X)\to ((X\in X)\to Y)$

   from 1

3. $(X\in X)\to Y$

   from 2, contraction

4. $((X\in X)\to Y)\to (X\in X)$

   from 1

5. $X\in X$

   from 3 and 4, modus ponens

6. $Y$

   from 3 and 5, modus ponens

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.

Logic with a string Eval function

Suppose there is a function called Eval, that takes a string and converts it into a logical expression. Then consider the string,

s = "Eval(s) → y"

then the expression,

Eval(s) = Eval(s) → y

again gives Currys's paradox.

Lambda calculus

Curry's paradox may be expressed in Lambda calculus. Consider a function $r$ defined as,

$r=(\lambda x.xx\to y)$

Then $rr$ is,

$rr=(rr\to y)$

If $rr$ is true then $y$ is true. If $rr$ is false then $y$ is true. So $y$ is true and as $y$ can be any statement, any statement may be proved true.

$rr$ is a non-terminating computation. Considered as logic $rr$ is an expression for a value that does not exist.

Combinatory logic

Currys Paradox may also be expressed in Combinatory logic. Combinatorial logic 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.

If m is the implication function taking two parameters (that is m A B is equivalent to A → B), then r in combinatory logic is,

r = S (S (K m) (S I I)) (K y)

then

r r = m (r r) y

The paradox may also be produced using the Curry's paradoxical combinator, where,

$f=\lambda x.x\to y$ = S m (K y)

Then,

Y f

is the solution of,

$x=x\to y$

so

Y f = m (Y f) y

Discussion

Terminology

Natural language and mathematical logic are both based on asserting some statements to be true. A statement may be represented as a logical (or boolean) expression (or formula) which may be evaluated to give a value of true or false. An assertion is a statement or logical expression that, it is asserted, when evaluated, will give the value true.

Statements may also be considered in more complex ways. Statements may be qualified by who states, or believe them, and by level of certainty. However, for logic, the simple definitions given above are sufficient.

Existence problem

This paradox is similar to,

• Liar Paradox
• Russel's Paradox

in that each paradox attempts to give a name for something that does not exist. These paradoxes all attempt to give a name or representation to a solution to the equation,

X = ¬X

Note that the paradox does not arise from asserting the statement of ¬X, as such a statement would be a lie. It arises from the consideration and naming of the statement. The paradox arises by naming or representing an expression of the form ¬X to be X. In the case of Curry's Paradox, the negation is constructed from implication,

X = X → false = ¬X ∨ false = ¬X

The domain of a boolean variable X is the set {true, false}. However neither true or false is a solution to the above equation. So it must be wrong to assert the existance of X, and it is falsehood to name the expression ¬X as X.

The paradox exists whenever an expression can be constructed whose value does not exist. This may be achieved using "this statement", but there are many other language features that allow the construction of an expression that does not exist.

Language capabilities for expressing the paradox

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. The following list gives some mechanisms that support the construction of the paradox but the list is not exhaustive.

1. Self reference; "this sentence".
2. Through naming of an expression which includes the name.
3. Apply naive set theory (Unrestricted comprehension).
4. Lambda expressions.
5. An Eval function on a string.

The logic rules used in the construction of the proof are,

1. rule of assumption
2. contraction
3. modus ponens

The self-recursive function can then be used to define a non terminating computation whose value is solution to an equation. In Curry's Paradox we use implication to construct a negation, that constructs an equation with no solution.

The recursive expression then represents a value that does not exist. The laws of logic are only valid for Boolean values in {true, false}, so any deduction made from the expression may be in error.

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 countenance explicit reference to its own sentences. However the heart of Gödel's incompleteness theorems is the observation that a 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.

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.

• Lambda calculus
• Combinatory logic

Consequences for combinatory logics

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:

1. 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.
2. 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.

Resolution

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.

Resolution in natural language

Consideration of the sentence "If A then B" where A refers to the sentence creates a falsehood if B is false, because in fact there is no value for A that satisfies the expression A = "if A then false". Therefore the rest of the argument is invalid because it is arguing from an expression that has no possible value (does not exist).

Resolution in languages supporting self recursion

Languages which allow expressions (formulas) that are self-recursive, are inconsistent, and the paradox cannot be resolved.

However the languages may be made consistent by extending the domain of self-recursive expressions to allow all values that may be represented by the recursive expression. This domain is sometimes expressed as {true, false, meaningless}. This means that a recursive expression does not necessarily belong to the Boolean domain even if it is used in a Boolean expression.

The axioms and theorems of logic are valid only in the Boolean domain, {true, false}, so are not valid for those self-recursive expressions that are "meaningless". Any function that uses the value "meaningless" also returns the value "meaningless".

Resolution in Lambda Calculus

Applying Beta reduction

on $rr$ where,

$r=(\lambda x.xx\to y)$

Then $rr$ is,

$rr=(rr\to y)$

If y = false then,

$rr=\neg rr$

However no contradiction may be concluded because lambda expressions are not restricted to returning values from the Boolean domain. In this case $rr$ is meaningless and so $rr=\neg rr$ is meaningless. This allows $y$ to be either true or false, so no paradox.

Also axioms of logic like contraction and modus ponens do not apply as $rr$ is not a Boolean value. Logical axioms apply to a lambda expression only if its value is in {true, false}. This would be assumed for a Boolean expression which is not self recursive, but for Lambda Calculus expressions it may not be assumed.

Resolution in Logic with a string Eval function

A similar argument applies to the use of a string Eval function. If,

s = "Eval(s) → y"

then if y is false the expression Eval(s) is "meaningless". No deductions may be applied to it because it is not in {true, false}.

Semantics of "meaningless"

Any statement (other than a meta-statement) about "meaningless" has the value meaningless. So if the parameter or the function is meaningless the result is meaningless. These statements must be considered as meta-statements, which describe the behaviour of "meaningless" in other statements.

Consider the statement,

This statement is not meaningless.

Which might be interpreted as,

$X=X\neq meaningless$

So the above statement is meaningless.

$meaningless=meaningless\neq meaningless$

But this statement also is "meaningless". The equals operator if given either value as meaningless returns meaningless. And meaningless statements are ignored by logic. In fact we cant even assert,

¬y → Eval(s) = meaningless

as this statement is also meaningless. The only statements that can be made about "meaningless" are meta-statements.

How do we determine if a value is meaningless

Previously we appear to work out that the value of $rr$ is meaningless after applying logic to the expression. The following meta-identity for lambda calculus helps clarify the situation. It is a meta statement because it interprets the use of Beta reduction, which is a meta step in the evaluation of lambda expressions,

If x is a lambda expression,

$lval[x]\in domain[x]\iff (\exists a:a\in domain[x]\land a=lval[x]\land a=lval[betared[x]])$

In the paradox for lambda calculus, x is "r r" and,

• domain[x] = {true, false}
• lval[x] = r r
• lval[betared[x]] = r r → y

and

$rr\in \{true,false\}\iff (\exists a:a\in \{true,false\}\land a=rr\land a=rr\to y)$

which reduces to,

$rr\in \{true,false\}=y$

This tells us when $rr$ has a meaningful value. If y is false no deductions can be made, and if y is true then $rr$ is true.

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.

$\forall A\exists XX=A$

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 $\exists X$ is inside the scope of $\forall A$. The order of the quantifiers may be reversed using Skolemization.

$\forall Af(A)=A$

However now instantion gives,

$f(X\to Y)=X\to Y$

which is not the starting point for the proof and does not lead to a contradiction. There are no other instantiations that for A that lead to to the starting point to the paradox.

Resolution in set theory

In Zermelo–Fraenkel set theory 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.

See also

• Russell's paradox
• Girard's paradox
• Kleene–Rosser paradox
• List of paradoxes
• Richard's paradox

External links

• "Curry's paradox" entry by J. C. Beall in the Stanford Encyclopedia of Philosophy
• "Paradoxes and Contemporary Logic" entry by Cantini, Andrea in the Stanford Encyclopedia of Philosophy
• Penguins Rule the Universe: 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 by Jaykov Foukzon
• Inconsistent countable set by Jaykov Foukzon