The neat embedding problem and the number of variables required in proofs

Abstract:

By constructing special relation algebras we show that if $3 < \alpha < \omega$, then \[ {\mathbf {S}}N{{\text {r}}_3}C{A_\alpha } \ne {\mathbf {S}}N{{\text {r}}_3}C{A_{3\alpha - 7}}\] and there is a logically valid first-order sentence containing at most three variables with a proof in which every sentence has at most $3\alpha - 7$ variables, but no proof in which every sentence has at most a variables.