COMPLEXITY OF EQUATIONS VALID IN ALGEBRAS OF RELATIONS

Part I: Strong nonfinitizability.

Hajnal Andréka^{1}

Abstract. 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, 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 RCA_{n} of cylindric algebras of n-ary relations, RP EA_{n} of polyadic equality algebras of n-ary relations, and RRA of binary relations with composition. We prove that any axiomatization, say E, of RCA_{n} 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 < ω. 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 nonfinitizability properties of the larger varieties SNr_{n}CA_{n+k}. We prove that the complementation-free (i.e. positive) subreducts of RCA_{n} do not form a variety. We also investigate the reason for the above “non-finite axiomatizability” behaviour of RCA_{n}. We look at all the possible reducts of RCA_{n} 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 RP EA_{n} 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 L_{n} of first order logic. The reason for this is that RCA_{n} and RP EA_{n} are the natural algebraic counterparts of L_{n} while the varieties SNr_{n}CA_{n+k} are in connection with the proof theory of L_{n}.

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.

1This work contains the material in the author’s Doctoral Dissertation with Hungar. Acad. Sci., Budapest 1991. Research supported by Hungarian National Foundation for Scientific Research OTKA grants No T16448, T7255.

CONTENTS

Part I. Nonfinite axiomatizability of algebras of relations of higher rank (Simple proof for nonfinitizability in algebraic logic.) Introduction

Theorem 1 (simple proof) Theorem 2 (neat reducts) Theorem 3 (diagonals in case n ≥ ω) Theorem 4 (diagonals in case n < ω) Theorem 5 (unary, additive, permutation invariant functions don’t help) Theorem 6 (diagonals in the polyadic case) Theorem 7 (complementation) Theorem 8 (complementation in RRA)

References

Part II. Complementary finite axiomatizability results Proposition 1 (axiomatization of permutations) Proposition 2 (axiomatization of diagonals) Proposition 3 (axiomatization of diagonals and permutations) Figure 1 (summary of results) Figure 2 (interconnections of operations of RRA)

References INTRODUCTION

\underline{Subject:} This work deals with algebras of relations: the elements of our algebras are relations and the operations on these relations are those that arise naturally from the nature of relations. This topic has been investigated for almost 140 years with several, equally important, kinds of motivation (or intuition). Here we briefly sketch some of these motivations. (1) We can look at these algebras with purely algebraic “eyes”, we can investigate them from purely algebraic point of view. E.g. these algebras served as the starting point for the universal algebraic concept “discriminator variety”, and indeed, the theory of discriminator varieties can fruitfully be applied to algebras of relations (see e.g. Andréka–Jónsson–Németi[88], Németi[90]). Works in this line are e.g. Jónsson[82],[84], Jónsson–Tarski[52], Henkin–Monk–Tarski[HMT71],[HMT85], Givant[94], Andréka–Givant–Németi[95], Andréka–Bredikhin[95], Schein[70], Bredikhin–Schein[78], Bredikhin[77], Wagner[56], Börner[86], but already De Morgan[1860] can be considered as such. (2) These kinds of algebras arise frequently and naturally in computer science. E.g., the meaning, or semantics, of a program is often defined as the relation it defines between its inputs and outputs. Ways of building new programs from existing ones correspond then to natural operations on relations, e.g. the meaning of concatenation of two programs is just the so called relation composition of the meanings of the two programs. Kleene–algebras and dynamic algebras are typically such algebras. Works in this line are e.g. Pratt[79],[90],[91], Kozen[79],[91], Trnková–Reiterman[87], Jónsson[90], Redko[64], Németi[80],[81], [82], Daneczki[84], Fischer–Ladner[79]. Algebras of relations arise in computer science in numerous other ways, too, Andréka–Schobbens-Ryan[95] is an example. Another one is the following. A relational data–base at a given time can be considered as a relation, and the operations we perform on the data– base are natural operations on relations. Works in this line are e.g. Imielinski– Lipski[84], Düntsch[90],[90a],[93],[94], Comer[90],[93], Cosmadakis[87], Cirulis[88], Plotkin [88],[94]. For a survey on algebras of relations in computer science see e.g. Schmidt– Ströhlein[89] or Németi[90]. (3) In the investigation of first–order predicate logic, algebras of relations play an important role. The intuition here is very natural: the meanings of predicates are relations and logical connectives mean operations between these relations. For example, the meaning of the conjunction of two predicates is just the intersection of the meanings of the two predicates. It is very natural therefore to investigate algebras of relations in connection with first– order logic. This is so in such an extent, that the first versions of first–order logic were just algebras of relations (De Morgan, Peirce, Schröder, Löwenheim beginning with 1859), and first–order logic was defined on the basis of these investigations, cf. in this direction Pratt[92], Maddux[90a], and Anellis-Houser[88]. For the connection between first–order logic and our algebras we refer to section 4.3 of [HMT85], and Andréka-Németi-Sain[93], or Németi-Andréka[94]. (4) Algebras of relations play an important role in nonclassical logic, too. See e.g. van Benthem[89],[90], Orlowska[90], Venema[89],[90], Goldblatt[90], Marx–Pólos–Masuch[96], Mikulás[95], Marx[95].

\underline{Historical background:} Algebras of relations of higher ranks have been investigated since the middle of the last century beginning with the works of De Morgan, Peirce, Macfarlane, Schröder and Löwenheim. For example, Peirce[1870] investigates n–ary relations for arbitrary n. There has always been an emphasis on investigating and/or trying to characterize the equations valid in these algebras. In the last century, these valid equations were called laws (e.g. “distributive law”, “De Morgan law”, “Peircean law” etc). The goal of obtaining a mathematically transparent, elegant characterization of these laws (equations valid in the algebras of relations) appeared very early. Schröder’s impressive book contains a very large number of such laws, and it was sometimes conjectured that all laws (equations valid in algebras of relations) could be deduced from the laws in Schröder’s book. In modern terminology, this conjecture would amount to conjecturing that the equations valid in the algebras of relations are finitely axiomatizable. This conjecture was open for a very long time^{2} and there have been efforts trying to prove the conjecture. Among others, Tarski and his co–workers made efforts in the direction of trying to prove the conjecture. Monk[69] proved that the conjecture in this form is not true. The equations valid in the algebras of relations of higher ranks (defined the usual way) do not admit a finite axiomatization^{3}. For the special case of binary relations he proved the result already five years earlier in Monk[64] (confirming a conjecture of Roger Lyndon and improving Jónsson’s and Lyndon’s method of connecting projective planes to algebraic logic i.e. to algebras of relations, cf. Jónsson[59], Lyndon [61]). Monk’s negative results gave rise to two kinds of new questions raised more or less independently by Craig, Henkin, Jónsson, Tarski, and others. These two questions are the following: (i) If in this form the conjecture above is not true, then in what other form is it true? (ii)

2We will see that in a certain special form the conjecture is still open. Cf. e.g. in Németi[90] the subsections devoted to the finitization problem.

3A possible choice for the algebra of n-ary relations is the class RCA_{n} of representable cylindric algebras. Other choices are the class RSCA_{n} of representable substitution-cylindric algebras and the class RQP EA_{n} of representable quasi-polyadic equality algebras. These choices are strongly tied together, cf. Németi[90], Andréka–Givant–Mikulás–Németi–Simon[96], and Sain– Thompson[88] for discussions and comparisons of these choices.

What is the complexity (from various points of view) of the equations valid in the algebras of relations of higher ranks? (These questions will be made somewhat more concrete later.)

These two (groups of) questions have been studied for a long time. For example, a partial positive result in connection with (i) is in Lyndon[56] which gives a recursive enumeration of the equations valid in algebras of binary relations. (A different enumeration was given by Ralph McKenzie and was generalized by Monk to algebras of relations of arbitrary ranks.) A recent work giving recursive axiomatizations is Hirsch-Hodkinson[95]. The present work is also devoted to these two (groups of) questions.

One of the more concrete versions of (i) is the following. (i.1) If there is no finite set of axioms, perhaps still there is a finite schema (in some satisfactory sense) of axioms axiomatizing the equations valid in the algebras of relations (e.g. Jónsson[59], Monk[69], Henkin–Monk[74], [HMT85] Problems 4.1,4.16, Németi[90]). The book [HMT85] §4.1, pp.115–119 summarizes positive results in this direction each of which is found in the book unsatisfactory from some important point of view. That is why the quoted problems are stated in the same book at a later point. Monk[69] proved that a certain kind of schema will not work, and recently Németi–Sági[96] proved that no schema at all works for the infinite dimensional polyadic case. In this work we restrict ourselves to the finite-dimensional case to which the above Németi–Sági result does not apply. Positive results about both the algebraic form and the logical equivalent of the problem were proved in Simon[90] and Venema[90], Mikulás[95], Sain–Gyuris[96], Sain[87,92], Németi– Simon[96], Németi[96]. In the last two references it is shown, among others, that in a certain non-well founded set theory, some of the nonfinitely axiomatizable classes will become finitely axiomatizable. These are major improvements but do not settle the problem completely.

\underline{In the present work} Thm.s 3,4,6,7,8 point in the direction that it will be quite hard to find a finite schema of axioms with the desired property. Roughly speaking, if Σ is a set of equations axiomatizing the class RCA_{ω} of algebras of relations of arbitrary ranks, then for every number n, there is an equation σ ∈ Σ such that σ contains more than n operation symbols and more than n variables. Moreover, complementation “-”, and either “∪” or “∩”, and one of the identity relations d_{ij} must occur in σ. Further, to every choice of n and d_{ij} there must exist such a σ in Σ. Similar results are obtained for the other distinguished kinds (RCA_{n} with 2 < n < ω, RP EA_{n}, RRA) of algebras of relations. The above quoted results on the complexity of Σ (longer and longer equations etc.) can be interpreted to show what kind of schema will not work in solving part (i.1) of problem (i) mentioned earlier. This generalizes the negative result on schemata in Monk[69] and solves the problem on p.342 there. These theorems also provide solutions for problems formulated in Jónsson[59], Johnson[69] and in Henkin–Monk–Tarski[HMT71],[HMT85].

The above quoted Thm.s 3,4,6,7,8 (concerning Σ) are also relevant to question (ii) which concerns the complexity of the (possible axiomatizations of the) equational theory of the algebras of relations. Further results in this work concerning question (ii) are summarized on Figures 1,2. Roughly speaking, Figure 1 addresses the question “Which ones of our operations on relations bring in an infinity of new axioms?”. The answer may depend on which operations are added to our algebras first. Since we wanted to represent all the possibilities, Figure 1 is of the form of a tree.

The second part of question (i) is the following. (i.2) Could we choose the basic operations on relations of higher ranks such that

(a) the operations would remain invariant under permutations (see Thm.5 for definition),

(b) the new class of algebras of relations would become a finitely axiomatizable variety or quasi–variety, and

(c) the most important classical operations on relations would be term definable.

This problem was raised independently e.g. by Bjarni Jónsson in 1984, in Henkin –Monk[74], in Tarski–Givant[87], and is discussed in Németi[90] beginning with Remark 2 therein.

In Theorem 5 we prove a negative result in this direction, improving Biró’s one Biró[89] and showing that Sain’s positive result can not be improved in certain ways. (Sain[87a] was able to give a positive result to the variant of (i.2) in which condition (c) is not extended to the identity relation but is extended to the substitution and permutation operations, like R ↦ R^{−1}, instead. Cf. also Sain–Gyuris[96], Sain[92], Németi[96].)

Let us briefly return to problem (i.1). In this connection, Jónsson[59] investigated the subreducts of the usual algebras RRA of binary relations obtained by omitting the operations “-” and “∪” from RRA. So, the extra–Boolean operations remain the same and of the Booleans we keep only intersection (or meet). For these subreducts of RRA, Jónsson[59] gave an infinite set Σ_{∞} of quasi–equations axiomatizing the class in question. Though Σ_{∞} does not follow from any of its finite subsets, its mathematical content is more explicit and understandable than that of the axiomatizations discussed way above. Jónsson[59] raised the question whether an axiomatization of RRA can be obtained from Σ_{∞} by adding finitely many quasi–equations to Σ_{∞}. Because of the relative simplicity of Σ_{∞}, a positive answer to this question would have yielded a kind of a positive solution to Problem (i.1). We show that the answer to Jónsson’s question is in the negative. (Theorem 8) Moreover, we prove that if Σ_{∞} ∪ Σ_{1} is an axiomatization of RRA consisting of quasi–equations, then there is a σ ∈ Σ_{1} such that all Boolean operations together with relation composition “∘” occur in σ as operation symbols. (Since ∪ is expressible with “-” and “∩”, by all Booleans we mean either “-” and “∪”, or “-” and “∩”, or “∩” and “∪”.)

We try to use conventional notation. We introduce less usual notation at their first occurrence in the text. We refer to items in the bibliography by names of authors and by years. There are two exceptions: [HMT71] and [HMT85] refer to Henkin-Monk-Tarski[HMT71] and to Henkin-Monk-Tarski[HMT85] respectively.

This paper will appear in two parts. This is the first part, it contains the nonfinite axiomatizability results. The second part contains finite axiomatizability results together with the figure summarizing the results obtained and the problems left open.

\underline{Acknowledgements.} I am grateful to I. Düntsch for a very thorough reading of the paper. Very special thanks go to J. D. Monk for his invaluable comments and careful reading.

NONFINITE AXIOMATIZABILITY OF ALGEBRAS OF RELATIONS OF HIGHER RANK. (Simple proof for non–finitizability in algebraic logic.)

Boolean set algebras can be considered as algebras of unary relations, and the theory of Boolean algebras proved to be very useful in different areas of mathematics. Beginning with De Morgan[1860], many mathematicians made efforts to generalize Boolean algebras to algebras of relations of higher arity (e.g. Peirce[1870], Schröder[1895]). Continuing this line of research, Tarski, around 1949, defined the class RCA_{n} of algebras of n–ary relations as a candidate for playing the same role in first–order logic what Boolean algebras played in propositional logic. The first, most natural task was to generalize the finite axiom system known for Boolean algebras to axiom systems for RCA_{n}. Tarski proposed several such strengthenings of the axiom system of Boolean algebras, but it always turned out that the proposed axiom system was not strong enough to axiomatize RCA_{n}. Finally, Monk proved in 1969 that RCA_{n} is not finitely axiomatizable for n ≥ 3. (The hypothesis n ≥ 3 is important here because Henkin gave finite axiom systems for RCA_{n}, n ≤ 2.) Monk’s result is still one of the most important theorems in algebraic logic and trying to understand the equational theory of RCA_{n} is one of the central questions of the field.

If RCA_{n} is not finitely axiomatizable, then the next question is to see how complicated its equational theory is. W. Craig asked around 1968 whether RCA_{n} can be axiomatized with equations using only three variables. This was a natural question because of the following. Boolean algebras are axiomatized with equations using three variables, and Diamond–McKinsey[47] proved that Boolean algebras cannot be axiomatized with two variables, thus RCA_{n} cannot be axiomatized with two variables, either. At the same time, all the natural non–trivial equations valid in RCA_{n} that one could think of were consequences of ones using only three variables^{4}, so there was a possibility of obtaining an affirmative answer to Craig’s question.

Craig’s above problem is the first one in the last section of Monk[69], where he raises several open problems concerning the structure of the equational theory of RCA_{n}. We will give a negative answer to Craig’s problem published in Monk[69], see Theorem.1 below.

Theorem 1 is a corollary of the much stronger Theorem 3 in this section. Yet, we give a separate proof for Theorem 1. The reason for this is that the proof we give for Thm.1 is a proof for Monk’s original theorem, too, and at the same time this proof is much simpler than the ones existing in the literature. Because of its importance in algebraic logic, there already were efforts to simplify Monk’s original proof. Works in this line are e.g. Comer[85], Maddux[89]. The proofs of Monk, Comer, Maddux all use ultraproducts, they construct nonrepresentable algebras an ultraproduct of which is representable. Our proof does not use ultraproduct, we construct big nonrepresentable algebras the small–generated subalgebras of which are representable. This latter method was used in Jónsson[84] Thm.3.5.6 to show that the class of representable relation algebras cannot be axiomatized by using finitely many variables.

Another reason for including a separate proof for Theorem 1 is that the proofs of later stronger theorems are refinements of the one of Theorem 1, and we believe that these refinements can be understood easier after reading the simple proof of Theorem 1.

Let U be a set. Then P(U) denotes the powerset of U and 𝔓(U) denotes the Boolean algebra of all subsets of U. Let n be an ordinal. Then ^{n}U is the set of all U–termed sequences of length n, and thus P(^{n}U) is the set of all n–ary relations on U. Let s ∈ ^{n}U, i < n and u ∈ U. Then s(i/u) denotes the sequence we obtain from s by replacing its i–th value with u. Let i, j < n. The unary operation c_{i}^{U} on n–ary relations over U and the constant d_{ij}^{U} ∈ P(^{n}U) are defined as

4The equations in [HMT71]2.6.11 use many variables, but they all follow from c_{0}(x·y)·c_{0}(x−y) ≤ c_{0}c_{1}(c_{1}x · s_{1}^{0}c_{1}x − d_{01}).

c_{i}^{U}(X) = {s ∈ ^{n}U : s(i/u) ∈ X for some u ∈ U},
d_{ij}^{U} = {s ∈ ^{n}U : s_{i} = s_{j}}.

We often omit the upper indices U. Because of their geometrical meaning, the operations c_{i} and d_{ij} are also called cylindrifications and diagonal constants, respectively.

Let

F ullRA_{n} = {⟨𝔓(^{n}U), c_{i}^{U}, d_{ij}^{U}⟩_{i,j<n} : U is a set}.

The class of all subalgebras of elements of F ullRA_{n} is called the class Cs_{n} of n– dimensional cylindric set algebras. The variety generated by F ullRA_{n} is the class of all subdirect products of Cs_{n}’s^{5} and is called RCA_{n}, the class of representable cylindric algebras of dimension n. ω denotes the smallest infinite ordinal.

THEOREM 1. Let n ≥ 3 be an arbitrary (possibly infinite) ordinal. Then RCA_{n} is not axiomatizable with a set Σ of quantifier–free formulas such that Σ contains only finitely many variables.

Proof: \underline{PLAN:} For all k < ω we will construct an algebra 𝔄_{k} such that

a) 𝔄_{k} ∉ RCA_{n}

b) every k–generated subalgebra of 𝔄_{k} is in RCA_{n}.

This will prove the theorem because of the following: Assume that Σ is a set of quantifier–free formulas such that Σ contains at most k variables (|var(Σ)| ≤ k < ω) and RCA_{n} ⊧ Σ. Then 𝔄_{k} ⊧ Σ is easily seen as follows. Every k–generated subalgebra of 𝔄_{k} is in RCA_{n}, and the validity of Σ in any algebra 𝔅 depends only on the validity of Σ in the k–generated subalgebras of 𝔅 because |var(Σ)| ≤ k and Σ contains no quantifiers. Thus 𝔄_{k} ⊧ Σ. However, 𝔄_{k} ∉ RCA_{n}, hence Mod(Σ) ⊈ RCA_{n} showing that Σ does not axiomatize RCA_{n}.

First we will give the proof for n ≥ ω, because in this case we can use a simpler construction, and thus the idea of the proof will be easier to see. After this, we will give a proof that works for all n ≥ 3.

The proof for n ≥ ω :

5For n < ω, this is a result of Tarski[55], originally proved by using representation theory. Today, using the theory of discriminator varieties, a fairly simple proof can be given for n < ω, see e.g.

Németi[90]. For n ≥ ω, this is a result in Henkin–Tarski[61] (Thm.2.19), where they ask for a purely algebraic proof which can be found in Henkin–Monk–Tarski–Andréka–Németi[81], p.100, Thm.I.7.15, or in [HMT85]3.1.103. This proof further can be simplified following the outline in Németi[90].

\underline{CONSTRUCTION OF 𝔄_{k}:} Let m ≥ 2^{k}, m < ω and let ⟨U_{i} : i < n⟩ be a system of disjoint sets each of cardinality m. Let

U = ⋃{U_{i} : i < n}, let

q ∈ ×_{i<n}U_{i} = {s ∈ ^{n}U : s_{i} ∈ U_{i} for all i < n} be arbitrary,

R = {z ∈ ×_{i<n}U_{i} : |{i < n : z_{i} ≠ q_{i}}| < ω}, and let

𝔄′ be the subalgebra of ⟨𝔓(^{n}U), c_{i}, d_{ij}⟩_{i,j<n} generated by R.

Then R is an atom of 𝔄′ because of the following: For any two sequences s, z ∈ R there is a permutation σ : U ↣ → U of U taking s to z and fixing R, i.e. σ ∘ s = z and R = {σ ∘ p : p ∈ R}. If σ is a permutation of U fixing R, then σ fixes all the elements generated by R because the operations of RCA_{n} are permutation invariant. Thus if a ∈ A′ and s ∈ a ∩ R then R ⊆ a, showing that R is an atom of 𝔄′.

We now “split R into m + 1 new ‘abstract’ atoms R_{j} each imitating R”. I.e. let R_{j}, j ≤ m be m + 1 distinct elements, not in A′, and let 𝔄 be an algebra of the same similarity type as 𝔄′ such that

𝔄′ ⊆ 𝔄, the Boolean part of 𝔄 is a Boolean algebra, R_{j} are atoms of 𝔄 and c_{i}R_{j} = c_{i}R for all j ≤ m, i < n, each element of 𝔄 is a join of an element of 𝔄′ and of some R_{j}’s, c_{i} distributes over joins, for any i < n, i.e. c_{i}(x + y) = c_{i}x + c_{i}y for all x, y ∈ A.

By the above, we have constructed our algebra 𝔄 = 𝔄_{k}.

CLAIM 1. 𝔄 ∉ RCA_{n}.

Proof: For i, j < n, i ≠ j, let s_{j}^{i}(x) = c_{i}(d_{ij} ∩ x) and let s_{i}^{i}(x) = x. Let

τ(x) = ⋂_{i≤m} s_{i}^{0}c_{1}...c_{m}x ∩ ⋂_{i<j≤m} −d_{ij}.

Then 𝔄′ ⊧ τ(R) = 0, because of the following. Let ^{n}U^{(q)} = {z ∈ ^{n}U : |{i < n : z_{i} ≠ q_{i}}| < ω}.

c_{1}...c_{m}R = U_{0} × \underbrace{U × ⋯ × U}_{m times} ×U_{m+1} × ... ∩^{n}U^{(q)},

s_{i}^{0}c_{1}...c_{m}R = U × ... × U_{0} × ... × U × U_{m+1} × ... ∩^{n}U^{(q)},

⋂_{i≤m} s_{i}^{0}c_{1}...c_{m}R = \underbrace{U_{0} × ⋯ × U_{0}}_{m+1 times} ×U_{m+1} × ... ∩^{n}U^{(q)} .

Then by |U_{0}| ≤ m we have that there is no repetition–free sequence in U_{0} ×...×U_{0} (m + 1 times). Thus 𝔄′ ⊧ τ(R) = 0.

Then 𝔄 ⊧ τ(R) = 0 by 𝔄′ ⊆ 𝔄. Assume that 𝔄 is represented somehow. Then there is a homomorphism h : 𝔄 → ⟨𝔓(^{n}W), c_{i}, d_{ij}⟩_{i,j<n} for some set W such that h(R) ≠ ∅. We will derive a contradiction. By h(R) ≠ ∅ there is s ∈ h(R). By R ≤ c_{0}R_{i} we have h(R) ⊆ c_{0}h(R_{i}), so there is w_{i} such that s(0/w_{i}) ∈ h(R_{i}), for all i ≤ m. These w_{i}’s are different from each other since the R_{i}’s are disjoint from each other, and so the h(R_{i})’s are disjoint from each other. Consider the sequence

z = ⟨w_{0}, w_{1}, ..., w_{m}, s_{m+1}, ...⟩.

Now z ∈ τ(h(R)) can be seen as follows. Let i, j ≤ m, i ≠ j. Then z ∈ −d_{ij} by w_{i} ≠ w_{j}. Next we show z ∈ s_{i}^{0}c_{1}...c_{m}h(R). By the definition of w_{i}, ⟨w_{i}, s_{1}, ...⟩ ∈ h(R_{i}) ⊆ h(R), so ⟨w_{i}, w_{1}, ..., w_{m}, s_{m+1}, ...⟩ ∈ c_{1}...c_{m}h(R), and thus z ∈ c_{0}(d_{0i} ∩ c_{1}...c_{m}h(R)) = s_{i}^{0}c_{1}...c_{m}h(R). Therefore z ∈ τ(h(R)), a contradiction by 𝔄 ⊧ τ(R) = 0. QED(Claim 1)

CLAIM 2. The k–generated subalgebras of 𝔄 are in RCA_{n}.

Proof: Let G ⊆ A, |G| ≤ k. For all i, j ≤ m define

R_{i} ≡ R_{j} iff (∀g ∈ G)[R_{i} ≤ g ↔ R_{j} ≤ g].

Then ≡ is an equivalence relation on {R_{j} : j ≤ m} which has ≤ 2^{k} blocks by |G| ≤ k. Let p denote the number of blocks of ≡, i.e. p = |{R_{j}/ ≡ : j ≤ m}| ≤ 2^{k} ≤ m. Define

B = {a ∈ A : (∀i, j ≤ m)([R_{i} ≡ R_{j} and R_{j} ≤ a] ⇒ R_{i} ≤ a)}.

We now show that B is closed under the operations of 𝔄. Let i < l < n.

1) B clearly is closed under the Boolean operations.

2) d_{il} ∈ B since R_{j} ≰ d_{il} for all j ≤ m.

3) Clearly, A′ ⊆ B (since R is an atom of 𝔄′), and c_{i}a ∈ A′ for all a ∈ A. Thus c_{i}b ∈ B for all b ∈ B.

Let 𝔅 ⊆ 𝔄 be the subalgebra of 𝔄 with universe B. By G ⊆ B, it is enough to show that 𝔅 ∈ RCA_{n}.

We will define an embedding h : 𝔅 ↣ ⟨𝔓(^{n}U), c_{i}, d_{ij}⟩_{i,j<n}. Notation: If 𝔅 is any Boolean algebra, X ⊆ B and x ∈ B, then we say that X is a \underline{partition} of x (in 𝔅) provided that ∑ X = x, and for all different a, b ∈ X we have a · b = 0 ≠ a. Let {y_{j} : j < p} = {∑(R_{j}/ ≡) : j ≤ m}. Then {y_{j} : j < p} is a partition of R in 𝔅, c_{i}y_{j} = c_{i}R for all j < p and i < n and every element of 𝔅 is a join of some element of A′ and of some y_{j}’s. So, 𝔅 looks like

We are going to define the images of the y_{j}’s under the embedding h. Let Q = {0, 1, ..., m − 1} and let (Q, +, 0) be any commutative group. For each i < n let f_{i} : U_{i} ↣ → Q be a bijection such that f_{i}(q_{i}) = 0. For j < m define

R′′_{j} = {z ∈ R : ∑⟨f_{i}(z_{i}) : i < n⟩ = j}.

(Here Σ denotes taking sum in the group (Q, +, 0).) Then R′′_{j} ⊆ ^{n}U and it is not difficult to check that the R′′_{j}’s are disjoint from each other and

c_{i}R′′_{j} = c_{i}R for all i < n.

Define for all j < p − 1

R′_{j} = R′′_{j}
R′_{p−1} = ⋃{R′′_{j} : p − 1 ≤ j < m}.

We are ready to define the embedding h of B.: We define for all b ∈ B

h(b) = (b − R) ∪ ⋃{R′_{j} : j < p, y_{j} ≤ b}.

It is not difficult to check that h is an embedding h : 𝔅 ↣ ⟨𝔓(^{n}U), c_{i}, d_{ij}⟩_{i,j<n}.

In more detail: h preserves ∪, −. h(b) = 0 implies b = 0. h(d_{il}) = d_{il}. Now we check c_{i}h(b) = h(c_{i}b).

c_{i}h(b) = c_{i}[(b − R) ∪ ⋃{R′_{j} : y_{j} ≤ b}] =
= c_{i}(b − R) ∪ ⋃{c_{i}R′_{j} : y_{j} ≤ b} =
= c_{i}(b − R) ∪ ⋃{c_{i}y_{j} : y_{j} ≤ b}  =
= c_{i}[(b − R) ∪ ⋃{y_{j} : y_{j} ≤ b}] = c_{i}b.

h(c_{i}b) = (c_{i}b − R) ∪ ⋃{R′_{j} : y_{j} ≤ c_{i}b} = c_{i}b, since (∃j)y_{j} ≤ c_{i}b iff R ≤ c_{i}b, and R ≰ c_{i}b iff c_{i}b = c_{i}b − R. QED(Claim 2)

By the above we have proved Theorem 1 for n ≥ ω.

REMARK 1. In the above proof, we used n ≥ ω only in the proof of Claim 1, where we expressed |U_{0}| ≤ m by translating the formula

