Editing Curry's paradox (section)

===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''".