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.