Substitutions of variables are finitely axiomatizable over quantifications and permutations

TL;DR

This paper demonstrates that the axioms governing variable substitutions in finite-variable first-order logic can be finitely characterized over a base algebraic structure, simplifying the understanding of logical substitutions.

Contribution

It establishes that the equational theory of representable polyadic algebras with substitutions is finitely axiomatizable over the substitution-free reduct for finite variable cases.

Findings

Finitely axiomatizable substitution theory for finite-variable logic.

Equational theory of $RA_{\alpha}^{csp}$ over $RA_{\alpha}^{cp}$.

Simplifies the algebraic understanding of variable substitutions.

Abstract

This paper proves that the equational theory of the class $RA_{\alpha}^{csp}$ of representable polyadic algebras is finitely axiomatizable over its substitution-free reduct $RA_{\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.