Relation algebras from cylindric algebras, II Original Research Article

We prove, for each 4⩽n<ω, that View the MathML source cannot be defined, using only finitely many first-order axioms, relative to View the MathML source. The construction also shows that for View the MathML source is not finitely axiomatisable over View the MathML source, and that for View the MathML source is not finitely axiomatisable over View the MathML source. 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.