¬∃v_{0}...v_{m}(U_{0}(v_{0}) ∧ ... ∧ U_{0}(v_{m}) ∧ ⋀_{i<j≤m}v_{i} ≠ v_{j})

into an RCA_{n}–term. ( ⋂_{i≤m}s_{i}^{0}c_{1}...c_{m}R ∩ ⋂_{i<j≤m} − d_{ij} = 0 is a direct translation

of this.) In the above formula we use m + 1 variables, therefore we need m + 1 “indices” in the translated term, i.e. we need n ≥ m + 1.

Therefore in the case n ≤ m we cannot use the above straightforward method for “counting U_{0}”. In the case n ≤ m we will use the following idea: If U_{0} × U_{0} is the union of m functions, then |U_{0}| ≤ m. The formula expressing U_{0} × U_{0} is the union of m functions F_{0}, ..., F_{m−1} is the following.

(U_{0}(v_{0}) ∧ U_{0}(v_{1}) → ⋁_{j<m}F_{j}(v_{0}v_{1})) ∧ ⋀_{j<m}(F_{j}(v_{0}v_{1}) ∧ F_{j}(v_{0}v_{2}) → v_{1} = v_{2}).

The translation of this formula will be the equations

c_{1}R ∩ s_{1}^{0}c_{1}R ⊆ ⋃{F_{j} : j < m}, F_{j} ∩ s_{2}^{1}F_{j} ⊆ d_{12}, for j < m.

■

The following proof works for all n ≥ 3. However, in order to make the proof shorter (i.e. to avoid writing down some details needed only in the case n ≥ ω), we will assume n < ω.

The proof for 3 ≤ n < ω :

\underline{CONSTRUCTION OF 𝔄_{k}:} Let m > 2^{k}, m < ω and let ⟨U_{i} : i < n⟩ be a system of disjoint sets each of cardinality m such that U_{0} = {0, ..., m − 1}. Let

U = ⋃{U_{i} : i < n},

R = ×_{i<n}U_{i} = {s ∈ ^{n}U : s_{i} ∈ U_{i} for all i < n},

F = {s ∈ ^{n}U : s_{0}, s_{1} ∈ U_{0}, s_{1} = s_{0} + 1(mod m)}, and let 𝔄′ be the subalgebra of ⟨𝔓(^{n}U), c_{i}, d_{ij}⟩_{i,j<n} generated by R, F.

Now R is an atom of 𝔄′ and this can be seen exactly as in the case of n ≥ ω. Let 𝔄 be the algebra we obtain from 𝔄′ by splitting R into m + 1 new atoms R_{j}, j ≤ m.

CLAIM 3. 𝔄 ∉ RCA_{n}.

Proof: For any j define

F_{j} = {s ∈ ^{n}U : s_{0}, s_{1} ∈ U_{0}, s_{1} = s_{0} + j(mod m)}.

We will show that F_{j} ∈ A′, for all j. F = F_{1} ∈ A′ by definition. Assume that F_{j} ∈ A′, we will show that F_{j+1} ∈ A′, too. It is easy to check that

F_{j+1} = c_{2}(s_{2}^{1}F_{j} ∩ s_{2}^{0}F)

as follows. s_{2}^{1}F_{j} = {s ∈ ^{n}U : s_{2} = s_{0} + j(mod m)}, s_{2}^{0}F = {s ∈ ^{n}U : s_{1} = s_{2} + 1(mod m)}, hence s_{2}^{1}F_{j} ∩ s_{2}^{0}F = {s ∈ ^{n}U : s_{0}, s_{1}, s_{2} ∈ U_{0}, s_{2} = s_{0} + j(mod m), s_{1} = s_{2} + 1(mod m)}, therefore c_{2}(s_{2}^{1}F_{j} ∩ s_{2}^{0}F) = {s ∈ ^{n}U : s_{0}, s_{1} ∈ U_{0}, s_{1} = s_{0} + j + 1(mod m)} = F_{j+1}. By F_{0} = F_{m}, we have shown

(1)  F_{0}, ..., F_{m−1} ∈ A′.

Also, each F_{j} satisfies

(2)  F_{j} ∩ s_{2}^{1}F_{j} ⊆ d_{12}

by F_{j} ∩ s_{2}^{1}F_{j} = {s ∈ ^{n}U : s_{0}, s_{1}, s_{2} ∈ U_{0}, s_{1} = s_{0} + j(mod m), s_{2} = s_{0} + j(mod m)} ⊆ d_{12}. Finally, we also have

U_{0} × U_{0} ×^{n−2}U = ⋃{F_{j} : j < m}

since for any u, v ∈ U_{0} if j = v −u(mod m) then v = u+j, hence s(0/u, 1/v) ∈ F_{j}, for any s ∈ ^{n}U. Thus

(3)  c_{1}R ∩ s_{1}^{0}c_{1}R ⊆ ⋃{F_{j} : j < m}

since c_{1}R ∩ s_{1}^{0}c_{1}R ⊆ {s ∈ ^{n}U : s_{0}, s_{1} ∈ U_{0}}. By 𝔄′ ⊆ 𝔄, (2)–(3) hold in 𝔄, too.

Assume that 𝔄 is represented somehow. Then for some W there is a homomorphism h : 𝔄 → ⟨𝔓(^{n}W), c_{i}, d_{ij}⟩_{i,j<n} such that h(R) ≠ 0. We will derive a contradiction. By h(R) ≠ 0 there is s ∈ h(R). By R ≤ c_{0}R_{i} we have h(R) ⊆ c_{0}h(R_{i}), so there is w_{i} such that s(0/w_{i}) ∈ h(R_{i}), for all i ≤ m. These w_{i}’s are different from each other since the R_{i}’s are disjoint from each other, and so the h(R_{i})’s are disjoint from each other. Consider the sets

H = {w_{i} : i ≤ m} and
G = {w ∈ H : s(1/w) ∈ h(F_{j}) for some j < m}.

Then |H| = m + 1. |G| ≤ m can be seen as follows. Assume w, w′ ∈ G such that s(1/w), s(1/w′) ∈ h(F_{j}). Then s(1/w, 2/w′) ∈ c_{2}h(F_{j}) ∩ s_{2}^{1}c_{2}h(F_{j}) = h(c_{2}F_{j} ∩ s_{2}^{1}c_{2}F_{j}) ⊆ h(d_{12}) = d_{12}, therefore w = w′. We have seen |G| ≤ m. By |H| = m+1 then there is i ≤ m with w_{i} ∈ H ∖ G. Consider the sequence

z = ⟨s_{0}, w_{i}, s_{2}, s_{3}, ...⟩ = s(1/w_{i}).

Then z ∈ c_{1}h(R) ∩ s_{1}^{0}c_{1}h(R) by s ∈ h(R), s(0/w_{i}) ∈ h(R_{i}) ⊆ h(R). But z ∉ ⋃{h(R_{j}) : j < m} by w_{i} ∉ G. Thus c_{1}h(R) ∩ s_{1}^{0}c_{1}h(R) ⊈ ⋃{h(F_{j}) : j < m} contradicting c_{1}R ∩ s_{1}^{0}c_{1}R ⊆ ⋃{F_{j} : j < m}. Therefore 𝔄 is not representable, i.e. 𝔄 ∉ RCA_{n}. QED(Claim 3)

CLAIM 4. The k–generated subalgebras of 𝔄 are in RCA_{n}.

\underline{The proof} of Claim 4 is exactly the same as that of Claim 2. We omit the proof of Claim 4.

QED(Theorem 1)

REMARK 2. We can obtain from the proof of Theorem 1 a set of equations “witnessing” nonfinite axiomatizability of RCA_{n}. Below, we will give a sequence ⟨e_{m} : m < ω⟩ of stronger and stronger equations valid in RCA_{n} such that any first–order formula valid in RCA_{n} can imply only finitely many of the equations e_{m}, m < ω.

The equations we can get from the proof of Theorem 1 if n ≥ ω are

∏_{i≤m} c_{0}(x · x_{i} · ∏_{i≠j≤m} −x_{j}) ≤ c_{0}...c_{m}( ∏_{i,j≤m,i≠j} s_{i}^{0}c_{1}...c_{m}x · −d_{ij}).

Let us denote the above equation by e_{m}. Then RCA_{n} ⊧ {e_{m} : m < ω} follows by the proof of Claim 1. Let 𝔄 be the algebra constructed in the proof of Theorem 1 (case n ≥ ω) with |U_{0}| = m. Then 𝔄 |̸= e_{m} by the proof of Claim 1, while 𝔄 ⊧ {e_{i} : i < m} can be proved by a similar argument as in the proof of Claim 2. Thus the sequence ⟨e_{m} : m < ω⟩ is strictly “getting stronger” in the sense that {e_{i} : i < m} |̸= e_{m} for all m < ω.

Let Σ be a set of quantifier–free formulas valid in RCA_{n}, and using only k variables. Let m ≥ 2^{k}. Then 𝔄 ⊧ Σ by Claim 2, while 𝔄 |̸= e_{m}, showing that Σ |̸= e_{m} for all m ≥ 2^{k}. Thus Σ can imply only finitely many of the equations e_{m}, m < ω. Let φ be any first–order formula valid in RCA_{n}. Then φ follows from a finite set Σ of equations valid in RCA_{n}, because RCA_{n} is a variety (and by the compactness theorem). Thus φ can imply only finitely many of the equations e_{m}, m < ω.

The analogous equations for all n ≥ 3 are the following. Let x, x_{0}, ..., x_{m}, y_{0}, ...y_{m−1} be variables and let ε_{m} denote the following equation^{6}

∏_{i≤m} c_{0}(x · x_{i} · ∏_{i≠j≤m} −x_{j}) ≤ c_{0}c_{1}c_{2} ∏_{j<m} c_{1}x · s_{1}^{0}c_{1}x − [c_{2}y_{j} − c_{2}(s_{2}^{1}c_{2}y_{j} − d_{12})].

■ The class CA_{n} of “n–dimensional cylindric algebras” is defined with the following finite set (of schemas) of equations valid in RCA_{n}. For any i, j, k < n, i, j, k different

6The following simplification is due to Ágnes Kurucz: lhs ≤ c_{0}c_{1}c_{2}([c_{1}x · s_{1}^{0}c_{1}x − ∑ c_{2}y_{j}] + ∑_{j<m}(c_{2}y_{j} · s_{2}^{1}c_{2}y_{j} − d_{12})).

the Boolean equations,

x ≤ c_{i}x = c_{i}c_{i}x, c_{i}(x + y) = c_{i}x + c_{i}y, c_{i} − c_{i}x = −c_{i}x, c_{i}c_{j}x = c_{j}c_{i}x, d_{ii} = 1, d_{ij} = d_{ji} = c_{k}(d_{ik} · d_{kj}), d_{ij} · c_{i}(d_{ij} · x) ≤ x.

Clearly, RCA_{n} ⊂ CA_{n}. The class CA_{n} is considered as an “approximation” of RCA_{n}, and it is of interest to see what kinds of equations are valid in RCA_{n} that do not hold in CA_{n}. The equations in Remark 2 are all such^{7}. CA_{n} is the first member in a sequence of varieties SNr_{n}CA_{m} approximating RCA_{n}. We now define the classes SNr_{n}CA_{m}.

If 𝔄 ∈ CA_{m} and n ≤ m then it is easy to check that the subset Nr_{n}𝔄 = {x ∈ A : x = c_{j}x for all j ≥ n, j < m} is closed under the operations of CA_{n}. Then one defines^{8}

𝔑𝔯_{n}𝔄 = ⟨Nr_{n}𝔄, +^{𝔄}, −^{𝔄}, c_{i}^{𝔄}, d_{ij}^{𝔄}⟩_{i,j<n} and
SNr_{n}CA_{m} = {𝔄 : 𝔄 ⊆ 𝔑𝔯_{n}𝔅 for some 𝔅 ∈ CA_{m}}.

It is easy to check that CA_{n} = SNr_{n}CA_{n} ⊇ SNr_{n}CA_{n+1} ⊇ ... ⊇ RCA_{n}. Henkin[55] proved that RCA_{n} = ⋂{SNr_{n}CA_{n+m} : m < ω} = SNr_{n}CA_{n+k} for all k ≥ ω and Monk[69] proved that RCA_{n} ≠ SNr_{n}CA_{n+m} for all m < ω. Monk[61] proved that SNr_{n}CA_{m} are varieties^{9}.

So the varieties SNr_{n}CA_{n+m} approximate the variety RCA_{n} better and better as m approaches infinity, but they never reach RCA_{n}. Monk[69] asked whether SNr_{n}CA_{n+m} is finitely axiomatizable (if m > 0). The following theorem gives a negative answer for m ≥ 2. For m = 1 an affirmative answer is given in Andréka[90c]. We note that Thm.2 is a generalization of Thm.1, by RCA_{n} = SNr_{n}CA_{n+ω}.

7With the exception of e_{0},ε_{0}.

8Cf. e.g. [HMT71]2.6.28. This class was introduced by Henkin.

9For proof see also [HMT71]2.6.32(ii). Ferenczi[92] investigates the question: for which superclasses K of CA_{n+ω} is it true that RCA_{n} = SNr_{n}K. These questions are related to the proof theory of first–order logic.

THEOREM 2. Let n ≥ 3 and m ≥ 2. Then SNr_{n}CA_{n+m} is not finitely axiomatizable. Moreover SNr_{n}CA_{n+m} is not axiomatizable with any set of quantifier-free formulas containing only finitely many variables.

Proof. Let ⟨ε_{m} : m < ω⟩ be the second sequence of equations in Remark 2. We will show that

(1) SNr_{n}CA_{n+2} ⊧ ε_{m} for all m < ω.

(2) 𝔄 |̸= ε_{m}, where 𝔄 is the algebra constructed in the proof of Thm.1 for the case n ≥ 3, with |U_{0}| = m.

This will prove the theorem because of the following. Let 2 ≤ p and assume that Σ is a set of quantifier-free formulas valid in SNr_{n}CA_{n+p} and using only k variables. Let m ≥ 2^{k} and let 𝔄 be the algebra constructed in the proof of Thm.1 for the case n ≥ 3 with |U_{0}| = m. Then 𝔄 ⊧ Σ by Claim 4 because RCA_{n} ⊆ SNr_{n}CA_{n+p}. But 𝔄 |̸= ε_{m} by (2). Thus 𝔄 ∉ SNr_{n}CA_{n+p} by (1) because SNr_{n}CA_{n+p} ⊆ SNr_{n}CA_{n+2} ⊧ ε_{m}. This shows that Σ is not an axiomatization of SNr_{n}CA_{n+p}.

We now start proving (1). Being in SNr_{n}CA_{n+2} means that, in deriving equations, we can use the operations c_{i}, d_{ij} for i, j ∈ {0, 1, …, n, n + 1}, and apart from the cylindric equations for these we also can use x = c_{n}x = c_{n+1}x if x is a variable. Let us define the following term^{10}:

x ∘ y = c_{n}(s_{n}^{1}x · s_{n}^{0}y).

Clearly, x ∘ 0 = 0. We will prove the following:

(3) x · c_{0}y ≤ (c_{1}x · s_{1}^{0}c_{1}y) ∘ y

(4) x ∘ y ≤ c_{1}x

(5) x ∘ (y + z) = (x ∘ y) + (x ∘ z), (x + y) ∘ z = (x ∘ z) + (y ∘ z)

(6) x ∘ (y · z) = (x ∘ y) · (x ∘ z) if x · s_{2}^{1}x ≤ d_{12}, x = c_{2}x.

(Of these, (3)–(5) hold in SNr_{n}CA_{n+1}, but (6) does not hold in SNr_{n}CA_{n+1}.) Assuming now (3)–(6) above we prove ε_{m}, and after this we will derive (3)–(6).

To simplify notation, let us introduce

X_{i} = x · x_{i} · ∏_{j≠i} − x_{j},

Y_{j} = c_{2}y_{j} − c_{2}(s_{2}^{1}c_{2}y_{j} − d_{12}), X = ∑{X_{i} : i ≤ m}, u = c_{1}X · s_{1}^{0}c_{1}X, g = u · ∏{−Y_{j} : j < m}.

10This is the n–ary version of composition defined e.g. in [HMT85]5.3.7.

Then X ≤ x, and therefore it is enough to prove ∏_{i≤m}c_{0}X_{i} ≤ c_{0}c_{1}g. Clearly the X_{i}’s

are disjoint, X_{i} ≤ X. Also, u ≤ g +∑_{j<m} Y_{j} and we note that c_{i}z ·c_{i}y = c_{i}(z ·c_{i}y) holds in CA_{n}. Also, it is easy to show that Y_{j} · s_{2}^{1}Y_{j} ≤ d_{12}, Y_{j} = c_{2}Y_{j} as follows^{11} . Let z = s_{2}^{1}c_{2}y_{j} −d_{12}. Then c_{2}Y_{j} = c_{2}(c_{2}y_{j} −c_{2}z) = c_{2}y_{j} ·c_{2}−c_{2}z = c_{2}y_{j} −c_{2}z = Y_{j}. Also

Y_{j} · s_{2}^{1}Y_{j} · −d_{12} ≤
−c_{2}(s_{2}^{1}c_{2}y_{j} − d_{12}) · s_{2}^{1}c_{2}y_{j} · −d_{12} ≤
−c_{2}(s_{2}^{1}c_{2}y_{j} − d_{12}) · c_{2}(s_{2}^{1}c_{2}y_{j} − d_{12}) = 0.

Now by the above and (3),(5) we obtain

∏_{i≤m}c_{0}X_{i} = c_{0}X_{0} · c_{0} ∏_{i≤m}c_{0}X_{i} = c_{0}(X_{0} · ∏_{i≤m}c_{0}X_{i}) = c_{0} ∏_{i≤m}(X_{0} · c_{0}X_{i}) ≤

c_{0} ∏_{i≤m}(u ∘ X_{i}) ≤ c_{0} ∏_{i≤m}(g ∘ X_{i} + ∑_{j<m}Y_{j} ∘ X_{i}) =

c_{0} ∑{ ∏_{i≤m}(f_{i} ∘ X_{i}) : f ∈ ^{m+1}{g, Y_{0}, ..., Y_{m−1}}}.

Let f ∈ ^{m+1}{g, Y_{0}, ..., Y_{m−1}}. If g ∈ Rng f then by (5) and (4), ∏{f_{i} ∘ X_{i} : i ≤ m} ≤ g ∘ X ≤ c_{1}g. Assume g ∉ Rng f. Then by |{Y_{j} : j < m}| < m + 1, there are i < j < m + 1 with f_{i} = f_{j}. Then by (6), by Y_{k} · s_{2}^{1}Y_{k} ≤ d_{12}, Y_{k} = c_{2}Y_{k} and by X_{i} · X_{j} = 0 we obtain (f_{i} ∘ X_{i}) · (f_{j} ∘ X_{j}) = 0, hence ∏{f_{i} ∘ X_{i} : i ≤ m} = 0. Thus ∏_{i≤m}c_{0}X_{i} ≤ c_{0}c_{1}g and we are done.

To finish showing SNr_{n}CA_{n+2} ⊧ ε_{m}, we are going to prove (3)–(6). First we note that the following hold in every CA_{m}: Let i, j, k < m.

s_{j}^{i}(x · y) = s_{j}^{i}x · s_{j}^{i}y [HMT71]1.5.3.
s_{j}^{i}c_{i}x = c_{i}x [HMT71]1.5.8(i).
s_{j}^{i}s_{i}^{k}c_{i}y = s_{j}^{k}c_{i}y [HMT71]1.5.11(i).
c_{i}x · c_{i}y = c_{i}(x · c_{i}y) [HMT71]p.162.
c_{i}s_{i}^{k}c_{i}x = c_{k}c_{i}x
s_{j}^{i}s_{k}^{i}x = s_{k}^{i}x [HMT71]1.5.10(i).
s_{k}^{i}d_{ij} = d_{kj} if i ≠ j [HMT71]1.5.4(i).
d_{ij} · s_{i}^{k}x = d_{ij} · s_{j}^{k}x [HMT71]1.5.6.
s_{j}^{i}c_{k}x = c_{k}s_{j}^{i}x if k ∉ {i, j}. [HMT71]1.5.8(ii).

11Actually, it is true in CA_{n}, n ≥ 3 that (y = c_{2}y ∧ y · s_{2}^{1}y ≤ d_{12}) iff y = c_{2}y − c_{2}(s_{2}^{1}c_{2}y − d_{12}).

Proof of (3):

(c_{1}x · s_{1}^{0}c_{1}y) ∘ y = c_{n}(s_{n}^{1}(c_{1}x · s_{1}^{0}c_{1}y) · s_{n}^{0}y) = c_{n}(s_{n}^{1}c_{1}x · s_{n}^{1}s_{1}^{0}c_{1}y · s_{n}^{0}y) = c_{n}(c_{1}x · s_{n}^{0}c_{1}y · s_{n}^{0}y) = c_{n}(c_{1}x · s_{n}^{0}y) = c_{n}(c_{1}c_{n}x · s_{n}^{0}c_{n}y) = c_{n}(c_{n}c_{1}x · s_{n}^{0}c_{n}y) = c_{n}c_{1}x · c_{n}s_{n}^{0}c_{n}y = c_{1}c_{n}x · c_{0}c_{n}y = c_{1}x · c_{0}y ≥ x · c_{0}y.

Proof of (4):

x ∘ y = c_{n}(s_{n}^{1}x · s_{n}^{0}y) ≤ c_{n}s_{n}^{1}x = c_{n}s_{n}^{1}c_{n}x = c_{1}c_{n}x = c_{1}x.

Proof of (5): This is true because c_{n}, s_{n}^{1}, s_{n}^{0} are “additive”. Proof of (6): Assume x · s_{2}^{1}x ≤ d_{12}, c_{2}x = x and let k = n + 1. First we show that s_{n}^{1}x · s_{k}^{1}x = s_{n}^{1}x · d_{nk}.

s_{n}^{1}x · s_{k}^{1}x = s_{n}^{1}x · s_{n}^{1}s_{k}^{1}x = s_{n}^{1}(x · s_{k}^{1}x) = s_{n}^{1}(c_{2}x · s_{k}^{1}c_{2}x) = s_{n}^{1}(s_{k}^{2}c_{2}x · s_{k}^{2}s_{2}^{1}c_{2}x) = s_{n}^{1}s_{k}^{2}(x · s_{2}^{1}x) ≤ s_{n}^{1}s_{k}^{2}d_{12} = d_{nk}, hence s_{n}^{1}x · s_{k}^{1}x = s_{n}^{1}x · s_{k}^{1}x · d_{nk} = s_{n}^{1}x · d_{nk}.

It is proved in [HMT85]p.216 that

c_{n}(s_{n}^{1}x · s_{n}^{0}y) = c_{k}(s_{k}^{1}x · s_{k}^{0}y) if x = c_{n}c_{k}x, y = c_{n}c_{k}y. Now

(x ∘ y) · (x ∘ z) = c_{n}(s_{n}^{1}x · s_{n}^{0}y) · c_{n}(s_{n}^{1}x · s_{n}^{0}z) = c_{n}(s_{n}^{1}x · s_{n}^{0}y · c_{n}(s_{n}^{1}x · s_{n}^{0}z)) = c_{n}(s_{n}^{1}x · s_{n}^{0}y · c_{k}(s_{k}^{1}x · s_{k}^{0}z)) = c_{n}(s_{n}^{1}c_{k}x · s_{n}^{0}c_{k}y · c_{k}(s_{k}^{1}x · s_{k}^{0}z)) = c_{n}(c_{k}s_{n}^{1}x · c_{k}s_{n}^{0}y · c_{k}(s_{k}^{1}x · s_{k}^{0}z)) = c_{n}c_{k}(s_{n}^{1}x · s_{n}^{0}y · s_{k}^{1}x · s_{k}^{0}z) = c_{n}c_{k}(d_{nk} · s_{n}^{1}x · s_{n}^{0}y · s_{k}^{0}z) = c_{n}c_{k}(d_{nk} · s_{n}^{1}x · s_{n}^{0}y · s_{n}^{0}z) =

