Searching for logic [axioms]

For axiom systems of the form {…  a} one finds:

{((b ∘ b) ∘ a) ∘ (a ∘ b)  a} allows the k = 3 operator 15552 for which the Nand theorem (p ∘ p) ∘ q  (p ∘ q) ∘ q is not true. {(((b ∘ a) ∘ c) ∘ a) ∘ (a ∘ c)  a} allows the k = 4 operator 95356335 for which even p ∘ q  q ∘ p is not true. Of the 100 cases that remain when k = 4, the 25 inequivalent under renaming of variables and reversing arguments of ∘ are

{(b ∘ (b ∘ (a ∘ a))) ∘ (a ∘ (b ∘ c)), (b ∘ (b ∘ (a ∘ a))) ∘ (a ∘ (c ∘ b)), (b ∘ (b ∘ (a ∘ b))) ∘ (a ∘ (b ∘ c)), (b ∘ (b ∘ (a ∘ b))) ∘ (a ∘ (c ∘ b)), (b ∘ (b ∘ (a ∘ c))) ∘ (a ∘ (c ∘ b)), (b ∘ (b ∘ (b ∘ a))) ∘ (a ∘ (b ∘ c)), (b ∘ (b ∘ (b ∘ a))) ∘ (a ∘ (c ∘ b)), (b ∘ (b ∘ (c ∘ a))) ∘ (a ∘ (b ∘ c)), (b ∘ ((a ∘ b) ∘ b)) ∘ (a ∘ (b ∘ c)), (b ∘ ((a ∘ b) ∘ b)) ∘ (a ∘ (c ∘ b)), (b ∘ ((a ∘ c) ∘ b)) ∘ (a ∘ (c ∘ b)), ((b ∘ c) ∘ a) ∘ (b ∘ (b ∘ (a ∘ b))), ((b ∘ c) ∘ a) ∘ (b ∘ (b ∘ (a ∘ c))), ((b ∘ c) ∘ a) ∘ (b ∘ ((a ∘ a) ∘ b)), ((b ∘ c) ∘ a) ∘ (b ∘ ((a ∘ b) ∘ b)), ((b ∘ c) ∘ a) ∘ (b ∘ ((a ∘ c) ∘ b)), ((b ∘ c) ∘ a) ∘ (b ∘ ((b ∘ a) ∘ b)), ((b ∘ c) ∘ a) ∘ (b ∘ ((c ∘ a) ∘ b)), ((b ∘ c) ∘ a) ∘ (c ∘ (c ∘ (a ∘ b))), ((b ∘ c) ∘ a) ∘ (c ∘ (c ∘ (a ∘ c))), ((b ∘ c) ∘ a) ∘ (c ∘ ((a ∘ a) ∘ c)), ((b ∘ c) ∘ a) ∘ (c ∘ ((a ∘ b) ∘ c)), ((b ∘ c) ∘ a) ∘ (c ∘ ((a ∘ c) ∘ c)), ((b ∘ c) ∘ a) ∘ (c ∘ ((b ∘ a) ∘ c)), ((b ∘ c) ∘ a) ∘ (c ∘ ((c ∘ a) ∘ c))}

Of these I was able in 2000—using automated theorem proving—to show that the ones given as (g) and (h) in the main text are indeed axiom systems for logic. (My proof essentially as found by Waldmeister is given on page 810.)

If one adds a ∘ b  b ∘ a to any of the other 23 axioms above then in all cases the resulting axiom system can be shown to reproduce logic. But from any of the 23 axioms on their own I have never managed to derive p ∘ q  q ∘ p. Indeed, it seems difficult to derive much at all from them—though for example I have found a fairly short proof of (p ∘ p) ∘ (p ∘ q)  p from {(b ∘ (b ∘ (b ∘ a))) ∘ (a ∘ (b ∘ c))  a}.

It turns out that the first of the 25 axioms allows the k = 6 operator 1885760537655023865453442036 and so cannot be logic. Axioms 3, 19 and 23 allow similar operators, leaving 19 systems as candidate axioms for logic.

It has been known since the 1940s that any axiom system for logic must have at least one axiom that involves more than 2 variables. The results above now show that 3 variables suffice. And adding more variables does not seem to help. The smallest axiom systems with more than 3 variables that work up to k = 2 are of the form {(((b ∘ c) ∘ d) ∘ a) ∘ (a ∘ d)  a}. All turn out also to work at k = 3, but fail at k = 4. And with 6 Nands (as in (g) and (h)) no system of the form {…  a} works even up to k = 4.

For axiom systems of the form {…  a, a ∘ b  b ∘ a}:

With 2 variables the inequivalent cases that remain are

{(a ∘ b) ∘ (a ∘ (b ∘ (a ∘ b))), (a ∘ b) ∘ (a ∘ (b ∘ (b ∘ b))), (a ∘ (b ∘ b)) ∘ (a ∘ (b ∘ (b ∘ b)))}

but all of these allow the k = 6 operator

1885760537655125429738480884

and so cannot correspond to basic logic. With 3 variables, all 32 cases with 6 Nands are equivalent to (a ∘ b) ∘ (a ∘ (b ∘ c)), which is axiom system (f) in the main text. With 7 Nands there are 8 inequivalent cases:

{(a ∘ a) ∘ (b ∘ (b ∘ (a ∘ c))), (a ∘ b) ∘ (a ∘ (b ∘ (a ∘ b))), (a ∘ b) ∘ (a ∘ (b ∘ (a ∘ c))), (a ∘ b) ∘ (a ∘ (b ∘ (b ∘ b))), (a ∘ b) ∘ (a ∘ (b ∘ (b ∘ c))), (a ∘ b) ∘ (a ∘ (b ∘ (c ∘ c))), (a ∘ b) ∘ (a ∘ (c ∘ (a ∘ c))), (a ∘ b) ∘ (a ∘ (c ∘ (c ∘ c)))}

and of these at least 5 and 6 can readily be proved to be axioms for logic.

Any axiom system must consist of equivalences valid for the operator it describes. But the fact that there are fairly few short such equivalences for Nand (see page 818) implies that there can be no axiom system for Nand with 6 or less Nands except the ones discussed above.