Two-operator logic [axioms]

If one allows two operators then one can get standard logic if one of these operators is forced to be Not and the other is forced to be And, Or or Implies—or in fact any of operators 1, 2, 4, 7, 8, 11, 13, 14 from page 806.

A simple example that allows Not and either And or Or is the Robbins axiom system from page 773. Given the first two axioms (commutativity and associativity) it turns out that no shorter third axiom will work in this case (though ones such as f[g[f[a, g[f[a, b]]]], g[g[b]]]  b of the same size do work).

Much as in the single-operator case, to reproduce logic two pairs of operators must be allowed for k = 2, none for k = 3, 12 for k = 4, and so on. Among single axioms, the shortest that works up to k = 2 is (¬ (¬ (¬ b ∨ a) ∨ ¬ (a ∨ b)))  a. The shortest that works up to k = 3 is (¬ (¬ (a ∨ b) ∨ ¬ b) ∨ ¬ (¬ a ∨ a))  b. It is known, however, that at least 3 variables must appear in order to reproduce logic, and an example of a single axiom with 4 variables that has been found recently to work is {(¬ (¬ (c ∨ b) ∨ ¬ a) ∨ ¬ (¬ (¬ d ∨ d) ∨ ¬ a ∨ c))  a}.