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.