Editing Curry's paradox (section)

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