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 CAn strictly contains S RaCAn+1 for each n with 3 \leq n < \omega. We do this by defining a finite weakly associative algebra An and showing that it belongs to S Ra CAn but not SRa CAn+1. This confirms a conjecture of Maddux. It also shows that S Nrn CAn+i\neq SNrnCAn+i+1(Nrn 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.
