Junctional calculus

Expressions are equivalent when Union[Level[expr, {-1}]] is the same, and this canonical form can be obtained from the axiom system of page 803 by flattening using (a ∘ b) ∘ c a ∘ (b ∘ c), sorting using a ∘ b b ∘ a, and removing repeats using (a ∘ a) a. The operator can be either And or Or (8 or 14). With k = 3 there are 9 operators that yield the same results:

{13203, 15633, 15663, 16401, 17139, 18063, 19539, 19569, 19599}

With k = 4 there are 3944 such operators (see below). No single axiom can reproduce all equivalences, since such an axiom must of the form expr a, yet expr cannot contain variables other than a, and so cannot for example reproduce a ∘ b b ∘ a.