The inconsistency of

Abstract

In [4] Curry raised the possibility that his system proposed in ξ15C of [3] might be inconsistent. In this paper this inconsistency is proved using a method also employed in [1]. From Curry's axiom ⊦LH, it follows that holds for arbitrary X . The other results from that are required are Modus Ponens, and the Deduction Theorem for implication: Assuming ⊦ HA , we define as in [1]: and let where Y is the paradoxical (or fixed point) combinator. We have X = G 2 X , so, by (2), H X ⊦ X ⊃ G 2 X which is H X ⊦ X ⊃. H 2 X ⊃ G 1 X . Clearly H X ⊦ H( G 1 X ) and, by (5), H X ⊦ H 3 X , so that, by (3), H X ⊦ H 2 X ⊃. X ⊃ G 1 X and by (5) and Modus Ponens H X ⊦ X ⊃ G 1 X . This is H X ⊦ X ⊃: H X ⊃. X ⊃ A which by (3) and Modus Ponens gives which gives, by (4), H X ⊦ X ⊃ A . Now, by (1) and (DT), which is ⊦ G 1 X . But we have ⊦H 2 X so, by the (DT), ⊦H 2 X ⊃ G 1 X which is ⊦ G 2 X . Thus we have proved ⊦ X .