Implicational calculus

With k=2 the operator can be either 2 or 11 (Implies), with k=3 {2694, 9337, 15980}, and with k=4 any of 16 possibilities. (Operators exist for any k.) No single axiom, at least with up to 7 operators and 4 variables, reproduces all equivalences. With *modus ponens* as the rule of inference, the shortest single-axiom system that works is known to be {((a · b) · c) · ((c · a) · (d · a))}. Using the method of page 1151 this can be converted to the equational form

{((a · b) · c) · ((c · a) · (d · a)) == d · d, (a · a) · b == b, (a · b) · b == (b · a) · a}

from which the validity of the axiom system in the main text can be established.