Transposition of variables is hard to axiomatize

The function p x y that interchanges two logical variables x , y in formulas is hard to describe in the following sense. Let F denote the Lindenbaum–Tarski formula-algebra of a finite-variable first-order logic, endowed with p x y as a unary function. We prove that each equational axiom system for the equational theory of F has to contain, for each finite n , an equation that contains together with p x y at least n algebraic variables, and each of the operations ∃ , = , ∨ . This gives an answer to a problem raised by Johnson [ J. Symb. Logic ] in 1969: the class R P E A α of representable polyadic equality algebras of a finite dimension α ≥ 3 cannot be axiomatized by adding finitely many equations to the equational theory of representable cylindric algebras of dimension α . Consequences for proof systems of finite-variable logic and for defining equations of polyadic equality algebras are given. The proof uses a family of nonrepresentable polyadic equality algebras A n that are more and more nearly representable as n increases: their n -generated subalgebras as well as their proper reducts are representable. The lattice of subvarieties of R P E A α is investigated and new open problems are asked about the interplay between the transposition operations and about generalizability of the results to infinite dimensions.