The Neat Embedding Problem and the Number of Variables Required in Proofs
Roger D. Maddux · Proceedings of the American Mathematical Society · 1991
By constructing special relation algebras we show that if $3 < \alpha < \omega$, then \[ {\mathbf {S}}N{{\text {r}}_3}C{A_\alpha } e {\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.