Relation algebras from cylindric algebras, II

Robin Hirsch and Ian Hodkinson

We prove, for each 4 \leq n <\omega, that  S Ra CA_n+1  cannot be defined, using only finitely many first-order axioms,  relative to S Ra CA_n.  The construction also shows that for 3 \leq m<n<\omega, S Nr_mCA_n+1 is not finitely axiomatisable over S Nr_mCA_n .  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.