Curry's Paradox - Combinatory Logic

Combinatory Logic

In the study of illative 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:

(i) 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.

(ii) 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.