c_{n}c_{k}(d_{nk} · s_{n}^{1}x · s_{n}^{0}(y · z)) =
c_{n}c_{k}(d_{nk} · s_{n}^{1}c_{k}x · s_{n}^{0}(c_{k}y · c_{k}z)) =
c_{n}c_{k}(d_{nk} · c_{k}(s_{n}^{1}x · s_{n}^{0}(y · z)) =
c_{n}(s_{n}^{1}x · s_{n}^{0}(y · z)) = x ∘ (y · z).

Finally, we prove (2). Let 𝔄 and m be as in the statement of (2). Let us evaluate the variables x, x_{0}, …, x_{m}, y_{0}, …, y_{m−1} to R, R_{0}, …, R_{m}, F_{0}, …, F_{m−1} respectively. Then for all i ≤ m we have R_{i} = R ∩ R_{i} ∩ ⋂_{i≠j≤m} − R_{j}, and so the

left-hand-side of ε_{m} will be c_{0}R ≠ ∅, by c_{0}R_{i} = c_{0}R for all i ≤ m. On the other side, c_{2}F_{j} − c_{2}(s_{2}^{1}c_{2}F_{j} − d_{12}) = F_{j} for all j < m, and thus the right-hand-side of ε_{m} is ∅ by c_{1}R ∩ s_{1}^{0}c_{1}R = U_{0} × U_{0} × U_{2} × ⋯ ⊆ F_{0} ∪ ⋯ ∪ F_{m−1}. This finishes the proof of (2). QED(Theorem 2)

REMARK 3. Let e be an equation valid in RCA_{n}. We say that the “complexity of e is m” if e can be derived with m extra dimensions but e cannot be derived with m − 1 extra dimensions, i.e. if SNr_{n}CA_{n+m} ⊧ e but SNr_{n}CA_{n+m−1} |̸= e if m > 0. It is showed in Andréka[90c] that the members of the second sequence of equations in Remark 2 have all complexity 2 (except ε_{0} whose complexity is 0).

It follows from the results of Henkin and Monk quoted just before Thm.2 that every equation valid in RCA_{n} has a finite complexity and that there are equations of arbitrary big complexities. The question naturally arises whether there are equations of complexity m, for all m < ω. This is asked in Monk[69], and this is Problem 2.12 in [HMT71]. The answer is affirmative for n ≥ ω, this is an unpublished result of Don Pigozzi. The problem for n < ω is still open, only the following partial results are known: Maddux[90] proved that if n = 3 then for every m ≥ 3 there is an equation whose complexity is between m and (3m − 7). Andréka[90c] proved that^{12} for every n ≥ 3, m ≤ n, m < ω there is an equation valid in RCA_{n} whose complexity is m. To prove this, the members e_{m} of the first sequence of equations given in Remark 2 are used, namely it is proved in Andréka[90c] that SNr_{n}CA_{n+m+1} ⊧ e_{m} while SNr_{n}CA_{n+m} |̸= e_{m}. We note that the equation e_{m} is “meaningful” whenever m < n. ■

The next question to ask is which operations cause the nonfinite axiomatizability. One immediately thinks of the cylindrifications as responsible for this, and indeed Johnsson[69] proved that already the diagonal–free reducts of RCA_{n} are not finitely axiomatizable. (The cylindrifications in themselves are finitely axiomatizable see Hansen[92,95], their interconnection with the Boolean operations is so complex as to cause nonfinite axiomatizability.) Do the diagonal constants contribute to nonfinite axiomatizability of RCA_{n}? In other words: Can the behaviour of the diagonal constants be described by finitely many formulas assuming that we know (as an oracle) all the formulas holding for the other operations? An equivalent formulation of this question is whether there is an axiom system for RCA_{n} in which the diagonal constants occur finitely many times only. This question is Problem 1 in Johnson[69] and is restated as Problem 5.4 in the monograph Henkin–Monk–Tarski[HMT85]. The next two theorems give a negative solution to these problems. They state that the diagonal constants are not so “simple” as they seem to be, their interconnections with the Boolean and cylindric operations cannot be described with finitely many variables. (We note that the interconnections of the diagonal constants with the Boolean operations can be described with finitely many formulas (see Proposition 2 in Part II) and the interconnections of the diagonal constants with the cylindrifications clearly can be described with one variable, since the cylindrifications are unary operations.)

12As special cases of the result, it was already known that there are equations of complexity 1 (see Monk[69]), if n = 3 then there are equations of complexities 2 and 3 (see Maddux[90]), and if n ≥ ω, then there are equations of complexity m for all m < ω (Don Pigozzi).

The proofs of the theorems to come are variations of the one of Thm.1. Therefore we state some parts of the proof of Thm.1 as lemmas, because we want to use them several times. In the following lemmas, let α be any set.

LEMMA 1. Let 𝔄 be the subalgebra of ⟨𝔓(^{α}U), c_{i}^{U}, d_{ij}^{U}⟩_{i,j∈α} generated by G ⊆ P(^{α}U). Let S(U) denote the set of all permutations of U and let

F ix(G) = {σ ∈ S(U) : g = {σ ∘ s : s ∈ g} for all g ∈ G}.

Assume that R ∈ A is such that

(*)  (∀s, z ∈ R)(∃σ ∈ F ix(G))σ ∘ s = z.

Then R is an atom of 𝔄.

Proof: For x ⊆ ^{α}U let us write σx for {σ ∘ s : s ∈ x}.^{13} It is easy to check that if σx = x, σy = y then for all i, j ∈ α

σ(x + y) = x + y, σ(−x) = −x, σ(d_{ij}) = d_{ij}, σ(c_{i}x) = c_{i}x.

Thus σx = x for all x ∈ A, σ ∈ F ix(G). Let x ∈ A, and assume that x ∩ R ≠ ∅. We will show R ⊆ x, and this will prove that R is an atom of 𝔄. Let s ∈ x ∩ R and let z ∈ R be arbitrary. Then there is σ ∈ F ix(G) such that z = σ ∘ s, by (*). Then z ∈ x by x ⊆ σx, s ∈ x, z = σ ∘ s. Thus R ⊆ x and we are done. QED(Lemma 1)

13This is denoted by σ̃x in [HMT85],3.1.37.

LEMMA 2. Let m be any cardinal, ⟨U_{i} : i ∈ α⟩ be a system of sets each having cardinality ≥ m, and let U ⊇ ⋃{U_{i} : i ∈ α}. Then there is a partition ⟨R_{j} : j < m⟩ of R = ×_{i∈α}U_{i} such that

c_{i}^{U}R_{j} = c_{i}^{U}R for all i ∈ α and j < m.

Proof: We define an equivalence relation on R: For any s, z ∈ R

s ≡ z ⟺ |{i ∈ α : s_{i} ≠ z_{i}}| < ω.

Let S ⊆ R be a set of representatives for ≡, i.e. S contains exactly one sequence from each block of ≡. Let (Q, +, 0) be any commutative group with Q = {j : j < m}. For any s ∈ S and i ∈ α let f_{i}^{s} : U_{i} ↠ Q be an onto mapping such that f_{i}^{s}(s_{i}) = 0. If x is a finite subset of Q, then we let Σx be the sum of the elements of x, computed in the group (Q, +, 0). We note that s ≡ z implies that f_{i}^{s}(z_{i}) ≠ 0 for only finitely many i < α, so that for s ≡ z, the sum Σ{f_{i}^{s}(z_{i}) : i ∈ α} is always defined. For j < m define

R_{j}^{s} = {z ∈ R : z ≡ s and Σ{f_{i}^{s}(z_{i}) : i ∈ α} = j},
R_{j} = ⋃{R_{j}^{s} : s ∈ S}.

Now clearly, ⟨R_{j} : j < m⟩ is a partition of R.

Let i ∈ α, j < m and z ∈ R. We want to show z ∈ c_{i}^{U}R_{j}. Let s ∈ S be such that z ≡ s. Let u ∈ Q be such that u+Σ{f_{l}^{s}(z_{l}) : l ∈ α, l ≠ i} = j. Then z(i/u) ∈ R_{j}, hence z ∈ c_{i}^{U}R_{j}. QED(Lemma 2)

DEFINITION. If 𝔅 is a Boolean algebra and f : B ⟶ B then we say that f is additive if f(x + y) = f(x) + f(y) for all x, y ∈ B. Let 𝔄 be any Boolean algebra with additive operations c_{i}, i ∈ α and possibly with some extra constants. Let m be any cardinal and let R be any atom of 𝔄 (i.e. any atom of the Boolean part of 𝔄). We say that the algebra 𝔄′ is obtained from 𝔄 by splitting R into m parts R_{j}, j < m if the following (i)-(iv) hold^{14}.

(i) 𝔄′ is a Boolean algebra with additive operations c′_{i}, i ∈ α and with the same constants as 𝔄.

(ii) 𝔄 ⊆ 𝔄′.

(iii) c′_{i}R_{j} = c_{i}R for all j < m and i ∈ α, and ⟨R_{j} : j < m⟩ is a partition of R. (iv) Each element of 𝔄′ is a (Boolean) join of an element of 𝔄 and of finitely or

cofinitely (in m) many R_{j}’s, i.e. for any x ∈ A′ there are a ∈ A and J ⊆ m such that x = a + ∑{R_{j} : j ∈ J} and either J or m ∖ J is finite.

14Though we call 𝔄′ obtained from 𝔄 by splitting, this is not a special case of splitting as described in [HMT71]2.6.12. This is a special case of “dilation” as described in [HMT85]3.2.69 (we take a_{κ} = a_{λ} for all κ, λ ∈ α). The name “splitting” is justified by aiming in both constructions at having disjoint elements ⟨a_{j} : j < m⟩ such that c_{i}a_{j} = c_{i}a_{0} for all i ∈ α, j < m.

It is easy to check that for any 𝔄, R, m as in the hypothesis part of the definition, there is, up to isomorphism, exactly one 𝔄′ satisfying (i)–(iv). We shall denote the algebra obtained from 𝔄 by splitting R into m parts with split(𝔄, R, m). ■

Since split(𝔄, R, m) is defined only up to isomorphism, everything in the following lemma is understood up to isomorphism. Let 𝔄, 𝔅 be not necessarily similar algebras and let h : A ⟶ B. Let f be a common operation symbol of 𝔄 and 𝔅. We say that h : 𝔄 ⟶ 𝔅, or h : A ⟶ B, is a \underline{homomorphism w.r.t. f} if h : (A, f^{𝔄}) ⟶ (B, f^{𝔅}) is a homomorphism. We say that h : 𝔄 ⟶ 𝔅 is a Boolean homomorphism if h is a homomorphism w.r.t. the Boolean operations +, −.

LEMMA 3. Let 𝔄, 𝔅 be Boolean algebras with additive operations c_{i}, i ∈ α and, possibly, with additional constants, let R be an atom of 𝔄, and m, m_{1}, m_{2}, k be nonzero cardinals, k < ω. Then (1)–(5) below hold.

(1) 𝔄 = split(𝔄, R, 1) and split(𝔄, R, m_{1}) ⊆ split(𝔄, R, m_{2}) if m_{1} ≤ m_{2}.

(2) c_{i}a ∈ A for all i ∈ α and a ∈ split(𝔄, R, m).

(3) Any k–generated subalgebra of split(𝔄, R, m) is a subalgebra of split(𝔄, R, 2^{k}).

(4) Let Z be an atom of 𝔅 and let h : 𝔄 ⟶ 𝔅 be a Boolean homomorphism taking R to Z. Let m_{1} ≤ m_{2}. Then there is an extension \overline{h} of h with the following properties for all i ∈ α: \overline{h} : split(𝔄, R, m_{1}) ⟶ split(𝔅, Z, m_{2}) is a Boolean homomorphism. \overline{h} is a homomorphism w.r.t. c_{i} iff h is such. \overline{h} is one–to–one iff h is such.

(5) Assume that h : 𝔄 ↣ ⟨𝔓(^{α}U), c_{i}^{U}, d_{ij}^{U}⟩_{i,j∈α} is a Boolean embedding and h(R) = ×_{i∈α}U_{i} such that ⟨U_{i} : i ∈ α⟩ is a system of disjoint sets each

having cardinality ≥ m. Then h can be extended to a Boolean embedding \overline{h} : split(𝔄, R, m) ↣ ⟨𝔓(^{α}U), c_{i}^{U}, d_{ij}^{U}⟩_{i,j∈α} such that \overline{h} is a homomorphism w.r.t. the same operations of split(𝔄, R, m) w.r.t. which h is such.

Proof: Checking \underline{(2)} and 𝔄 = split(𝔄, R, 1) is straightforward by using the definition of split(𝔄, R, m).

\underline{(4):} For any set H, let Cof(H) denote the set of all finite and cofinite subsets of H. Assume m_{1} ≤ m_{2} and let χ : m_{1} ⟶ Cof(m_{2}) be such that

the sets χ(j), j < m_{1} are nonempty and pairwise disjoint, and

⋃{χ(j) : j < m_{1}} = m_{2} if m_{1} < ω.

Let ρ = m_{2} ∖ ⋃{χ(j) : j < m_{1}}. For any x ∈ split(𝔄, R, m_{1}) let J(x) = {j < m_{1} : R_{j} ≤ x} and define

\overline{h}(x) = \{ \begin{matrix}h(x − R) + ∑\{Z_{i} : i ∈ ⋃\{χ(j) : j ∈ J(x)\}\} & if |J(x)| < ω \\ h(x − R) + ∑\{Z_{i} : i ∈ ⋃\{χ(j) : j ∈ J(x)\} ∪ ρ\} & if |J(x)| ≥ ω. \end{matrix}

It is easy to check that \overline{h} is a Boolean homomorphism into split(𝔅, Z, m_{2}), \overline{h} is an extension of h and \overline{h}(x) ≠ 0 whenever 0 ≠ x ≤ R. Thus \overline{h} is one–to–one iff h is such. Let i ∈ α and x ∈ split(𝔄, R, m_{1}). Assume that h is a homomorphism w.r.t. c_{i}. If x · R = 0 then x ∈ A, hence \overline{h}(c_{i}x) = h(c_{i}x) = c_{i}h(x) = c_{i}\overline{h}(x). So assume x · R ≠ 0. Then c_{i}(x · R) = c_{i}R and c_{i}(\overline{h}(x · R)) = c_{i}Z by 0 ≠ \overline{h}(x · R) ≤ Z. Now

\overline{h}(c_{i}x) = \overline{h}(c_{i}(x − R) + c_{i}(x · R)) = c_{i}h(x − R) + c_{i}h(R), and

c_{i}\overline{h}(x) = c_{i}(\overline{h}((x−R)+(x·R)) = c_{i}(h(x−R)+\overline{h}(x·R)) = c_{i}h(x−R)+c_{i}Z.

Thus \overline{h}(c_{i}x) = c_{i}\overline{h}(x) by h(R) = Z. \underline{(4)} has been proved.

The second part of \underline{(1)}, i.e. split(𝔄, R, m_{1}) ⊆ split(𝔄, R, m_{2}) if m_{1} ≤ m_{2} follows immediately from (4).

\underline{(5):} Let everything be as in the hypothesis part of (5). Let ⟨R′_{j} : j < m⟩ be a partition of R′ = ×_{i∈α}U_{i} which exists by Lemma 2, i.e. c_{i}^{U}R′_{j} = c_{i}^{U}R′ for all i ∈ α

and j < m. Define for all x ∈ split(𝔄, R, m)

\overline{h}(x) = h(x − R) + ∑\{R′_{j} : R_{j} ≤ x\}.

It is easy to check, exactly as above in the proof of (4), that \overline{h} satisfies the requirements in (5).

\underline{(3):} Let 𝔄′ be obtained from 𝔄 by splitting R into m parts R_{j}, j < m and let 𝔄′′ be the subalgebra of 𝔄′ generated by some G ⊆ 𝔄′, |G| ≤ k. We want to show 𝔄′′ ⊆ split(𝔄, R, 2^{k}).

We define an equivalence relation ≡ on m as follows. For all i, j < m

i ≡ j iff (∀g ∈ G)[R_{i} ≤ g ⟺ R_{j} ≤ g].

Then ≡ has ≤ 2^{k} blocks by |G| ≤ k. Define

B = {a ∈ 𝔄′ : (∀i, j < m)[i ≡ j and R_{j} ≤ a ⟹ R_{i} ≤ a]}.

We now show that B is closed under the operations of 𝔄′. B clearly is closed under the Boolean operations. Clearly, A ⊆ B since R is an atom of 𝔄. Hence c_{i}b ∈ B for all i ∈ α, b ∈ B by (2), and all the constants of 𝔄 are in B. Let 𝔅 be the subalgebra of 𝔄′ with universe B. Clearly, G ⊆ B, hence 𝔄′′ ⊆ 𝔅 and so it is enough to show 𝔅 ⊆ split(𝔄, R, 2^{k}).

First we show that there is at most one infinite block of ≡. Indeed, assume that J_{1}, J_{2} are infinite blocks of ≡, and let i ∈ J_{1}, j ∈ J_{2}. By i ≢ j there is g ∈ G such thatR_{i} ≤ g and R_{j} ≰ g or R_{j} ≤ g and R_{i} ≰ g. We may assume R_{i} ≤ g, R_{j} ≰ g. Then R_{l} ≤ g for all l ∈ J_{1} and R_{l} ≰ g for all l ∈ J_{2}. This is a contradiction by {l < m : R_{l} ≤ g} ∈ Cof(m). Thus there is at most one infinite block of ≡. Let p be the number of blocks of ≡. Since k < ω and p ≤ 2^{k}, then ≡ has finitely many blocks. Thus if ≡ has an infinite block, it has to be cofinite. Let ⟨J_{l} : l < p⟩ be the partition belonging to ≡. For any l < p define

R′_{l} = ∑{R_{j} : j ∈ J_{l}}.

This sum always exists because J_{l} ∈ Cof(m) by the above. Then ⟨R′_{l} : l < p⟩ is a partition of R in 𝔅, i.e. R′_{l} are disjoint, nonzero elements of 𝔅 such that ∑{R′_{l} : l < p} = R. Also, c′_{i}R′_{l} = c_{i}R for all l < p and i ∈ α, and |{R′_{l} : l < p}| = p. Clearly, 𝔄 ⊆ 𝔅 ⊆ split(𝔄, R, m), hence conditions (i)–(iii) in the definition of split(𝔄, R, p) are satisfied. Finally, we check condition (iv). Let x ∈ B. Then x = a + ∑{R_{j} : j ∈ J} for some a ∈ A and J ∈ Cof(m) such that J is a union of some blocks of ≡. Let J′ = {l < p : J_{l} ⊆ J}. Then clearly ∑{R_{j} : j ∈ J} = ∑{R′_{j} : j ∈ J′} and we are done. Therefore condition (iv) also holds, so 𝔅 ≅ split(𝔄, R, p). QED(Lemma 3)

We will need one more lemma. For any σ ∈ ^{α}α and any set x of α–sequences let s_{σ}(x) = {s : s ∘ σ ∈ x}. We will use the part of Lemma 4 below concerning s_{σ} later in Theorem 6.

LEMMA 4. Let U, W be sets and let g : ^{α}W ⟶ ^{α}U. Let h : P(^{α}U) ⟶ P(^{α}W) be defined by

h(x) = {s ∈ ^{α}W : g(s) ∈ x}

for all x ⊆ ^{α}U. Then (i)–(iii) below hold for all i, j ∈ α and x ⊆ ^{α}U:

(i) h is a Boolean homomorphism.

(ii) h(d_{ij}^{U}) = d_{ij}^{W} iff (∀s ∈ ^{α}W)[s_{i} = s_{j} ⟺ g(s)_{i} = g(s)_{j}].

(iii) c_{i}^{W} h(x) = h(c_{i}^{U}x) iff for all s ∈ ^{α}W we have

[(∃u ∈ U)g(s)(i/u) ∈ x ⟺ (∃w ∈ W)g(s(i/w)) ∈ x]. (iv) Assume that t_{i} : W ⟶ U for all i ∈ α, W ≠ ∅ and g is such that

g(s)_{i} = t_{i}(s_{i}) for all s ∈ ^{α}W, i ∈ α. Let i ∈ α and σ ∈ ^{α}α. Then h is a homomorphism w.r.t. c_{i} iff t_{i} is onto U, h is one–one iff (t_{i} is onto U for all i ∈ α), h is a homomorphism w.r.t. s_{σ} iff (t_{i} = t_{σ(i)} for all i ∈ α).

Proof: The proofs of (i),(ii) are straightforward, therefore we omit them. The proof of (iii) is straightforward, too, but we include it. Let s ∈ ^{α}W. Then

s ∈ c_{i}^{W} h(x) iff (∃w ∈ W)s(i/w) ∈ h(x) iff (∃w ∈ W)g(s(i/w)) ∈ x

and

s ∈ h(c_{i}^{U}x) iff g(s) ∈ c_{i}^{U}x iff (∃u ∈ U)g(s)(i/u) ∈ x,

which immediately imply (iii). \underline{(iv):} It is easy to check that

g(s(i/w)) = g(s)(i/t_{i}w) for all s ∈ ^{α}W, i ∈ α, w ∈ W

therefore h is a homomorphism w.r.t. c_{i} if t_{i} is onto U by (iii). Let x ⊆ ^{α}W, s ∈ x. If t_{i} is onto U for all i ∈ α, then there is z ∈ ^{α}W such that s_{i} = t_{i}z_{i} for all i ∈ α, thus z ∈ h(x). This shows that h is one–one if t_{i} are onto U for all i ∈ α. Assume that t_{i} = t_{σi} for all i ∈ α. Then

g(s ∘ σ) = g(s) ∘ σ for all s ∈ ^{α}W

because for i ∈ α, g(s∘σ)_{i} = t_{i}(s∘σ)_{i} = t_{i}(s_{σi}) and (g(s)∘σ)_{i} = g(s)_{σi} = t_{σi}(s_{σi}). Then s ∈ h(s_{σ}x) iff g(s) ∈ s_{σ}(x) iff g(s) ∘ σ ∈ x iff g(s ∘ σ) ∈ x iff s ∘ σ ∈ h(x) iff s ∈ s_{σ}h(x). Thus h is a homomorphism w.r.t. s_{σ}. We are going to check the “only if” parts. Assume that u ∈ U ∖ Rng t_{i} and let s ∈ ^{α}W be arbitrary. Let z = g(s)(i/u). Then h({z}) = 0 and s ∈ h(c_{i}{z}), s ∉ c_{i}h({z}) showing that h is not one–one and is not a homomorphism w.r.t. c_{i}. Let σ ∈ ^{α}α, i ∈ α and assume that t_{i} ≠ t_{σi}, say t_{i}(w) ≠ t_{σi}(w). Let z ∈ ^{α}W be such that z_{i} = w and let x = {g(z ∘ σ)}. Then g(z ∘ σ) ≠ g(z) ∘ σ and so z ∈ s_{σ}h(x) but z ∉ h(s_{σ}x). QED(Lemma 4)

We are ready to state Thm.3. Let _{∞}Cs_{n} denote the class of all Cs_{n}’s with greatest elements of form ^{n}U with U infinite.

THEOREM 3. Let Σ be a set of quantifier–free formulas axiomatizing RCA_{n}, n ≥ ω. Let k be any natural number and let ℓ < n. Then Σ contains infinitely many formulas in which at least one diagonal constant with index ℓ, more than k cylindrifications, and more than k variables occur. The same holds with K in place of RCA_{n} for any K such that _{∞}Cs_{n} ⊆ K ⊆ RCA_{n}.

Proof: \underline{PLAN:} Assume first that ℓ = 0. At the end of the proof we will show how to eliminate this assumption.

Let Σ and k be as in the statement of the theorem. Let 𝔄_{k} be the algebra constructed in the proof of Theorem 1. We will prove the following:

(i) For any I ⊆ n, |I| ≤ k there is a representation of 𝔄_{k} as a _{∞}Cs_{n} in which all the operations are the natural ones except for c_{i}, i ∉ I.

(ii) There is a representation of 𝔄_{k} as a _{∞}Cs_{n} in which all the operations are the natural ones except for d_{0i}, d_{i0}, i < n.

I_{∞}Cs_{n} denotes the class of all algebras isomorphic to an element of _{∞}Cs_{n}. We proved in Theorem 1 that

(iii) Any k–generated subalgebra of 𝔄_{k} is representable, in fact in I_{∞}Cs_{n} .

This will prove the theorem because of the following: Let _{∞}Cs_{n} ⊆ K ⊆ RCA_{n}. Let Σ^{c} denote the set of all quantifier–free formulas valid in K which contain at most k cylindrifications, Σ^{d} denote the set of all quantifier–free formulas valid in K which contain no diagonal with index 0 and let Σ^{v} denote the set of all quantifier– free formulas valid in K which contain at most k variables. By (i)–(iii) above and ∞Cs_{n} ⊆ K we have that 𝔄_{k} ⊧ Σ^{c} ∪ Σ^{d} ∪ Σ^{v} (an argument for this is given below). Since 𝔄_{k} is not in RCA_{n} by Claim 1, and since K ⊆ RCA_{n}, we have 𝔄_{k} |̸= Σ. Thus Σ ⊈ Σ^{c} ∪ Σ^{d} ∪ Σ^{v}, which means that Σ contains a formula with more than k cylindrifications, more than k variables and with a diagonal constant with index 0.

We can show that (i)–(iii) imply 𝔄_{k} ⊧ Σ^{c} ∪ Σ^{d} ∪ Σ^{v} as follows. Let 𝔄 = 𝔄_{k}. First we show that (i) implies 𝔄 ⊧ Σ^{c}. Let φ ∈ Σ^{c}, say φ contains only c_{i} with i ∈ I where |I| ≤ k. By (i), there is a representation of 𝔄 as a ∞Cs_{n} in which all the operations are the natural ones, except for c_{i}, i ∉ I. This means that there is a one-one homomorphism h : 𝔄^{c} ↣ 𝔓^{c} where 𝔄^{c} = ⟨A, +^{𝔄}, −^{𝔄}, c_{i}^{𝔄}, d_{jk}^{𝔄}⟩_{i∈I,j,k<n} and 𝔓^{c} = ⟨𝔓(^{n}W), c_{i}^{W} , d_{jk}^{W}⟩_{i∈I,j,k<n} for some infinite set W. Let 𝔓 = ⟨𝔓(^{n}W), c_{i}^{W} , d_{ij}^{W} ⟩_{i,j<n}. Now 𝔓 ⊧ φ because φ is valid in K and 𝔓 ∈ _{∞}Cs_{n} ⊆ K, thus 𝔓^{c} ⊧ φ because no c_{i} with i ∉ I occurs in φ. Then 𝔄^{c} ⊧ φ because 𝔄^{c} is isomorphic to a subalgebra of 𝔓^{c} and φ is quantifier–free. Therefore 𝔄 ⊧ φ. The proofs of 𝔄 ⊧ Σ^{d}, 𝔄 ⊧ Σ^{v} are similar, we omit them.

We could prove (i)–(iii) above for the algebras 𝔄_{k} constructed in the proof of Theorem 1. However, to make the proof simpler, we will use modified versions of the algebras used in the proof of Theorem 1.

\underline{CONSTRUCTION OF 𝔄:} Let m ≥ 2^{k}, m < ω and let ⟨U_{i} : i ≤ n⟩ be a system of disjoint sets such that |U_{0}| = m and |U_{i}| > n for all i > 0. Let

U = ⋃{U_{i} : i ≤ n},

R = ×_{i<n}U_{i}, and let

𝔄′ be the subalgebra of ⟨𝔓(^{n}U), c_{i}^{U}, d_{ij}^{U}⟩_{i,j<n} generated by R.

Then R is an atom of 𝔄′, because it satisfies (*) in Lemma 1. Let 𝔄 be the algebra we obtain from 𝔄′ by splitting R into m + 1 new atoms R_{j}, j ≤ m. The proof of 𝔄 ∉ RCA_{n} is exactly the same as the proof of Claim 1. The proof of (iii) (i.e. that the k–generated subalgebras of 𝔄 are in I_{∞}Cs_{n}’s) is basically the same as that of Claim 2, but now we can use our lemmas: Let 𝔅 be a k–generated subalgebra of 𝔄. Then 𝔅 ⊆ split(𝔄′, R, 2^{k}) ⊆ split(𝔄′, R, m) by Lemma 3(3),(1), and split(𝔄′, R, m) is in _{∞}Cs_{n} by Lemma 3(5), hence 𝔅 is in _{∞}Cs_{n}, too.

We now want to show that 𝔄 can be represented in such a way that only some cylindrifications are not “real”.

Let W be any set such that U ⫋ W and |W ∖ U| < ω.

CLAIM 5. For any I ⊆ n, |I| = m there is an embedding h : A ↣ ⟨𝔓(^{n}W), c_{i}^{W} , d_{ij}^{W} ⟩_{i,j<n} which is a homomorphism w.r.t. all operations of 𝔄 except for c_{i}, i ∉ I.

Proof: Let W_{0} = U_{0} ∪(W ∖U), and W_{i} = U_{i} for all 0 < i ≤ n. First we define an embedding h : A′ ↣ P(^{n}W) with the above properties such that h(R) = ×_{i<n}W_{i}.

Let S ⊆ W_{0} × W_{0} be such that every element of W_{0} is in relation with exactly m elements including itself, i.e.

{(w, w) : w ∈ W_{0}} ⊆ S  and  |{v ∈ W_{0} : v S w}| = m for all w ∈ W_{0}.

Some notation: For any functions f, f′ and set Ω we define f[Ω/f′] = f ↾ (Dom f ∖ Ω) ∪ f′ ↾ Ω. For a function f, kerf = {(i, j) : i, j ∈ Domf and f(i) = f(j)}. We note that if n is an ordinal, then we consider n = {m : m < n} and a sequence s ∈ ^{n}W is considered to be a function mapping n to W. Using S, we will define a function g : ^{n}W ⟶ ^{n}U. Let s ∈ ^{n}W be arbitrary. Let Ω_{s} = Ω = {i < n : s_{i} ∈ W_{0}}.

Assume Ω ⊆ I. Let s′ ∈ ^{Ω}U_{0} be such that ker(s′) = ker(s ↾ Ω). Such an s′ exists by |Ω| ≤ |I| = m = |U_{0}|. We define

g(s) = s[Ω/s′].

Assume Ω ⊈ I. Let μ = min(Ω ∖ I), the smallest element of the set Ω ∖ I of ordinals. Let s′ ∈ ^{Ω}U be such that for all j ∈ Ω,

s′_{j} ∈ U_{0} if s_{j} S s_{μ}
s′_{j} ∈ U_{n} ∖ Rng(s) if s_{j} S̸ s_{μ}, and
ker(s′) = ker(s ↾ Ω).

Such an s′ exists by |{v : v S s_{μ}}| ≤ m = |U_{0}| and by |U_{n}| > n. We again define

g(s) = s[Ω/s′].

By the above, we defined g : ^{n}W ⟶ ^{n}U. We define h : A′ ⟶ P(^{n}W) by

h(x) = {s ∈ ^{n}W : g(s) ∈ x} for all x ∈ A′.

We begin with showing h(R) = ×_{i<n}W_{i}. Let s ∈ ^{n}W and Ω = {i < n : s_{i} ∈ W_{0}}.

Proof of s ∈ ×_{i<n}W_{i} ⟹ s ∈ h(R) : (Here we will use Id_{W_{0}} ⊆ S.) Assume s ∈ ×_{i<n}W_{i}.

Then Ω = {0}. If 0 ∈ I then Ω ⊆ I and hence g(s)_{0} ∈ U_{0}. If 0 ∉ I then 0 = min(Ω ∖ I) and hence g(s)_{0} ∈ U_{0} by s_{0} S s_{0}. Thus, in both cases g(s)_{0} ∈ U_{0}. Let 0 < i < n. Then i ∉ Ω, hence g(s)_{i} = s_{i} ∈ W_{i} = U_{i}. We have seen g(s) ∈ ×_{i<n}U_{i} = R. Proof of s ∈ h(R) ⟹ s ∈ ×_{i<n}W_{i}: Assume g(s) ∈ R and let

i < n. Then g(s)_{i} ∈ U_{i}, hence g(s)_{i} ∉ U_{n} because U_{i} and U_{n} are disjoint from each other. By inspecting the definition of g, we can see that this implies s_{i} ∈ W_{i}. Thus h(R) = ×_{i<n}W_{i} is proved.

We turn to proving that h is a one–one homomorphism w.r.t. all operations except for c_{i}, i ∉ I.

By Lemma 4, h is a homomorphism w.r.t. the Boolean operations. Therefore to show that h is one–one, it is enough to show that h(x) ≠ 0 whenever x ≠ 0.

We define an equivalence relation ≡ on ^{H}W, for any set H. Let s, z ∈ ^{H}W. Then we define

s ≡ z iff [ker(s) = ker(z) and (∀l ≤ n)(∀i ∈ H)(s_{i} ∈ W_{l} ⇔ z_{i} ∈ W_{l})].

In other words, s ≡ z iff there is a permutation π of W such that π^{∗}W_{l} = W_{l} for all l ≤ n and z = π ∘ s. This is true because |W ∖ U| < ω. Therefore each element of A′ is closed w.r.t. ≡, i.e. for all s, z ∈ ^{n}U

s ∈ x and z ≡ s implies z ∈ x

for all x ∈ A′. In the following, we will use this fact several times. If u, v ∈ W then we define u ≡ v to hold iff ⟨u⟩ ≡ ⟨v⟩.

In the rest of the proof we will often use the following properties of the function g (these properties are easy to check). Let s ∈ ^{n}W, Ω = {i < n : s_{i} ∈ W_{0}}, w ∈ W and i ∈ I.

(G1) ker(g(s)) = ker(s) (G2) g(s) ≡ s if Ω ⊆ I. (G3) g(s) ↾ (n ∖ {i}) ≡ g(s(i/w)) ↾ (n ∖ {i}).

We now turn to proving that h is one–one. Let x ∈ A′, x ≠ 0. Let s ∈ x be arbitrary and Ω = {i < n : s_{i} ∈ U_{0}}. If Ω ⊆ I then s ≡ g(s) by (G2). Hence g(s) ∈ x, therefore s ∈ h(x) showing that h(x) ≠ 0. Assume Ω ⊈ I and let μ = min(Ω ∖ I). Let u ∈ U_{0} be arbitrary and let s′ ∈ ^{Ω}({v ∈ W_{0} : v S u}) be such that s′_{μ} = u and ker(s′) = ker(s ↾ Ω). Such an s′ exists by s ↾ Ω ∈ ^{Ω}U_{0} and |U_{0}| = |{v ∈ W_{0} : v S u}|. Let z = s[Ω/s′]. Then g(z) ≡ s, hence z ∈ h(x) showing h(x) ≠ 0.

By Lemma 4 and (G1), h is a homomorphism for all d_{ij}, i, j < n.

Let i ∈ I and x ∈ A′. We want to show h(c_{i}^{U}x) = c_{i}^{W} h(x). By Lemma 4, we have to show that for all s ∈ ^{n}W,

(∃u ∈ U)g(s)(i/u) ∈ x  iff  (∃w ∈ W)g(s(i/w)) ∈ x.

Let s ∈ ^{n}W be arbitrary. Let Ω = {i < n : s_{i} ∈ W_{0}}, and let μ = min(Ω ∖ I) if Ω ∖ I is nonempty. Let u ∈ U and w ∈ W be arbitrary. First we show that

g(s)(i/u) ≡ g(s(i/w))

whenever one of (1),(2) below hold.

(1) u = g(s)_{j} and w = s_{j} for some j ∈ n ∖ {i}.

(2) u ∉ {g(s)_{j} : j ∈ n ∖ {i}}, w ∉ {s_{j} : j ∈ n ∖ {i}}, and either u ≡ w, (w ∈ W_{0}, Ω ⊈ I ⟹ w S s_{μ}), or u ∈ U_{n}, w ∈ W_{0}, Ω ⊈ I, w S̸ s_{μ}.

Indeed, let p = g(s)(i/u) and q = g(s(i/w)). By i ∈ I and (G3) we have p ↾ (n ∖ {i}) ≡ q ↾ (n ∖ {i}). Thus we have only to show p_{i} ≡ q_{i} and (p_{i} = p_{l} iff q_{i} = q_{l}) for all l ∈ n ∖ {i}.

Assume that (1) holds. Then u = p_{i} = p_{j}. By w = s_{j} we have (i, j) ∈ ker(s(i/w)) = ker(q), thus q_{i} = q_{j}. By p ↾ (n ∖ {i}) ≡ q ↾ (n ∖ {i}), j ≠ i we have p_{j} ≡ q_{j}, therefore p_{i} = p_{j} ≡ q_{j} = q_{i}. Let l ∈ n ∖ {i} be arbitrary. Then by (G1), p_{i} = p_{l} iff u = p_{j} = p_{l} iff(by ker(g(s)) = ker(s)) s_{j} = s_{l} iff(by ker(s(i/w)) = ker(q)) q_{j} = q_{l} iff(by q_{i} = q_{j}) q_{i} = q_{l}.

Assume now that (2) holds. Let l ∈ n ∖ {i} be arbitrary. Then p_{i} = u ≠ g(s)_{l} = p_{l} and, by letting z = s(i/w), z_{i} = w ≠ s_{l} = z_{l}, hence q_{i} ≠ q_{l} by (G1). Assume u ≡ w and (w ∈ W_{0}, Ω ⊈ I ⟹ w S s_{μ}). Then either w ∉ W_{0} or Ω ⊆ I or w ∈ W_{0}, w S s_{μ}. In all these three cases q_{i} ≡ w (by q = g(s(i/w)), i ∈ I), thus q_{i} ≡ w ≡ u = p_{i}. Assume u ∈ U_{n}, w ∈ W_{0}, Ω ⊈ I, w S̸ s_{μ}. Then g(s(i/w))_{i} ∈ U_{n} therefore q_{i} ≡ u = p_{i}.

By the above, to show that h is a homomorphism w.r.t. c_{i}, it is enough to show that for any u ∈ U there is w ∈ W satisfying (1) or (2), and vice versa, for any w ∈ W there is u ∈ U satisfying (1) or (2). We are now going to check this.

Let u ∈ U be arbitrary. If u = g(s)_{j} for some j ∈ n ∖ {i} then let w = s_{j}. Then (1) is satisfied. Assume that u ∉ {g(s)_{j} : j ∈ n ∖ {i}}. If u ∉ U_{0} then there is w ≡ u with w ∉ {s_{j} : j ∈ n ∖ {i}} by |U_{l}| > n for all l > 0. This w will satisfy (2). Assume now u ∈ U_{0}. Assume further Ω ⊆ I. Then |U_{0} ∩ {s_{j} : j ∈ n ∖ {i}}| = |U_{0} ∩ {s_{j} : j ∈ I ∖ {i}}| < m by |I| = m, i ∈ I. Thus there is w ∈ U_{0} ∖ {s_{j} : j ∈ n ∖ {i}} by |U_{0}| = m, and this w will then satisfy (2). Assume now Ω ⊈ I. By u ∈ U_{0} ∖ {g(s)_{j} : j ∈ n ∖ {i}} and |U| = m we have |U_{0} ∩ {g(s)_{j} : j ∈ n ∖ {i}}| < m. By our construction, g(s)_{j} ∈ U_{0} iff s_{j} S s_{μ}, for all j ∈ n. By (G1) then |{s_{j} : s_{j} S s_{μ}, j ∈ n ∖ {i}}| < m. Since |{w ∈ W_{0} : w S s_{μ}}| = m by our assumption on S, there is w ∈ W_{0} ∖ {s_{j} : j ∈ n ∖ {i}} such that w S s_{μ}. This w satisfies (2).

Conversely, let w ∈ W_{0} be arbitrary. If w = s_{j} for some j ≠ i then let u = g(s)_{j}. Then (1) is satisfied. Assume that w ∉ {s_{j} : j ∈ n ∖ {i}}. If w ∉ W_{0} then there is u ≡ w with u ∉ {g(s)_{j} : j ∈ n ∖ {i}} by |U_{l}| > n for all l > 0. Assume w ∈ W_{0}. Assume further Ω ⊆ I. Then by g(s)_{j} ∈ U_{0} ⟹ s_{j} ∈ W_{0} for all j, we have {j ∈ n ∖ {i} : g(s)_{j} ∈ U_{0}} ⊆ {j ∈ n ∖ {i} : s_{j} ∈ W_{0}} ⊆ I ∖ {i}, then by |I ∖ {i}| = m − 1, |U_{0}| = m there is u ∈ U_{0} ∖ {g(s)_{j} : j ∈ n ∖ {i}}. This u will satisfy (2). Assume now Ω ⊈ I, w S s_{μ}. Then {j ∈ n ∖ {i} : g(s)_{j} ∈ U_{0}} ⊆ J = {j ∈ n ∖ {i} : s_{j} S s_{μ}}, then by w ∉ {s_{j} : j ∈ n ∖ {i}}, w S s_{μ}, we have |{s_{j} : j ∈ J}| < m, thus there is u ∈ U_{0} ∖ {g(s)_{j} : j ∈ n ∖ {i}}. This u satisfies (2). Assume finally Ω ⊈ I, w S̸ s_{μ}. Then let u ∈ U_{n} ∖ {g(s)_{j} : j ∈ n ∖ {i}} be arbitrary. Such a u exists by |U_{n}| > n, and this u satisfies (2).

We have checked that h is a homomorphism w.r.t. c_{i}, i ∈ I.

By the above we have shown that h is a one–to–one homomorphism for all operations of 𝔄′ except perhaps for c_{i}, i ∉ I. We note that h is not a homomorphism w.r.t. c_{i} if i ∉ I, i ≠ 0. To see this, let i ∉ I, i ≠ 0, j ∈ I, j ≠ 0. (We may assume m > 2, so we do have such a j.) Let x = c_{0}(d_{0j} · c_{j}R). Let s ∈ ^{n}W be such that

s_{i}, s_{j} ∈ W_{0}, s_{j} S̸ s_{i}
s_{k} ∈ U_{k} if k ≠ i, j, 0, s_{0} ∉ W_{0}.

Then Ω_{s} = {i, j} ⊈ I, μ = i. By g(s)_{j} ∈ U_{n} then g(s)_{j} ∉ U_{0}, so g(s) ∉ c_{i}x, hence s ∉ h(c_{i}x). On the other hand, let w ∈ U_{i}, and z = s(i/w). Then Ω_{z} = {j} ⊆ I, so g(z) ≡ z ∈ x. Hence s ∈ c_{i}h(x).

Now, Lemma 3(5) finishes the proof of Claim 5. QED(Claim 5)

CLAIM 6. There is an embedding h : A ↣ ⟨𝔓(^{n}W), c_{i}^{W} , d_{ij}^{W} ⟩_{i,j<n} such that h is a homomorphism w.r.t. all operations of 𝔄 except for d_{0i}, d_{i0}, i < n.

Proof: By Lemma 3(5), it is enough to show that there is an embedding

h : A′ ↣ ⟨𝔓(^{n}W), c_{i}^{W} , d_{ij}^{W} ⟩_{i,j<n} such that h(R) = ×_{i∈n}W_{i} and h is a homomorphism

w.r.t. all operations of 𝔄′ except for d_{0i}, d_{i0}, i < n.

Let t, r : W ⟶ U be functions such that

t, r are identity on U ∖ U_{n},
t^{∗}(W ∖ U) ⊆ U_{0}, t^{∗}(U_{n}) = U_{n} and t ↾ U_{n} is bijective,
r^{∗}((W ∖ U) ∪ U_{n}) = U_{n} and r ↾ ((W ∖ U) ∪ U_{n}) is bijective.

Such an r exists because |U_{n}| ≥ ω, |W ∖ U| ≤ |U_{n}|. Then t, r : W ↠ U are onto U and r is one–one. For any s ∈ ^{n}W define g(s) ∈ ^{n}U by

g(s)_{i} = \{ \begin{matrix}t(s_{i}) & if i = 0 \\ r(s_{i}) & if i ≠ 0. \end{matrix}

Define h : A′ ⟶ P(^{n}W) by

h(x) = {s ∈ ^{n}W : g(s) ∈ x}, for all x ∈ A′.

Now h(R) = ×_{i<n}W_{i} by g(s)_{i} ≢ s_{i} ⟹ i ≠ 0, g(s)_{i} ∈ U_{n} (by a similar argument

to the ones in the previous proofs). Also, x ≠ 0 implies h(x) ≠ 0 by g(s) ≡ s for all s ∈ ^{n}U, where ≡ is the equivalence relation defined in the proof of Claim 5. Assume 0 ∉ {j, l}. Then s_{j} = s_{l} iff r(s_{j}) = r(s_{l}) iff g(s)_{j} = g(s)_{l}, hence h is a homomorphism w.r.t. d_{jl}, by Lemma 4.

Let i < n. We want to show that h is a homomorphism w.r.t. c_{i}. This follows from the following easy observation.

g(s)(i/u) = g(s(i/w)) if i = 0, u = t(w) or i ≠ 0, u = r(w).

QED(Claim 6)

We turn to showing how to eliminate the assumption ℓ = 0. Let us define the algebra 𝔅 as follows. Intuitively, 𝔅 is the same algebra as 𝔄 (in this proof) except that we interchange the indices 0 and ℓ. I.e., the universe of 𝔅 is the same as that of 𝔄, and all the operations of 𝔅 are the same as those of 𝔄 except that c_{0}^{𝔅} = c_{ℓ}^{𝔄}, c_{ℓ}^{𝔅} = c_{0}^{𝔄}, d_{0i}^{𝔅} = d_{i0}^{𝔅} = d_{0ℓ}^{𝔄}, d_{ℓi}^{𝔅} = d_{iℓ}^{𝔅} = d_{0i}^{𝔄}, for i ∈ n ∖ {0, ℓ}. (This algebra is denoted in [HMT71] by ℜ𝔡^{ξ}𝔄 where ξ is the permutation of n interchanging 0 and ℓ and fixing the other elements of n.) Now, by using the corresponding properties of 𝔄, it is easy to see that 𝔅 ∉ SNr_{n}CA_{n+2}, 𝔅 satisfies (i), (iii) as stated at the beginning of the proof of Theorem 3, and also 𝔅 satisfies (ii) if we replace 0 in it by ℓ. This proves Theorem 3 by the argument given at the beginning of the proof of Theorem 3. QED(Theorem 3)

THEOREM 4. Let Σ be a set of quantifier–free formulas axiomatizing RCA_{n}, 2 < n < ω. Let k be any natural number and let ℓ < n. Then Σ contains infinitely many formulas that contain all the cylindrifications c_{0}, ..., c_{n−1}, contain a diagonal constant with index ℓ and contain more than k variables. The same holds for K in place of RCA_{n} if _{∞}Cs_{n} ⊆ K ⊆ RCA_{n}.

REMARK 4. We want to prove Theorem 4 with an argument similar to the one in the proof of Theorem 3. I.e. we want to show nonrepresentable algebras 𝔄 which e.g. can be represented whenever we omit one of the cylindrifications. To this end, however, we have to modify our construction used in the proof of Theorem 1 for n < ω, because in that construction the “cause of nonrepresentability” was contained entirely in the indices 0, 1, 2, i.e. those algebras cannot be represented in such a way that c_{i}, d_{ij} for i, j < 3 would be “real”. To prove Theorem 4, we will “merge” the constructions (used in the proof of Theorem 1) for n ≥ ω and for n < ω. ■

Proof of Theorem 4: \underline{PLAN:} Let n, Σ, k and ℓ be as in the statement of Theorem 4. We will construct an algebra 𝔄 with the following properties:

(i) 𝔄 ∉ RCA_{n}.

(ii) For any i < n there is a representation of 𝔄 as a _{∞}Cs_{n} in which all the

operations are the natural ones except c_{i}. (iii) There is a representation of 𝔄 as a _{∞}Cs_{n} in which all the operations are

the natural ones except d_{ij} with ℓ ∈ {i, j}. (iv) Every k–generated subalgebra of 𝔄 is in I_{∞}Cs_{n}.

Let Σ^{c} denote the set of all quantifier–free formulas valid in K which do not contain all the cylindrifications c_{0}, ...c_{n−1}, let Σ^{d} denote the set of all quantifier– free formulas valid in K in which no d_{ij} with ℓ ∈ {i, j} occurs and let Σ^{v} denote the set of all quantifier–free formulas valid in K in which at most k variables occur. Then 𝔄 ⊧ Σ^{c} ∪ Σ^{d} ∪ Σ^{v} by (ii)–(iv) above and by _{∞}Cs_{n} ⊆ K. However, 𝔄 |̸= Σ by (i) and K ⊆ RCA_{n}, hence Σ ⊈ Σ^{c} ∪ Σ^{d} ∪ Σ^{v} which means that Σ contains a formula in which all the cylindrifications c_{0}, ..., c_{n−1} occur, in which some d_{ij} with ℓ ∈ {i, j} occurs and in which more than k variables occur.

If Σ contains at least one formula as described for all k < ω, then Σ contains infinitely many such formulas for all k: Assume that we already have φ_{1}, …, φ_{m} of the desired form for k. Ket K be bigger than the number of variables occurring in φ_{1} ∧ ⋯ ∧ φ_{m}, and let φ_{m+1} be a formula of the described form containing more than K variables. There is at least one such, and this φ_{m+1} will be different from φ_{1}, …, φ_{m} and will contain more than k variables.

Just as in the proof of Theorem 3, we may assume ℓ = 0.

\underline{CONSTRUCTION OF 𝔄:} Let K < ω be such that 2^{k} ≤ K · (n − 1) and let m = K · (n − 1). Let ⟨U_{i} : i ≤ n⟩ be a system of disjoint sets such that

|U_{0}| = m and |U_{i}| ≥ ω for all 0 < i ≤ n.

Let f : U_{0} ↣ → U_{0} be a bijection such that all orbits of f have cardinality K. E.g. we can choose U_{0} = K × (n − 1) and define for i < K, j < n − 1 f(i, j) = (i + 1(mod K), j). Let

U = ⋃{U_{i} : i ≤ n},

R = ×_{i<n}U_{i},

F = {s ∈ ^{n}U : s_{0}, s_{1} ∈ U_{0} and s_{1} = f(s_{0})}, and let

𝔄′ be the subalgebra of ⟨𝔓(^{n}U), c_{i}^{U}, d_{ij}^{U}⟩_{i,j<n} generated by R, F.

Now R is an atom of 𝔄′, this can be seen exactly as in the previous proofs, i.e. R satisfies condition (*) in Lemma 1. Let 𝔄 be the algebra we obtain from 𝔄′ by splitting R into m + 1 new atoms R_{j}, j ≤ m.

CLAIM 7. 𝔄 ∉ RCA_{n}.

Proof: For any j define

F_{1} = F
F_{j+1} = c_{2}(s_{2}^{1}F_{j} ∩ s_{2}^{0}F), and
E = F_{1} ∪ ... ∪ F_{K}.

Then F_{1}, ..., F_{K}, E ∈ A′ and it is easy to check that the following hold:

F_{j} = {s ∈ ^{n}U : s_{0}, s_{1} ∈ U_{0}, s_{1} = f^{j}(s_{0})},
E = {s ∈ ^{n}U : s_{0} and s_{1} are in the same orbit of f}.

Therefore the following equations are easily seen to hold in 𝔄′ for all i, j < n, i ≠ j ((1) and (2),(3) below express that “E is the union of K functions”, “E is an equivalence relation with < n blocks on U_{0}”):

F_{i} ∩ s_{2}^{1}F_{i} ⊆ d_{12}, E = F_{1} ∪ ... ∪ F_{K}, F_{i} = c_{2}F_{i}. (1)

c_{2}(s_{2}^{1}E ∩ s_{2}^{0}E) ⊆ E, E = s_{0}^{2}s_{1}^{0}s_{2}^{1}c_{2}E, d_{01} ∩ c_{1}E ⊆ E. (2)

⋂_{i<n}s_{i}^{0}c_{1}E ∩ ⋂_{i<j<n} − s_{i}^{0}s_{j}^{1}E = 0, c_{1}E = c_{1}...c_{n−1}R. (3)

By 𝔄′ ⊆ 𝔄, (1)–(3) hold in 𝔄, too.

Assume that 𝔄 is represented somehow. Then there is a homomorphism h : 𝔄 → ⟨𝔓(^{n}W), c_{i}^{W} , d_{ij}^{W} ⟩_{i,j<n} such that h(R) ≠ 0. We will derive a contradiction. By h(R) ≠ 0 there is s ∈ h(R). By R ≤ c_{0}R_{i} we have h(R) ⊆ c_{0}h(R_{i}) so there is w_{i} such that s(0/w_{i}) ∈ h(R_{i}), for all i ≤ m. These w_{i}’s are different from each other since the R_{i}’s are disjoint from each other and so the h(R_{i})’s are disjoint from each other. Let

H = {w_{i} : i ≤ m} and
G = {(u, v) ∈ H × H : s(0/u, 1/v) ∈ h(E)}.

Then |H| = m+1, by the above. Also, G is an equivalence relation on H such that each block of G is smaller than K+1, this can be inferred from (1)–(2) as follows: If (u, v), (v, w) ∈ G, then s(0/u, 1/w, 2/v) ∈ s_{2}^{1}h(E) ∩ s_{2}^{0}h(E), thus s(0/u, 1/w) ∈ c_{2}(s_{2}^{1}h(E) ∩ s_{2}^{0}h(E)) ⊆ h(E), thus (u, w) ∈ G. This shows that G is transitive. If (u, v) ∈ G, then s(0/u, 1/v) ∈ h(E), therefore s(0/u, 2/v) ∈ s_{2}^{1}c_{2}h(E), thus s(1/u, 2/v) ∈ s_{1}^{0}s_{2}^{1}c_{2}h(E). Then s(1/u, 0/v) ∈ s_{0}^{2}s_{1}^{0}s_{2}^{1}c_{2}h(E) = h(E), so (v, u) ∈ G. This shows that G is symmetric. Finally, G is reflexive because s(0/w_{i}) ∈ h(R_{i}) ⊆ h(R), therefore s(0/w_{i}, 1/w_{i}) ∈ d_{01}∩c_{1}h(R) ⊆ d_{01}∩c_{1}h(E) ⊆ h(E), thus (u, u) ∈ G for all u ∈ H. We have seen that G is an equivalence relation.

Assume that (u, v_{i}) ∈ G for all i ≤ K. We will show that v_{i} = v_{j} for some i < j < K. By (u, v_{i}) ∈ G we have s(0/u, 1/v_{i}) ∈ h(E) = h(F_{1}) ∪ ... ∪ h(F_{K}). So, for each i ≤ K let pi be such that s(0/u, 1/v_{i}) ∈ h(F_{pi}). Then pi = pj for some i < j ≤ K. But then s(0/u, 1/v_{i}, 2/v_{j}) ∈ h(F_{pi}) ∩ s_{2}^{1}h(F_{pi}) ⊆ d_{12}, thus v_{i} = v_{j}. This shows that each block of G is smaller than K + 1.

We have seen that G is an equivalence relation on H such that each block of G is smaller than K + 1. By |H| = m + 1 > K · (n − 1), then G has at least n blocks. Let v_{0}, ..., v_{n−1} be elements of H in n different blocks and let

z = ⟨v_{0}, v_{1}, ..., v_{n−1}⟩.

Then z ∈ ⋂_{i<j<n} − s_{i}^{0}s_{j}^{1}h(E), by (v_{i}, v_{j}) ∉ G for i < j < n. But also z ∈

⋂_{i<n}s_{i}^{0}c_{1}...c_{n−1}h(R) by v_{i} ∈ H, i.e. by s(0/v_{i}) ∈ h(R). These contradict (3).

QED(Claim 7)

Let W_{0} ⫌ U_{0} be disjoint from U ∖ U_{0}, |W_{0}| = K · n, let W_{i} = U_{i} for 0 < i ≤ n and let W = ⋃{W_{i} : i ≤ n}.

CLAIM 8. Let γ < n. There is an embedding h : A′ ↣ ⟨𝔓(^{n}W), c_{i}^{W} , d_{ij}^{W} ⟩_{i,j<n} such that h is a homomorphism w.r.t. all operations of 𝔄′ except for c_{γ}, and such

that h(R) = ×_{i<n}W_{i}.

Proof: Let us extend our earlier permutation f of U_{0} from U_{0} to a permutation of W such that f permutes W_{0}, all orbits of f ↾ W_{0} are of size K, and f is the identity on W ∖ W_{0}. We will denote this extension with f, too. Let e denote the equivalence relation on W_{0} with blocks the orbits of f, i.e.

e = ⋃{f^{l} : 1 ≤ l ≤ K} ∩ (W_{0} × W_{0}).

Let S′ be a binary relation on the blocks of e satisfying the same conditions as in the proof of Claim 5, i.e. S′ contains the identity relation and each block is in relation with exactly n − 1 blocks (since we have n blocks, this means that to each block there is exactly one, other, block not related to it). It will be more convenient to view S′ as a relation on W_{0}. Thus we formulate the above conditions as follows. Let S ⊆ W_{0} × W_{0} be a relation with the following properties for all u, v, w ∈ W_{0}:

(i) There is z such that (z, w) ∉ S.

(ii) v S̸ w, u S̸ w imply u e v and v e̸ w.

(iii) v S w, u e v imply u S w.

In other words, the relation S is such that (I)-(III) below are true for it.

(I) (−S)^{−1}|(W_{0} × W_{0}) = W_{0} × W_{0} (II) (−S)|(−S)^{−1} ⊆ e ⊆ S (III) e|S ⊆ S.

Such a relation S clearly exists.

We will need an equivalence relation on sequences of perhaps different length. Let s, z be two sequences. We define s ≡ z to hold iff the following are satisfied:

Dom(s) = Dom(z) and Rng(s), Rng(z) ⊆ W. Let H = Dom(s).
s_{i} ∈ W_{j} iff z_{i} ∈ W_{j} for all i ∈ H, j ≤ n
s_{l} = f^{j}s_{i} iff z_{l} = f^{j}z_{i} for all i, l ∈ H, 1 ≤ j ≤ K.

We note that by f^{K} = Id_{W} = {(w, w) : w ∈ W }, s ≡ z implies ker(s) = ker(z). It is easy to see that for s, z ∈ ^{n}U we have s ≡ z iff s = π ∘ z for some permutation π of U fixing R and F, therefore

(1) s ≡ z implies s ∈ x iff z ∈ x for all x ∈ A′.

We now define a function g : ^{n}W ⟶ ^{n}U. Let s ∈ ^{n}W be arbitrary. Let Ω_{s} = Ω = {i < n : s_{i} ∈ W_{0}}. Let I = n ∖ {γ}.

Assume γ ∉ Ω, i.e. Ω ⊆ I. Let s′ ∈ ^{Ω}U_{0} be such that s′ ≡ s ↾ Ω. Such s′ exists by |Ω| < n. We define

g(s) = s[Ω/s′].

Assume γ ∈ Ω, i.e. Ω ⊈ I. Let Ω′ = {i ∈ Ω : s_{i} S s_{γ}}, Ω′′ = Ω ∖ Ω′. Let s′ ∈ ^{Ω′}U_{0} be such that s′ ≡ s ↾ Ω′ and let s′′ ∈ ^{Ω′′}(U_{n} ∖ Rng s) be such that ker(s′′) = ker(s ↾ Ω′′). Such s′, s′′ exist by |{s_{i} : i ∈ Ω′}| ≤ n − 1, |U_{n}| ≥ ω. We define

g(s) = s[Ω′/s′][Ω′′/s′′].

This function g is defined analogously to the function in the proof of Theorem 3, and has analogous properties. E.g. it satisfies the following (G1)–(G5) (this is easy to check). Let s ∈ ^{n}W, Ω = {i < n : s_{i} ∈ W_{0}}, and u ∈ W. Let ℤ denote the set of all integers.

(G1) ker(g(s)) = ker(s), and [s_{i} = f^{l}s_{j} iff g(s)_{i} = f^{l}g(s)_{j}] whenever s_{i} ≡ g(s)_{i},

for all i, j ∈ n, l ∈ ℤ. (G2) g(s) ≡ s if γ ∉ Ω. (G3) g(s) ↾ (n ∖ {i}) ≡ g(s(i/u)) ↾ (n ∖ {i}) if i ≠ γ. (G4) g(s)_{i} ≢ s_{i} implies g(s)_{i} ∈ U_{n}, s_{i}, s_{γ} ∈ W_{0}, s_{i} S̸ s_{γ} and i ≠ γ. (G5) s_{i}, s_{γ} ∈ W_{0}, s_{i} S̸ s_{γ}, i ≠ γ imply g(s)_{i} ∈ U_{n}.

We include verification of the second part of condition (G1). If γ ∉ Ω, then we are done by (G2). So assume γ ∈ Ω.

To check direction →, assume s_{i} ≡ g(s)_{i} and s_{i} = f^{l}s_{j}. If i ∉ Ω, then j ∉ Ω by s_{i} = f^{l}s_{j}, and so g(s)_{i} = s_{i} and g(s)_{j} = s_{j} and we are done. If i ∈ Ω, then i ∈ Ω′ by s_{i} ≡ g(s)_{i}, and thus j ∈ Ω′ by s_{i} = f^{l}s_{j} and condition (iii) on S. Then g(s)_{i} = s′_{i} and g(s)_{j} = s′_{j} and so we are done by s′ ≡ s ↾ Ω′.

To show direction ←, assume s_{i} ≡ g(s)_{i} and g(s)_{i} = f^{l}g(s)_{j}. If i ∉ Ω, then j ∉ Ω by g(s)_{i} = f^{l}g(s)_{j}, and so g(s)_{i} = s_{i}, g(s)_{j} = s_{j} and we are done. If i ∈ Ω, then i ∈ Ω′ by s_{i} ≡ g(s)_{i}. Then j ∈ Ω′ by g(s)_{i} = f^{l}g(s)_{j}, because g(s)_{i} ∈ W_{0} by i ∈ Ω′ and g(s)_{j} ∉ W_{0} if j ∉ Ω′. Then g(s)_{i} = s′_{i} and g(s)_{j} = s′_{j} and so we are done by s′ ≡ s ↾ Ω′.

We define h : A′ ⟶ P(^{n}W) by

h(x) = {s ∈ ^{n}W : g(s) ∈ x}, for all x ∈ A′.

We begin with showing h(R) = ×_{i<n}W_{i}. Now s ∈ h(R) iff g(s) ∈ R iff

g(s)_{i} ∈ U_{i} for all i < n iff(by (G4)) s_{i} ∈ W_{i} for all i < n iff s ∈ ×_{i<n}W_{i}.

Next we show that h is one–one. Let x ∈ A′, x ≠ 0. Let s ∈ x be arbitrary and Ω = {i < n : s_{i} ∈ U_{0}}. If γ ∉ Ω then g(s) ≡ s by (G2), hence g(s) ∈ x by (1), i.e. s ∈ h(x). Assume γ ∈ Ω. Let w ∈ U_{0} be arbitrary and let s′ ∈ ^{Ω}({v ∈ W_{0} : v S w}) be such that s′_{γ} = w and s′ ≡ s ↾ Ω. Such an s′ exists by s ∈ ^{n}U. Let z = s[Ω/s′]. Then g(z) ≡ s, hence g(z) ∈ x by (1), i.e. z ∈ h(x).

By Lemma 4 and (G1), h is a Boolean homomorphism preserving d_{ij} for all i, j < n.

It remains to show that h is a homomorphism w.r.t. c_{i}, i ≠ γ. Let i < n, i ≠ γ. Let s ∈ ^{n}W be arbitrary. Let Ω = {j < n : s_{j} ∈ W_{0}}. Let u ∈ U, w ∈ W. Consider conditions (2),(3) below.

(2) [s_{j} ≡ g(s)_{j}, u = f^{l}g(s)_{j}, w = f^{l}s_{j}] or [s_{j} ≢ g(s)_{j}, w = f^{l}s_{j}, u ∈ U_{n} and (∀k ∈ n ∖ {i})(u = g(s)_{k} iff w = s_{k})], for some 1 ≤ l ≤ K and j ∈ n ∖ {i}.

(3) u ∉ {f^{l}g(s)_{j} : 1 ≤ l ≤ K, j ∈ n∖{i}}, w ∉ {f^{l}s_{j} : 1 ≤ l ≤ K, j ∈ n∖{i}}, and either u ≡ w, (w ∈ W_{0}, Ω ⊈ I ⟹ w S s_{γ}), or u ∈ U_{n}, w ∈ W_{0}, Ω ⊈ I, w S̸ s_{γ}.

Then it is easy to adapt the argument in the proof of Theorem 3 to show that g(s)(i/u) ≡ g(s(i/w)) whenever (2) or (3) holds, as follows.

Let p = g(s)(i/u), q = g(s(i/w)), and z = s(i/w). By i ∈ I and (G3) we have

(+) p ↾ (n ∖ {i}) ≡ q ↾ (n ∖ {i}).

Thus we have to show

(*) p_{i} ≡ q_{i} and (**) (p_{i} = f^{r}p_{k} iff q_{i} = f^{r}q_{k}), for k ∈ n ∖ {i}, r ∈ ℤ.

Assume that (2) holds with s_{j} ≡ g(s)_{j}. Then z_{j} ≡ g(z)_{j} because by s_{j} ≡ g(s)_{j} we have that it is not the case that s_{j}, s_{γ} ∈ W_{0} and s_{j} S̸ s_{γ}, and z_{j} = s_{j}, z_{γ} = s_{γ}. Thus z_{i} = w = f^{l}s_{j} = f^{l}z_{j} implies, by (G1), that q_{i} = f^{l}q_{j}. Also p_{i} = u = f^{l}p_{j}. By j ≠ i and (+) we have p_{j} ≡ q_{j}. Thus p_{i} = f^{l}p_{j} ≡ p_{j} ≡ q_{j} ≡ f^{l}q_{j} = q_{i}, hence p_{i} ≡ q_{i}. Let k ∈ n ∖ {i}, r ∈ ℤ be arbitrary. Now p_{i} = f^{r}p_{k} iff f^{l}p_{j} = f^{r}p_{k} iff p_{j} = f^{(r−l)}p_{k} iff(by (+)) q_{j} = f^{(r−l)}q_{k} iff f^{l}q_{j} = f^{r}q_{k} iff q_{i} = f^{r}q_{k}. Assume now that (2) holds with s_{j} ≢ g(s)_{j}. Then s_{γ}, s_{j} ∈ W_{0}, s_{j} S̸ s_{γ}, and g(s)_{j} ∈ U_{n} by (G4). By z_{i} = w = f^{l}s_{j} and condition (iii) on S then w S̸ s_{γ} = z_{γ}, so q_{i} = g(z)_{i} ∈ U_{n}. Thus q_{i} ≡ p_{i} = u ∈ U_{n}. This verifies (*). To show (**), let k ∈ n∖{i}. Then p_{i} = f^{l}p_{k} iff(by p_{i} = u ∈ U_{n}) u = p_{k} iff u = g(s)_{k} iff(by our assumption) w = s_{k} iff z_{i} = z_{k} iff(by (G1), q = g(z)) q_{i} = q_{k} iff(by q_{i} ∈ U_{n}) q_{i} = f^{l}q_{k}. Assume now that (3) holds. To show (**), let k ∈ n ∖ {i} and r ∈ ℤ be arbitrary. Then p_{i} = u ≠ f^{r}g(s)_{k} = f^{r}p_{k} and z_{i} = w ≠ f^{r}s_{k} = f^{r}z_{k}. We show that z_{i} ≡ g(z)_{i} or z_{k} ≡ g(z)_{k}, so z_{i} ≠ f^{r}z_{k} implies g(z)_{i} ≠ f^{r}g(z)_{k} by (G1), i.e. q_{i} ≠ f^{r}q_{k}. Assume the contrary, i.e. assume that z_{i} ≢ g(z)_{i} and z_{k} ≢ g(z)_{k}. Then z_{i}, z_{k}, z_{γ} ∈ W_{0} and z_{i} S̸ z_{γ}, z_{k} S̸ z_{γ} by (G5). Thus z_{i} e z_{k} by condition (ii) on S. Hence w e s_{k} by w = z_{i}, s_{k} = z_{k}, contradicting our hypothesis (3).

To show (*), notice that p_{i} = u and z_{i} = w. Assume first that Ω ⊆ I, i.e. γ ∉ Ω. Then u ≡ w and z_{i} ≡ q_{i} by (G2), so p_{i} ≡ q_{i}. Assume now that Ω ⊈ I. Assume u ≡ w and (w ∈ W_{0} ⟹ w S s_{γ}). By z_{γ} = s_{γ}, if w ∈ W_{0} then w = z_{i} S z_{γ}, so q_{i} ≡ z_{i} by (G4) and hence p_{i} ≡ q_{i}. Assume u ∈ U_{n}, w ∈ W_{0}, w S̸ s_{γ}. Then by (G5) we have q_{i} ∈ U_{n}, so q_{i} ≡ u = p_{i}.

Also, it is easy to modify the argument in the proof of Thm.3 to show that for every u ∈ U there is w ∈ W and for every w ∈ W there is u ∈ U such that u, w satisfy (2) or (3). We include the modified argument here.

Let u ∈ U be arbitrary. Assume that u = f^{l}g(s)_{j} for some j ≠ i and l ∈ ℤ. If s_{j} ≡ g(s)_{j} then let w = f^{l}s_{j}. If s_{j} ≢ g(s)_{j}, then u = g(s)_{j} ∈ U_{n} and let w = s_{j}. Then (2) is satisfied, because u = g(s)_{k} iff g(s)_{j} = g(s)_{k} iff s_{j} = s_{k} iff w = s_{k}. Assume that u ∉ {f^{l}g(s)_{j} : j ∈ n ∖ {k}, l ∈ ℤ}. If u ∉ U_{0} then there is w ≡ u with w ∉ {f^{l}s_{j} : j ∈ n ∖ {i}, l ∈ ℤ} by |U_{k}| ≥ ω, f^{l} ↾ U_{k} ⊆ Id for all k > 0. This w will satisfy (3).

Assume now u ∈ U_{0}. Assume further Ω ⊆ I, i.e. s_{γ} ∉ W_{0}. Then |U_{0} ∩ {f^{l}s_{j} : j ∈ n ∖ {i}, l ∈ ℤ}| = |U_{0} ∩ {f^{l}s_{j} : j ∈ n ∖ {i, γ}, l ∈ ℤ}| ≤ K · (n − 2). Thus there is w ∈ U_{0} ∖ {f^{l}s_{j} : j ∈ n ∖ {i}, l ∈ ℤ} and this w will satisfy (3).

Assume now Ω ⊈ I. Then g(s)_{j} ∈ U_{0} iff s_{j} S s_{γ}, for all j ∈ n. By u ∈ U_{0} ∖ {f^{l}g(s)_{j} : j ∈ n ∖ {i}} and |U_{0}| = K · (n − 1) we have |{g(s)_{j}/e : j ∈ n ∖ {i}, g(s)_{j} ∈ U_{0}}| ≤ n − 2. Then {g(s)_{j}/e : s_{j} S s_{γ}}| ≤ n − 2, hence by {w/e : w S s_{γ}}| = n − 1 there is w ∈ W_{0} ∖ {f^{l}s_{j} : j ∈ n ∖ {i}, l ∈ ℤ} with w S s_{γ}. This w satisfies (3).

Conversely, let w ∈ W_{0} be arbitrary. Assume that w = f^{l}s_{j} for some j ∈ n ∖ {i}, l ∈ ℤ. If s_{j} ≡ g(s)_{j}, then let u = f^{l}g(s)_{j}. Assume s_{j} ≢ g(s)_{j}. If w = s_{k} for some k ∈ n ∖ {i}, then let u = g(s)_{k}. By w = f^{l}s_{j} then s_{k} e s_{j}, so g(s)_{k} ∈ U_{n} by condition (iii) on S. If w = s_{r} for some r ∈ n ∖ {i, k}, then s_{r} = s_{k}, so u = g(s)_{k} = g(s)_{r}. Thus u satisfies (2). Assume that w ≠ s_{k} for all k ∈ n ∖ {i}. Then let u ∈ U_{n} ∖ {g(s)_{k} : k ∈ n} be arbitrary. Then (2) is satisfied.

Assume that w ∉ {f^{l}s_{j} : j ∈ n ∖ {i}, l ∈ ℤ}. If w ∉ W_{0} then there is u ≡ w with u ∉ {f^{l}g(s)_{j} : j ∈ n ∖ {i}, l ∈ ℤ} by |U_{k}| ≥ ω for all k > 0. Assume w ∈ W_{0}. Assume further Ω ⊆ I. Then by g(s)_{j} ∈ U_{0} → s_{j} ∈ W_{0} for all j, we have {g(s)_{j} ∈ U_{0} : j ∈ n ∖ {i}} ⊆ {s_{j} ∈ W_{0} : j ∈ n ∖ {i}} = {s_{j} ∈ W_{0} : j ∈ n ∖ {i, γ}}, thus |{g(s)_{j} ∈ U_{0} : j ∈ n ∖ {i}}| ≤ n − 2. Then by |U_{0}| = K · (n − 1) there is u ∈ U_{0} ∖ {f^{l}g(s)_{j} : j ∈ n ∖ {i}, l ∈ ℤ}. This w will satisfy (3).

Assume now Ω ⊈ I, w S s_{γ}. Then {j ∈ n ∖ {i} : g(s)_{j} ∈ U_{0}} ⊆ {j ∈ n ∖ {i} : s_{j} S s_{γ}}. So by w ∉ {f^{l}s_{j} : j ∈ n ∖ {i}, l ∈ ℤ}, w S s_{γ} we have |{s_{j}/e : s_{j} S s_{γ}}| ≤ n − 2, so |{g(s)_{j}/e : g(s)_{j} ∈ U_{0}, j ∈ n ∖ {i}}| ≤ n − 2. Thus there is u ∈ U_{0} ∖ {f^{l}g(s)_{j} : j ∈ n ∖ {i}, l ∈ ℤ}. This u satisfies (3).

Assume finally Ω ⊈ I, w S̸ s_{γ}. Then let u ∈ U_{n} ∖ {g(s)_{j} : j ∈ n ∖ {i}} be arbitrary. Such a u exists by |U_{j}| ≥ ω, and this u satisfies (3). QED(Claim 8)

CLAIM 9. There is an embedding h : A′ ↣ ⟨𝔓(^{n}W), c_{i}^{W} , d_{ij}^{W} ⟩_{i,j<n} such that h(R) = ×_{i<n}W_{i} and h is a homomorphism w.r.t. all operations of 𝔄′ except for

d_{0i}, d_{i0}, i < n.

The proof of Claim 9 is exactly the same as that of Claim 6, therefore we omit it. Now (ii),(iii) at the beginning of the proof of Theorem 4 follow from Claims 8,9 and Lemma 3(5).

CLAIM 10. Every k–generated subalgebra of 𝔄 is in I_{∞}Cs_{n}.

Proof: This follows from Lemma 3(3), 2^{k} ≤ K · (n − 1) = |U_{0}| and from Lemma 2. QED(Claim 10) QED(Theorem 4)

Let U be a set and f : P(^{n}U) ⟶ P(^{n}U) be a unary function on n–ary relations over U. We say that f is \underline{additive} (or distributes over join) if

f(R ∪ S) = f(R) ∪ f(S) for all R, S ⊆ ^{n}U.

Let S(U) denote the set of all permutations of U. For any π ∈ S(U) and n–ary relation R ⊆ ^{n}U, π(R) denotes the image of R under the permutation π, i.e.

π(R) = {π ∘ s : s ∈ R}.

We say that f is \underline{permutation–invariant} if for all permutation π of U and for all n–ary relation R ⊆ ^{n}U we have

f(πR) = π(fR).

Let α, U be sets, i, j ∈ α. Then [i, j]^{(α)} ∈ S(α) denotes the permutation of α which interchanges i and j and leaves all other elements fixed. Let σ ∈ S(α) and τ : α ⟶ α. Then p_{σ}^{U}, s_{τ}^{U} : P(^{α}U) ⟶ P(^{α}U) are defined as follows. For any x ⊆ ^{α}U

p_{σ}^{U}(x) = {s ∘ σ : s ∈ x},
s_{τ}^{U}(x) = {s ∈ ^{α}U : s ∘ τ ∈ x},
p_{ij}^{U} = p_{[i,j]}^{U} and
s_{ij}^{U}(x) = {s ∈ ^{α}U : s(i/s_{j}) ∈ x},

i.e. s_{ij}^{U} = s_{[i/j]}^{U}, where [i/j] : α ⟶ α is identity everywhere except on i where its value is j. We often omit the upper indices.

We note that c_{i}^{U}, p_{σ}^{U}, s_{τ}^{U} are all additive, permutation–invariant, unary operations and s_{ij}(x) = s_{j}^{i}(x), and s_{ij}(x) = c_{i}(d_{ij} ∩ x) if i ≠ j.

The next theorem states that no unary, additive, permutation invariant functions help in finitely axiomatizing RCA_{n} for 3 ≤ n < ω. Theorem 5 below complements Sain[87a]’s result and extends Biró[89]’s result from first–order to “beyond first–order”. For more detail on this see Remark 5 after Theorem 5.

THEOREM 5. Let 3 ≤ n < ω. For any set U let f_{1}^{U}, ..., f_{r}^{U} be at most unary, additive, permutation–invariant functions on P(^{n}U). Let

RA_{n}^{+} = S{⟨𝔓(^{n}U), c_{i}^{U}, d_{ij}^{U}, f_{1}^{U}, ..., f_{r}^{U}⟩_{i,j<n} : U is a set}.

Let Σ be any set of quantifier–free formulas valid in RA_{n}^{+} and containing only finitely many variables. Then Σ does not axiomatize the set of equations valid in RCA_{n}, i.e. there is an equation valid in RCA_{n} which does not follow from Σ. Moreover, there is an equation e with RCA_{3} ⊧ e but Σ |̸= e.

Proof: \underline{PLAN:} Let k < ω be arbitrary. We will construct an algebra 𝔄 with the following properties.

a) 𝔄 ∉ RA_{n}^{+}, moreover 𝔄 |̸= e for an equation e valid in RCA_{3}.

b) Every k–generated subalgebra of 𝔄 is in RA_{n}^{+}.

This will prove the theorem because of the following. Let Σ be as in the statement of the theorem, let Σ contain k variables. Let 𝔄, e satisfy a),b). Then 𝔄 ⊧ Σ by b), and 𝔄 |̸= e by a), hence Σ |̸= e and e is an equation valid in RCA_{3}.

