Relation algebras from cylindric algebras, II
Robin Hirsch and Ian Hodkinson
We prove, for each 4 \leq n <\omega, that S Ra CAn+1 cannot be defined, using only finitely many first-order axioms, relative to S Ra CAn. The construction also shows that for 3 \leq m<n<\omega, S NrmCAn+1 is not finitely axiomatisable over S NrmCAn . In consequence, for a certain standard n-variable first-order proof system |-m,n of m-variable formulas, there is no finite set of m-variable schemata whose m-variable instances, when added to |-m,n as axioms, yield |-m,n+1.
Postscript file