The inconsistency of
Martin W. Bunder · Journal of Symbolic Logic · 1976
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 = G2X, so, by (2), H X ⊦ X ⊃ G2X which is HX ⊦ X ⊃. H2X ⊃ G1X. Clearly HX ⊦ H(G1X) and, by (5), HX ⊦ H3X, so that, by (3), H X ⊦ H2X ⊃. X ⊃ G1X and by (5) and Modus Ponens HX ⊦ X ⊃ G1X. This is HX ⊦ X ⊃: HX ⊃. X ⊃ A which by (3) and Modus Ponens gives which gives, by (4), HX ⊦ X ⊃ A. Now, by (1) and (DT), which is ⊦G1X. But we have ⊦H2X so, by the (DT), ⊦H2X ⊃ G1X which is ⊦G2X. Thus we have proved ⊦X.