\underline{CONSTRUCTION OF 𝔄:} Let m ≥ 2^{(1+k·n!)}, m < ω. Let U_{0} = m = \{i : i < m}, U_{i} = S(m) × {i} for all 0 < i < n and let U = ⋃{U_{i} : i < n}. Let

R = ×_{i<n}U_{i},

F = {s ∈ ^{n}U : s_{0}, s_{1} ∈ U_{0}, s_{1} = s_{0} + 1(mod m)}, and let

𝔄′ be the subalgebra of ⟨𝔓(^{n}U), c_{i}^{U}, d_{ij}^{U}, p_{ij}^{U}⟩_{i,j<n} generated by R, F.

Then R is an atom of 𝔄′, this can be seen by checking that R satisfies (*) in Lemma 1 and that Lemma 1 remains true if we add any permutation–invariant functions to our algebras. (Now we added p_{ij}.)

Our algebra 𝔄 will be obtained from 𝔄′ basically by splitting R into m + 1 parts, R_{j}, j ≤ m. Then 𝔄 will be nonrepresentable by the arguments used so far. However, we have to define the operations f_{1}, ..., f_{r} on the new atoms R_{j}, j ≤ m in such a way that the k–generated subalgebras stay representable. This is now difficult because we know almost nothing about the operations f_{1}, ..., f_{r}. Therefore first we will split R in 𝔄′ into m parts R′_{j}, j < m only, but in a “good way”. Then we will observe how the “real” operations f_{1}^{U}, ..., f_{r}^{U} behave on R′_{j}, j < m, and then try to copy this behaviour to the abstract atoms R_{j}, j ≤ m.

