It also shows that S Nrn CAn+i \neq S Nrn CAn+i+1, for 2 < n <\omega and i <\omega. Here, Nrn denotes the neat reduct of a higher-dimensional cylindric algebra to n dimensions. This answers question 2.12 of Henkin, Monk & Tarski [Cylindric Algebras Part I, North-Holland, 1971].
Our results show that for n\geq4, n-variable proof theory for binary relations is less powerful than (n+1)-variable proof theory.
We characterise the class S Ra CAn of subalgebras of relation algebra reducts of n-dimensional cylindric algebras (for finite n, at least 4) by the notion of a hyperbasis,analogous to the cylindric basis of Maddux, and by relativised representations. A corollary is that S Ra CAn =S Ra(CAn \cap Crsn)=S Ra(CAn\cap Gn). We give a game-theoretic approximation to the existence of a representation, and use it to obtain a recursive equational axiomatisation of S Ra CAn. We include notes on n-variable proof theory, homogeneity, and related matters, and some open problems.
We prove, for each 4 \leq n < \omega, that S Ra CAn+1
cannot be defined, using only finitely many axioms, relative to S Ra
CAn. The construction also shows that for 3\leq m<n<\omega,
S
Nrm CAn+1
is not finitely axiomatisable over S Nrm CAn.
In consequence, for a certain standard n-variable first-order
proof system \vdash_{m,n} of m-variable formulas, there is no finite
set of m-variable schemata whose m-variable instances, when added to \vdash_{m,n}
as axioms, yield \vdash_{m,n+1}.