The shortest axioms of the implicational calculus.
Richard Tursman · Notre Dame Journal of Formal Logic · 1968
Jan Lukasiewicz has proved that all theses of the Implicational Calculus of Propositions are derivable from the axiom (I) CCCpqrCCrpCsp and has outlined a proof to the effect that (I) is the shortest single axiom from which all theses are derivable.1 Whether or not there are 13 letter axioms other than (I) which could serve as single axioms of the Calculus, ίiUkasiewicz noted, 2 is not known.In this article it is proved that (I) is the only 13 letter single axiom with the possible exception of (II) CCrpCCCpqrCsp.This article leaves unanswered the question of whether or not (II) does serve as a single axiom.If it does, then there are a total of two 13 letter single axioms; if it does not, then (I) is the only 13 letter single axiom.Since there are 132 forms of punctuation for these 13 letter wff 's, and since there are 877 unique combinations and permutations of seven variables, there are 115,764 unique 13 letter wff's.Each of these which is analytic is, initially, a candidate for single axiom status.The first practical problem is to determine the analytic wff's without writing out 115,764 128 row truth tables.The easiest way to determine the analytic wff's is to use three charts:Chart I is a list of the 132 forms of punctuation.Chart II is a list of the 877 unique combinations and permutations of seven variables.Chart III is a list of which of these 877 unique combinations and permutations can be assigned to each of 64 symmetrical couplets.(These couplets result from reducing 128 standard assignments of two values, involving seven variables, to 64; the second member of each couplet is superfluous, since anything ending in a '1' is analytic.)(What follows is only part of Chart IΠ.)