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.