Proceedings of the Royal Irish Academy: The shortest axiom of the implicational calculus of propositions