Some notes on: 'A deduction theorem for restricted generality'

is a somewhat unsatisfying axiom. In particular with E = A it is inconsistent with the others (see [l]). Also the rules obtained by applying Rule Ξ once to each of the remaining axioms are consistent. This was shown in an unpublished paper by H. B. Curry and the author. Curry in [3] proved that for an equivalent system no nonpropositions are provable and Seldin in [4] has shown consistency in a stronger sense. We show here that the deduction theorem for Ξ can be proved without H-LH. We achieve this by taking L as primitive (rather than as defined by L = FAH) and we define H as BLK. Axiom 3 leads to the rule