 Łukasiewicz used many-valued matrices to establish the independence of logical axioms in systems of Frege, Russell and others. He proved the completeness of full, implicational and equivalential calculi, and proved that the equivalential calculus could be based on the single axiom \(EEpqErqEpr\), with substitution and detachment for equivalence, and showed further that no shorter axiom could be the sole axiom of the system. Tarski showed in 1925 that the pure implicational calculus could be based on a single axiom, but a series of improvements by Wajsberg and Łukasiewicz led to the latter’s discovering in 1936 that the formula \(CCCpqrCCrpCsp\) could serve as single axiom and that no shorter axiom would suffice, though the publication of this result had to wait until 1948.