Computer implication and the Curry paradox (Q704044)

Turing's classical ``Halting Problem'' is an early example of a serious limitation on the capabilities of any general computer. In this note, the authors discuss a weaker computational limitation, viz., on the strength of computational (natural) inference and even theorem-proving. They defend the assertion that no sufficiently powerful inference program can successfully use an unrestricted form of modus ponens. Their argument parallels the very approach used in formulation of the classical Curry paradox. The source of their paradox seems to be the misuse of modus ponens, i.e., the unrestricted use of modus ponens. However, Myhill has already suggested that modus ponens is even the source of the classical Curry paradox itself [\textit{J. Myhill}, ``Paradoxes'', Synthese 60, No. 1, 129--143 (1984; MR 86g:03008)].