Transposition of variables is hard to describe

TL;DR

This paper demonstrates the complexity of describing variable transpositions in finite-variable first-order logic, showing that certain algebraic classes cannot be finitely axiomatized and exploring implications for proof systems.

Contribution

It proves that the class of representable polyadic equality algebras of finite dimension cannot be finitely axiomatized, addressing a long-standing open problem and analyzing the structure of related algebraic varieties.

Findings

Finitely axiomatizing representable polyadic algebras is impossible for dimensions ≥ 3.

Constructs a family of nonrepresentable algebras approaching representability.

Investigates the lattice of subvarieties and poses open problems.

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.