Transposition of variables is hard to describe

Abstract

The function $p_{xy}$ 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_{xy}$ as a unary function. Each equational axiom system for the equational theory of $F$ has to contain, for each finite $n$, an equation that contains together with $p_{xy}$ at least $n$ algebraic variables, and each of the operations $\exists, =, \lor$. This solves a problem raised by Johnson [J. Symb. Logic] more than 50 years ago: the class of representable polyadic equality algebras of a finite dimension $\alpha\ge 3$ cannot be axiomatized by adding finitely many equations to the equational theory of representable cylindric algebras of dimension $\alpha$. 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 ${\cal 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 $RPEA_{\alpha}$ is investigated and new open problems are asked about the interplay between the transposition operations and about generalizability of the results to infinite dimensions.