The shortest possible length of the longest implicational axiom

A four-valued matrix is presented which validates all theorems of the implicational fragment, IF, of the classical sentential calculus in which at most two distinct sentence letters occur. The Wajsberg/Diamond-McKinsley Theorem for IF follows as a corollary: every complete set of axioms (with substitution and detachment as rules) must include at least one containing occurrences of three or more distinct sentence letters.Additionally, the matrix validates all IF theses built from nine or fewer occurrences of connectives and letters. So the classic result of Jaskovski for the full sentential calculus —that every complete axiom set must contain either two axioms of length at least nine or else one of length at least eleven—can be improved in the implicational case: every complete axiom set for IF must contain at least one axiom eleven or more characters long.Both results are best possible, and both apply as well to most subsystems of IF, e.g., the implicational fragments of the standard relevance logics, modal logics, the relatives of implicational intutionism, and logics in the ukasiewicz family.Earlier proofs of these results, utilizing a five-valued matrix built from the product matrix of C2 with itself via the method of [8], were obtained in 1988 while the author was a Visiting Research Fellow at the Automated Reasoning Project, Research School of Social Sciences, Australian National University, and were presented in [9]. The author owes thanks to the RSSS for creating the Project, and to the members of the Project generally for the stimulating atmosphere they created in turn, but especially to Robert K. Meyer for making the visit possible, and for many discussions over the years.