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