In principia Russell and Whitehead used five axioms for non-predicated logic. I believe around 20 years after this, Bernays proved that the fourth axiom is unnecessary. Meaning, it can be derived from the axioms one, two, three and five. I've been sitting here for the last while trying to figure out myself how to derive it, but the experiment is not going so well. Apparently I'm not as clever as Bernays - who could have guessed that! Anyway, I also have been unable to find a resource that shows Bernay's proof. If anyone remembers this or happens to have a rilliant moment of insight as to the solution or can find a websource, it would be much appreciated. Danke!
I haven't bothered to check it through, but it looks like there's a proof here: The Axioms of the Whitehead Russell Calculus
