On the uniqueness of the shortest single axiom or the implicational calculus of propositions
Toshihiko Sekimoto · Proceedings of the Japan Academy Series A Mathematical Sciences · 1972
By the ICP (implicational calculus of propositions), we mean the implicational fragment of the classical propositional calculus.It can be axiomatized in various ways by axiom schemes and the rules of substitution and detachment as inference rules.In 1948, Jan Lukasiewicz [1] showed that the single axiom ( 1 ) CCCpqrCCrpCsp suffices to characterize the ICP, and gave a proof sketch of the fact that this is one of the shortest single axioms that can characterize the ICP.He left open, however, the question whether (1) is the unique axiom of the shortest length.In 1968, Richard Tursman [2] showed that (1) is the only 13 letter single axiom with a possible exception of ( 2 )CCpqCCCqrpCsq.