   Pure equivalential calculus has the quaint property, shown by Leśniewski, that a formula is a theorem if and only if every propositional variable in it occurs an even number of times. After universally quantifying these axioms, a further axiom was added to introduce propositional functions, in this case two-placed ones