The shortest possible length of the longest implicational axiom (Q1914373)

This interesting paper shows that every complete set of axioms of classical implicational logic (IF) must have at least one axiom of length 11 (in Polish notation). The matrix methods employed by the author also allow a simple proof of the Wajsberg/Diamond-McKinsley Theorem that every complete set of axioms must include at least one containing occurrences of 3 or more distinct propositional variables. Both results are ``best possible'' and also apply to all commonly used subsystems of IF.