Substitutions of variables are finitely axiomatizable over quantifications and permutations

This paper proves that the equational theory of the class $R{A}_{\alpha }^{csp}$ of representable polyadic algebras is finitely axiomatizable over its substitution-free reduct $R{A}_{\alpha }^{cp}$, for finite $\alpha$. That is, substitutions of variables in finite variable first-order logic can be described by finitely many axioms over the Boolean operations, existential quantifiers and permutations of variables.