# On the number of variables required for proofs

Robin Hirsch, Ian Hodkinson and Roger Maddux.

This is a preprint of "Relation Algebra Reducts of Cylindric Algebra and an Application to Proof Theory" which appears in JSL 67(1).

We show that **S Ra CA _{n} **strictly contains

**S RaCA**for each n with 3 \leq n < \omega. We do this by defining a finite weakly associative algebra

_{n+1 }**A**and showing that it belongs to

_{n}**S Ra CA**but not

_{n}**SRa CA**. This confirms a conjecture of Maddux. It also shows that

_{n+1}**S Nrn CA**neq

_{n+i}\**SNr**(

_{n}CA_{n+i+1}**Nr**is the neat reducts to n dimensions), for 2 < n <\omega and i < \omega, answering open question 2.12 of Henkin, Monk & Tarski (1971). We deduce that for every n with 3 \leq n < \omega there is a logically valid sentence \phi, in a first-order language with equality and exactly one nonlogical binary relation symbol, such that \phi contains only 3 variables, \phi has a proof containing exactly n+1 variables but no proof containing only n variables.

_{n }