CLAIM 11. There is a partition ⟨R_{j} : j < m⟩ of R satisfying the following properties (R1)–(R3) for all j < m, 0 < i < n and s ∈ R.

(R1) |{u ∈ U : s(0/u) ∈ R_{j}}| = 1. (R2) |{u ∈ U : s(i/u) ∈ R_{j}}| ≥ 2n. (R3) For every ρ ∈ S(m) there is π ∈ S(U) such that π(R_{j}) = R_{ρ(j)} and π(a) = a

for all j < m and a ∈ 𝔄′.

Proof: Recall that U_{0} = m = {i : i < m} and U_{i} = S(U_{0}) × {i} for all 0 < i < n. For any j < m define

R_{j} = {⟨u, (σ_{1}, 1), ..., (σ_{n−1}, n−1)⟩ : u ∈ U_{0}, σ_{1}, ..., σ_{n−1} ∈ S(U_{0}), σ_{1}...σ_{n−1}(u) = j}.

Now ⟨R_{j} : j < m⟩ is a partition of R satisfying (R1).

Let 0 < i < n and s = ⟨u, (σ_{1}, 1), ..., (σ_{n−1}, n − 1)⟩ ∈ R be arbitrary. Let σ = σ_{1} ∘ σ_{2} ∘ ... ∘ σ_{i−1} and v = σ_{i+1}...σ_{n−1}(u). Let δ ∈ S(U_{0}) be such that δ(v) = σ^{−1}(j). There are (m−1)! ≥ 2n many such choices for δ. Let z = s(i/(δ, i)). Then z ∈ R_{j} by σ_{1}σ_{2}...σ_{i−1}δσ_{i+1}...σ_{n−1}(u) = σδ(v) = j. Thus (R2) is satisfied.

To prove (R3), let ρ ∈ S(m) be arbitrary. Let π ∈ S(U) be defined by

π ↾ (U ∖ U_{1}) ⊆ Id and π((σ, 1)) = (ρ ∘ σ, 1) for all σ ∈ S(U_{0}).

Let j < m. We show that πR_{j} = R_{ρ(j)}. Let s ∈ R. Then s = ⟨u, (σ_{1}, 1), ..., (σ_{n−1}, n − 1)⟩ for some u ∈ U_{0} and σ_{1}, ..., σ_{n−1} ∈ S(U_{0}) and πs = ⟨u, (ρ∘σ_{1}, 1), ..., (σ_{n−1}, n−1)⟩. Now s ∈ R_{j} iff σ_{1}...σ_{n−1}(u) = j iff ρσ_{1}...σ_{n−1}(u) = ρj iff (π ∘ s) ∈ R_{ρ(j)}. Thus π(R_{j}) = R_{ρ(j)}. Clearly, πR = R and πF = F, thus πa = a for all a ∈ A′ since A′ is generated by R, F. QED(Claim 11)

Let R_{0}, ..., R_{m−1} be a partition of R satisfying (R1)–(R3). Let A′′ be the universe of the subalgebra of ⟨𝔓(^{n}U), c_{i}^{U}, d_{ij}^{U}, p_{ij}^{U}⟩_{i,j<n} generated by {R_{0}, ..., R_{m−1}, F }. We first show that A′′ is closed under f_{1}^{U}, ..., f_{r}^{U} whatever they may be.

CLAIM 12. A′′ is closed under all unary, additive, permutation–invariant functions.

Proof: To begin, we show that 𝔄′ is closed under all permutation–invariant functions. Recall the notation F ix(R, F) from Lemma 1. Then F ix(R, F) = {π ∈ S(U) : π^{∗}(U_{i}) = U_{i} for all i < n and there is l ∈ U_{0} such that π(u) = u + l(mod m) for all u ∈ U_{0}}. From this it is not difficult to check that

{π ∘ s : π ∈ F ix(R, F)} ∈ A′ for all s ∈ ^{n}U.

This, together with π(a) = a for all a ∈ A′ and π ∈ F ix(R, F) implies that

A′ = {a ⊆ ^{n}U : π(a) = a for all π ∈ F ix(R, F)}.

This immediately implies that

(1)  A′ is closed under all permutation-invariant functions.

Let R = {p_{σ}R_{j} : σ ∈ S(n), j < m}. Next we show that

(2)  A′′ = {a + ∑ X : a ∈ A′, X ⊆ R}.

Indeed, let H = {a + ∑ X : a ∈ A′, X ⊆ R}, i, j < n and σ ∈ S(n). Clearly, H ⊆ A′′ and H is closed under the Boolean operations. By (R1),(R2) we have that

c_{i}p_{σ}R_{j} = c_{i}p_{σ}R for all j < m, σ ∈ S(n),

thus H is closed under c_{i}. Since p_{σ} is additive and both A′ and R are closed under p_{σ}, we have that H is closed under p_{σ}. Finally, d_{ij} ∈ A′ ⊆ H. We have proved (2). By (2) we have that every element of R is an atom of A′′.

Let f be any unary, additive, permutation–invariant function on P(^{n}U). We turn to proving that A′′ is closed under f. Since f is additive and R is finite, by (1) it is enough to show that f(p_{σ}R_{j}) ∈ A′′ for all σ ∈ S(n), j < m. Let σ ∈ S(n), j < m, a = p_{σ}R_{j}. Since ^{n}U is finite, A′′ is also finite, thus every element of A′′ is a finite sum of atoms. Let y be any atom of A′′. We will show that y ∩ f(a) ≠ 0 implies y ⊆ f(a). This will imply that f(a) is a union of atoms of A′′, hence f(a) ∈ A′′.

Let s ∈ y ∩ f(a) and z ∈ y be arbitrary. By finiteness of ^{n}U and additivity of f, s ∈ f(a) implies that s ∈ f({q}) for some q ∈ a. We will construct a π ∈ S(U) such that π ∘ q ∈ a and π ∘ s = z. This will suffice because then z = π ∘ s ∈ πf{q} = f{π ∘ q} ⊆ f(a).

Let V = Rng q ∖ Rng s. If V = ∅ then s = q ∘ δ for some δ ∈ S(n), because q is repetition–free. Then s ∈ p_{δ}a, hence z ∈ p_{δ}a because s, z are contained in the same atom y. Let q′ = z ∘ δ^{−1}. Then z = q′ ∘ δ and q′ ∈ a by z ∈ p_{δ}a. Let π ∈ S(U) be such that π ∘ q = q′. Such a π exists because q, q′ are repetition–free. Now π ∘ s = z by s = q ∘ δ, z = q′ ∘ δ and we are done.

Assume V ≠ ∅. Let V = {q_{p0}, ..., q_{pt}} for some t such that q_{p0} ∈ U_{0} if U_{0} ∩V ≠ ∅ and the sequence q_{p0}, ..., q_{pt} is without repetitions. By q ∈ p_{σ}R_{j} we have q_{i} ∈ U_{σ(i)} for all i < n. Let i < n be such that q_{i} ∉ V. Then q_{i} = s_{l} for some l < n. Let us define

q′_{i} = z_{l}.

This definition is sound by ker(s) = ker(z). Also, q′_{i} ∈ U_{σ(i)} because s, z are contained in the same atom of A′′ and q_{i} = s_{l} ∈ U_{σ(i)}. Now for any i ≤ t choose q′_{pi} ∈ U_{σ(pi)} ∖ Rng z such that for all l ≤ t q′_{pi} ≠ q′_{pl} if pi ≠ pl. Such a choice is possible because |U_{σ(pi)}| ≥ 2n. By the above we defined q′_{i} for all i < n. Let q′ = ⟨q′_{i} : i < n⟩. Then q′ ∈ p_{σ}R and q_{i} = s_{l} ⟺ q′_{i} = z_{l} for all i, l < n.

Let i = pt. We will show that there is u ∈ U_{σ(i)} ∖ Rng z such that q′(i/u) ∈ a. If σ(i) ≠ 0 then by (R2) we can choose such a u. Assume therefore σ(i) = 0. Then by (R1), the u ∈ U_{0} for which q′(i/u) ∈ a is unique. We will show that u ∉ Rng z. By σ(i) = 0 we have q_{i} ∈ U_{0}. Then t = 0 and V = {q_{i}} by our hypothesis on the order of enumerating V (and since |V ∩ U_{0}| ≤ 1). Also, s = q(i/v) ∘ δ and z = q′(i/v′) ∘ δ for some δ ∈ S(n) and v, v′ ∈ U. By σ(i) = 0 and (R1), there is only one w for which q(i/w) ∈ a. By v ≠ q_{i} and q ∈ a then q(i/v) ∉ a. Thus s ∉ p_{δ}a, hence z ∉ p_{δ}a since s and z are contained in the same atom of A′′, and thus q′(i/v′) ∉ a. Hence u ≠ v′ by q′(i/u) ∈ a. By z = q′(i/v′) ∘ δ then u ∉ Rng z and we are done. Let q′′ = q′(i/u). Then q′′ ∈ a.

Now there is π ∈ S(U) such that π ∘ q = q′′ and π ∘ s = z because q, q′′ are repetition–free, ker(s) = ker(z) and q′′_{i} = z_{l} iff q_{i} = s_{l} for all i, l < n. QED(Claim 12)

We define

𝔄′′ = ⟨A′′, ∪, ∖, c_{i}^{U}, d_{ij}^{U}, f_{1}^{U}, ..., f_{r}^{U}⟩_{i,j<n}.

Clearly, 𝔄′′ ∈ RA_{n}^{+}.

We will define our algebra 𝔄 ∉ RA_{n}^{+} by modifying 𝔄′′ ∈ RA_{n}^{+}. The idea is that we split R into more than m parts, but otherwise we let the construction be “the same”. In order to be able to do this, we prove that the operations f_{1}^{U}, ..., f_{r}^{U} do not “distinguish” the R_{j}’s, moreover they are defined on the R_{j}’s according to some scheme that can be applied to an “imaginary R_{j} ”, too. Here we will use condition (R3) in Claim 11. Then we will prove that the k–generated subalgebras of 𝔄 are isomorphic to subalgebras of 𝔄′′. We shall need the second statement of Claim 13 below when showing this.

CLAIM 13. Let f be a unary, additive, permutation–invariant function on P(^{n}U) and let σ ∈ S(n). Then there are terms τ_{σ}(x), τ′_{σ}(x) using the operations +, −, c_{i}, d_{ij}, p_{δ}, i, j < n, δ ∈ S(n) and some constants from A′ (i.e. τ_{σ}, τ′_{σ} are terms of the language of 𝔓 = ⟨𝔓(^{n}U), c_{i}^{U}, d_{ij}^{U}, p_{δ}^{U}, a⟩_{i,j<n,δ∈S(n),a∈A′}) such that (i)–(ii) below hold.

(i) f(p_{σ}^{U}R_{j}) = τ_{σ}(R_{j}) for all j < m (in 𝔓).

(ii) Let ℭ be any algebra similar to 𝔓 and such that (C, +^{ℭ}, −^{ℭ}) is a Boolean algebra and the p_{δ}^{ℭ}’s are additive. Let |J| ≥ 2, J finite, and let a_{j}, j ∈ J be disjoint elements of C. Then ∑{τ_{σ}(a_{j}) : j ∈ J} = τ′_{σ}(∑{a_{j} : j ∈ J}) in ℭ.

Proof: Let f, σ be as in the statement of Claim 13. For any permutation δ ∈ S(n) let

