Complexity of equations valid in algebras of relations part I: Strong non-finitizability Original Research Article

We study algebras whose elements are relations, and the operations are natural “manipulations” of relations. This area goes back to 140 years ago to works of De Morgan, Peirce and Schröder (who expanded the Boolean tradition with extra operators to handle algebras of binary relations). Well known examples of algebras of relations are the varieties RCAn of cylindric algebras of n-ary relations, RPEAn of polyadic equality algebras of n-ary relations, and RRA of binary relations with composition. We prove that any axiomatization, say E, of RCAn has to be very complex in the following sense: for every natural number k there is an equation in E containing more than k distinct variables and all the operation symbols, if 2 < n < ω. A completely analogous statement holds for the case n ⩾ ω. This improves Monkʹs famous non-finitizability theorem for which we give here a simple proof. We prove analogous non-finitizability properties of the larger varieties SNrnCAn + k. We prove that the complementation-free (i.e. positive) subreducts of RCAn do not form a variety. We also investigate the reason for the above “non-finite axiomatizability” behaviour of RCAn. We look at all the possible reducts of RCAn and investigate which are finitely axiomatizable. We obtain several positive results in this direction. Finally, we summarize the results and remaining questions in a figure. We carry through the same programme for RPEAn and for RRA. By looking into the reducts we also investigate what other kinds of natural algebras of relations are possible with more positive behaviour than that of the well known ones. Our investigations have direct consequences for the logical properties of the n-variable fragment Ln of first order logic. The reason for this is that RCAn and RPEAn are the natural algebraic counterparts of Ln while the varieties SNrnCAn + k are in connection with the proof theory of Ln. This paper appears in two parts. This is the first part, it contains the non-finite axiomatizability results. The second part contains finite axiomatizability results together with a figure summarizing the results in this area and the problems left open.