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.