Curry's paradox

Curry's paradox is a paradox that Haskell Curry described in 1942; it allows any statement to be derived from a self-referential expression, which presupposes its own validity, by means of simple, general logical rules. In this way he showed the inconsistency of axiom systems with such an expression.

Verbal version

Curry's paradox can be expressed and derived verbally through the following self-referential sentence:

If this theorem holds, then any statement A.

Curry's derivation of the paradox becomes easy to understand when this sentence is abbreviated with S. In short , S reads : If S holds, then A holds . Now, of course, if S holds, then S holds . If you insert S in the short version, the result is: If S applies, then “If S applies, then A” applies . Now one can simply omit a repeated condition without changing the meaning, so that the following results: If S holds, then A holds . This is exactly the set S . Thus the premise of S applies and one can deduce A. Any statement can thus be proven, even if one chooses it absurdly.

Linguistic requirements

Curry's paradox can be formulated in any language that meets the following conditions:

• The language allows the mode ponens : From A and "if A , then B " one concludes B :

${\displaystyle A,A\to B\vdash B}$.

• The language allows the contraction , after which a repeated premise can be left out without changing the meaning:

${\displaystyle A\to (A\to B)\vdash A\to B}$

• The language allows the tautology "if A , then A ":

${\displaystyle A\to A}$

• Language can express a self- reference through a statement that has an equivalent formula in which occurs, so that the self-reference has the following form: ${\displaystyle S}$ ${\displaystyle F(S)}$ ${\displaystyle S}$

${\displaystyle S\iff F(S)}$

The classical logic and many non-classical logics, especially intuitionistic logics and even paraconsistent logics meet these criteria, of course, but also expresses the verbal language, self-references with pronouns instead of variables. Curry's Paradox deliberately does not use negation or indirect evidence, which is usually used to infer paradoxes, but instead develops a more general direct derivation.

Derivation of the paradox

The special self-reference in Curry's paradox is with a free variable for any statement. The formal proof of this variable statement is then: ${\displaystyle S\iff (S\to A)}$ ${\displaystyle A}$

The following applies as a tautology:

${\displaystyle {\mbox{(1) }}S\to S}$

The replacement of the right side by self-reference results in:

${\displaystyle {\mbox{(2) }}S\to (S\to A)}$

From this it follows by contraction:

${\displaystyle {\mbox{(3) }}S\to A}$

The replacement with self-reference leads to:

${\displaystyle {\mbox{(4) }}S}$

From (4) and (3) it finally follows with the modus ponens:

${\displaystyle {\mbox{(5) }}A}$

With this derivation the inconsistency of the axiom system is shown, because all statements are provable. It should be noted that the self-reference is an additional axiom that is used twice in the derivation in addition to the linguistic requirements mentioned above! The derivation shows that this self-reference, used as an additional argument, is wrong: it is not relatively consistent with axiom systems in which the linguistic prerequisites apply; here only the formulability of self-reference is required, but not its validity.

Set theoretical variant

In naive set theory , a variant of the paradox arises in the following class:

${\displaystyle C\ {\stackrel {\mathrm {def} }{=}}\ \left\{x\mid x\in x\to A\right\}}$

If the unrestricted abstraction principle is applied, this results in the following self-reference:

${\displaystyle C\in C\iff (C\in C\to A)}$

From this self-reference, the statement can be proven as above and thus the inconsistency of this self-reference can be demonstrated. ${\displaystyle A}$

Since for class logic and general set theory (without the axiom of infinity ) proofs of freedom of contradiction are provided, Curry's derivation does not lead to a contradiction here, but rather proves that the class is not a set, but a so-called real class . The self-reference here follows from the naive, unrestricted abstraction principle, which cannot apply; only a bound, quantified abstraction for sets is allowed. ${\displaystyle C}$

Classic special cases

Special cases of the paradox arise in classical logic or intuitionist logic when a contradiction is inserted into the free variable , which then follows from the self-reference. Then per contraposition and the principle of contradiction is equivalent to . The paradox thus has the form of the liar's paradox in a propositional formulation by negation . The set-theoretical variant is equivalent to Russell's class , which is responsible for Russell's antinomy . ${\displaystyle S\to (X\land \neg X)}$ ${\displaystyle \neg S}$ ${\displaystyle S=\neg S}$ ${\displaystyle \left\{x\mid x\in x\to (Y\wedge \neg Y)\right\}}$ ${\displaystyle \left\{x\mid x\notin x\right\}}$

Löbs application

Curry's paradox was used in 1955 by Martin Hugo Löb to show that sentences that claim that they can be proven must be true. Hence it is sometimes referred to in the literature as Löb's paradox.

Individual evidence

1. ^ Haskell B. Curry: The inconsistency of certain formal logics. In: Journal of Symbolic Logic. Vol. 7, No. 3, 1942, ISSN  0022-4812 , pp. 115-117.
2. ^ Haskell B. Curry: The inconsistency of certain formal logics. In: Journal of Symbolic Logic. Vol. 7, No. 3, 1942, p. 115, but there with a typo in the reflexive law, correct in: Haskell B. Curry: The Combinatory Foundations of Mathematical Logic. In: Journal of Symbolic Logic. Vol. 7, No. 2, 1942, pp. 49-64, here p. 62.
3. ↑ Requirement in Lemma p. 115 in: Haskell B. Curry: The inconsistency of certain formal logics. In: Journal of Symbolic Logic. Vol. 7, No. 3, 1942, pp. 115-117.
4. ^ Martin Hugo Löb : Solution of a Problem of Leon Henkin. In: Journal of Symbolic Logic. Vol. 20, No. 2, 1955, pp. 115-118, Paradoxon p. 117.

Web links

• Stanford Encyclopedia of Philosophy : " Curry's Paradox " - by JC Beall.
• Grossman, Jason, University of Sydney History & Philosophy of Science: A Proof that Penguins Rule the Universe. Brief entertaining discussion of Curry's paradox.