Relation algebras are a common way to treat binary relations algebraically, and n-dimensional cylindric algebras handle n-ary relations. There are various connections between cylindric and relation algebras, and also between cylindric algebras of differing dimension. For example, taking the

This neat reduct process is closely related to first-order proof theory. Roughly, the laws holding in m-dimensional neat reducts of n-dimensional cylindric algebras correspond to the first-order sentences written with m variables (perhaps re-used) that can be proved using up to n variables.

Finding an intrinsic characterisation of when an
algebra is a reduct of another of larger dimension, and studying the hierarchy
so induced, has been of interest to workers such as Maddux, Monk, and Tarski
since the 1960s. Maddux developed the *n-dimensional cylindric basis* for
this purpose, and the related notion of *relational basis.* The work
in the papers below

- shows strict hierarchy results for neat reducts, with consequences for proof theory
- develops a representation theory for reducts and for algebras defined by relational bases

RelMiCS, Warszawa, 1998

Revised version in Ann. Pure Appl. Logic 101 (2000) 227-274

Fix n with 3≤ n<ω. Write B_{n}
for the class of semi-associative algebras with an n-dimensional relational
basis, and RA_{n} for the variety generated by B_{n}. We define
a notion of representation for algebras in RA_{n}, and use it to
give an explicit (hence recursive) equational axiomatisation of RA_{n},
and to reprove Maddux's result that RA_{n} is canonical. We show that
the algebras in RA_{n} are precisely those that have a complete representation.

Then we prove that whenever 3< n<k≤ω,
RA_{k} is not finitely axiomatisable over RA_{n}. This confirms
a conjecture of Maddux. We also prove that B_{n} is elementary for
n=3,4 only.

J. Symbolic Logic 67 (2002) 197-213

It also shows that **S Nr**_{n} **CA**_{n+i}
≠ **S Nr**_{n} **CA**_{n+i+1}, for 2 < n <ω
and i <ω. Here, **Nr**_{n} 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≥4, n-variable proof theory for binary relations is less powerful than (n+1)-variable proof theory.

Bull. Symbolic Logic 8 (2002) 348-379

- S
_{n}contains only 3 variables (each of which occurs many times); - S
_{n}contains exactly one nonlogical binary relation symbol (no function symbols, no constants, and no equality symbol); - S
_{n}has a proof in first-order logic with equality that contains exactly n variables, but no proof containing only n-1 variables.

Ann. Pure Appl. Logic 112 (2001) 225-266

doi: 10.1016/S0168-0072(01)00084-7

Ann. Pure Appl. Logic, 112 (2001) 267-297

doi: 10.1016/S0168-0072(01)00085-9

J. Symbolic Logic 76 (2011) 870-882.

Algebra Universalis 68 (2012) 257-285, doi 10.1007/s00012-012-0202-3.

It follows that there is no algorithm to determine whether a finite n-dimensional cylindric algebra, diagonal-free cylindric algebra, polyadic algebra, or polyadic equality algebra is representable (for diagonal-free algebras this was known). We also obtain a new proof that the classes of completely representable n-dimensional algebras of these types are non-elementary, a result that remains true for infinite dimensions if the diagonals are present, and also for infinite-dimensional diagonal-free cylindric algebras.

Springer International Publishing Switzerland 2015 --- Proc. RAMiCS 2015, W. Kahl et al. (Eds.), Springer LNCS 9348, pp. 27-42, 2015.

DOI: 10.1007/978-3-319-24704-5_2