F_{δ} = f(p_{σ}R_{0}) ∩ p_{δ}R

and define the term ε_{δ}(x) as

ε_{δ}(x) = \{ \begin{matrix}1 & if F_{δ} = p_{δ}R \\ x & if F_{δ} = p_{δ}R_{0} \\ 0 & if F_{δ} = 0 \\ −x & otherwise. \end{matrix}

Let b = f(p_{σ}R_{0}) − ∑{p_{δ}R : δ ∈ S(n)} and define the term τ_{σ}(x) as

τ_{σ}(x) = ∑{p_{δ}ε_{δ}(x) · p_{δ}R : δ ∈ S(n)} + b.

We note that b ∈ A′ by Claim 12 and (2) in the proof of Claim 12. We now will use (R3) to prove that τ_{σ}(x) has the desired property. We will also use that p_{δ} is permutation–invariant for all δ. Let j < n. We want to show f(p_{σ}R_{j}) = τ_{σ}(R_{j}).

From (R3) we prove the following statements (3)–(6). (3) p_{δ}R_{i} ⊆ f(p_{σ}R_{j}) for some i < n, i ≠ j implies p_{δ}R_{i} ⊆ f(p_{σ}R_{j}) for all i < n, i ≠ j.

Indeed, let i, l ≠ j. Assume p_{δ}R_{i} ⊆ f(p_{σ}R_{j}). Let π ∈ S(U) be such that π(R_{i}) = R_{l} and π(R_{j}) = R_{j}. Then p_{δ}R_{l} = p_{δ}πR_{i} = πp_{δ}R_{i} ⊆ πf(p_{σ}R_{j}) = f(πp_{σ}R_{j}) = f(p_{σ}(πR_{j})) = f(p_{σ}R_{j}).

By (3) we have that f(p_{σ}R_{j}) ∩ p_{δ}R ∈ {p_{δ}R, p_{δ}R_{j}, p_{δ}R − p_{δ}R_{j}, 0}.

(4)  p_{δ}R_{j} ⊆ f(p_{σ}R_{j}) implies p_{δ}R_{i} ⊆ f(p_{σ}R_{i}).

Indeed, let π ∈ S(U) be such that πR_{j} = R_{i}. Then p_{δ}R_{i} = p_{δ}πR_{j} = πp_{δ}R_{j} ⊆ πf(p_{σ}R_{j}) = f(πp_{σ}R_{j}) = f(p_{σ}πR_{j}) = f(p_{σ}R_{i}).

(5)  p_{δ}R − p_{δ}R_{j} ⊆ f(p_{σ}R_{j}) implies p_{δ}R − p_{δ}R_{i} ⊆ f(p_{σ}R_{i}).

Indeed, let l ∈ n∖{i, j} and let π ∈ S(U) be such that π(R_{j}) = R_{i} and π(R_{l}) = R_{l}. Then p_{δ}R_{l} = πp_{δ}R_{l} ⊆ πf(p_{σ}R_{j}) = f(p_{σ}R_{i}), and we are done by (3).

By (3)–(5) we have f(p_{σ}R_{j}) ∩ p_{δ}R = τ_{σ}(R_{j}) ∩ p_{δ}R, for all δ ∈ S(n) and j < m. Let X = − ∑{p_{δ}R : δ ∈ S(n)}.

(6)  f(p_{σ}R_{j}) ∩ X = f(p_{σ}R_{i}) ∩ X for all i, j < m.

By (2) we have that X ∈ A′ and f(p_{σ}R_{i}) ∩ X ∈ A′. Let π ∈ S(U) be such that πR_{i} = R_{j} and πa = a for all a ∈ A′. Then f(p_{σ}R_{j}) ∩ X = f(p_{σ}πR_{i}) ∩ πX = πf(p_{σ}R_{i}) ∩ πX = π(f(p_{σ}R_{i}) ∩ X) = f(p_{σ}R_{i}) ∩ X.

We have proved f(p_{σ}R_{j}) = τ_{σ}(R_{j}) for all j < m. To prove the second statement of Claim 13, let us define for all δ ∈ S(n)

ε′_{δ}(x) = \{ \begin{matrix}1 & if ε_{δ}(x) = −x \\ ε_{δ}(x) & otherwise, \end{matrix}

and

τ′_{σ}(x) = ∑{p_{δ}ε′_{δ}(x) · p_{δ}R : δ ∈ S(n)} + b.

Now it is easy to check that τ′_{σ} has the desired property. QED(Claim 13)

We are ready to define our final algebra 𝔄. For any σ ∈ S(n) and j ≤ m let X_{σj} be new elements, different for different pairs ⟨σ, j⟩. We will write X_{j} for X_{Id j}. Let X = {X_{σj} : σ ∈ S(n), j ≤ m}, Y = At𝔄′ ∖ {p_{σ}R : σ ∈ S(n)}. For f_{1}^{U}, ..., f_{r}^{U} and σ ∈ S(n) let the terms τ_{σ}^{1}, ..., τ_{σ}^{r} be as in Claim 13. Below, we will define the auxiliary functions p_{δ}^{𝔄}, too. We will need them when defining f_{i}^{𝔄}. We define 𝔄 = ⟨A, +, −, c_{i}^{𝔄}, d_{ij}^{𝔄}, f_{1}^{𝔄}, ..., f_{r}^{𝔄}⟩ as follows. Let i < n, δ, σ ∈ S(n), j ≤ m.

⟨A, +, −⟩ is a Boolean algebra with atoms Y ∪ X. 𝔄′ ⊆ ⟨A, +, −, c_{i}^{𝔄}, d_{ij}^{𝔄}⟩_{i,j<n}, R = ∑{X_{j} : j ≤ m}.

the operations c_{i}^{𝔄}, p_{δ}^{𝔄}, f_{1}^{𝔄}, ..., f_{r}^{𝔄} are additive,

c_{i}^{𝔄}X_{σj} = c_{i}^{U}p_{σ}^{U}R, p_{δ}^{𝔄}X_{σj} = X_{σ∘δj}, p_{δ}^{𝔄} ↾ A′ = p_{δ}^{U} ↾ A′ and f_{1}^{𝔄}(X_{σj}) = τ_{σ}^{1𝔄}(X_{j}), ..., f_{r}^{𝔄}(X_{σj}) = τ_{σ}^{r𝔄}(X_{j}), f_{1}^{𝔄} ↾ A′ = f_{1}^{U} ↾ A′, ..., f_{r}^{𝔄} ↾ A′ = f_{r}^{U} ↾ A′.

CLAIM 14. There is an equation e valid in RCA_{n} such that 𝔄 |̸= e. Moreover, RCA_{3} ⊧ e.

Proof: Our algebra 𝔄 is very similar to the one used in the proof of Theorem 1 for finite n; and the proof of Claim 14 is practically the same as that of Claim 3. Now we indicate how the equation e exhibited in Remark 2 fails in 𝔄. Let x, x_{0}, ..., x_{m}, y_{0}, ...y_{m} be variables and let e denote the following equation

∏_{j≤m} c_{0}(x · x_{j} ∏_{j≠k≤m} −x_{k}) ≤ c_{0}c_{1}c_{2} ∏_{j<m} c_{1}x · s_{1}^{0}c_{1}x − [c_{2}y_{j} − c_{2}(s_{2}^{1}c_{2}y_{j} − d_{12})].

Now 𝔄 |̸= e can be seen by evaluating the variable x to R, the variables x_{j} to X_{j} ∈ A and evaluating the variables y_{j} to F_{j} ∈ A′. Then the value of the term on the left–hand side of ≤ in e is c_{0}R ≠ 0 while the value of the term on the right–hand side of ≤ is 0. Next we show that RCA_{n} ⊧ e. Indeed, this equation e is the same as ε_{m} from Remark 2, and we showed in the proof of Thm.2 that SNr_{n}CA_{n+2} ⊧ ε_{m}. By RCA_{n} ⊆ SNr_{n}CA_{n+2} this implies RCA_{n} ⊧ e. QED(Claim 14)

CLAIM 15. Every k–generated subalgebra of 𝔄 is isomorphic to a subalgebra of 𝔄′′.

Proof: Let G ⊆ A, |G| ≤ k. We define the equivalence relation ≡ on m + 1 by

i ≡ j iff (∀g ∈ G)(∀σ ∈ S(n))[X_{i} ≤ p_{σ}g ⟺ X_{j} ≤ p_{σ}g].

Let p be the number of blocks of ≡. Then p ≤ 2^{k·n!} because |{p_{σ}g : g ∈ G, σ ∈ S(n)}| ≤ k · n!. Define

B = {a ∈ A : (∀i, j ≤ m)(∀σ ∈ S(n))[i ≡ j and X_{i} ≤ p_{σ}a imply X_{j} ≤ p_{σ}a]}.

We now show that B is closed under the operations of 𝔄. Let b ∈ A be arbitrary. Then for any σ ∈ S(n) there are sets H_{σ} ⊆ m + 1 and there is a ∈ A′ such that a · p_{σ}R = 0 for all σ ∈ S(n) and

b = a + ∑{X_{σj} : σ ∈ S(n), j ∈ H_{σ}}.

It is not difficult to check that A′ ⊆ B and

b ∈ B iff for every σ ∈ S(n) H_{σ} is a union of blocks of ≡ .

This immediately implies that B is closed under the Boolean operations. By c_{i}X_{σj} = c_{i}p_{σ}R ∈ A′ we have c_{i}b ∈ A′ for all b ∈ A, hence B is closed under c_{i}. Let δ ∈ S(n). Then

p_{δ}b = p_{δ}a + ∑{X_{σ∘δj} : σ ∈ S(n), j ∈ H_{σ}},

and hence p_{δ}b ∈ B by p_{δ}a ∈ A′. Finally, we show that B is closed under the functions f_{1}, ..., f_{r}. Let f be one of f_{1}, ..., f_{r} and let τ_{σ}, τ′_{σ} be the terms using +, −, c_{i}, d_{ij}, p_{δ} and constants from A′ belonging to f according to Claim 13. By additivity of f,

f(b) = f(a) + ∑{f(∑{X_{σj} : j ∈ H_{σ}}) : σ ∈ S(n)}.

Now f(a) ∈ A′ ⊆ B by (1) in the proof of Claim 12. Let σ ∈ S(n) be such that H_{σ} ≠ ∅. Then f(∑{X_{σj} : j ∈ H_{σ}}) = ∑{f(X_{σj}) : j ∈ H_{σ}} = ∑{τ_{σ}(X_{j}) : j ∈ H_{σ}} = τ′′_{σ}(∑{X_{j} : j ∈ H_{σ}}), where τ′′_{σ} is τ_{σ} if |H_{σ}| = 1, otherwise τ′′_{σ} is τ′_{σ}. Now x = ∑{X_{j} : j ∈ H_{σ}} ∈ B since H_{σ} is a union of blocks of ≡, hence τ′′_{σ}(x) ∈ B because B is closed under +, −, c_{i}, d_{ij}, p_{δ} and A′ ⊆ B. We have seen that f(b) ∈ B for all b ∈ B.

Let 𝔅 be the subalgebra of 𝔄 with universe B. Clearly, G ⊆ B, hence the subalgebra of 𝔄 generated by G is contained in 𝔅. Therefore it is enough to show that 𝔅 is isomorphic to a subalgebra of 𝔄′′.

Let us recall that ≡ contains ≤ 2^{k·n!} blocks and m ≥ 2^{1+k·n!} = 2 · 2^{k·n!}. Let ⟨E_{j} : j < p⟩ be the partition of m + 1 belonging to ≡. Then there is a partition ⟨G_{j} : j < p⟩ of m with the following property:

|E_{j}| > 1 iff |G_{j}| > 1, for all j < p.

For any H ⊆ m + 1 define

γ(H) = ⋃{G_{k} : k < p, E_{k} ⊆ H}.

We define h : B ⟶ A′′ as follows. For a ∈ A′ and ⟨H_{σ} : σ ∈ S(n)⟩ with H_{σ} ⊆ m + 1 for all σ ∈ S(n),

h(a + ∑{X_{σj} : σ ∈ S(n), j ∈ H_{σ}}) = a + ∑{p_{σ}R_{j} : σ ∈ S(n), j ∈ γ(H_{σ})}.

In more explicit form, the definition of h is: For any b ∈ B

h(b) = b − (∑{X_{σj} : σ ∈ S(n), j ≤ m})
+ ∑{p_{σ}R_{j} : σ ∈ S(n), (∃k, i)[j ∈ G_{k}, i ∈ E_{k}, X_{σi} ≤ b]}.

We want to show that h is a one–one homomorphism. It is easy to check that h is a Boolean homomorphism and h is one–one. Also, it is not difficult to check that h is a homomorphism w.r.t. c_{i} and p_{δ} for i < n, δ ∈ S(n), and that h is the identity on A′. Let f be one of the operations f_{1}^{𝔄}, ..., f_{r}^{𝔄}. We check that h is a homomorphism w.r.t. f.

Let b ∈ B. Then b = a + ∑{X_{σj} : σ ∈ S(n), j ∈ H_{σ}} for some a ∈ A′ and sets H_{σ} ⊆ m + 1 such that each H_{σ} is a union of blocks of ≡. Thus b = a + ∑{b_{σj} : σ ∈ S(n), j ∈ P_{σ}} where P_{σ} ⊆ p and b_{σj} = ∑{X_{σk} : k ∈ E_{j}}. Consider b_{σj} for j ∈ P_{σ}. Then

f(b_{σj}) = \{ \begin{matrix}τ_{σ}(∑\{X_{k} : k ∈ E_{j}\}) & if |E_{j}| = 1 \\ τ′_{σ}(∑\{X_{k} : k ∈ E_{j}\}) & if |E_{j}| > 1. \end{matrix}

and

h(b_{σj}) = ∑{p_{σ}R_{k} : k ∈ G_{j}},

fh(b_{σj}) = \{ \begin{matrix}τ_{σ}(∑\{R_{k} : k ∈ G_{j}\}) & if |G_{j}| = 1 \\ τ′_{σ}(∑\{R_{k} : k ∈ G_{j}\}) & if |G_{j}| > 1. \end{matrix}

By h being a homomorphism w.r.t. +, −, c_{i}, d_{ij}, p_{δ} and being identity on A′ then

hf(b_{σj}) = \{ \begin{matrix}τ_{σ}(∑\{R_{k} : k ∈ G_{j}\}) & if |E_{j}| = 1 \\ τ′_{σ}(∑\{R_{k} : k ∈ G_{j}\}) & if |E_{j}| > 1. \end{matrix}

By |E_{j}| > 1 iff |G_{j}| > 1 we then have hf(b_{σj}) = fh(b_{σj}). Now h(fb) = h(f(a) + ∑{f(b_{σj}) : σ ∈ S(n), j ∈ P_{σ}}) = f(ha) + ∑{fh(b_{σj}) : σ ∈ S(n), j ∈ P_{σ}} = f(h(a) + ∑{h(b_{σj}) : σ ∈ S(n), j ∈ P_{σ}}) = fh(a + ∑{b_{σj} : σ ∈ S(n), j ∈ P_{σ}}) = fh(b). We have seen that h is a one–one homomorphism, therefore 𝔅 is isomorphic to a subalgebra of 𝔄′′. QED(Claim 15)

QED(Theorem 5)

REMARK 5. (i) In Sain[87a] it is proved that if n ≥ ω then there are unary, additive, permutation invariant functions f_{1}^{U}, ..., f_{5}^{U} such that the variety generated by {⟨𝔓(^{n}U), c_{0}^{U}, f_{1}^{U}, ..., f_{5}^{U}⟩ : U is a set} is finitely axiomatizable (in fact, axiomatizable over Boolean algebras by using only one variable) and the operations c_{i}(i < n) are all term-definable. Thus our Theorem 5 shows that the condition n ≥ ω and dropping the diagonal constants in Sain’s result are essential: without these there is a very strong negative result.

(ii) The condition n < ω cannot be omitted from Theorem 5, because of the following. Assume n ≥ ω and let H, G be a partition of n into two parts of size |n|. Let f, g, h, k be functions mapping n into n with the following properties:

f : n ↣ → H, g ⊇ f^{−1},
h : n ↣ → G, k ⊇ h^{−1}.

For any set U, Γ ⊆ n and X ⊆ ^{n}U define

c_{(Γ)}^{U}X = {s ∈ ^{n}U : s ↾ Γ ⊆ z for some z ∈ X}.

We claim that the equational theory of

RA_{n}^{+} = {⟨𝔓(^{n}U), c_{i}, d_{ij}, s_{f}, s_{g}, s_{h}, s_{k}, c_{(H)}, c_{(G)}⟩_{i,j<n} : U is a set}

follows from the set of all equations containing only one variable and valid in RA_{n}^{+}. The reason for this is that the extra operations can be used to “code together two variables” as follows. Let

τ(x, y) = s_{f}x ∩ s_{h}y.

Then it is not difficult to check that

s_{g}c_{(G)}τ(x, y) = x if y ≠ 0 and s_{g}c_{(G)}τ(x, y) = y if x ≠ 0.

(iii) In Biró[89] it is proved that no “first–order definable” functions help in finitely axiomatizing RCA_{n}, n < ω, in the following sense. Let f_{1}^{U}, ..., f_{r}^{U} be any first–order definable functions. Then the variety generated by {⟨𝔓(^{n}U), c_{i}^{U}, d_{ij}^{U}, f_{1}^{U}, ..., f_{r}^{U}⟩_{i,j<n} : U is a set} is not finitely axiomatizable. Thus our Theorem 5 extends Biró’s result beyond first–order definable, in the case the extra operations are unary and additive. We do not know whether “unary, additive” can be omitted^{15} in Theorem 5. That “permutation invariant” cannot be omitted from Theorem 5 is proved both in Biró[89] and in Maddux[89b]. We note that permutation invariance of the operations of RA_{n}^{+} is very desirable. More on this can be read in Németi[90].

(iv) It is proved in Andréka[90d] that Theorem 5 remains true if we replace the condition “f_{i} is additive” with “f_{i} is an exotic quantifier”, where this latter is defined as follows. We say that ⟨f^{U} : U is a set⟩ is an exotic quantifier, if for all U there is a subset Q_{U} ⊆ P(U) of the powerset of U such that for all X ⊆ ^{n}U

f^{U}(X) = {s ∈ ^{n}U : {u : s(0/u) ∈ X} ∈ Q_{U}}.

Exotic quantifiers are not additive, and are not first–order definable, in general. ■

Let n < ω. Then RP A_{n} denotes the variety generated by

{⟨𝔓(^{n}U), c_{i}^{U}, s_{ij}^{U}, p_{ij}^{U}⟩_{i,j<n} : U is a set}

and RP EA_{n} denotes the variety generated by

{⟨𝔓(^{n}U), c_{i}^{U}, d_{ij}^{U}, s_{ij}^{U}, p_{ij}^{U}⟩_{i,j<n} : U is a set}.

15Added in proof: The condition “at most unary” was shown superfluous in Theorem 5 by Madarász. J. and Németi, I. For further improvements of Theorem 5 see the 1997 version of Németi[90], and Madarász-Németi-Sági[97].

(RP A_{n} and RP EA_{n} are called in the literature the classes of all representable polyadic and representable polyadic equality algebras, respectively.^{16}) Johnson[69] proved that none of RP A_{n} and RP EA_{n} is finitely axiomatizable if 3 ≤ n < ω, and he asked whether the diagonal constants contribute to nonfinite axiomatizability of RP EA_{n}, i.e. whether RP EA_{n} is finitely axiomatizable over RP A_{n}. This is Problem 2a in Johnson[69]. Theorem 6 below gives a negative solution to this problem. We note that Problem 2a in Johnson[69] is equivalent to asking whether RP EA_{n} has an equational axiomatization in which the diagonal constants occur in finitely many equations only.

For n ≥ ω, the analogous algebras are called representable quasi-polyadic equality algebras, and their class is denoted by RQP EA_{n}. We do not know whether Theorem 6 remains true if we drop the condition n < ω and replace RP EA_{n} with RQP EA_{n} in it.

We note that for n ≥ ω, the algebras in RP EA_{n} as defined in the literature have much more operations, e.g. they have all the s_{τ} ’s where τ : n → n is any map. It is proved in Németi–Sági[96] that the set of equations valid in RP EA_{ω} is at least Π_{1}^{1}- hard, hence, in particular, is not recursively enumerable. There are more theorems in Németi–Sági[96] supporting the claim that there is no schema-axiomatization of RP EA_{ω}.

THEOREM 6. Let Σ be a set of quantifier–free formulas axiomatizing RP EA_{n}, 3 ≤ n < ω. Let k < ω be any number. Then Σ contains a formula with more than k variables in which some diagonal constant occurs. Thus the diagonal constants occur in infinitely many elements of Σ.

Proof: We will use the proof of Theorem 5 with letting {f_{1}^{U}, ..., f_{r}^{U}} = {p_{ij}^{U}, s_{ij}^{U} : i, j < n}. Take the algebra 𝔄 constructed in the proof of Theorem 5. We choose for p_{ij} the terms of Claim 13 to be τ_{σ} = τ′_{σ} = p_{σ∘[i,j]}(x). We proved in the proof of Theorem 5 that

(i) 𝔄 ∉ RP EA_{n} (ii) every k–generated subalgebra of 𝔄 is in RP EA_{n}.

16Polyadic algebras were introduced and extensively studied by Halmos (see Halmos[54,60,62] and [HMT85]section 5.4). Sometimes they are called Halmos algebras, cf. e.g. Plotkin[88]. Usually, more basic operations are present in polyadic algebras than the ones we use, but these are all term–definable from our basic operations if n < ω. The connections between the two kinds of definitions of polyadic algebras are investigated in Sain–Thompson[88].

So to prove Theorem 6, it is enough to prove that

(iii) there is a representation of 𝔄 in which all operations are the natural ones except for the diagonal constants.

Let U be as in the proof of Theorem 5, and let W ⫌ U be any set.

CLAIM 16. There is a one-one mapping h : A ↣ ⟨𝔓(^{n}W), c_{i}^{W} , d_{ij}^{W} , s_{ij}^{W} , p_{ij}^{W} ⟩_{i,j<n} such that h is a homomorphism w.r.t. all operations of 𝔄 except for d_{ij}, i, j < n.

Proof: Recall U_{i}, i < n and R from the proof of Theorem 5. Let W_{0} = U_{0} ∪(W ∖ U), W_{i} = U_{i} for 0 < i < n. First we define a function h : P(^{n}U) ⟶ P(^{n}W) with the desired properties satisfying in addition h(R) = ×_{i<n}W_{i}.

Let t : W ↠ U be a surjective function which is the identity on U and which maps W_{0} to U_{0}, i.e. t ↾ U = Id_{U} and t^{∗}W_{0} ⊆ U_{0}. Define g : ^{n}W ⟶ ^{n}U by g(s) = t ∘ s for all s ∈ ^{n}W, and for all x ⊆ ^{n}U define

h(x) = {s ∈ ^{n}W : g(s) ∈ x}.

Clearly, h(R) = h( ×_{i<n}U_{i}) = ×_{i<n}W_{i}, and h is a one–one homomorphism w.r.t. all

operations of ⟨𝔓(^{n}U), c_{i}, s_{ij}, p_{ij}⟩_{i,j<n} by Lemma 4(iv).

Recall from the proof of Theorem 5 that |U_{0}| = m, and |U_{i}| > m for all 0 < i < n. Therefore |W_{i}| ≥ m + 1 for all i < n and hence, by Lemma 2, there is a partition

⟨R′_{j} : j ≤ m⟩ of R′ = ×_{i<n}W_{i} such that c_{i}^{W} R′_{j} = c_{i}^{W} R′ for all i < n and j ≤ m.

Then ⟨p_{σ}R′_{j} : j ≤ m⟩ is an analogous partition of p_{σ}R′, for all σ ∈ S(n). We define \overline{h} : A ⟶ P(^{n}W) by

\overline{h}(a) = h(a) if a ∈ A′
\overline{h}(X_{σj}) = p_{σ}R′_{j} if σ ∈ S(n), j ≤ m and
\overline{h}(x + y) = \overline{h}(x) + \overline{h}(y) for x, y ∈ A.

Now it is easy to check that \overline{h} is a one–one homomorphism w.r.t. the operations +, −, c_{i}, p_{ij}, i, j < n. Let i, j < n, i ≠ j. We are going to check homomorphism w.r.t. s_{ij}.

The quantifier–free formula x ≤ −d_{ij} → s_{ij}(x) = 0 is valid in RA_{n}^{+}, hence it is valid in 𝔄 since the k–generated subalgebras of 𝔄 are in RA_{n}^{+} and we may assume k ≥ 1. Let σ ∈ S(n), l ≤ m. Then s_{ij}(X_{σl}) = 0 in 𝔄. Now \overline{h}(s_{ij}(X_{σl})) = \overline{h}(0) = 0 = s_{ij}p_{σ}R′_{l} = s_{ij}\overline{h}(X_{σl}). Assume that a ∈ A′. Then \overline{h}(s_{ij}a) = h(s_{ij}a) = s_{ij}h(a) = s_{ij}\overline{h}(a) since A′ is closed under s_{ij} and h is a homomorphism w.r.t. s_{ij}. Since both \overline{h} and s_{ij} are additive, we are done. QED(Claim 16) QED(Theorem 6)

Problem 2.16 in Henkin–Monk–Tarski[HMT71] asks if RCA_{n} can be axiomatized with a set of equations in which complementation occurs in only finitely many equations. One reason for asking this was that the “perfect extension” of an RCA_{n} is an RCA_{n} again, and the natural condition for equations to be preserved under “perfect extensions” is that complementation − does not occur in them. Theorem 7 below gives a negative answer to this problem.

Subalgebras of complementation–free reducts of RCA_{n}’s arise in a natural way in the study of databases, cf. Comer[89], Cosmadakis[87], Imielinski–Lipski[84], Düntsch[90,90a,93]. Comer asked in the problem session of the 1988 Algebraic Logic Conference in Budapest whether the class RCA_{n}^{−} of all these subreducts is a variety or not. This was Problem 11 in Maddux[88]. Comer proved that RCA_{n}^{−} is a quasi–variety which is not finitely axiomatizable. Theorem 7 below states that RCA_{n}^{−} is not a variety, thus giving a negative answer to Comer’s question.

Theorem 7 below states that not only complementation, but also the other Boolean operations, + or · , have to occur infinitely many times in any axiomatization of RCA_{n}.

For any algebra ℭ similar to RCA_{n}’s, the complementation–free reduct ℭ^{−} of ℭ is defined as

ℭ^{−} = ⟨C, +^{ℭ}, ·^{ℭ}, 0^{ℭ}, 1^{ℭ}, c_{i}^{ℭ}, d_{ij}^{ℭ}⟩_{i,j<n}.

Then RCA_{n}^{−} is the class of all subalgebras of ℭ^{−} for some ℭ ∈ RCA_{n}.

THEOREM 7. (i) Let Σ be a set of equations axiomatizing RCA_{n}, n ≥ 3. Let ℓ < n, and k < n, k′ < ω be natural numbers. Then Σ contains infinitely many equations in which − occurs, one of + or · occurs, a diagonal constant with index ℓ occurs, more than k cylindrifications and more than k′ variables occur. The same holds for any K in place of RCA_{n} such that _{∞}Cs_{n} ⊆ K ⊆ RCA_{n}.

(ii) RCA_{n}^{−} is not a variety.

Proof: To prove Theorem 7, we shall use the constructions of the proofs of Theorem 3, Theorem 4. We proved earlier that several reducts of these algebras 𝔄 are representable. Here we shall prove that

(a) the complementation–free reduct 𝔄^{−} of 𝔄 is a homomorphic image of a subalgebra ℭ of the complementation free reduct 𝔓^{−} of a 𝔓 ∈ _{∞}Cs_{n}.

(b) 𝔄^{−} ∉ RCA_{n}^{−}.

(c) 𝔄 can be represented as a _{∞}Cs_{n} such that every operation of 𝔄 except for “∪” and “∩” are the natural ones.

These will prove Theorem 7 as follows. Let Σ^{−} denote the set of all equations valid in _{∞}Cs_{n} in which − does not occur. Let ℭ, 𝔓 be as in (a). Then 𝔓 ⊧ Σ^{−} because 𝔓 ∈ _{∞}Cs_{n}. Then 𝔓^{−} ⊧ Σ^{−}, because − does not occur in Σ^{−}. Then ℭ ⊧ Σ^{−} by ℭ ⊆ 𝔓^{−}, and then 𝔄^{−} ⊧ Σ^{−} since 𝔄^{−} is a homomorphic image of ℭ and Σ^{−} consists of equations. Then 𝔄 ⊧ Σ^{−}. This, together with our previous arguments, proves (i) of Thm.7. To prove (ii) of Thm.7, notice that (a) implies that 𝔄^{−} is a homomorphic image of a member of RCA_{n}^{−}, namely of ℭ, and thus (b) implies that RCA_{n}^{−} is not closed under taking homomorphic images, showing that RCA_{n}^{−} is not a variety.

First we prove (a),(b) for the case n ≥ ω. Let ⟨W_{i} : i ≤ n⟩, m be as in the proof of Theorem 3, i.e. let w ∉ U, and W_{0} = U_{0} ∪ {w}, |U_{0}| = m, W_{i} = U_{i} if 0 < i ≤ n and let W = ⋃{W_{i} : i ≤ n} = U ∪ {w}.

Let R′ = ×_{i<n}W_{i} and let R′_{j}, j ≤ m be a partition of R′ such that c_{i}R′_{j} = c_{i}R′

for all i < n, j ≤ m. Such a partition exists by |W_{i}| ≥ m + 1 for all i < n and by Lemma 2.

Let u ∈ U_{0} be fixed. Let [w/u] : W ⟶ W be the mapping of W that sends w to u and leaves all other points of W fixed, and let [w, u] be the permutation of W that interchanges w and u and leaves all other elements of W fixed. For any s ∈ ^{n}W let s(w/u) = [w/u] ∘ s, i.e.

s(w/u)_{i} = \{ \begin{matrix}s_{i} & if s_{i} ≠ w, \\ u & if s_{i} = w. \end{matrix}

Let π = [u, w]. Let G denote the set of all permutations of U which leave each U_{i} (i ≤ n) fixed. For a ⊆ ^{n}U let

Ga = {g ∘ s : s ∈ a, g ∈ G}.

Let

D = {s ∈ ^{n}W : {u, w} ⊆ Rng s},

B′ = {x ⊆ ^{n}W : x = πx, (x ∩^{n}U) = G(x ∩^{n}U), and (∀s ∈ x ∩ D)s(w/u) ∈

x},
B = {⋃{R′_{j} : j ∈ J} ∪ x : J ⊆ m + 1, x ∈ B′}.

We are going to show that B is closed under ∪, ∩, c_{i}^{W} and {∅,^{n}W, d_{ij}^{W} } ⊆ B′ ⊆ B for all i, j < n. It is not difficult to see that B′ is closed under ∪, ∩ and ∅,^{n}W, d_{ij}^{W} ∈ B′. Next we show that B′ is closed under c_{i}^{W}. Let i < n and x ∈ B′. Clearly, c_{i}x = πc_{i}x by x = πx. Let s ∈ c_{i}x ∩ ^{n}U and g ∈ G. Then z = s(i/v) ∈ x for some v. If v ∈ U, then z ∈ x ∩^{n}U, and then g ∘ z ∈ x. But g ∘ s and g ∘ z differ at most at place i, so g ∘ s ∈ c_{i}x and we are done. Assume therefore v ∉ U, i.e. v = w. Then i is the only element of n for which z_{i} = w, hence z(w/u) differs from s only at place i. So it is enough to show z(w/u) ∈ x. If z ∈ D, then this is immediate by x ∈ B′. If z ∉ D, then u ∉ Rng z, and hence z(w/u) = π ∘ z ∈ x. We have seen (c_{i}x ∩^{n}U) = G(c_{i}x ∩^{n}U). To verify the last condition for c_{i}x, let s ∈ D, s ∈ c_{i}x. Then z = s(i/v) ∈ x for some v. If z ∈ D then z(w/u) ∈ x by x ∈ B′, and therefore s(w/u) ∈ c_{i}x because s(w/u) = z(w/u)(i/v′) for some v′. Assume therefore z ∉ D. Then s_{i} ∈ {u, w} and s_{i} ∉ Rng z by s ∈ D. If s_{i} = w then s(w/u) = s(i/u) ∈ c_{i}x and we are done. Assume s_{i} = u. Then z(w/u) = [w, u] ∘ z by u ∉ Rng z, hence z(w/u) ∈ x by x ∈ B′, z ∈ x. Then s(w/u) ∈ c_{i}x as in the previous case and we are done with showing c_{i}x ∈ B′.

Now we are going to show that B is also closed under ∪, ∩, and c_{i}^{W}. It is clear that B is closed under ∪. To show closure of B under ∩, notice first that R′ ∈ B′, and R′ ⊆ x whenever x ∩ R′ ≠ ∅ and x ∈ B′. (To show this latter, we use x ∩^{n}U = G(x ∩^{n}U) and x = πx.) Thus x ∩ R′_{j} = ∅ or x ∩ R′_{j} = R′_{j} for all x ∈ B′ and j ≤ m. This implies that B is closed under ∩. To show closure of B under c_{i}, let b = r + x where r = ⋃{R′_{j} : j ∈ J} for some J ⊆ m + 1 and x ∈ B′. Then c_{i}b = c_{i}r + c_{i}x. By c_{i}R′_{j} = c_{i}R′ then c_{i}r = c_{i}R′ or c_{i}r = ∅. Thus c_{i}r, c_{i}x ∈ B′ by R′, ∅, x ∈ B′, hence c_{i}b ∈ B′ ⊆ B.

We have seen that B is closed under ∪, ∩, c_{i}^{W} and ∅,^{n}W, d_{ij}^{W} ∈ B. Let 𝔅 = ⟨B, ∪, ∩, ∅,^{n}W, c_{i}^{W} , d_{ij}^{W} ⟩_{i,j<n}. Then 𝔅 is a subalgebra of the complementation– free reduct 𝔓^{−} of 𝔓 = ⟨𝔓(^{n}W), c_{i}^{W} , d_{ij}^{W} ⟩_{i,j<n}.

We are going to show that the complementation–free reduct 𝔄^{−} of 𝔄 is embeddable into a homomorphic image of 𝔅. To this end, first we define an algebra ℭ and a homomorphism of 𝔅 into ℭ. Let

V = ^{n}W ∖ D,
C = P(V), c_{i}^{ℭ}(x) = (c_{i}^{W} x) ∩ V, d_{ij}^{ℭ} = d_{ij}^{W} ∩ V,
ℭ = ⟨C, ∪, ∩, ∅, V, c_{i}^{ℭ}, d_{ij}^{ℭ}⟩_{i,j<n}.

Let g : B ⟶ C be defined by g(x) = x ∩ V for all x ∈ B. We are going to show that g : 𝔅 ⟶ ℭ is a homomorphism. It is clear that g is a homomorphism w.r.t. +, ·, 0, 1, d_{ij}, i, j < n.

Let i < n and x ∈ B. We want to show that g(c_{i}^{𝔅}x) = c_{i}^{ℭ}g(x), i.e. that (c_{i}^{W} x) ∩ V = c_{i}^{W} (x ∩ V) ∩ V. It is enough to check this for x ∈ {R′_{j} : j ≤ m} ∪ B′.

Now R′ ∩ D = ∅ because if s ∈ R′ = ×_{i<n}W_{i}, then the only i for which s_{i} ∈ W_{0}

is 0, i.e. (Rng(s)) ∩ W_{0} = {s_{0}}. Then if s_{0} = u then w ∉ Rng(s), and if s_{0} = w then u ∉ Rng(s) by u ∈ U_{0}. So, if x = R′_{j} for some j ≤ m then x ∩ V = x and we are done. Assume x ∈ B′. The inclusion ⊇ is clear. Let s ∈ c_{i}^{W} x, s ∉ D. Then z = s(i/v) ∈ x for some v. If z ∉ D then z ∈ x ∩ V and we are done. Assume z ∈ D. Then v ∈ {u, w} and v ∉ Rng s. Assume v = w. By z ∈ x∩D, x ∈ B′ then z(w/u) = s(i/u) ∈ x, and s(i/u) ∈ V by w ∉ Rng s. Thus s(i/u) ∈ x ∩ V and we are done. The case v = u is similar: By z ∈ x∩D we have z(u/w) = π∘z(w/u) ∈ x. By u ∉ Rng(s) then z(u/w) = s(i/w) ∈ x ∩ V and we are done with showing that g is a homomorphism w.r.t. c_{i}.

Let M = {x ∩ V : x ∈ B} and 𝔐 = ⟨M, ∪, ∩, ∅, V, c_{i}^{ℭ}, d_{ij}^{ℭ}⟩_{i,j<n}. Then 𝔐 is a homomorphic image of 𝔅.

We now show that 𝔄^{−} is embeddable into 𝔐. Recall that any element of A is of form ∑{R_{j} : j ∈ J} + a where J ⊆ m + 1 and a ∈ A′, a ∩ R = 0, because 𝔄 is obtained from 𝔄′ by splitting R into m + 1 parts R_{j}, j ≤ m. Let π = [u, w]. We define h : A ⟶ M as follows. For any J ⊆ m + 1 and a ∈ A′, a ∩ R = 0 we define

h(∑{R_{j} : j ∈ J} + a) = ⋃{R′_{j} : j ∈ J} ∪ a ∪ πa.

First we check that h is well defined, h is one–to–one, and h(a) ∈ M for all a ∈ A. Now, h is well defined because if ∑{R_{j} : j ∈ J} + a = ∑{R_{j} : j ∈ J′} + a′ a, a′ ∈ A′, a · R = a′ · R = 0, then J = J′ and a = a′. h is one-to-one because if a ≠ a′, a, a′ ∈ A′, a · R = a′ · R = 0, and s ∈ a − a′, then s ∉ R′ ∪ a′ ∪ πa′. Finally, let y = ∑{R_{j} : j ∈ J} + a, a ∈ A′, a · R = 0. We want to show that h(y) ∈ M. Let x = a ∪ πa. Then x = πx by π ∘ π = Id. Also, x ∩ D = ∅ since if s ∈ a then w ∉ Rng(s) by a ⊆ ^{n}U, w ∉ U, and thus u ∉ Rng(π ∘ s). Finally, x ∩ ^{n}U = a because if s ∈ a, then π ∘ s ∈ ^{n}U only if u ∉ Rng s, and then π ∘ s = s. By a ∈ A′, R = G(R), and since A′ is generated by R, we have that a = G(a). Thus x ∩^{n}U = G(x ∩^{n}U). This shows x ∈ B′ and x ⊆ V. We have already seen that R′ ⊆ V. Thus h(y) ∈ B and h(y) ⊆ V, i.e. h(y) ∈ M.

We are going to check that h is a homomorphism on 𝔄^{−}. It is easy to see that h preserves +, ·, ∅, d_{ij} and h(^{n}U) = V. (When checking ·, we use a ∩ (πb) ⊆ a ∩ b if a, b ⊆ ^{n}U.) It remains to show that h preserves c_{i}. Let a ∈ A′ be arbitrary. First we show that

(*) h(c_{i}^{U}a) = c_{i}^{U}a ∪ π(c_{i}^{U}a).

Indeed, if R ∩ c_{i}^{U}a = ∅, then (*) is immediate by the definition of h. Assume R ∩ c_{i}^{U}a ≠ ∅. Then R ⊆ c_{i}^{U}a by a ∈ A′. Now by using R′ = R ∪ πR and R ⊆ c_{i}^{U}a we get

h(c_{i}^{U}a) =  R′ ∪ (c_{i}^{U}a ∖ R) ∪ π(c_{i}^{U}a ∖ R)
=  R ∪ πR ∪ (c_{i}^{U}a ∖ R) ∪ (πc_{i}^{U}a ∖ πR)
=  R ∪ (c_{i}^{U}a ∖ R) ∪ πR ∪ (πc_{i}^{U}a ∖ πR)
=  c_{i}^{U}a ∪ πc_{i}^{U}a.

Next, we will prove that

(**) c_{i}^{U}a ∪ π(c_{i}^{U}a) = c_{i}^{W} (a ∪ πa) ∩ V.

Indeed, the inclusion ⊆ is clear. Let s ∈ c_{i}^{W} (a ∪ πa) ∩ V. Then s(i/v) ∈ a ∪ πa for some v ∈ W. Assume s_{i} ∉ {u, w}. Then s ∈ c_{i}^{U}a ∪ πc_{i}^{U}a. Assume s_{i} = w. Then u ∉ Rng s by s ∈ V. If s(i/v) ∈ a, then s_{j} ≠ w for all j ≠ i, hence π ∘ s ∈ c_{i}^{U}a. If s(i/v) ∈ πa, then π ∘ s ∈ c_{i}^{U}a. Assume s_{i} = u. Then w ∉ Rng s by s ∈ V. If s(i/v) ∈ a, then s ∈ c_{i}^{U}a. If π ∘ s(i/v) ∈ a, then s_{j} ≠ u for all j ≠ i, hence s and π ∘ s(i/v) differ only at i, so s ∈ c_{i}^{U}a.

We are ready to prove that h preserves c_{i}. Let i < n, j ≤ m, and a ∈ A′, a∩R = ∅ be arbitrary. Now h(c_{i}^{𝔄}R_{j}) = h(c_{i}^{U}R) = c_{i}^{W} (R ∪ πR) ∩ V =(c_{i}^{W} R′) ∩ V =(c_{i}^{W} R′_{j}) ∩ V =c_{i}^{ℭ}h(R_{j}). Also, h(c_{i}^{𝔄}a)=h(c_{i}^{U}a)=c_{i}^{W} (a ∪ πa) ∩ V =c_{i}^{ℭ}h(a). Since h preserves +, we are done.

We showed that 𝔄^{−} is embeddable into 𝔐, and 𝔐 is a homomorphic image of 𝔅 ⊆ 𝔓^{−}. Thus, by basic universal algebraic facts we have that 𝔄^{−} is a homomorphic image of a subalgebra of 𝔓^{−}. We proved (a).

To show (b), let q denote the following formula

ε ∧ χ → ∏_{i≤m}c_{0}x_{i} = 0

where ε, χ are the following formulas respectively

∏_{i≤m}s_{i}^{0}c_{1} … c_{m}x ≤ ∑_{i<j≤m}d_{ij}

⋀_{i,k≤m+1,i≠k}x_{i} · x_{k} = 0 ∧ x_{i} ≤ x.

Then it is not difficult to check that RCA_{n} ⊧ q and 𝔄^{−} |̸= q. One way of doing this is noticing that we basically did this in the proof of Claim 1, since our formula ε is equivalent to τ(x) = 0 for the τ(x) used in the proof of Claim 1. This proves that 𝔄^{−} ∉ RCA_{n}^{−}.

Now we show how to modify the above proofs of (a)-(b) for the case n < ω. Let W, ⟨W_{i} : i ≤ n⟩, f : W ↣ → W be as in the proof of Theorem 4 (cf. the proof of Claim 8). Let e be the smallest equivalence relation containing f. Fix some u ∈ U_{0}, w ∈ W ∖U and let w/e = {v : v e w}, u/e = {v : v e u}. Let δ : w/e ↣ → u/e be such that δ preserves f, and let

σ = δ ∪ Id ↾ U_{0},
π = δ ∪ δ^{−1} ∪ Id ↾ (U_{0} ∖ u/e).

Then σ : W_{0} ⟶ U_{0} and π : W_{0} ↣ → W_{0}. Define s(w/u) = σ ∘ s. Let R′ = ×_{i<n}W_{i}

and let R′_{j}, j ≤ n be a partition of R′ such that c_{i}R′_{j} = c_{i}R′ for all i < n, j ≤ m. Let G be the set of all permutations of U that leave R and F (in the definition of 𝔄) fixed. Let

D = {s ∈ ^{n}W : u/e ∩ Rng(s) ≠ ∅, w/e ∩ Rng(s) ≠ ∅},

B′ = {x ⊆ ^{n}W : x = πx, (x ∩^{n}U) = G(x ∩^{n}U), and (∀s ∈ x ∩ D)s(w/u) ∈

x},
B = {⋃{R′_{j} : j ∈ J} ∪ x : J ⊆ m + 1, x ∈ B′}.

Then B is closed under the operations of 𝔓^{−} = ⟨P(^{n}W), ∪, ∩, ∅,^{n}W, c_{i}^{W} , d_{ij}^{W} ⟩_{i,j<n}. Let 𝔅 ⊆ 𝔓^{−} with universe B. Let V, C and g be as in the previous case (n ≥ ω). Then g : 𝔅 ⟶ ℭ is a homomorphism, and the function h defined as in the previous proof embeds 𝔄^{−} into the image of 𝔅 along g.

This shows (a). To prove 𝔄^{−} ∉ RCA_{n}^{−} let q′ denote the following formula

φ ∧ ε ∧ δ ∧ χ → ∏_{i≤m}c_{0}x_{i} = 0

where m = K · (n − 1) and φ, ε, δ, χ are the following formulas respectively

⋀_{i<K}y_{i} · s_{2}^{1}y_{i} ≤ d_{12} ∧ y_{i} = c_{2}y_{i} ∧ z = ∑_{i<K}y_{i}

c_{2}(s_{2}^{1}z · s_{2}^{0}z) ≤ z ∧ z = s_{0}^{2}s_{1}^{0}s_{2}^{1}c_{2}z ∧ d_{01} · c_{1}z ≤ z

⋀_{i<n}s_{i}^{0}c_{1}z · ⋀_{i<j<n} − s_{i}^{0}s_{j}^{1}z = 0

⋀_{i<j≤m}x_{i} · x_{j} = 0 ∧ c_{1} … c_{n−1} ∑_{i≤m}x_{i} = c_{1}z.

Then what we did in Claim 7 was to show that RCA_{n} ⊧ q′ while 𝔄 |̸= q′. Since complementation does not occur in q′, this shows that 𝔄^{−} ∉ RCA_{n}^{−}.

Finally we show how to represent the “∪” and “∩”–free reducts of our algebras. We will treat the cases n ≥ ω and n < ω together.

Let m, U, ⟨U_{i} : i ≤ n⟩, R, 𝔄′, R_{j}, j ≤ m and 𝔄 be as in the proofs of Theorem 3, Theorem 4. We may assume that m ≥ 3. Let R′_{j}, j < m be a partition of R such that c_{i}R′_{j} = c_{i}R for all i < n, j < m. Let z ∈ R ∖ (R′_{0} ∪ R′_{1}) be fixed and let η : {J ⊆ m + 1 : 0 ∈ J} ↣ {G ⊆ R ∖ (R′_{0} ∪ R′_{1}) : z ∈ G} be an arbitrary injection. We are going to define a function h : A ⟶ P(^{n}U). Recall that every element of A is of form ∑{R_{j} : j ∈ J} + a where J ⊆ m + 1 and a ∈ A′ ⊆ P(^{n}U). Let J ⊆ m + 1. Then we define

h(∑\{R_{j} : j ∈ J\}) = \{ \begin{matrix}R′_{0} ∪ η(J) & if 0 ∈ J, J ≠ m + 1 \\ R ∖ (R′_{0} ∪ η((m + 1) ∖ J)) & if 0 ∉ J, J ≠ ∅ \\ 0 & if J = ∅ \\ R & if J = m + 1. \end{matrix}

Let a ∈ A be arbitrary. Then we define

h(a) = (a ∖ R) ∪ h(a ∩ R).

It is easy to see that h : 𝔄 ↣ ⟨𝔓(^{n}U), c_{i}^{U}, d_{ij}^{U}⟩_{i,j<n} is a one–one homomorphism w.r.t. −, ∅,^{n}U, c_{i}^{U}, d_{ij}^{U}. QED(Theorem 7)

ON ALGEBRAS OF BINARY RELATIONS.

Besides the class RCA_{n} of algebras of n–ary relations, Tarski proposed another class for generalizing Boolean algebras, the class RRA of algebras of binary relations. This class RRA differs from RCA_{2} in having one additional binary operation, namely the composition of binary relations and in having also p_{01}.

This new operation makes the algebras very “strong”: RRA is not finitely axiomatizable (Monk[64]), though RCA_{2} and RP EA_{2} are finitely axiomatizable (a result of Henkin and Tarski^{17}). The theory of RRA is very similar to that of RCA_{n}, n ≥ 3, and it is a general practice that theorems proved for RCA_{n} can be proved for RRA, and vice versa (though this “transfer” is not trivial or mechanical at all). Each of these two kinds of algebras of relations has its own advantage and disadvantage over the other one. The classes RCA_{n} are more convenient in that they have only unary operations in addition to the Boolean ones (unary operations are much easier to handle than binary ones), and the connection between equations of RCA_{n} and first–order formulas is very close, almost trivial. On the other hand, algebras in RRA are very familiar in the general mathematical practice, their definition is very simple and easy to grasp. The strength of RRA comes from the operation of composition of relations, which forms a semigroup. So, basically, RRA’s are Boolean algebras endowed with a semigroup structure.

17For proofs see [HMT85]3.2.65, 5.4.33.

There are, however, differences between RCA_{n}’s and RRA’s. We saw that the “strength of RCA_{n}” is distributed among the operations of RCA_{n} quite evenly. We shall see that all the strength of RRA is concentrated in relation composition: this operation is so strong that relative to it, all the other non–Boolean operations are finitely axiomatizable.

Let U be a set, and R, S be binary relations on U, i.e. R, S ⊆ U × U. Then we define

R | S = {(u, v) : (u, w) ∈ R and (w, v) ∈ S for some w ∈ U},
R^{−1} = {(v, u) : (u, v) ∈ R},
Id_{U} = {(u, u) : u ∈ U},
ℜ𝔢(U) = ⟨𝔓(U × U), |,^{−1}, Id_{U}⟩,
Ra_{2} = {ℜ𝔢(U) : U is a set }.

ℜ𝔢(U) is called the full relation set algebra on U. The class of all subalgebras of Ra_{2} is called the class Rs of all relation set algebras, or of all proper relation algebras (this is the analogon of Cs_{n}). The variety generated by Ra_{2} is the class of all subdirect products of Rs’s and is called RRA, the class of all representable relation algebras. We note that IRs, the class of isomorphic copies of elements of Rs, is axiomatizable by quantifier–free formulas. We are going to show that every axiomatization of Rs (or of RRA) (by quantifier–free formulas) must contain infinitely many formulas in which all of the Boolean operations and also relation composition occur. This answers, in the negative, a problem raised in Jónsson[59].

The operations |,^{−1} and Id_{U} in (proper) relation algebras are often denoted by ; ,˘ and 1′, respectively. We often write x̆ in place of x˘ (or ˘ (x)). Let 𝔄 = ⟨A, +, ·, −, 0, 1,; ,˘ , 1′⟩ be an algebra similar to Rs’s. We say that 𝔄 is a relation algebra if it satisfies the following finite set of equations (introduced in Chin– Tarski[51], see also Henkin–Monk–Tarski[HMT85]5.3.1 or Jónsson[82]Def.2.1).

⟨A, +, ·, −, 0, 1⟩ is a Boolean algebra,

⟨A,; ,˘ , 1′⟩ is an involuted monoid, ; and˘ distribute over join, x̆; [−(x; y)] ≤ −y.

A relation algebra 𝔄 is called weakly representable (a wRRA) if it is representable as an algebra of binary relations where all the operations except perhaps + and − have their natural set theoretic meanings (i.e. ·, 0, 1,; ,˘ , 1′ denote set theoretic intersection, empty set, biggest set, relation composition, inverse or converse, and identity relation respectively but + and − do not necessarily denote union and complementation). This notion was introduced in Jónsson[59], where an infinite set of quasi–equations was given to axiomatize the class of all weakly representable relation algebras. Problem 3 in Jónsson[59] asks if every wRRA is representable such that every operation including + and − is standard (is an RRA) or not. This amounts to asking whether there is a cause of nonrepresentability that can be attributed to “union and complementation” solely. In this sense, the subject belongs to the investigation of reducts of relation algebras, a survey paper on which is Schein[88]. The infinite set Σ of quasi–equations given in Jónsson[59] and characterizing wRRA is such that + and − occur only in finitely many formulas in it. Therefore our theorem stating that RRA cannot be axiomatized with such sets (Theorem 7 below) implies that wRRA ≠ RRA, thus giving a negative answer to Problem 3 in Jónsson[59]. (We will state a stronger theorem.)

We note that it is proved in Haiman[87] that wRRA is not axiomatizable with a finite set of quantifier–free formulas (answering the first part of Problem 1 in Jónsson[59]).

THEOREM 8. Let Σ be a set of quantifier–free formulas axiomatizing RRA over wRRA, i.e. such that RRA = Mod(Σ) ∩ wRRA. Assume that no formula in Σ contains both + and ·. Then there are infinitely many formulas in Σ in which all of ; , − and one of +, · occur. The same holds for IRs in place of RRA.

The proof of Theorem 8 can be found in Andréka[94].

REMARK 7. The conditions of Theorem 8 are best possible because of the following. The operation · is term–expressible with −, + and + is term–expressible with −, · in Boolean algebras (e.g. x · y = −(−x + −y)), thus Theorem 7 becomes false if we replace “one of +, ·” in it with “+” or with “·”. Also, − is expressible with + and ·, namely x · y = 0 ∧ x + y = 1 → y = −x holds in Boolean algebras. Hence the condition “no formula in Σ contains both + and ·” cannot be omitted in Theorem 8. We note that this condition can be omitted if we replace “quantifier– free formulas” with “equations” in Theorem 8. This is proved in Andréka[90b] by using relation algebras belonging to finite projective geometries, i.e. using the so called Lyndon algebras 𝔏_{n} for n < ω. It is proved in Andréka[90b] that the complementation–free reduct 𝔏_{n}^{−} of 𝔏_{n} is a homomorphic image of a subalgebra of 𝔏_{m}^{−} if m ≥ n. Since 𝔏_{m} ∈ RRA for infinitely many m, this implies that all the equations valid in RRA that do not contain − are valid in all Lyndon algebras. This argument replaces the one in the proof of Theorem 8 for showing that 𝔅(n, ω) is weakly representable. The rest of the proof in Andréka[90b] is very similar to that of Theorem 8. Jónsson[84] proved by using the above mentioned Lyndon algebras that RRA cannot be axiomatized with a set of quantifier–free formulas using finitely many variables. This result is strengthened in Andréka[90b] to the statement that in any equational axiomatization of RRA, for any k < ω, there are infinitely many equations containing more than k variables, and containing at the same time ; , − and one of +, ·. We also note that ˘ , 1′ do not necessarily have to occur infinitely many times in an axiomatization of RRA.: There is an equational axiomatization of RRA in which ˘ and 1′ occur in finitely many formulas only. This is proved in Andréka–Németi[96]. ■

REMARK 8. Subreducts of RRA are extensively investigated, a survey paper on this is Schein[88]. There are still many interesting open problems in this area.

Clearly, | is characterised as a semigroup, |, ⊆ was characterized by Zaretskij[59], and |, ∩ was characterized by Bredikhin–Schein[78]. Characterizations for |, ⊆, Id or for |, ∩, Id are not known.

The characterization of |, ∩ is very simple: Any semilattice–ordered semigroup is isomorphic to a set of binary relations with the operations |, ∩. The corresponding question for |, ∪ was investigated since at least 1962. It was conjectured that every distributive semilattice–ordered semigroup is representable with binary relations, |, ∪. It was also not known whether the class

K = I{⟨A, |, ∪⟩ : A is a set of binary relations closed under |, ∪}

is a variety or not. It is proved in Andréka[89] that the answer is in the negative:

THEOREM. K is not axiomatizable with finitely many variables, and K is not a variety.

In the proof of the above theorem, the following set of quasi–equations witnessing non–finite axiomatizability of K is exhibited: Let m < ω and let q_{m} denote the following quasi–equation

⋀_{i<m}[x ⊆ x′_{i} ∪ x′′_{i} ∧ y ⊆ y′_{i} ∪ y′′_{i}] →

x | y ⊆ (x | y′_{0}) ∪ ⋃_{i<n−1}(x′_{i} | y′′_{i}) ∪ (x′′_{i} | y′_{i+1}) ∪ (x′_{n−1} | y′′_{n−1}) ∪ (x_{n−1} | y).

Then it is proved in Andréka[89] that K ⊧ {q_{m} : m < ω} but any set Σ of universal formulas containing finitely many variables, or any finite set of first–order formulas, can imply only finitely many of q_{m}, m < ω. We know that {q_{m} : m < ω} does not axiomatize K. To find a (relatively simple) axiom system for the quasi– equational theory of K is still an open problem.

It is proved in Andréka[91] Theorem 1, that a distributive semilattice–ordered semigroup is isomorphic to an algebra of binary relations iff it can be embedded into such a structure where the semilattice part is distributive in the lattice–theoretical sense, i.e. if

a ≤ b ∪ c implies a = b′ ∪ c′ for some b′ ≤ b, c′ ≤ c.

This theorem might help in finding an axiomatization of K.

It is proved in Andréka[89] and in Andréka[91] together, that no distinguished familiar operations on binary relations help in finitely axiomatizing |, ∪ in the following sense. Let ^{∗} denote the operation of forming transitive closure of a binary relation and let M be a set of operations on binary relations such that {|, ∪} ⊆ M ⊆ {|, ∪, ∩, −, ∅, Id,^{−1},^{∗}}. Let

K(M) = I{⟨A, f⟩_{f∈M} : A is a set of binary relations closed under all f ∈ M}.

Then K(M) is not finitely axiomatizable, moreover if ∩ ∉ M then the quasi– equational theory of K(M) is not axiomatizable by using finitely many variables. It would be interesting to know whether there are operations definable in RRA which together with |, ∪ can be finitely axiomatized.

The operation ^{∗} is investigated in Kleene–algebras, and the above theorem applies to Kleene–algebras (studied in computer science), too. The operations of Kleene–algebras are |, ∪, ∅,^{−1},^{∗}, Id. Redko[64] proved that the equational theory of the ^{−1}–free Kleene–algebras is not finitely axiomatizable, and Kozen[81] proved that the equational theory of the ^{∗}–free Kleene–algebras is finitely axiomatizable. By our theorem above, the quasi–equational theory of any of these reducts is not finitely axiomatizable. ■

References

Andréka,H. [88], On taking subalgebras of relativized relation algebras, Algebra Universalis 25

(1988), 96–100. Andréka,H. [89], On the union–relation composition reducts of relation algebras, Abstracts of

Amer. Mat. Soc. 10,2 (March 1989), 174. (*89T–08–21). Preprint of Math. Inst., Budapest, Sept. 1988.

Andréka,H. [90], One variable is not enough for defining relation algebras but two are, Algebra

Universalis 28 (1991), 274-279. Andréka,H. [90a], Weakly representable but not representable relation algebras, Algebra Uni-

versalis 32 (1994), 31-43. Andréka,H. [90b], Positive reducts of representable relation algebras is not closed under ho-

momorphisms. Preprint, Budapest, 1990. Andréka,H. [90c], Finite axiomatizability of SNr_{n}CA_{n+1} and non–finite axiomatizability of

SNr_{n}CA_{n+2}. Lecture notes for a series of lectures given at Algebraic Logic Meeting, Oakland, CA, June 1990.

Andréka,H. [90d], The completeness problem of logics with finitely many variables, tools from beyond first–order logic, algebraic logic. Manuscript, 1990. Material presented at Sixth Southeastern Logic Symposium, Miami Beach, USA, March 1990.

Andréka,H. [91], Representations of distributive lattice–ordered semigroups with binary rela-

tions, Algebra Universalis 28 (1991), 12–25. Andréka,H. and Bredikhin,D. [95], The equational theory of union-free algebras of relations,

Algebra Universalis 33,4 (1995), 516-532. Andréka,H. Comer,S.D. and Németi,I. [83], Epimorphisms in cylindric algebras. Preprint,

Math. Inst. Budapest. Andréka,H. Comer,S.D. and Németi,I. [85], Clones of operations on relations. In: Universal

algebra and lattice theory (Proc. Conf. Charleston 1985) Lecture Notes in Mathematics Vol. 1149, Springer–Verlag, Berlin, 1985. pp.17–21.

Andréka,H. Givant,S.R. Mikulás,Sz. Németi,I. and Simon,A. [96], Notions of density that imply

representability in algebraic logic, Annals of Pure and Applied Logic. To appear. Andréka,H. Givant,S.R. and Németi,I. [94], The lattice of varieties of representable relation

algebras, Journal of Symbolic Logic 59,2 (1994), 631-661. Andréka,H. Guessarian,I. and Németi,I. [87], A unifying theorem for algebraic semantics and

dynamic logics, Information and Computation 72,1 (1987), 31–45. Andréka,H. Jónsson,B. and Németi,I. [88], Free algebras in discriminator varieties, Algebra

Universalis 28 (1991), 401-447. Andréka,H. Maddux,R.D. and Németi,I. [87], Splitting in relation algebras, Proc. Amer. Math.

Soc 111,4 (1991), 1085-1093. Andréka,H. Monk,J.D. and Németi,I.(ed.s) [88], Algebraic Logic. Colloq. Math. Soc. J. Bolyai

Vol. 54, North–Holland, Amsterdam, 1991. Andréka,H. and Németi,I. [75], A simple purely algebraic proof of the completeness of some

first–order logics, Algebra Universalis 5 (1975), 8–15. Andréka,H. and Németi,I. [80], On systems of varieties definable by schemes of equations,

Algebra Universalis 11 (1980), 105–116. Andréka,H. and Németi,I. [81], Dimension complemented and locally finite dimensional cylin-

dric algebras are elementarily equivalent, Algebra Universalis 13 (1981), 157–163. Andréka,H. and Németi,I. [96], Axiomatization of identity-free equations valid in relation

algebras, Algebra Universalis 35 (1996), 256-264. Andréka,H. Németi,I. and Sain,I. [93], Applying algebraic logic to logic. In: Algebraic method-

ology and software technology (AMAST’93), Proc. Twente, The Netherlands, June 1993), Nivat.M. Rattray,C. Rus,T. and Scollo,G. (eds.), Springer-Verlag, London, 1994. pp.7-28. Full version available as Preprint, Math. Inst. Hung. Acad. Sci. 1995.

Andréka,H. Ryan,M. and Schobbens,P-Y. [95], Operators and laws for combining preferential relations (Extended abstract). In: Information Systems: Correctness and Reusability (Selected papers), eds. R.J. Wieringa and R.B. Feenstra, World Scientific Publishing Co, 1995. pp.191-206.

Anellis,I.H. Houser,N., The nineteenth century roots of universal algebra and algebraic logic: A critical-bibliographical guide for the contemporary logician.. In: Algebraic Logic (Proc. Conf. Budapest 1988) Colloq. Math. Soc. J. Bolyai Vol 54, North-Holland, Amsterdam, 1991. pp.1–36.

Bednarek,A.R. and Ulam,S.M. [77], Some remarks on relational composition in computational theory and practice. In: Fundamentals of Computation Theory’77, Lecture Notes in Computer Science Vol. 56, Springer–Verlag, Berlin, 1977. pp. 33–38.

van Benthem,J. [89], Modal logic and relational algebra. Manuscript, University of Amster-

dam, ILLC, 1989. van Benthem,J. [90], General dynamics. In: Theoretical Linguistics (ed. Ph. A. Luelsdorff),

1991. pp.151–201. van Benthem,J. [90a], Temporal logic. In: Handbook of Logic in Artificial Intelligence and

Logic Programming (ed.s: D. Gabbai, Chr. Hogger and J. Robinson), Vol. 4, Oxford University Press, 1993. pp.241–350.

Berghammer,R. Kempf,P. Schmidt,G. and Ströhlein,T. [88], Relation algebra and logic of programs. In: Algebraic Logic , Colloq. Math. Soc. J. Bolyai Vol. 54, North–Holland, Amsterdam, 1991. pp.37-58.

Biró,B. [89], Non–finite–axiomatizability results in algebraic logic, J. of Symbolic Logic 57,3

(1992), 832-843. Biró,B. [89a], Isomorphic but not lower base–isomorphic cylindric algebras of finite dimension,

Notre Dame J. of Formal Logic 30,2 (1989), 262–267. Biró,B. and Shelah,S. [88], Isomorphic but not lower–base–isomorphic cylindric set algebras,

J. of Symbolic Logic 53,3 (1988), 846–853. Blok,W.J. and Pigozzi,D. [89], Algebraizable logics, Memoirs of Amer. Math. Soc. 77 (1989),

vi+78pp. Börner,F. [86], One–generated clones of operations on binary relations, Beitrage Alg. u. Geom.

23 (1986), 73–84. Bredikhin,D.A. [77], Abstract characteristics of some relation algebras (in Russian), Algebra

and Theory of Numbers (Nalchik) 2 (1977), 3–19. Bredikhin,D.A. [77a], Multiplicative algebra of relations (in Russian). Dissertation, Saratov

State University, Saratov, USSR, 1977. Bredikhin,D.A. and Schein,B.M. [78], Representations of ordered semigroups and lattices by

binary relations, Colloq. Math. 39 (1978), 1–12. Cirulis,J. [88], Relational algebras in databases and generalized cylindric algebras (in Russian),

Theoretical Questions of Programming, Latvian University, Riga (1988), 100–107. Comer,S.D. [84], Galois theory of cylindric algebras and its applications, Trans. Amer. Math.

Soc. 286 (1984), 771–785. Comer,S.D. [85], Combinatorial types. In: Algebra, Combinatorics and Logics in Computer

Science (Proc. Györ 1983) Colloq. Math. Soc. J. Bolyai Vol. 42, North–Holland, Amsterdam, 1985. pp.267–284.

Comer,S.D. [88], The representation of dimension three cylindric algebras. In: Algebraic

Logic, Colloq. Math. Soc. J. Bolyai Vol. 54, North–Holland, Amsterdam, 1991. pp.147-172. Comer,S.D. [89], A remark on representable positive cylindric algebras, Algebra Universalis

28 (1991), 150–151. Comer,S.D. [90], An algebraic approach to the approximation of information, Fundamenta

Informaticae XIV (1991), 492-503. Comer,S.D. [93], On connections between information systems, rought sets, and algebraic

logic. In: Algebraic Methods in Logic and Computer Science, C. Rauszer (ed), Banach Center Publications Vol. 28, Warsaw, 1993. pp.117-124.

Cosmadakis,S.S. [87], Database theory and cylindric lattices. (Extended abstract). In: IEEE

28th Annual Symposium on Foundations of Computer Science, 1987. pp. 411-420. Craig,W. [74], Logic in algebraic form. North–Holland, Amsterdam, 1974. viii+204pp. Craig,W. [74a], Unification and abstraction in algebraic logic, Studies in Algebraic Logic,

Math. Assoc. Amer. (1974), 6–57. Daigneault,A. [69], Lawvere’s elementary theories and polyadic and cylindric algebras, Fund.

Math. 66 (1969), 307–328. Daneczki,R. [84], Nondeterministic dynamic logic with intersection is decidable. In: Compu-

tation Theory (Proc. Zaborov, Poland, 1984), Lecture Notes in Computer Science Vol. 208, Springer–Verlag, Berlin, 1984. pp.34–53.

Demaree,D. [72], Copeland algebras, J. of Symbolic Logic 37 (1972), 646–656. De Morgan, A. [1860], On the syllogism: IV, and on the logic of relations. Read before

the Cambridge Philosophical Society on April 23, 1860. Transactions of the Cambridge Philosophical Society 10 (1964). 331–358.

Diamond,A.H. and McKinsey,J.C.C. [47], Algebras and their subalgebras, Bull. Amer. Math.

Soc. 53 (1947), 147–154. Düntsch,I. [90], Cylindric lattices. Preprint, Universiti of Brunei, Darussalam, Negara Brunei,

1990. Düntsch,I. [90a], Join dependencies and cylindric algebras. Preprint, Universiti of Brunei,

Darussalam, Negara Brunei, 1990. Düntsch,I. [93], A note on cylindric lattices. In: Algebraic Methods in Logic and Computer

Science, C. Rauszer (ed), Banach Center Publications Vol. 28, Warsaw, 1993. pp.231-238. Düntsch,I. [94], Rough relation algebras, Fundamenta Informaticae 21 (1994), 321-331. Feldman,N. [89], Cylindric algebras with terms, J. of Symbolic Logic 55,2 (1990), 865–866. Ferenczi,M. [90], On inducing homomorphisms between relation set algebras, Algebra Univer-

salis 27,4 (1990), 474–479. Ferenczi,M. [92], On representability of cylindric algebras, Abstracts of papers presented to

the American Math. Soc. 336/13/3 (1992). full version submitted. Fischer,M.J. and Ladner,R.E. [79], Propositional dynamic logic of regular programs, J. of

Computation and System Sciences 18,2 (1979), 194–211. Givant,S.R. [94], The structure of relation algebras generated by relativizations. Contemporary

Mathematics Vol. 156, Amer. Math. Soc., 1994. xv+134 pages. Goldblatt,R.I. [90], Varieties of complex algebras, Annals of Pure and Applied Logic 44 (1990),

173–242. Greenwood,R. and Gleason,A. [55], Combinatorial relations and chromatic graphs, Can. J.

Math. 7 (1955), 1–7. Haiman,M.D. [87], Arguesian lattices which are not linear, Bull. Amer. Math. Soc. 16,1 (1987),

121–123. Halmos,P.R. [54], Polyadic Boolean algebras, Proc. Nat. Acad. Sci. U.S.A. 40 (1954), 296–301. Halmos,P.R. [60], Polyadic algebras. Summaries of talks presented at the Summer Institute

for Symbolic Logic, Cornell University, 1957, second edition, Communications Research Division, Institute for Defense Analyses, 1960. pp.252–255.

Halmos,P.R. [62], Algebraic Logic. Chelsea Publ. Co., New York, 1962. 271pp. Hansen,B. [92], Representation theorems of reducts of cylindric agebras. In: Abstracts of the

1992 European Summer Meeting of the Assoc. Symb. Logic, J. Symbolic Logic 58,3 (1993), 1125.

Hansen,B. [95], Finitizability questions for some reducts of cylindric algebras. In: Logic Colloquium’92, Csirmaz,L. Gabbay,D.M. and de Rijke,M. (eds), CSLI Publications, Stanford, 1995. pp.115-134.

Henkin,L. [55], The representation theorem for cylindric algebras. Mathematical interpreta-

tion of formal systems, North–Holland, Amsterdam, 1955. pp.85–97. Henkin,L. [70], Extending Boolean operations, Pac. J. Math. 22 (1970), 723–752. Henkin,L. and Monk,J.D. [74], Cylindric algebras and related structures. In: Proc. Tarski

Symposium, Amer. Math. Soc., 1974. pp.105–121. Henkin,L. Monk,J.D. and Tarski,A. [HMT71], Cylindric Algebras, Part I. North–Holland,

Amsterdam, 1971, 1985. Henkin,L. Monk,J.D. and Tarski,A. [81], Cylindric set algebras and related structures. In:

Lecture Notes in Mathematics Vol 883, North–Holland, Amsterdam, 1981. pp.1–130. Henkin,L. Monk,J.D. and Tarski,A. [HMT85], Cylindric Algebras, Part II. North–Holland,

Amsterdam, 1985. Henkin,L. Monk,J.D. Tarski,A. Andréka,H. and Németi,I. [81], Cylindric set algebras. Lecture

Notes in Mathematics Vol. 883, Springer–Verlag, Berlin, 1981. Henkin,L. and Tarski,A. [61], Cylindric algebras. In: Proc. of symposia in pure math. 2, Amer.

Math. Soc., Providence, Rhode Island, 1961. pp.83–113. Hennessey,M. [80], A proof system for the first–order relational calculus, J. Computer and

System Sciences 20 (1980), 96–110. Hirsch,R. and Hodkinson,I. [95], Step-by-step - building representations in algebraic logic, J.

Symbolic Logic. to appear. Howard,C.M. [65], An approach to algebraic logic. Doctoral Dissertation, University of Cali-

fornia, Berkeley, 1965. 83pp. Imielinski,T. and Lipski,W. [84], The relational model of data and cylindric algebras, J. of

Computer and System Sciences 28 (1984), 80–102. Immerman,N. and Kozen,D. [89], Definability with bounded number of bound variables, Infor-

mation and Computation 83 (1989), 121–139. Jipsen,P. Jónsson,B. and Rafter,J. [95], Adjoining units to residuated Boolean algebras, Alge-

bra Universalis 34 (1995), 118–127. Johnson,J.S. [69], Nonfinitizability of classes of representable polyadic algebras, J. Symbolic

Logic 34 (1969), 344–352. Jónsson,B. [59], Representation of modular lattices and of relation algebras, Trans. Amer.

Math. Soc. 92 (1959), 449–464. Jónsson,B. [82], Varieties of relation algebras, Algebra Universalis 15 (1982), 273–298. Jónsson,B. [84], The theory of binary relations. In: Algebraic Logic, Colloq. Math. Soc. J.

Bolyai Vol. 54, North–Holland, Amsterdam, 1991. pp. 245-292. Jónsson,B. [84a], Maximal algebras of binary relations. In: Contributions to Group Theory:

Papers published in honor of Roger Lyndon on his sixty–fifth birthday, Contemporary Mathematics Vol. 33, Amer. Mat. Soc., Providence, 1984. pp.299–307.

Jónsson,B. [90], Program specification as Boolean operators. Preprint, Vanderbilt University,

circulated at the Jónsson Conference, Iceland, 1990. Kozen,D. [79], On the duality of dynamic algebras and Kripke models. In: Proc. Workshop on

Logic of Programs, Lecture Notes in Computer Science Vol. 125, Springer–Verlag, Berlin, 1979. pp.1–11.

Kozen,D. [80], A representation theorem for models of *–free PDL. In: Proc. 7–th Colloq. on

Automata, Languages and Programming, July 1980. pp.351–362. Kozen,D. [81], On induction vs. *–continuity. Proc. Workshop on Logics of Programs 1981,

Lecture Notes in Computer Science Vol 131, Springer– Verlag, Berlin, 1981. pp.167–176. Kozen,D. [90], On Kleene algebras and closed semirings. In: Mathematical Foundations of

Computer Science’90, Lecture Notes in Computer Science Vol. 452, Springer–Verlag, Berlin, 1990. pp.26–47.

Lyndon,R.C. [56], The representation of relation algebras II, Ann. of Math. 63 (1956), 294–307. Lyndon,R. [61], Relation algebras and projective geometries, Michigan Math. J. 8 (1961),

21–28. Madarász,J.X.Q. Németi,I. and Sági,G. [97], On the finitization problem of relation algebras.

Extended abstract. Mathematical Institute, Budapest. Preprint, 1997. On ftp://circle.math-inst.hu- /pub/algebraic-logic.

Maddux,R.D. [78], Topics in relation algebras. Dissertation, University of California, Berkeley,

1978. Maddux,R.D. [88], Problems posed during the Conference on Algebraic Logic. Preprint, Oc-

tober 6, 1988. In: Andréka-Monk-Németi[88], pp.727-746. Maddux,R.D. [89], Nonfinite axiomatizability results for cylindric and relation algebras, J.

Symbolic Logic 54,3 (1989), 951–974. Maddux,R.D. [89a], Canonical relativized cylindric set algebras, Proc. Amer. Math. Soc. 107,2

(1989), 465–478. Maddux,R.D. [89b], Finitary algebraic logic, Z. Math. Logic. Grundl. Math. 35 (1989), 321–332. Maddux,R.D. [89c], A collection of research problems on relation algebras. Preprint, Iowa

State University, Ames, Iowa, 1989. Maddux,R.D. [90], The neat embedding problem and the number of variables required in proofs,

Proc. Amer. Math. Soc. 112 (1991), 195–202. Maddux,R.D. [90a], The origin of relation algebras in the development and axiomatization of

the calculus of relations, Studia Logica 50,3-4 (1991), 421-456. Makkai,M. [87], Stone duality for first–order logic, Advances in Mathematics 65,2 (1987),

97–170. Marx,M. Pólos,L. and Masuch,M. (eds) [96], Arrow Logic and Multi-Modal Logic. CSLI Pub-

lications, Stanford, 1996. vi+247pp. Marx,M. [95], Algebraic relativization and arrow logic. PhD Dissertation, University of Ams-

terdam, Amsterdam, 1995. Mikulás,Sz. [95], Taming Logic. PhD Dissertation, University of Amsterdam, Amsterdam,

1995. Mikulás,Sz. Sain,I. and Simon,A. [90], On the complexity of the equational theory of rela-

tion algebras with standard projection elements. Bulletin of Section of Logic 21,3 (1992), 103-111.

Monk,J.D. [61], On the representation theory for cylindric algebras, Pacific J. Math. 11 (1961),

1447–1457. Monk,J.D. [64], On representable relation algebras, Michigan Math. J. 11 (1964), 207–210. Monk,J.D. [69], Nonfinitizability of classes of representable cylindric algebras, J. Symbolic

Logic 34 (1969), 331–343. Monk,J.D. [70], On an algebra of sets of finite sequences, J. Symbolic Logic 35 (1970), 19–28. Monk,J.D. [74], Connections between combinatorial theory and algebraic logic. In: Studies

in algebraic logic, MAA Studies in Mathematics Vol. 9, The Mathematical Association of America, 1974. pp.58–91.

Németi,I. [80], Some constructions of cylindric algebra theory applied to dynamic algebras of

programs, Comput. Linguist. Comput. Lang. 14 (1980), 43–65. Németi,I. [81], Dynamic algebras of programs. In: Fundamentals of Computation Theory’81,

Lecture Notes in Computer Science Vol. 117, Springer–Verlag, Berlin, 1981. pp.281–290. Németi,I. [82], Every free algebra in the variety generated by the representable dynamic alge-

bras is separable and representable, Theoretical Computer Science 17 (1982), 343–347. Németi,I. [83], Combinatorial problem for algebraic logic, Abstracts of Amer. Math. Soc., 4,5

(1983), p.389. *83T–05–330.

Németi,I. [87], On varieties of cylindric algebras with aplications to logic, Annals of Pure and

Applied Logic 36 (1987), 235–277. Németi,I. [90], Algebraizations of quantifier logics: an introductory overview. Version 12,

Preprint No 13/1996, Mathematical Institute, Budapest. On ftp:/circle.math-inst.hu/pub- /algebraic-logic. Shortened version appeared as: Studia Logica 50/3-4(1991)458-569.

Németi,I. [90a], On cylindric algebraic model theory. In: Algebraic Logic and Universal Algebra in Computer Science, Lecture Notes in Computer Science Vol. 425, Springer–Verlag, Berlin, 1990. pp.37–76.

Németi,I. [96], Ontology can turn negative results to positive (An overview of recent results.),

Bulletin of Section of Logic 25,1 (1996), 29-40. Németi,I. and Andréka,H. [94], General algebraic logic: a perspective on “what is logic”. In:

What is a logical system, Gabbay,D.M. (ed), Clarendron Press, Oxford, 1994. pp.393-444. Németi,I. and Kurucz,Á. [97], Representability of pairing relation algebras depends on your

ontology, Journal of Symbolic Logic. To appear. Németi,I. and Sági,G. [96], On the equational theory of representable polyadic equality alge-

bras. Preprint, Mathematical Institute, Budapest, 1996. On ftp:/circle.math-inst.hu/pub- /algebraic-logic.

Németi,I. and Simon,A. [95], Weakly higher order cylindric algebras and finite schema axiom-

atization of the representables. Preprint, Mathematical Institute, Budapest, 1995. Ng,K.C. [84], Relation algebras with transitive closure. Dissertation, University of California,

Berkeley, 1984. iv+157 pp. Orlowska,E. [89], Dynamic logic with program specifications and its relational proof system.

Preprint, Polish Acad. Sci., Warsaw, Poland, 1989. Orlowska,E. [90], Nonclassical relation and cylindric algebras. Preprint, Polish Acad. Sci.,

Warsaw, Poland, 1990. Pálfy,P.P. [85], On the chromatic number of certain highly symmetric graphs, Discrete Math.

54,3 (1985), 31–38. Peirce,C.S. [1870], Description of a notation for the logic of relatives, resulting from an am-

plification of the conceptions of Boole’s calculus of logic, Memoirs of the Amer. Acad. Sci. 9 (1870), 317–378.

Pinter,C. [73], Cylindric algebras and algebras of substitutions, Trans. Amer. Math. Soc. 175

(1973), 167–179. Plotkin,B.I. [88], Halmos (polyadic) algebras in the database theory. In: Algebraic Logic,

Colloq. Math. Soc. J. Bolyai Vol. 54, North–Holland, Amsterdam, 1991. pp.505-518. Plotkin,B.I. [94], Universal algebra, algebraic logic and data–bases. Kluwer Academic Pub-

lishers, 1994. Pratt,V.R. [79], Dynamic algebras: Examples, Constructions, Applications. Technical Report

MIT/LCS/TM–138, MIT Laboratory for Computer Science, July 1979. Pratt,V.R. [90], Dynamic algebras as a well behaved fragment of relation algebras. In: Alge-

braic logic and universal algebra in computer science, Lecture Notes in Computer Science Vol. 425, Springer–Verlag, Berlin, 1990. pp.77–110.

Pratt,V.R. [91], Dynamic algebras, Studia Logica 50,3-4 (1991), 57-607. Pratt,V.R. [92], Origins of the calculus of binary relations. In: Proc. 7th Annual IEEE

Symposium on Logic in Computer Science, Santa Cruz, CA, June 1992. pp.248-254. Preller,A. [70], Substitution algebras in their relation to cylindric algebras, Arch. Math. Logik

Grundl. 30 (1970), 91–96. Redko,V.N. [64], On defining relations for the algebra of regular events (in Russian), Ukrain.

Mat. Z. 16 (1964), 120–126.

Sain,I. [87], Positive results related to the Jónsson, Tarski–Givant representation problem.

Expanded version of Preprint Math. Inst. Hungar. Acad. Sci., 1987. Sain,I. [87a], Searching for a finitizable algebraization of first order logic, Annals of Pure and

Applied Logic. To appear. Sain,I. [92], On the problem of finitizing first order logic and its algebraic counterpart. (A

survey of results and methods.). In: Logic Colloquium’92, Csirmaz,L. Gabbay,D.M. and de Rijke,J. (eds), CSLI Publications, Stanford, 1995. pp.243-292.

Sain,I. and Gyuris,V. [96], Finite schematizable algebraic logic, Journ. IGPL. In press. Sain,I. and Németi,I. [97], Fork algebras in usual and in non-well-founded set theories (an

overview). Studia Logica Library (a special volume dedicated to the memory of Helena Rasiowa), to appear.

Sain,I. and Thompson,R.J. [88], Strictly finite schema axiomatization of quasi–polyadic algebras. In: Algebraic Logic, Colloq. Math. Soc. J. Bolyai Vol. 54, North–Holland, Amsterdam, 1991. pp.539-572.

Schein,B.M. [70], Relation algebras and function semigroups, Semigroup Forum 1 (1970), 1–62. Schein,B.M. [88], Representation of reducts of Tarski relation algebras. In: Algebraic Logic,

Colloq. Math. Soc. J. Bolyai Vol. 54, North–Holland, Amsterdam, 1991. pp.621-636. Schmidt,G. and Ströhlein,T. [89], Relationen und Graphen. Series Mathematik für Infor-

matiker, Springer–Verlag, Berlin, 1989. Schönfeld,W. [77], Applications of relation algebras in computer science, Notices Amer. Math.

Soc. 24 (1977), A–254. Schröder,E. [1895], Vorlesungen über die Algebra der Logik (exacte Logik). Volume 3, “Algebra

und Logik der Relative”, Part I, Leipzig, 1895. Serény,Gy. [85], Compact cylindric set algebras, Bull. Section of Logic 14,2 (Warsaw–Lodz,

1985), 57–64. Simon,A. [90], A finite schema completeness result for algebraic logic. In: Algebraic Logic,

Colloq. Math. Soc. J. Bolyai Vol. 54, North–Holland, 1991. pp.665-670. Tarski,A. [55], Contributions to the theory of models, III. Nederl. Akad. Wetensch. Proc. Ser.

A, vol.57 (Indag. Math., Vol. 17) (1955), 56–64. Tarski,A. and Givant,S. [87], A formalization of set theory without variables. AMS Colloquium

Publications Vol. 41, Providence, Rhode Island, 1987. Thompson,R.J. [81], Transformational structure of algebraic logics. Dissertation, University

of California, Berkeley, 1981. Thompson,R.J. [87], Semigroups of finite transformations and cylindric algebras. Preprint

No 45/1987, Mathematical Institute, Budapest, 1987. Thompson,R.J. [93], Complete description of substitutions in cylindric algebras and other

algebraic logic. In: Algebraic Methods in Logic and in Computer Science. Banach Center Publications Vol 28. Polish Academy of Science, Warszawa, 1993. pp.327–342.

Trnková,V. and Reiterman,J. [87], Dynamic algebras with test, J. Computer System Sciences

35,2 (1987), 229–242. Venema,Y. [89], Two–dimensional modal logics for relational algebras and temporal logic of

intervals. Preprint, University of Amsterdam, 1989. Venema,Y. [90], Cylindric modal logic, Journal of Symbolic Logic 60,2 (1995), 591-623. Volkov,N.D. [86], The transition from a relation algebra to a Halmos algebra. In: Algebra

and Discrete Mathematics: Theoretical Foundations of Software, (in Russian), Latv. Gos. Univ., Riga, 1986.

Wagner,V.V. [56], Representation of ordered semigroups (in Russian), Mat. Sbornik 38 (1956), 203–240. English Transl.: Amer. Math. Soc. Transl. (2) 36 (1964), 295–336.

Zaretskij,K.A. [59], Representations of ordered semigroups with binary relations (in Russian),

Matematika 6 (1959), 48–50. Zierer,H. [83], Relationale Semantik. Diplomarbeit, Institut für Informatik, Technische Uni-

versitat, München, 1983.

Keywords. Algebraic logic, algebras of relations, cylindric algebras, polyadic algebras, relation algebras, representation theory, nonfinitizability, finitization problem, completeness theorems, incompleteness theorems, modal logic of quantification and substitution, logic of first–order formula schemas, logic with finitely many variables. 1980 Mathematics subject classifications: 03G15, 06, 08

H. Andréka : Mathematical Institute of Hung. Acad. Sci., Budapest, Pf.127, H–1364, Hungary. e-mail: andreka@math-inst.hu