Permutations, substitutions and finite axiomatizability

Algebras of relations form an algebraic framework for the study of logical systems, extending the correspondence between Boolean algebras and propositional logic. Tarski's representable cylindric algebras $RCA_{\alpha}$, and Halmos' representable polyadic algebras $RPA_{\alpha}$ both provide algebraic counterparts to first-order logic. In this paper, we show that the usual finite set of polyadic axioms axiomatize $RPA_{\alpha}$ over $RDf_{\alpha}$, the diagonal-free subreducts of elements in $RCA_{\alpha}$. In short: $RPA_{\alpha} = PA_{\alpha} + RDf_{\alpha}$.