Editing Curry's paradox (section)

== 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 [[Logic notation|list of logic symbols]].

# ''X'' := (''X'' → ''Y'')<br>{{block indent| ''assumption'', the starting point, equivalent to "If this sentence is true, then ''Y''"}}
# ''X'' → ''X''<br>{{block indent|''[[law of identity]]''}}
# ''X'' → (''X'' → ''Y'')<br>{{block indent|''substitute right side of 2'', since ''X'' is equivalent to ''X'' → ''Y'' by 1}}
# ''X'' → ''Y''<br>{{block indent|from 3 by ''[[rule of contraction|contraction]]''}}
# ''X''<br>{{block indent|''substitute 4'', by 1}}
# ''Y''<br>{{block indent|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 [[Axiom schema of specification#Unrestricted comprehension|unrestricted comprehension]], we can prove any logical statement ''Y'' by examining the set
<math display="block">X \ \stackrel{\mathrm{def}}{=}\  \left\{ x \mid (x \in x) \to Y \right\}.</math>One then shows easily that the statement <math>X\in X</math> is equivalent to <math>(X\in X) \to Y</math>. From this, <math>Y</math> may be deduced, similarly to the proofs shown above. ("<math>X\in X</math>" stands for "this sentence".)

Therefore, in a consistent set theory, the set <math>\left\{ x \mid (x \in x) \to Y \right\}</math> 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, <math>m</math> shall denote the implication function taking two parameters, that is, the lambda term <math>((m A) B)</math> shall be equivalent to the usual [[infix notation]] <math>A \to B</math>.

An arbitrary formula <math>Z</math> can be proved by defining a lambda function <math>N := \lambda p.((m p) Z)</math>, and <math>X := (\textsf{Y} N)</math>, where <math>\textsf{Y}</math> denotes Curry's [[fixed-point combinator]]. Then <math>X = (N X) = ((m X) Z)</math> by definition of <math>\textsf{Y}</math> and <math>N</math>, hence the [[#Sentential logic|above]] sentential logic proof can be duplicated in the calculus:<ref>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 <math>\textsf{Y}</math>.</ref><ref>{{cite book | url=http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz | author=Gérard Huet | author-link=Gérard Huet |title=Formal Structures for Computation and Deduction | location=Marktoberdorf | series=International Summer School on Logic of Programming and Calculi of Discrete Design | date=May 1986 | archive-url=https://web.archive.org/web/20140714171331/http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz | archive-date=2014-07-14 }} Here: p.125</ref>

<math display="block">
\begin{array}{cll}
\vdash & ((m X) X) & \mbox{ by the minimal logic axiom } A \to A \\
\vdash & ((m X) ((m X) Z)) & \mbox{ since } X = ((m X) Z) \\
\vdash & ((m X) Z) & \mbox{ by the theorem }  (A \to (A \to B)) \vdash (A \to B) \mbox{ of minimal logic } \\
\vdash & X & \mbox{ since } X = ((m X) Z) \\
\vdash & Z & \mbox{ by modus ponens } A, (A \to B) \vdash B \mbox{ from } X \mbox{ and } ((m X) Z) \\
\end{array}
</math>

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 <math>X</math> translates to <math>(r \ r)</math> in combinatory logic, where
<math display="block">r = \textsf{S} \ (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) \ (\textsf{K} Z);</math>
hence<ref>
{{nowrap|1=<math>(r r)</math>}}
{{nowrap|1=<math>=</math>}}
{{nowrap|1=<math>(\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)))</math>}}
{{nowrap|1=<math>\to</math>}}
{{nowrap|1=<math>(\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))))</math>}}
{{nowrap|1=<math>\to</math>}}
{{nowrap|1=<math>(\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)</math>}}
{{nowrap|1=<math>\to</math>}}
{{nowrap|1=<math>(\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)</math>}}
{{nowrap|1=<math>\to</math>}}
{{nowrap|1=<math>(m (\textsf{S} \textsf{I} \textsf{I} (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z))) Z)</math>}}
{{nowrap|1=<math>\to</math>}}
{{nowrap|1=<math>(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)</math>}}
{{nowrap|1=<math>\to</math>}}
{{nowrap|1=<math>(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)</math>}}
{{nowrap|1=<math>\to</math>}}
{{nowrap|1=<math>(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)</math>}}
{{nowrap|1=<math>=</math>}}
{{nowrap|1=<math>((m (r r)) \ Z)</math>}}
</ref>
<math display="block">(r \ r) = ((m (r r)) \ Z).</math>