Finite Schematizable Algebraic Logic ^{∗}

Ildikó Sain^{†}, Viktor Gyuris^{‡}

November 25, 1996 (Version 5.2)

Abstract

In this work, we attempt to alleviate three (more or less) equivalent negative results. These are (i) non-axiomatizability (by any finite schema) of the valid formula schemas of first order logic, (ii) non-axiomatizability (by finite schema) of any propositional logic equivalent with classical first order logic (i.e., modal logic of quantification and substitution), and (iii) non-axiomatizability (by finite schema) of the class of representable cylindric algebras (i.e., of the algebraic counterpart of first order logic). Here we present two finite schema axiomatizable classes of algebras that contain, as a reduct, the class of representable quasi-polyadic algebras and the class of representable cylindric algebras, respectively. We establish positive results in the direction of finitary algebraization of first order logic without equality as well as that with equality. Finally, we will indicate how these constructions can be applied to turn negative results (i), (ii) above to positive ones.

Contents

1 Introduction 2

2 Results 6 2.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2 Finitizing algebras of first order logic without equality . . . . . . 8 2.3 Finitizing algebras of first order logic with equality . . . . . . . . 17 2.4 Open Qusetions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.5 Application to logic . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.6 Comparisons with the polyadic notion of a schema . . . . . . . . 21 3 Proofs 22

∗This is a pre-publication version of the paper, final version will be prepared later and published elsewhere.

†sain@math-inst.hu ‡viktor@math.uic.edu or viktor@ludens.elte.hu. Research supported by Hungarian Research Fund, grants F17452, T16448.

3.1 An axiomatization of IGwdf_{G} . . . . . . . . . . . . . . . . . . . 22 3.2 Theorem 2.7 (1): finite schema axiomatizing IGwdf_{G} . . . . . . . 24 3.3 Theorem 2.11: compressing the unit element . . . . . . . . . . . 31 3.4 Quasi-axiomatizing ICdf_{H} . . . . . . . . . . . . . . . . . . . . . . 34 3.5 Theorem 2.30: the cylindric reduct of Mod(H1, H2) . . . . . . . 40 3.6 Further observations on Mod(H1, H2) . . . . . . . . . . . . . . . 43 3.7 The witness tree method . . . . . . . . . . . . . . . . . . . . . . . 49

1 Introduction

Since it was introduced, first order logic became the most frequently used and studied logical system. Its logical connectives and basic concepts are motivated by intuitive “mathematical” reasoning. It also plays a fundamental role in logical (formal) investigations of not necessarily mathematical reasoning, cf. e.g. [GG85], [vB91].

First order logic is only one of the logical systems investigated in modern logic. For many logical systems, or logics for short, the methodology of algebraic logic proved to be very useful. This methodology is summarized e.g. in [ANSK] and in [NA93]. Cf. also Blok–Pigozzi [BP89]. The key step in this methodology is that, to any logic L, we associate a class Alg(L) of algebras, called the algebraic counterpart of the logic L. In many cases, investigating Alg(L) is easier than investigating L, e.g. because, in the study of Alg(L), we can use the well developed tools of algebra. A number of problems concerning certain logics L were often solved by translating the problem to Alg(L), solving the algebraic problem by the methodology of algebra, and then translating the algebraic result back to the logical context in which L was originally investigated. Another equally important value of algebraization is obtaining insights into the essential nature of a logic L, via abstraction provided by algebraization.

The algebraic counterpart of classical propositional logic is the class of Boolean algebras. Boolean algebras proved immensely useful in studying classical propositional logic, and in understanding its connections with other logical systems. Similarly, for a great number of other logics, studying their algebraic counterparts has proven very useful. One example is propositional modal logic, the algebraic counterpart of which is Boolean algebras with operators. Similar positive examples are most of the non-classical propositional logics, e.g. intuitionistic propositional calculus whose algebraic counterpart is the variety of Heyting Algebras. Cf. e.g. [W88].

In the case of first order logic, when trying to apply the methodology of algebraic logic in the above outlined fashion, we have to face the following problem. As we said, the algebraic counterpart of classical propositional logic is the class of Boolean algebras. This class turns out to be a finitely axiomatizable equational class. The same is true for the other successful examples we referred to. In each case, Alg(L) is axiomatizable by a finite set of equations or quasi-equations^{1}. As a contrast, in the case of first order logic, all the algebraic counterparts found before 1987 are very far from being finitely axiomatizable. Namely, J. D. Monk proved in [M70] that the most thoroughly investigated algebraic counterpart of first order logic with equality, the class RCA_{ω} of representable cylindric algebras is not axiomatizable by a finite schema of equations^{2}. A similar result was obtained in Sain–Thompson [SaT91] about the class RQPA_{ω} of representable quasi-polyadic algebras (the algebraic counterpart of first order logic without equality)^{3}. Monk’s theorem was improved by Andréka in [A91]. She proved that any axiomatization of RCA_{ω}, besides being infinite, has to be extremely complex.

These results motivate the problem of finding an algebraization of first order logic where the class of algebras associated to this logic is axiomatizable by a preferably nice (simple, transparent, mathematically elegant) schema of equations or quasi-equations. There is a harder version of this problem asking for a strictly finite axiomatization. However, it is understood that a finite schema solution could already be very useful if the schema of axioms is simple enough. This problem is known as the finitization problem in algebraic logic. Actually, as it turns out, it is not a single problem, but rather a family of problems or, perhaps, even a research direction of algebraic logic, cf. e.g. Németi [N93], Simon [Si93], Sain [Sa92]. Here we will simply refer to it as the finitization problem. The problem as we formulated above is not concrete enough to be regarded as a tangible mathematical problem. To illustrate this, we note that Simon [Si93] is devoted to showing that many seemingly relevant results are, though mathematically interesting, not even partial solutions of the finitization problem. Therefore, below we recall a sufficiently concrete formulation of the finitization problem from the literature.

The problem of finding a “finitizable” algebraization of first order logic was raised in Monk [M70, p.20] and in Henkin–Monk [HM74].^{4} The formulation in the latter goes as follows:

“Devise an algebraic version of predicate logic in which the class of representable algebras forms a finitely based equational class.”

An equational class is called finitely based if it is axiomatizable by finitely many equations. In [HM74] an algebra is called representable if it is isomorphic to a subdirect product of set algebras. Therefore the key step is finding an appropriate notion of set algebra. In devising such definitions, usually, an ordinal α is fixed in advance, and then the elements of a set algebra are (certain) α-ary relations over some set called the base of the algebra. One piece of the connection with logic is that the base of the algebra corresponds to the universe of that model of first order logic from which it is obtained (see e.g. [HMTII, sections 4.3, 5.6] for details on this connection). Following Jónsson and Tarski, we require that the operations of a set algebra should be invariant under any permutation of the base set^{5}. An operation with this property is called logical. (This property is called “permutation invariant” in Jónsson [Jó86].) In this work we concentrate on that version of the above quoted problem of Henkin and Monk in which all operations of the set algebras are required to be logical.^{6} This condition admits the following equivalent formulation. The class of representable algebras can be obtained in the form Alg(L) for some logic L such that, in the model theory of L, isomorphic models satisfy the same formulas — the latter condition is one of the basic axioms of abstract model theory.

1Quasi-equations are equational implications.

2Monk obtained similar negative results for RCA_{3} already in 1964.

3The Sain–Thompson result was preceded by a relevant result of James Johnson [Jo69] who proved that RQPA_{n} (2 < n < ω) is not finitely axiomatizable.

4This problem has a long history and many people worked on it, e.g. A. Tarski did so already in the 1940’s; but the explicit formulation we would like to use is in the quoted papers of L. Henkin and J. D. Monk. For completeness, we also refer to Henkin–Tarski (1961) [HT61] to the open problem formulated below Theorem 1.14 therein (lines 21–29 on page 96). There they ask for a finite schema axiomatization of Eq(RCA_{ω}). This turns out possible (but only)

if we add to RCA_{ω} operations like s_{suc}, s_{pred} defined herein.

A solution to the truly finite axiomatization version of the finitization problem was given in Sain [Sa87a] part of which is revised as [Sa87] and abstracted in [Sa92] and [Sa94]. These papers give a complete solution to the case of first order logic without equality, while the solution there to logic with equality is slightly weaker. Much of the effort in the just quoted papers goes into ensuring that the number of axioms is strictly finite (as opposed to a finite schema). Therefore the idea comes up that if we require only a finite schema axiomatization (as opposed to “truly finite”) then, perhaps, we could achieve substantial improvements in other directions such as simplifying the axioms. Indeed, after [Sa87a] was presented at the Algebraic Logic conference in Asilomar, 1987, both Leon Henkin and J. Donald Monk suggested looking for a solution which, instead of a truly finite set of axioms, provides only a finite schema of axioms, but in such a way that this schema would be simple and easy to work with. This is one of the things we intend to do in the present paper. ^{7}

The question of comparing our notion of a schema with the notion used in Keisler’s completeness theorem and in the Daigneault–Monk representation theorem for polyadic algebras (without equality) comes up at this point (see [HMTII] 5.4). We will make such a comparison using results of [NS95] and [Sá95] in Subsection 2.6 at the end of this section.

5Tarski mentions this requirement already in his 1941 paper on the calculus of relations.

See also next footnote.

6This condition goes back to Lindenbaum–Tarski [LT36], and was extensively discussed in Tarski [Ta87] where it was suggested that the condition is essential for investigations of truly logical nature. Further considerations for necessity of requiring all the operations to be logical (i.e. permutation invariant) are in [Sh91] and [vB96] 3.3.2 (pp.67–68). It was proved e.g. in Biró [Bi89] that permutation invariance is a necessary condition in the finitization problem.

Cf. also Németi [N91].

7A related open problem is to simplify the axiomatization given in the original papers (e.g.

in [Sa87]).

A further aim of this paper is to improve the positive results to a tighter or more orthodox class of set algebras. This tighter class is denoted below as Cdf_{G}.

To first order logic without equality, we will associate a fairly simple and powerful class Cdf_{G} of set algebras. A Cdf_{G} algebra A is a subalgebra of the Boolean algebra of subsets of the Cartesian space ^{ω}U expanded with some extra operations corresponding to quantification and substitution^{8}. We will axiomatize Cdf_{G} by a relatively simple finite schema of quasi-equations (cf. Theorem 2.5). A modified version of this class will receive an equational axiomatization. It remains an open problem to simplify these axiomatizations. To the same logic we will also associate a slightly bigger class Gwdf_{G} of set algebras. We will be able to prove more results about this second class (and also we will be able to simplify the axioms for the latter). Cdf_{G} will meet all the requirements of the (schema version of the) finitization problem quoted way above. E.g., its operations will be logical and natural set theoretic operations on relations. The saem applies to Gwdf_{G}.

To first order logic with equality, we will associate a class Cs_{suc,pred} of set algebras, which has the following positive properties. The equational class V generated by Cs_{suc,pred} is axiomatizable by a finite schema of equations, which is even simpler than the one we give to logic without equality. Further, Cs_{suc,pred} is an expansion of cylindric set algebras with some extra operations. These extra operations are again logical and simple set theoretic ones, just as in the previous case. Now, our finite schema axiomatizable V has the property that if we omit the extra operations from its members then we get exactly the class RCA_{ω} of representable cylindric algebras. Let us see what this means in more detail.

To the natural algebraic counterpart RCA_{ω} of first order logic with equality, we add simple logical operations in such a way that, in the language of the so expanded class, we can write up a finite schema of axioms which completely describes the original operations of RCA_{ω}, but not necessarily the new operations themselves. More concretely, any model A of our finite schema is representable as a true set algebra in the following sense. A is isomorphic to some B, where the elements of B are real relations, and all the old cylindric algebraic operations are the usual set theoretic ones on B, but perhaps the new operations of B remain “abstract”.

At this point it might be of interest to note that, in the book [TaG87] (on page 62), the finitization problem was formulated in this weaker sense which we just described in connection with logic with equality. That is, Tarski and Givant ask for expanding the existing algebras with new logical operations in a way that there would be a finite set of axioms in the expanded language which describes the old operations completely, but not necessarily the new ones. For a comparison of the two versions of the finitization problem see the series of remarks in [N93] beginning with Remark 2.

8These algebras are often called “square algebras”.

Summing up, we can give a solution to the more “ambitious” formulation of the schema version of the finitization problem for logic without equality, while for logic with equality we could solve only the above outlined Tarski-Givant style formulation of the finitization problem.

When defining the finite schema axiomatizable (finitizable for short) algebraic counterparts Gwdf_{G}, Cs_{suc,pred} of first order logic, one has a certain freedom of choice concerning exactly how these algebras will look like. We will explore this freedom of choice in a metatheory, asking ourselves the question which of these choices of Gwdf_{G}, Cs_{suc,pred} are workable, and which are already non-finitizable.

We would like to note that our approach to the case with equality is strongly related to William Craig’s pioneering work summarized, e.g., in his book [Cr74]. Actually, our work can be viewed as a continuation of the approach initiated by Craig.

* * *

The formulation of the results mentioned above together with the basic definitions can be found in Section 2. In detail, Subsection 2.1 contains preliminary material for the rest of the paper, while Subsections 2.2 and 2.3 are devoted to the finitization of first order logic without equality and with equality, respectively. Subsection 2.5 concerns applications to ‘pure’ logic. The proofs are given in Section 3. At the end of the paper there are further historical remarks.

Any proof which would rely on references not available to the reader (or would seem incomplete for any other reason) is available with all such missing data added from the authors.

2 Results

2.1 Preliminaries

Throughout this paper, ω denotes the set of all natural numbers. If A and B are arbitrary sets then ^{A}B denotes the set of all functions from A into B. Thus, for any set U, ^{ω}U denotes the set of all ω–sequences over U. We often call the elements of ^{ω}ω transformations of ω. A function f ∈ ^{ω}ω is called a finite transformation of ω if f(i) = i for all but finitely many i ∈ ω. Examples of finite transformations of ω are transpositions and replacements, which are defined as follows. For each i, j ∈ ω, the transposition [i, j] interchanges i and j and leaves all the other elements of ω fixed; the replacement [i/j] maps i to j and leaves all the other elements of ω fixed. It is easy to see that the set of all finite transformations of ω forms a semigroup with function composition ∘ as the semigroup operation. Clearly, this semigroup is generated by the set of all replacements and transpositions.

Examples of transformations of ω that are not finite are the successor suc and the predecessor pred defined as follows. For every i ∈ ω, suc(i) = i + 1 and

pred(i) = \{ \begin{matrix}i − 1 & if i ≠ 0 \\ i & if i = 0 \end{matrix} .

If H is a set then H^{∗} denotes the set of sequences of elements of H. If T is a subset of ^{ω}ω then [T] denotes the subsemigroup of ⟨^{ω}ω, ∘⟩ generated by T.

For any class K of similar algebras, IK, HK, SK, PK and UpK denote, respectively, the classes of isomorphic copies, homomorphic images, subalgebras, isomorphic copies of direct products and isomorphic copies of ultraproducts of members of K. SirK denotes the class of subdirectly irreducible members of K.

Let t and t′ be similarity types with t′ ⊆ t. For any class K of algebras of similarity type t, Rd_{t′}K denotes the class of algebras of similarity type t′ defined as follows. A ∈ Rd_{t′}K if and only if A is the t′–reduct of some algebra in K. Informally speaking, we obtain the t′–reduct of an algebra by deleting those operations of it that are not in t′.

For any set Σ of first order formulas of similarity type t, Mod_{t}(Σ) denotes the collection of those models (of type t) in which Σ is valid. When t is known from context, we will often write Mod(Σ) instead of Mod_{t}(Σ).

For a class of algebras K, Eq(K) denotes the set of equations valid in K while Qeq(K) is the set of valid quasi-equations of K.

If f is a function and U is a subset of its domain then f⌈U denotes the restriction of f to U.

For the pair of sets U, V, U ⊆_{ω} V expresses the relation that U is a finite subset of V.

As we outlined in the Introduction, we will introduce several (new) kinds of set algebras. These algebras will be defined to be Boolean algebras of relations augmented with some extra operations. The greatest element of a Boolean algebra (with perhaps some extra operations) is called its unit. Therefore, when speaking about a class K of special Boolean algebras, then it is meaningful to talk about the class of unit elements of members of K. These will be called K–units.

Of these classes of set algebras, our first theorem (Theorem 2.5) will involve only the most important one called Cdf_{G}. Actually, one of the main results of this paper is Theorem 2.5 (i), (ii). To understand that result it is enough to read only a small fraction of the definitions below. Namely, after reading Definition 2.1 (i), the Cdf_{H} part of Definition 2.2 and Definition 2.4 the reader can go directly to read Theorem 2.5.

                                                                    df-unit

Definition 2.1 ([HMTII] Def.3.1.2) Let U be an arbitrary set. (i). The set ^{ω}U is called the Cartesian space with base U (and dimension ω). (ii). By a generalized Cartesian space we mean a disjoint union of Cartesian

spaces. That is, a set is called a generalized Cartesian space (of dimension ω) if it has the form ⋃_{i∈I} ^{ω}U_{i}, where I is a set, and for all distinct i, j ∈ I, U_{i} ∩ U_{j} = ∅.

(iii). For every p ∈ ^{ω}U, we set

ωU^{(p)} = {q ∈ ^{ω}U : {i ∈ ω : q(i) ≠ p(i)} is finite},

and we call ^{ω}U^{(p)} the weak Cartesian space (of dimension ω) determined by p. U is called the base of ^{ω}U^{(p)}.

(iv). By a generalized weak Cartesian space or Gws_{ω}–unit we mean a disjoint union of weak Cartesian spaces. That is, a set is called a generalized weak Cartesian space of dimension ω if it has the form ⋃_{i∈I} ^{ω}U_{i}^{(p_{i})} for some sets I, U_{i} and functions p_{i} ∈ ^{ω}U_{i} (i ∈ I) such that for all distinct i, j ∈ I, ωU_{i}^{(p_{i})} ∩^{ω}U_{j}^{(p_{j})} = ∅.

(v). We say that a Gws_{ω}–unit ⋃_{i∈I} ^{ω}U_{i}^{(p_{i})} is normal if for all distinct i, j ∈ I,

U_{i} and U_{j} are either disjoint or equal. (vi). Finally, we say that a Gws_{ω}–unit ⋃_{i∈I} ^{ω}U_{i}^{(p_{i})} is compressed if U_{i} = U_{j} for

all i, j ∈ I.

2.2 Finitizing algebras of first order logic without equality

                                                               d-igwsg

Definition 2.2 Suppose that H is a fixed subset of ^{ω}ω. An algebra is called a full generalized weak H–cylindric set algebra with unit V if it has the form

⟨P(V), ∪, −, s_{τ} , c_{k}⟩_{τ∈H,k∈ω} ,

where • V is a Gws_{ω}–unit,

• for every τ ∈ H and x ⊆ V, s_{τ} (x) = {q ∈ V : q ∘ τ ∈ x}, • s_{τ} (V) = V whenever τ ∈ H,

• c_{k} is the k-th cylindrification, that is, for any x ⊆ V,

c_{k}(x) = {q ∈ V : (∃q′ ∈ x)(∀i ∈ ω) i ≠ k ⇒ q(i) = q′(i)}.

If A is a full generalized weak H–cylindric set algebra with unit V, then A will often be denoted by \underline{P}(V), if H is known from context.

By a generalized weak H–cylindric set algebra (or briefly, by a Gwdf_{H}) we mean a subalgebra of a full generalized weak H–cylindric set algebra. The class of all generalized weak H–cylindric set algebras is denoted by Gwdf_{H}^{9}. The similarity type of Gwdf_{H} is denoted by t_{H}.

The classes of all algebras of Gwdf_{H}, whose unit elements are a Cartesian space, a generalized Cartesian space, a normal Gws_{ω}–unit or a compressed Gws_{ω}–unit, are denoted by Cdf_{H}, Gdf_{H}, Gwdf_{H}^{nm} or Gwdf_{H}^{cm} respectively.

                                                                    d-111

Definition 2.3 Let H ⊆ ^{ω}ω, V be a generalized Cartesian space^{10}, x ⊆ V. We define the operator c_{(ω)} : P(V) → P(V) as

c_{(ω)}x =^{def} {s ∈ V : (∃q ∈ c_{0}x) s(0) = q(0)}.

A = ⟨B, c_{(ω)}⟩ is called Gdf_{H}^{ec} iff B is a Gdf_{H} with unit V. An A ∈ Gdf_{H}^{ec} is called Cdf_{H}^{ec} if its unit element is a Cartesian space.

To help the intuition we point out that IGdf_{H}^{ec} = SPCdf_{H}^{ec} while in Cdf_{H}^{ec} c_{(ω)}x = 1 iff x > 0 and c_{(ω)}0 = 0.

Adding the new operator c_{(ω)} to Gdf_{H} amounts to adding the formation of existential closure φ → ∃\overline{x}φ to the logic being algebraized (where \overline{x} contains all the variables occuring in φ). The abbreviation ‘ec’ in Gdf_{H}^{ec} (and in Cdf_{H}^{ec}) refers to this fact.

                                                                    d-g

Definition 2.4 Throughout this paper, G denotes the following set.

G =^{def} {[i/j] : i, j ∈ ω} ∪ {suc, pred}.

The following theorem summarizes the main results of this section.

                                                                    csicsa1

9Gwdf refers to the name ‘\underline{g}eneralized \underline{w}eak \underline{d}iagonal \underline{f}ree cylindric set algebra’ used in [HMTI] to denote the H-free reduct of our class.

10The definition makes perfect sense for the case when V is only a generalized weak Cartesian space (or even any subset of ^{ω}U for some set U). For brevity, we will not discuss here the more general cases.

Theorem 2.5 (i). ICdf_{G} is a finite schema axiomatizable quasi-variety. That is, there is a finite schema Qx_{G}^{11} of quasi-equations such that

ICdf_{G} = Mod(Qx_{G}) .

(ii). IGdf_{G}^{ec} is a finite schema axiomatizable discriminator variety.

(iii). HCdf_{G} is a variety axiomatized by a finite set Ax_{G}^{12} of equation schemas. Thus, Ax_{G} axiomatizes Eq(Cdf_{G}) i.e.

Cdf_{G} ⊧ e iff Ax_{G} ⊢ e,

for any equation e in the language of Cdf_{G}.

The statements of this theorem are restated in Theorems 2.7, 2.15, 2.16 below in a more detailed form. In the following part of this section we present the finite sets of equations and quasi-equations that axiomatize HCdf_{G}, ICdf_{G} and IGdf_{G}^{ec}. Further, the related weak classes are examined and a detailed characterization is given. (Theorem 2.7) Finally, we show that many of the results remain valid if we replace the set G by an arbitrary set H of transformations provided that H satisfies certain properties. (Theorems 2.11, 2.19, 2.20)

                                                                    d-ax

Definition 2.6 We define the finite set Ax_{G} of axiom schemas to be the union of sets (1)–(6) below.

(1). A finite set of equations axiomatizing Boolean algebras.

(2). For every τ ∈ G, the following axioms stating that s_{τ} is a Boolean homomorphism:

s_{τ} (x ∨ y) = s_{τ} (x) ∨ s_{τ} (y), s_{τ} (−x) = −s_{τ} (x).

(3). The axioms governing s_{[i/j]}’s: for all distinct i, j, k ∈ ω,

s_{[j/i]}s_{[i/j]}x = s_{[j/i]}x, s_{[j/k]}s_{[i/j]}x = s_{[j/k]}s_{[i/k]}x.

(4). The axioms describing the connections between s_{[i/j]}’s, s_{suc} and s_{pred}:

s_{pred}s_{suc}x = x,
s_{suc}s_{pred}x = s_{[0/1]}x,
s_{suc}s_{[i/j]}x = s_{[suc(i)/suc(j)]}s_{suc}x for all distinct i, j ∈ ω.

(5). Two axiom schemas about c_{i} and the Boolean operations: for all i ∈ ω, x ≤ c_{i}x, c_{i}(x ∨ y) = c_{i}x ∨ c_{i}y.

(6). The axiom schemas describing the connection between s_{[i/j]}’s and c_{k}’s: for all distinct i, j, k ∈ ω,

s_{[i/j]}c_{i}x = c_{i}x,
c_{i}s_{[i/j]}x = s_{[i/j]}x,
c_{k}s_{[i/j]}x = s_{[i/j]}c_{k}x.

11Qx_{G} is presented in Definition 2.14 below.

12Ax_{G} is presented in Definition 2.6 below.

                                                                    th-main

Theorem 2.7 (characterization of IGwdf_{G} and related classes) Let G and Ax_{G} be as in Definitions 2.4 and 2.6. Then statements (1)–(4) below hold.

(1). IGwdf_{G} is axiomatizable by the finite set Ax_{G} of equation schemas i.e. IGwdf_{G} = Mod(Ax_{G}).

(2). IGwdf_{G} is a variety.

(3). IGwdf_{G} = IGwdf_{G}^{nm} = IGwdf_{G}^{cm} = HCdf_{G}.

(4). The set Eq(Cdf_{G}) of equations is axiomatizable by the finite set Ax_{G} of equation schemas i.e.

Cdf_{G} ⊧ e iff Ax_{G} ⊢ e,

for any equation e in the language of Cdf_{G}.

Proof (2) is a corollary of (1) while (1) is proved in Subsections 3.1 – 3.3.

To prove (3) we note that statement (3) is a special case of Theorem 2.11 (ii), (iii). To see that the later is applicable, we need to show that the successor, the predecessor and all the substitutions are bounded transformations of ω and they have right quasi-inverses in [G]. (Consult Definition 2.9 for the notion of bounded, quasi-bounded and quasi-invertible transformation.) It easy to verify that the given transformations have the required properties using facts as suc ∘ pred(i) = pred ∘ suc(i) = i whenever i > 0.

Finally, (4) follows from (3) and (1).

Later, in Remark 2.22, we show that for a slightly modified version of IGwdf_{G} (where only the 0-th cylindrification is a basic operation, the other cylindrifications are terms of the reduced language) similar results can be achieved.

In the proof of the previous theorem we referred to a metatheorem (2.11). There we show that if H satisfies certain requirements then the classes IGwdf_{H} and IGwdf_{H}^{cm} actually coincide with IGwdf_{H}^{nm}.

                                                                    nt-approx

Notation 2.8 We will often deal with pairs of sequences that agree on all but finitely many coordinates. If q_{1} and q_{2} are sequences then

q_{1} ≈ q_{2} iff |{i ∈ ω : q_{1}(i) ≠ q_{2}(i)}| < ω.

Clearly, ≈ is an equivalence relation.

                                                                    d-bounded

Definition 2.9 Let f, g ∈ ^{ω}ω be arbitrary.

• f is said to be bounded if it does not send infinitely many elements of ω into the same place, that is, if |f^{−1}(i)| < ω for all i ∈ ω.

• f is said to be quasi-bounded if there is a k ∈ ω for which |f^{−1}(f(k))| < ω.

• g is called the right (left) quasi-inverse of f if f ∘ g ≈ Id (g ∘ f ≈ Id), where Id is the identity transformation of ω. f is said to be right (left) quasi-invertible in H ⊆ ^{ω}ω if it has a left (right) quasi-inverse in H.

                                                                    d-rich

Definition 2.10 (rich semigroup) Suppose that i, j, k ∈ ω, A ⊆ ω, f, g ∈ ^{ω}ω. Then f[i/j] and f[A/g] are transformation of ω defined as

f[i/j](k) = \{ \begin{matrix}j & if k = i \\ f(k) & otherwise \end{matrix} f[A/g](k) = \{ \begin{matrix}g(k) & if k ∈ A \\ f(k) & otherwise. \end{matrix}

(Note that f[i/j] and f ∘ [i/j] are different transformations.)^{13} A semigroup Q ⊆ ^{ω}ω is called rich if it satisfies the following two conditions:

• (∀i, j ∈ ω)(∀f ∈ Q) f[i/j] ∈ Q,

• (∃ŝ, p̂ ∈ Q)(∀f ∈ Q)

p̂ ∘ ŝ = Id ∧ Rng(ŝ) ≠ ω ∧ (ŝ ∘ f ∘ p̂)[(ω − Rng(ŝ))/Id] ∈ Q.

                                                                    th-nc

Theorem 2.11 Let H be an arbitrary set of transformations.

(i). IGwdf_{H}^{nm} = HSPCdf_{H} is a variety. Thus Eq(Cdf_{H}) = Eq(Gwdf_{H}^{nm}).

(ii). If for all σ ∈ H, σ is bounded then

IGwdf_{H}^{nm} = IGwdf_{H}^{cm} = HCdf_{H}.

(iii). If for all σ ∈ H, σ is quasi-bounded and right quasi-invertible in [H], then

IGwdf_{H} = IGwdf_{H}^{nm}.

(iv). Assume that [H] is a finite schema presented^{14} rich semigroup. Then, IGwdf ^{nm} is axiomatizable by a finite schema Σ of equations.

(i) and (iv) are quoted from [Sa92] (Theorem 2.1 (2)), the proof of (ii) and (iii) can be found in Subsection 3.3.

The example below shows that the requirement given in Theorem 2.11 (iii) cannot be omitted. In some cases Eq(Gwdf_{H}) ≠ Eq(Gwdf_{H}^{nm}).

                                                                    ex0

Example 2.12 Let doub ∈ ^{ω}ω be defined by doub(i) = 2i for every i ∈ ω, let H = {doub} and let e be the equation c_{0}s_{doub}x = s_{doub}c_{0}x.

Then

Gwdf_{H}^{nm} ⊧ e but Gwdf_{H} |̸= e.

Proof Let V = ^{ω}2^{(⟨0,1,0,1,...⟩)} ∪^{ω}3^{(⟨0,0,0,0,...⟩)}. Then \underline{P}(V) ∈ Gwdf_{H} \IGwdf_{H}^{nm} since e fails in \underline{P}(V) (choose x = \{⟨2, 0, 0, 0, …⟩\}) but e is satisfied in every algebra of IGwdf_{H}^{nm}.

We turn our attention to the study of classes of algebras with square (Cartesian space) unit elements. We prove that the class ICdf_{G} is a finite schema axiomatizable quasi-variety and is strictly smaller than IGwdf_{G}.

                                                                    ex1

Example 2.13 Let q be the quasi-equation s_{pred}x = −x ⇒ 0 = 1. Then^{15}

Gdf_{G} ⊧ q but IGwdf_{G} |̸= q.

Proof In a G–cylindric generalized set algebra we can pick a constant sequence s in the universe. For any element x of the algebra, the chosen s is in x if and only if it is in s_{pred}x. It implies that q is in the symmetric difference of −x and s_{pred}x so s_{pred}x ≠ −x.

On the other hand, if we put V = ^{ω}2^{(⟨1,0,1,0,...⟩)} ∪^{ω}2^{(⟨0,1,0,1,...⟩)} then e fails in \underline{P}(V). (Put x to be ^{ω}2^{(⟨0,1,0,1,...⟩)} and for that x, s_{pred}x = −x.)

                                                                    d-qx1

Definition 2.14 (i). Let n ∈ ω. We define c_{(n)}x =^{def} c_{0}c_{1} … c_{n−1}x. Fur-

ther, s_{n-pred}x =^{def} s_{pred}s_{[0/1]}s_{[1/2]} … s_{[n−1/n]}x. Hence, s_{n-pred} is a term

function^{16}.

13f[i/j] can be distinguished from f[A/g] by noticing that always |g| ≥ ω > i.

14We use the notion of a finite schema presented semigroup in the usual sense. For completeness we will recall this concept in Definition 3.7 in the ‘Proofs’ section.

15For completeness we note connections of Example 2.13 and the theory of polyadic algebras (PA_{ω}’s) and PA’s with equality (PEA_{ω}’s) without recalling these two classes. We use the notation of [HMTII]. Although Ax_{G} |̸= q, we have PA_{ω} ⊧ q (e.g. by the Daigneault–Monk theorem). On the other hand, there are equations e such that PEA_{ω} |̸= e but RPEA_{ω} ⊧ e, cf. Németi-Sági [NS95].

16In set algebras, the term function s_{n-pred} coincides with s_{τ} for τ = ⟨0, 1, …, n − 1, n − 1, n, n + 1, …⟩, that is,

τ(i) = (pred⌈ω − n) ∪ (Id⌈n) = \{ \begin{matrix}i & if i < n \\ pred(i) & otherwise. \end{matrix}

(ii). We define Qx_{G} to be the following schema of quasi-equation.

⋃_{i≤m} c_{(n_{i})}x_{i} = 1 ∧ ⋀_{i≤m} s_{n_{i}-pred}x_{i} ≤ −x_{i} ⇒ 0 = 1,

for n_{0}, n_{1}, …, n_{m}, m ∈ ω.

                                                                    cj1

Theorem 2.15

ICdf_{G} = Mod(Ax_{G} ∪ Qx_{G}).

Proof ^{17} The general Theorem 2.19 should be applied to H = G. Qx can be simplified to Qx_{G} and Theorem 2.7 implies that Eq(IGwdf_{G}) follows from Ax_{G}. It is left to the reader to show the first implication.

We conjecture that Qx_{G} can be considerably simplified. Cf. e.g. the definition of Ax_{2} and proof of Proposition 1 in Andréka [A91] part II.

                                                                    t-nemeti

Theorem 2.16 IGdf_{G}^{ec} is a finite schema axiomatizable discriminator variety. Furthermore, IGdf_{G}^{ec} = Mod(Σ) where Σ is Ax_{G} together with the following set of axiom schemas:

(i). axioms stating that c_{(ω)} is a complemented closure operator, i.e. x ≤ c_{(ω)}x, c_{(ω)}(x ∪ y) = c_{(ω)}x ∪ c_{(ω)}y, c_{(ω)}c_{(ω)}x = c_{(ω)}x, c_{(ω)}−c_{(ω)}x = −c_{(ω)}x,

(ii). axiom schemas stating that c_{(ω)} majorizes all the other operators, i.e. c_{(ω)}x ≥ f(x) for all f ∈ {c_{i}, s_{τ} : i ∈ ω, τ ∈ G},

(iii). axioms corresponding to Qx_{G}: for all n_{0}, n_{1}, …, n_{m}, m ∈ ω,

−c_{(ω)}−( ⋃_{i≤m} c_{(n_{i})}x_{i}) ≤ ⋃_{i≤m} c_{(ω)}(x_{i} ∩ s_{n_{i}-pred}(x_{i})).

ICdf_{G}^{ec} is the class of subdirectly irreducible members of IGdf_{G}^{ec}.

Theorem 2.16 is a special case of the general Theorem 2.20.

                                                                    ques1

Open question 2.17 Find simpler axiom schemas aximatizing ICdf_{G} and IGdf_{G}^{ec}, respectively.

Below we show that ICdf_{H} is a quasi-variety, provided that H satisfies some properties. Furthermore, we give a set Qx of quasi-equations that axiomatize ICdf_{H} over IGwdf_{H}. Results 2.19 and 2.20 were obtained jointly with István Németi.

                                                                    d-qx2

Definition 2.18 (i). Let n ∈ ω, Γ = {γ_{0}, …, γ_{n−1}} ⊆ ω. We recall from [HMTI] that c_{(Γ)}x =^{def} c_{γ_{0}} … c_{γ_{n−1}}x.

17In [Sa87] a simple proof is given to the fact that ICdf_{G} is closed under SPUp, i.e. it forms a quasi-variety. Finite schema axiomatizability is not proved there.

(ii). We define Qx to be

⋃_{i≤m} c_{(Γ_{i})}x_{i} = 1 ∧ ⋀_{i≤m} ⋂_{τ∈H_{i}} s_{τ} (x) = 0 ⇒ 0 = 1,

for m ∈ ω, Γ_{0}, …, Γ_{n−1} ⊆_{ω} ω, H_{i} ⊆_{ω} [H] such that (τ ∈ H_{i} ⇒ τ⌈Γ_{i} =
Id⌈Γ_{i}).

                                                                    t-csax

Theorem 2.19 Let H ⊆ ^{ω}ω such that [H] contains all finite transformations and every element of H is bounded, left and right quasi-invertible in H. Then

(1). ICdf_{H} is a quasi-variety,

(2). ICdf_{H} is axiomatized by Qx over Gwdf_{H}, that is, Qx ∪ Eq(Gwdf_{H}) axiomatizes ICdf_{H}.

(1) is a consequence of (2) while (2) is proved in Subsection 3.4.

                                                                    t-222

Theorem 2.20 Assume that H ⊆ ^{ω}ω is such that ICdf_{H} is a quasi-variety. Then IGdf_{H}^{ec} is a discriminator variety whose subdirectly irreducible members are exactly the elements of ICdf_{H}^{ec}.

If all the assumptions of Theorem 2.19 hold for H then IGdf_{H}^{ec} is axiomatized over IGwdf_{H} by the axioms (i) and (ii) of Theorem 2.16 together with

(iii’). axioms corresponding to Qx: for all m ∈ ω, Γ_{0}, …, Γ_{n−1} ⊆_{ω} ω, H_{i} ⊆_{ω} [H] such that (τ ∈ H_{i} ⇒ τ⌈Γ_{i} = Id⌈Γ_{i}) we state

−c_{(ω)}−( ⋃_{i≤m} c_{(Γ_{i})}x_{i}) ≤ ⋃_{i≤m} c_{(ω)}( ⋂_{τ∈H_{i}} s_{τ} x).

Proof Let Σ be the set equations valid in Gdf_{H}^{ec}, that is, Σ = Eq(Gdf_{H}^{ec}). We want to prove IGdf_{H}^{ec} = Mod(Σ). IGdf_{H}^{ec} ⊆ Mod(Σ) is obvious.

For proving the other direction, it is enough to show that

Sir(Mod(Σ)) ⊆ ICdf_{H}^{ec} ⊆ IGdf_{H}^{ec}.

Therefore, assume A ∈ Sir(Mod(Σ)). A ⊧ x ≠ 0 → c_{(ω)}x = 1 can be verified as follows. Suppose for contradiction that c_{(ω)}x ≠ 1 for some element x of A. Since axioms (i) and (ii) certainly hold in Gdf_{H}^{ec}, they are in Σ. But using axioms (i) and (ii) we can prove that the relativization with x and that with −x decomposes A to the subdirect product of the two images.

Let A = ⟨B, c_{(ω)}⟩. If ⋀_{i<n} τ_{i} = σ_{i} → τ = σ is a quasi-equation valid in Cdf_{H}

then its equational translation c_{(ω)}(τ ⊕σ) ≤ ⋃_{i<n} c_{(ω)}(τ_{i}⊕σ_{i}) (⊕ is the symmetric

difference operator derivable from the Boolean connectives) holds in Cdf_{H}^{ec} and also in IGdf_{H}^{ec} = SPCdf_{H}^{ec} so it is in Σ. Further, if the equational translation of a quasi-equation is valid in A then the original quasi-equation is satisfied in B. This proves that Qeq(Cdf_{H}) holds in B so B ∈ ICdf_{H} using the assumption that ICdf_{H} is a quasi-variety. This immediately yields A ∈ ICdf_{H}^{ec}. Since every member of ICdf_{U}^{ec} is subdirectly irreducible we get Sir(IGdf_{H}^{ec}) = ICdf_{H}^{ec}

The second part of the theorem follows from the first and from Theorem 2.19.

                                                                    ques

Open question 2.21 The authors would like to know if the quasi-variety Gdf_{G^{×}} in Sain [Sa87], [Sa93] (cf. e.g. Section 4 in [Sa93]) admits a finite schema axiomatization (perhaps by the techniques of 2.15 or 2.16 herein).

                                                                    rm-allci

Remark 2.22 In fixing the basic operations, one of the motivations could have been that none of the operations shall be definable by any term of the others. One can easily notice that in Gwdf_{G} this is not the case. For any i ∈ ω, i > 0, c_{i} can be defined by a term of c_{0} and the other operations as follows.

c_{i}x = s_{[i,0]}c_{0}s_{[i,0]}x,

where s_{[i,j]} abbreviates the term s_{pred}s_{[0/suc(j)]}s_{[suc(j)/suc(i)]}s_{[suc(i)/0]}s_{suc}.

If we had chosen the smaller set {∪, −, s_{τ} , c_{0}}_{τ∈H} =^{def} t_{H}^{∗} ⊆ t_{H} to be the set of basic operations then the class Gwdf_{H}^{∗} of representable algebras would be defined as

Gwdf_{H}^{∗} = S {⟨P(V), ∪, −, s_{τ} , c_{0}⟩_{τ∈H} : V satisfies the conditions listed in Definition 2.2} .

With this modified class in place of Gwdf_{G}, Theorem 2.7 remains true provided that the set Ax_{G} is replaced with the following bigger set.

For all distinct i, j, k, l ∈ ω we state:

(’1). Same as (1).

(’2). Same as (2).

(’3). (3) together with the following 3 schemas:

s_{[i/k]}s_{[i/j]}x = s_{[i/j]}x, s_{[k/j]}s_{[i/j]}x = s_{[i/j]}s_{[k/j]}x,
s_{[k/l]}s_{[i/j]}x = s_{[i/j]}s_{[k/l]}x.

(’4). Same as (4).

(’5). (5) restricted to i = 0, that is, x ≤ c_{0}x, c_{0}(x ∨ y) = c_{0}x ∨ c_{0}y.

(’6). s_{[0/1]}c_{0}x = c_{0}x,

c_{0}s_{[0/1]}x = s_{[0/1]}x,
c_{0}s_{[i/j]}x = s_{[i/j]}c_{0}x.

2.3 Finitizing algebras of first order logic with equality

As we said in the Introduction, the present subsection is strongly related to Craig [Cr74], and can be viewed as a continuation of the approach initiated therein. Indeed, it is very likely that Theorem 2.27 below could be proved from Craig’s results. However, we show a generalization of these results and in later work we intend to generalize it in various directions, a part of which was indicated in [Sa87] and [Sa92].

                                                                    df-gwsp

Definition 2.23 Suppose that H is a fixed subset of ^{ω}ω. An algebra is called a generalized weak H–cylindric set algebra with equality (or briefly, a Gws_{H}) if it is of the form

⟨A, ∪, −, s_{τ} , c_{i}, d_{ij}⟩_{τ∈H,i,j∈ω}

where ⟨A, ∪, −, s_{τ} , c_{i}, ⟩_{τ∈H,i∈ω} ∈ Gwdf_{H} and the constants d_{ij} are the set theoretic diagonal elements (defined e.g. in [HMTII] Def. 3.1.1: d_{ij} = {q ∈ 1 : q(i) = q(j)} — where 1 is the unit element of the algebra).

The class of all generalized weak H–cylindric set algebras with equality is denoted by Gws_{H}. The similarity type of Gws_{H} is denoted by t_{H}^{=}.

Similarly to the case where equality was not present, we define subclasses of Gws_{H} on the bases of differences between the unit elements of the algebras.

                                                                    df-norm2

Definition 2.24 Let H be a subset of ^{ω}ω. The class of all algebras of Gws_{H}, whose unit elements are Cartesian spaces, (generalized Cartesian spaces) is denoted by Cs_{H} (Gs_{H} respectively).

The class Gs_{∅} is the class of representable cylindric algebras. In the literature (e.g. in [HMTII]) it is often denoted by Gs_{ω} or RCA_{ω}. Further parallel notations are Gws_{∅} = Gws_{ω}, Cs_{∅} = Cs_{ω}. Since the t_{∅}^{=}–reduct of a Gws_{H} is a cylindric algebra, we introduce the notation Rd_{CA} to be Rd_{t_{∅}^{=}}.

                                                                    csicsa2

Theorem 2.25 (i). HSPCs_{suc, pred} is a variety axiomatized by a finite set Ax^{=} of equation schemas. Thus, Ax^{=} axiomatizes Eq(Cs_{suc, pred}) i.e.

Cs_{suc, pred} ⊧ e iff Ax^{=} ⊢ e,

for any equation e in the language of Cs_{suc, pred}.

(ii). S Rd_{CA}HSPCs_{suc, pred} = RCA_{ω}.

Theorem 2.25 above is a corollary of Theorem 2.27. In the latter we give a more detailed description of the classes Cs_{suc, pred} and Gws_{suc, pred} i.e. we give a set of axioms (Definition 2.26) that axiomatizes them.

Results 2.15 and 2.16 have the corollary that Qeq(Cdf_{G}) and Eq(Cdf_{G}^{ec}) are finite schema axiomatizable. (*)

In view of the results above, it seems natural to expand some generalization of (*) for the case with equality. This was proved impossible in Craig [Cr74] Chapter 11. It is proved there (using a result of McKenzie) that neither Qeq(Cs_{suc, pred}) nor Eq(Gs_{suc, pred}^{ec}) is recursively enumerable.

Moreover, the following seems to be an even sharper contrast with 2.15 and 2.16. Let K be the class of algebras that are expansions of elements of Cs_{suc, pred} with the operation c_{(ω\2)} defined as follows:

c_{(ω\2)}x =^{def} {s ∈ V : (∃s′ ∈ x) s(0) = s′(0), s(1) = s′(1)}.

It is proved in [NS95] that Eq(K) is Π_{1}^{1} complete (i.e. highly non-computational).

                                                                    d-ax+

Definition 2.26 We define the finite set Ax^{=} of axiom schemas to be the union of sets (1)–(3) below.

(1). The set of axiom schemas characterizing cylindric algebras with equality (this set is quoted from [HMTI] Def. 1.1.1 p.162): for all i, j, k ∈ ω, a finite set of equations axiomatizing Boolean algebras

c_{i}0 = 0,  x ≤ c_{i}x,
c_{i}(x ∧ c_{i}y) = c_{i}x ∧ c_{i}y,  c_{i}c_{j}x = c_{j}c_{i}x,

d_{ii} = 1,

d_{ij} = c_{k}(d_{ik} ∧ d_{kj})  whenever k ∉ {i, j},
c_{i}(d_{ij} ∧ x) ∧ c_{i}(d_{ij} ∧ −x) = 0 whenever i ≠ j.

(2). The axioms stating that s_{suc} and s_{pred}are Boolean homomorphisms:

s_{suc}(x ∨ y) = s_{suc}(x) ∨ s_{suc}(y),  s_{suc}(−x) = −s_{suc}(x),
s_{pred}(x ∨ y) = s_{pred}(x) ∨ s_{pred}(y), s_{pred}(−x) = −s_{pred}(x).

(3). The axioms describing the connection between s_{suc}, s_{pred} and the other cylindric operations:

s_{pred}s_{suc}x = x, s_{suc}s_{pred}x = c_{0}(d_{01} ∧ x), s_{suc}c_{i}x  = c_{suc(i)}s_{suc}x, s_{suc}d_{ij}  = d_{suc(i)suc(j)}. s_{suc}(x − c_{0}(−d_{01})) = x − c_{0}(−d_{01}).

                                                                    th-rca

Theorem 2.27 (1). RCA_{ω} = SRd_{CA}Mod(Ax^{=}without (4)) that is, the equations valid in RCA_{ω} are exactly those consequences of Ax^{=} without (4) that do not use the new operations s_{suc}, s_{pred}.

(2). HGws_{suc, pred} = Mod(Ax^{=}).

(3). HSPCs_{suc, pred} = Mod(Ax^{=}).

(4). The set Eq(Cs_{suc, pred}) of equations valid in Cs_{suc, pred} is axiomatized by the finite set Ax^{=} of equations. I.e.

Cs_{suc, pred} ⊧ e iff Ax^{=} ⊢ e,

for any equation e in the language of Cs_{suc, pred}.

Proof We apply the general theorem 2.30 to the special case H = {suc, pred}. First we note that [\overline{suc, pred}] = G. (See Definition 2.29 below.) We have already seen that G is rich, the cardinality of G is ω, every element of G is bounded, and right quasi-invertible in G. (The right quasi-inverse of [i/j] is Id, while that of suc is pred and vica versa.)

(1) We apply Theorem 2.30 (1). Since all the equations valid in IGwdf_{G} — the equations of H2 — are consequences of Ax_{G} (Theorem 2.7 (1)), we need to show that the set Ax^{=} without (4) implies H1 and Ax_{G}. But most of the axioms of H1 and Ax_{G} is actually listed in Ax^{=} while the rest can be easily derived.

(2), (3) and (4) are corollaries of Theorem 2.30 (3). (We need only that H3 is also implied by Ax^{=}.)

Clearly, Mod(Ax^{=}) ⊃ Gws_{suc, pred}. We have seen in Theorem 2.27 (2) that equation (4) is valid in HGws_{suc, pred}. In the following example we show that it is not a consequence of Ax^{=} giving that the variety generated by Gws_{suc, pred}, that is HGws_{suc, pred}, is a strictly smaller class than Mod(Ax^{=}).

                                                                    ex2

Example 2.28 Let A be the four element Boolean algebra augmented with the unary operations c_{i} (i ∈ ω), s_{suc}, s_{pred} and the constants d_{ij} (i, j ∈ ω). s_{suc} and s_{pred} interchanges the atoms of A and fixes 1 and 0 while c_{i} (i ∈ ω) are the identity functions. d_{ij} = 1 for all (i, j ∈ ω). Equation (4) of Ax^{=} fails in A if we set x to be an atom of A.

Theorem 2.30 below states that we can obtain positive results not only for the specific choice H = {suc, pred} but for an arbitrary H ⊆ ^{ω}ω provided that H satisfies certain conditions. In that sense Theorem 2.30 is a metatheorem and Theorem 2.27 is its special case. In Definition 2.29 below we define those axioms that are used in the metatheorem 2.30.

                                                                    d-H13

Definition 2.29 For any set H ⊆ ^{ω}ω, we define H̄ = H ∪ {[i/j] : i, j ∈ ω}. Below we define the sets H1, H2, H3 of equations.

(H1). The set of all equations valid in Gwdf nm ; H̄, that is Eq(Gwdf nm ; H̄). Since tH̄ ⊈ t_{H}^{=}, we need to define, how to interpret an equation of Gwdf nm ; H̄ in Gws_{H}. If [i/j] ∉ H then the symbol s_{[i/j]}x denotes the term c_{i}(d_{ij} ∩ x) in the language of t_{H}^{=}.

(H2). s_{[i/j]}x = c_{i}(d_{ij} ∩ x) when [i/j] ∈ H,

s_{σ}d_{ij} = d_{σ(i)σ(j)}  when σ ∈ H,
c_{k}d_{ij} = d_{ij}  when i, j, k ∈ ω, i ≠ k ≠ j.

(H3).

s_{σ}(x − c_{0}(−d_{01})) = x − c_{0}(−d_{01}) when σ ∈ H,
c_{i}(−c_{0}(−d_{01})) = −c_{0}(−d_{01})  when i ∈ ω,
c_{i}c_{0}(−d_{01}) = c_{0}(−d_{01})  when i ∈ ω.

                                                               t-gen=

Theorem 2.30 (general) Let H be a set of transformations of ω. Then (1)–(4) below hold.

(1). If [H̄] is rich, then RCA_{ω} = S Rd_{CA}Mod(H1, H2).

(2). If the conditions (a)–(e) are satisfied then Eq(Cs_{H}) is finitely axiomatizable i.e. there is a finite schema Σ of equations such that

Cs_{H} ⊧ e iff Σ ⊢ e,

for any equation e in the language of Cs_{H}.

(a) [H̄] is rich,

(b) |H| ≤ ω,

(c) for any σ ∈ H, σ is bounded,

(d) for any σ ∈ H, σ is right quasi-invertible in [H̄],

(e) [H̄] is a finitely presented semigroup (see Definition 3.7).

(3). If the conditions (a)–(c) above and (f) below are satisfied then HGws_{H} = Mod(H1, H2, H3) and therefore,

Gws_{H} ⊧ e iff (H1, H2, H3) ⊢ e,

for any equation e in the language of Gws_{H}.

(f) for any ν, μ ∈ [H̄] there are ν^{∗}, μ^{∗} ∈ [H̄] with ν ∘ ν^{∗} ≈ μ ∘ μ^{∗}.

(4). If the conditions (a)–(d) are satisfied then HSPCs_{H} = Mod(H1, H2, H3)

and therefore,

Cs_{H} ⊧ e iff (H1, H2, H3) ⊢ e,

for any equation e in the language of Cs_{H}. Furthermore, if conditions (a)–(d) are satisfied then HGws_{H} = HGs_{H} = HSPCs_{H}.

(1) is proved in Subsection 3.5. (2) follows from the observation that H2, H3 are already finite schemas of equations, and that by Theorem 2.11 (iv) above there is a finite schema Σ_{0} such that Σ_{0} ⊢ H1. Now, Σ = Σ_{0} ∪ (H1, H2). (3) and (4) is proved in Subsection 3.7.

2.4 Open Qusetions

The authors would like to collect those questions that where raised in the sections listing the results of the paper.

Find simpler axiom schemas aximatizingICdf_{G} and IGdf_{G}^{ec}, respectively. (Cf. Theorem’s 2.15, 2.16 and the definition of Qx_{G}).

Is the quasi-variety Gdf_{G^{×}} in Sain [Sa87], [Sa93] (cf. e.g. Section 4 in [Sa93]) admits a finite schema axiomatization (perhaps by the techniques of 2.15 or 2.16 herein)?

2.5 Application to logic

Consider the following three types of algebraic results:

(i). IGwdf_{H} is axiomatizable by the finite schema Ax_{H} of equations (if H satisfies certain conditions).

(ii). IGdf_{H} is closed under ultraproducts (under some conditions in H).

(iii). Eq(Cdf_{H}) or Eq(Cs_{H}) is axiomatizable by a finite set of equation schemas.

In the present work we prove results of type (i)–(iii). A detailed elaboration of some of the logical applications of results of type (i)–(iii) is given in Sain [Sa93] Section 4. Though therein the explanation is given for a particular choice (denoted by G^{+}) of H, the same argument applies to any other choice of H (satisfying the conditions of our theorems). The reader interested in applications to logic and in relevance to the original logic oriented formulation of the finitization problem is referred to Sain [Sa93] Section 4 and Németi [N91].

We plan to elaborate these considerations together with new developments in this direction in a sequel to the present work.

2.6 Comparisons with the polyadic notion of a schema

First half of the material studied in this paper is concerned with algebras of logic without equality. This half seems to be related to the axiomatization of representable polyadic algebras of infinite dimension (RPA_{ω}). The set of axiom schemas approximating RPA_{ω} in [HMTII] p225 is denoted by P_{0}–P_{11}.

A difference between the polyadic approach and ours is that RPA_{ω} has uncountably many operation symbols, hence the computability or recursive enumerability aspects of, say, a completeness theorem (or equivalently of an axiomatizability theorem) are not automatic consequences of the existence of a finite schema axiomatization provided by the theorem in question. As a contrast, in our approach the basic operation symbols (s_{suc}, s_{pred}, s_{[i/j]}, c_{i} i, j ∈ ω) are effectively enumerated and hence the finite schemas (e.g. Ax_{G} in Definition 2.6) of axioms yield a recursive enumeration of their consequences. To illustrate the computational differences between the two notions of schema we recall the following result of Gábor Sági.

There are three primitive recursive functions τ_{1}, τ_{2}, τ_{3} ∈ ^{ω}ω such that the set E of equations of the language of RPA_{ω} that involve only {s_{τ_{i}} : i = 1, 2, 3} as operations and are consequences of P_{0}–P_{11} is not recursively enumerable. This seems to mean that there are effective and decidable sublanguages L of the language of RPA_{ω} such that E_{L} = {e ∈ L : P_{0}–P_{11} ⊢ e} is not recursively enumerable. Cf. Sági [Sá95]. Since L is decidable (as a subset of the full language of RPA_{ω}), this is in contrast with the expected behaviour of finite schema axiomatizations. This observation can be interpreted as saying that the finite schemas P_{0}–P_{11} are less informative from the effective or constructive point of view as one would normally expect. This seems to imply that for any reasonable generalization (from ω to L_{0}) of the notion of computability the set Eq(Mod(P_{0}–P_{11})) will turn non-recursively enumerable.

As a contrast, E_{L} becomes recursively enumerable if we replace P_{0}–P_{11} with any (e.g. Ax_{G}) of our axiom schemas and L with any decidable (or even recursively enumerable) subset of our equational language.

The other half of the present paper, that deals with algebras associated to logics with equality, does not seem to have a polyadic algebraic (RPA_{ω}– theoretic) counterpart in the literature yet. Such a counterpart would deal with SUpRPEA_{ω} or Eq(RPEA_{ω}). (It has been known for long that SUpRPEA_{ω} ≠ RPEA_{ω} hence the subject of study is not RPEA_{ω} but rather SUpRPEA_{ω}.)

In [NS95] it is proved about the polyadic notion (or Halmos’ notion) of a schema that Eq(RPEA_{α}) is not axiomatizable by any set of polyadic schemas if α ≥ ω. Therefore the schema P_{0}–E_{3} used by Halmos to axiomatize PEA_{α} and quoted in [HMTII, pp.225-6] does not describe Eq(RPEA_{α}), moreover, one cannot add similar schemas to P_{0}–E_{3} such that the result would axiomatize Eq(RPEA_{α}).

3 Proofs

3.1 An axiomatization of IGwdf_{G}

To prove Theorem 2.7 (1), we use the method and some theorems described in [Sa92].

                                                                    cl-rich

Claim 3.1 If the subsemigroup Q of ⟨^{ω}ω, ∘⟩ is rich then all the finite transformations belong to Q.

Proof Id ∈ Q since Id = p̂ ∘ ŝ. For all i, j ∈ ω, [i/j] ∈ Q since [i/j] = Id[i/j] and [i, j] ∈ Q since [i, j] = [i/j][j/i]. The semigroup of finite transformations is generated by the set of transpositions and replacements.

                                                                    cl-g-reach

Claim 3.2 The semigroup [G] is rich.

Proof All the transpositions belong to [G], since

[i, j] = pred ∘ [0/j] ∘ [j/i] ∘ [i/0] ∘ suc.

This implies that every finite transformation of ω belongs to [G].

A transformation f of ω is called n-shifted if f(x) = x + n for all but finitely many members of ω (n is a given integer). Clearly, suc^{n} is n-shifted, pred^{n} is (−n)-shifted and Id is 0-shifted i.e. it is a finite transformation. If f is n-shifted, g is (−n)-shifted then both f ∘ pred^{n} and suc^{n} ∘ g are finite transformations. (Here n is a natural number.) This implies that f is equal to the composition of a finite transformation (namely f ∘ pred^{n}) and suc^{n}, g is equal to the composition of pred^{n} and a finite transformation (namely suc^{n} ∘ g). So every n-shifted transformation is in [G].

An f ∈ ^{ω}ω is called shifted if it is n-shifted for some integer n. All shifted transformations belong to [G] and every member of [G] is shifted. (The generators of [G] are shifted, composition of shifted transformations is shifted.)

The first condition of Definition 2.10 is satisfied since if f is shifted then so is f[i/j] and that implies that it belongs to [G]. The elements ŝ and p̂ of [G] required in the second condition can be suc and pred. ω − Rng(suc) = {0}. The previous argument shows that (suc ∘ f ∘ pred)[{0}/Id] belongs to [G].

In the definition of Gwdf_{H}, τ ∈ H plays a double role. Namely, s_{τ} is a symbol hence τ itself is also used as a symbol. On the other hand, τ as an element of ^{ω}ω is a concrete function i.e. it occurs on the semantic side of Gwdf_{H}. In the proofs below, it will be most useful to distinguish τ as a symbol from τ as a function. (The reason for this will be clear e.g. in Definition 3.3 below.) Therefore, from that point on until the end of Subsection 3.2 we use temporarily \underline{τ} when we want to refer to τ as a concrete transformation of ω, and we use τ to refer to the symbol or name of the transformation. For example, suc, pred, [i/j], [i, j] are symbols while \underline{suc}, \underline{pred}, \underline{[i/j]}, \underline{[i, j]} are transformations of ω (i, j ∈ ω).

Furthermore, if σ is a finite sequence (or word) over H, that is ⟨τ_{1}, …, τ_{n}⟩ = σ ∈ H^{∗}, then \underline{σ} denotes the transformation \underline{τ}_{1} ∘ … ∘ \underline{τ}_{n}. If H is a set of symbols then \underline{H} = \{\underline{τ} : τ ∈ H\}. It follows that \underline{H^{∗}} = [\underline{H}].

                                                                    d-*17

Definition 3.3 (Definition 2.2.2 of [Sa93]) Let H be a set of names of transformations of ω with the property that c_{i} and s_{[i/j]} are term definable in IGwdf_{H}^{∗} for every i, j ∈ ω. Below we define postulates (*1)-(*7). The postulates are stated for all σ, ν ∈ H^{∗} and for all i, j ∈ ω. The symbols c_{i} and s_{[i/j]} abbreviate the terms that define c_{i} and s_{[i/j]} respectively. For any word σ ∈ H^{∗}, σ = ⟨τ_{1} … τ_{n}⟩, s_{σ}(x) abbreviates the term s_{τ_{1}} … s_{τ_{n}}(x).

(*1). The finite set of equations axiomatizing Boolean algebras. The axioms stating that c_{i} is an additive complemented closure operation and c_{i}, c_{j} commute: x ≤ c_{i}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.

(*2). The axioms stating that s_{σ} is a Boolean homomorphism:

s_{σ}(x ∨ y) = s_{σ}(x) ∨ s_{σ}(y), s_{σ}(−x) = −s_{σ}(x).

(*3). s_{σ}(x) = s_{ν}(x) if \underline{σ} = \underline{ν}.

(*4). s_{σ}(x) = x if \underline{σ} = Id.

(*5). s_{σ}c_{i}x = s_{ν}c_{i}x if j ≠ i ⇒ \underline{ν}(j) = \underline{σ}(j).

(*6). s_{σ}c_{i}x = c_{j}s_{σ}x if \underline{σ}^{−1}(j) = \{i\}.

(*7). c_{i}s_{[i/j]}x = s_{[i/j]}x if i ≠ j.

                                                                    th-*17

Theorem 3.4 (Theorem 2.2.4 of [Sa93]) Let H be a set as in the previous definition. Assume that [\underline{H}] is rich. Then

Mod_{t_{H}^{∗}} ((*1)-(*7)) = IGwdf_{H}^{nm}^{∗}.

                                                                    cr-*171

Corollary 3.5 Let H be as in the previous theorem. Also assume that the set theoretic operations c_{i} (i > 0) are term definable in Gwdf_{H}^{∗}. Then (*1)- (*7) together with the definition of c_{i} (i > 0) is a complete axiomatization of IGwdf_{H}^{nm}.

                                                                    cr-*17

Corollary 3.6 (*1)-(*7) together with the definition of c_{i} (i > 0) is a complete axiomatization of IGwdf_{G}^{nm}. Furthermore, that set is a complete axiomatization of IGwdf_{G} since the two class coincide as it will be proved in Subsection 3.3.

3.2 Theorem 2.7 (1): finite schema axiomatizing IGwdf_{G}

The axiom system defined in Definition 3.3 is not a schema axiomatization since the variable σ ranges over G^{∗} and not G. In this subsection we will correct the axiom system.

In the definition below we recall a standard concept of universal algebra. (See e.g. [HMTII].)

                                                                    d-fin-pr

Definition 3.7 An algebra A is said to be presented by a set Σ of defining equation in a variety V if all of the following conditions hold.

• A is generated by some set H ⊆ A.

• We denote the expansion of the algebra A with constants corresponding to H by A′. Σ is a set of equations of the language of A′ that contain no variables.

• For every pair of terms τ and ν of the language of A′ that contain no

variables

A′ ⊧ τ = ν ⇔ Σ ∪ Eq(V) ⊧ τ = ν.

Since the equational logic has a strongly complete and sound inference system, in the case when V is the variety SG of all semigroups we can simplify the last condition as

• (∀τ, ν ∈ H^{∗}) \underline{τ} = \underline{ν} ⇔ Σ ∪ Eq(SG) ⊢ τ = ν.

                                                                    th-g-pr

Theorem 3.8 [\underline{G}] is presented by the following set of equations in the variety of all semigroups:

(3.1). pred suc = λ where λ is the empty word,

(3.2). suc pred = [0/1],

(3.3). suc[i/j] = [i + 1/j + 1]suc for every distinct i, j ∈ ω,

(3.4). [i/j]pred = pred[i + 1/j + 1] for every distinct i, j ∈ ω with i ≠ 0,

(3.5). [0/j]pred = pred[0/j + 1][1/j + 1] for every j ∈ ω.

(3.6). Thompson’s axioms from [To93] that present the semigroup generated by the replacements only. All i, j, k, l ∈ ω are distinct.

(B1) [i/k][i/j] = [i/j],
(B2) [j/i][i/j] = [j/i],
(B3) [j/k][i/j] = [j/k][i/k],
(B4) [k/j][i/j] = [i/j][k/j],
(B5) [k/l][i/j] = [i/j][k/l],
(B6) [i/j][j/k][k/i][i/j] = [i/k][k/j][j/i],
(B7) [i/j][j/k][k/l][l/i] = [i/k][k/l][l/j][j/i][i/l].

Proof We will use Thompsons result saying that the semigroup generated by the replacements is presented by a set of axioms. The set listed in [To93] contains three additional axioms but they are derivable from the others: [i/j][i/j] = [i/j][i/i + j + 1][i/j] = [i/i + j + 1][i/j] = [i/j] [i/j][k/j][i/j] = [i/j][i/j][k/j] = [i/j][k/j] and [i/j][k/l][i/j] = [i/j][i/j][k/l] = [i/j][k/l].

In this proof we will write ⊢ instead of (3.1)-(3.6)∪Eq(SG) ⊢.

We say that τ ∈ G^{∗} is in normal form if τ = pred^{n}τ′suc^{m} for some τ′ ∈ {[i/j]}_{i,j∈ω}^{∗} and n, m ∈ ω. Every word can be reduced to a normal formed word using only (3.1)-(3.5). This implies that

(∀τ ∈ G^{∗})(∃τ′ ∈ G^{∗}) ⊢ τ = τ′ and τ′ is in normal form

Let τ and ν be arbitrary words from G^{∗}, assume that \underline{τ} = \underline{ν}. There are n, m, l, k ∈ ω and τ′, ν′ ∈ {[i/j]}_{i,j∈ω}^{∗} for that ⊢ τ = pred^{n}τ′suc^{m}, ⊢ ν = pred^{l}ν′suc^{k}.

Since \underline{τ} is m−n-shifted, \underline{ν} is k −l-shifted we can conclude that m−n = k −l or m = n + k − l.

Without loss of generality we may assume that l ≤ n. ⊢ pred^{l}ν′suc^{k} = pred^{l}pred^{n−l}suc^{n−l}ν′suc^{k} = pred^{n}ν′′suc^{n−l}suc^{k} = pred^{n}ν′′suc^{m} can be derived using (3.1), (3.3) and the previous observation. ⊢ suc^{n}τpred^{m} = [0/1]^{n}τ′[0/1]^{m} and similarly ⊢ suc^{n}νpred^{m} = [0/1]^{n}ν′′[0/1]^{m} using (3.2).

\underline{τ} = \underline{ν} implies \underline{suc}^{n} ∘ \underline{τ} ∘ \underline{pred}^{m} = \underline{suc}^{n} ∘ \underline{ν} ∘ \underline{pred}^{m} = \underline{[1/0]}^{n} ∘ \underline{τ′} ∘ \underline{[1/0]}^{m} = \underline{[1/0]}^{n} ∘ \underline{ν′′} ∘ \underline{[1/0]}^{m}.

¿From the main result of Thompson [To93] we know that \underline{[1/0]}^{n}∘\underline{τ′}∘\underline{[1/0]}^{m} = \underline{[1/0]}^{n} ∘ \underline{ν′′} ∘ \underline{[1/0]}^{m} imply ⊢ [0/1]^{n}τ′[0/1]^{m} = [0/1]^{n}ν′′[0/1]^{m}. Collecting all the information we have: ⊢ suc^{n}τpred^{m} = suc^{n}νpred^{m}. But this implies ⊢ pred^{n}suc^{n}τpred^{m}suc^{m} = pred^{n}suc^{n}νpred^{m}suc^{m}.

Using (3.1) again we can conclude ⊢ τ = ν and this completes the proof.

The set of defining equations listed in 3.8 is not independent. Below we show that equations (3.4), (3.5), (B6), (B7) are implied by the others.

                                                                    cl-b7

Claim 3.9 (3.1),(3.2),(3.3),(B1),(B3),(B4),(B5)⊢(B6)

Proof First we prove that the listed B-axioms imply

[i/j][j/k][k/i][i/j][a/b] = [i/k][k/j][j/i][a/b]

where all i, j, k, a, b are distinct:

[i/j][j/k][k/i][i/j][a/b]  =^{B1}  [i/j][j/k][k/i][i/j][a/j][a/b]
=^{B4}  [i/j][j/k][k/i][a/j][i/j][a/b]
=^{B1}  [i/j][j/k][k/i][a/i][a/j][i/j][a/b]
=^{B3,B4}  [i/j][j/k][a/i][k/a][a/j][i/j][a/b]
=^{B5,B3,B4,B1} [a/j][i/j][j/k][i/j][k/a][a/b]
=^{B3}  [a/j][i/j][j/k][i/k][k/a][a/b]

=^{B4,B1,B3} [a/j][i/k][j/i][k/a][a/b]
=^{B5}  [i/k][a/j][k/a][j/i][a/b]
=^{B3,B4,B5} [i/k][k/j][a/j][a/b][j/i]
=^{B1,B5}  [i/k][k/j][j/i][a/b].

Now we can compute:

[i/j][j/k][k/i][i/j] =^{3.1} pred suc[i/j][j/k][k/i][i/j] =^{3.3,3.1,3.2}

pred[i + 1/j + 1][j + 1/k + 1][k + 1/i + 1][i + 1/j + 1][0/1]suc =

pred[i + 1/k + 1][k + 1/j + 1][j + 1/i + 1][0/1]suc =^{3.3,3.1,3.2}

[i/k][k/j][j/i].

                                                                    cl-b8

Claim 3.10 (3.1),(3.2),(3.3),(B1),(B3),(B4),(B5)⊢(B7)

Proof First we prove that the listed B-axioms imply

[i/k][k/l][l/j][j/i][i/l][a/b] = [i/j][j/k][k/l][l/i][a/b]

where all i, j, k, l, a, b are distinct:

[i/k][k/l][l/j][j/i][i/l][a/b]  =^{B1,B4}  [i/k][k/l][l/j][j/i][a/l][i/l][a/b]
=^{B1,B4,B3} [i/k][k/l][l/j][a/i][j/a][a/l][i/l][a/b]
=^{B4,B5,B3} [a/k][i/k][k/l][l/j][i/l][j/a][a/b]
=^{B4,B3}  [a/k][i/k][k/l][i/j][l/i][j/a][a/b]
=^{B5,B1}  [a/k][i/j][k/l][l/i][j/a][a/b]
=^{B5}  [i/j][a/k][j/a][k/l][l/i][a/b]
=^{B3,B4,B5,B1} [i/j][j/k][a/k][a/j][k/l][l/i][a/b]
=^{B1,B5}  [i/j][j/k][k/l][l/i][a/b].

Now we can compute:

[i/k][k/l][l/j][j/i][i/l] =^{3.1} pred suc[i/k][k/l][l/j][j/i][i/l] =^{3.3,3.1,3.2}

pred[i + 1/k + 1][k + 1/l + 1][l + 1/j + 1][j + 1/i + 1][i + 1/l + 1][0/1]suc =

pred[i + 1/j + 1][j + 1/k + 1][k + 1/l + 1][l + 1/i + 1][0/1]suc =^{3.3,3.1,3.2}

[i/j][j/k][k/l][l/i].

                                                                    cl-35

Claim 3.11 (3.1),(3.2),(3.3),(B3),(B4)⊢(3.5)

Proof [0/j]pred =^{3.1} pred suc[0/j]pred =^{3.3} pred[1/j + 1]suc pred =^{3.2} pred[1/j + 1][0/1] =^{B3,B4} pred[0/j + 1][1/j + 1]

                                                                    cl-34

Claim 3.12 (3.1),(3.2),(3.3),(B4),(B5)⊢(3.4)

Proof [i/j]pred =^{3.1} pred suc[i/j]pred =^{3.3} pred[i + 1/j + 1]suc pred =^{3.2} pred[i + 1/j + 1][0/1] =^{B4orB5} pred[0/1][i + 1/j + 1] =^{3.2} pred suc pred[i + 1/j + 1] =^{3.1} pred[i + 1/j + 1]

We quote an important result of Pinter.

                                                                    cl-p

Claim 3.13 (Lemma 2.2 of [P73]) For every distinct i, j, k, l ∈ ω we have Ax_{G} ⊢ s_{[i/k]}s_{[i/j]} = s_{[i/j]}, Ax_{G} ⊢ s_{[k/j]}s_{[i/j]} = s_{[i/j]}s_{[k/j]}, Ax_{G} ⊢ s_{[k/l]}s_{[i/j]} = s_{[i/j]}s_{[k/l]}.

We will need the following technical observation that originates from Sándor Csizmazia:

                                                                    lm-uj7

Lemma 3.14 Ax_{G} together with the equations (*3), (*4), (*5), (*1) without c_{i}c_{j}x = c_{j}c_{i}x implies that for any τ ∈ {[i/j] | i, j ≥ 1} ∪ {[1/0]suc, pred[1/2]}

s_{τ} c_{0}x = c_{0}s_{τ} x

Proof There is nothing to prove in s_{[i/j]}c_{0}x = c_{0}s_{[i/j]}x (i, j ≥ 1) since it is included in Ax_{G}. It was formulated in the lemma only for further applications.

To prove the other two statements we will need the following claim quoted from Pinter [P73]:

                                                                    cl-ci

Claim 3.15 c_{i}x = min \overbrace{\{y | y = s_{[i/j]}y, y ≥ x\}}^{B}

Proof c_{i}x ∈ B since s_{[i/j]}c_{i}x = c_{i}x and c_{i}x ≥ x that is (5) and (6) of Ax_{G}.

For any y ∈ B y ≥ c_{i}x since c_{i}x ≤^{∗1} c_{i}y = c_{i}s_{[i/j]}y =^{∗7} s_{[i/j]}y = y.

Further observations are needed.

                                                                    cl-defci

Claim 3.16 c_{i}x = s_{[0,i]}c_{0}s_{[0,i]}x

Proof Using the previous claim, we have to prove that s_{[0,i]}c_{0}s_{[0,i]}x ∈ B =^{def} {y | y = s_{[i/j]}y, y ≥ x} and y ∈ B ⇒ y ≥ s_{[0,i]}c_{0}s_{[0,i]}x.

s_{[i/j]}s_{[0,i]}c_{0}s_{[0,i]}x =^{∗3} s_{[0,i]}s_{[0/j]}c_{0}s_{[0,i]}x =^{6} s_{[0,i]}c_{0}s_{[0,i]}x.

(5) implies c_{0}s_{[0,i]}x ≥ s_{[0,i]}x, using (2) we have s_{[0,i]}c_{0}s_{[0,i]}x ≥ s_{[0,i]}s_{[0,i]}x =^{∗4} x.

y ∈ B ⇒ y ≥ x ⇒^{∗1,2} s_{[0,i]}c_{0}s_{[0,i]}x ≤ s_{[0,i]}c_{0}s_{[0,i]}y =^{y∈B} s_{[0,i]}c_{0}s_{[0,i]}s_{[i/j]}y =^{∗3}

s_{[0,i]}c_{0}s_{[0/j]}s_{[0,i]}y =^{6} s_{[0,i]}s_{[0/j]}s_{[0,i]}y =^{∗3} s_{[0/j]}y =^{y∈B} y.

                                                                    cl-c1s01

Claim 3.17 c_{0}s_{[1/0]}x = c_{1}s_{[0/1]}x

Proof c_{0}s_{[1/0]}x =^{∗3} c_{0}s_{[1/2]}s_{[1/0]}x =^{6} s_{[1/2]}c_{0}s_{[1/0]}x =^{∗3} s_{[1/0]}s_{[1/2]}c_{0}s_{[1/0]}x =^{6}

s_{[1/0]}c_{0}s_{[1/2]}s_{[1/0]}x =^{∗3} s_{[1/0]}c_{0}s_{[1/0]}x =^{∗3} s_{[0,1]}s_{[0/1]}c_{0}s_{[0,1]}s_{[0/1]}x =^{6}

s_{[0,1]}c_{0}s_{[0,1]}s_{[0/1]}x =^{Cl.3.16} c_{1}s_{[0/1]}x

                                                                    cl-cisuc

Claim 3.18 c_{i+1}s_{suc}x = s_{suc}c_{i}x

Proof Let B_{1} = {y | s_{[i+1/i+2]}y = y, y ≥ s_{suc}x}, B_{12} = {y | s_{[i+1/i+2]}y = s_{[0/1]}y = y, y ≥ s_{suc}x}, B_{21} = {s_{suc}y | s_{[i/i+1]}y = y, y ≥ x}, B_{2} = {y | s_{[i/i+1]}y = y, y ≥ x}.

The following statements prove this claim: I c_{i+1}s_{suc}x = minB_{1}, II  minB_{1} = minB_{12}, III  B_{12} = B_{21}, IV minB_{21} = s_{suc}minB_{2}, V  minB_{2} = s_{suc}c_{i}x. .

I, V follow from Claim 3.15, IV from the observation that y ∈ B_{2} ↔ s_{suc}y ∈ B_{21}.

Similarly to the proof of the previous claim, in II we need to show that B_{12} ⊆ B_{1} (trivial) and (∀y ∈ B_{1}) − c_{0}(−y) ∈ B_{12} ∧ −c_{0}(−y) ≤ y.

So suppose y ∈ B_{1}. Then s_{[i+1/i+2]}(−c_{0}(−y)) =^{Ax} −c_{0}(−s_{[i+1/i+2]}y) = −c_{0}(−y),

s_{[0/1]}(−c_{0}(−y)) = −s_{[0/1]}c_{0}(−y) = −c_{0}(−y) and y ≥ s_{suc}x ⇒ −c_{0}(−y) ≥ −c_{0}(−s_{suc}x) = −c_{0}s_{suc}(−x) =^{∗} −s_{suc}(−x) = s_{suc}x. In * we used that s_{suc}x = s_{suc}s_{pred}s_{suc}x = s_{[0/1]}s_{suc}x = c_{0}s_{[0/1]}s_{suc}x = c_{0}s_{suc}x.

Turning to III, suppose that y ∈ B_{12}. Then y = s_{[0/1]}y = s_{suc}(s_{pred}y). s_{[i/i+1]}(s_{pred}y) = s_{pred}s_{suc}s_{[i/i+1]}(s_{pred}y) = s_{pred}s_{[i+1/i+2]}s_{suc}s_{pred}y = s_{pred}s_{[i+1/i+2]}s_{[0/1]}y = s_{pred}y, y ≥ s_{suc}x ⇒ s_{pred}y ≥ s_{pred}s_{suc}x = x.

On the other hand if we suppose that s_{suc}y ∈ B_{21} then s_{[i+1/i+2]}s_{suc}y = s_{suc}s_{[i/i+1]}y = s_{suc}y, s_{[0/1]}s_{suc}y = s_{suc}s_{[ssuc/y]} = s_{suc}y and y ≥ x ⇒ s_{suc}y ≥ s_{suc}x.

Now we can prove the two statements formulated in the lemma:

c_{0}s_{[1/0]}s_{suc}x =^{∗} s_{suc}c_{0}x =^{6} s_{suc}s_{[0/1]}c_{0}x =^{4} s_{[1/2]}s_{suc}c_{0}x =^{3}

=^{3} s_{[1/0]}s_{[1/2]}s_{suc}c_{0}x = s_{[1/0]}s_{suc}c_{0}x,

c_{0}s_{pred}s_{[1/2]}x =^{4} s_{pred}s_{suc}c_{0}s_{pred}s_{[1/2]}x =^{∗} s_{pred}c_{0}s_{[0/1]}s_{suc}s_{pred}s_{[1/2]}x = = s_{pred}c_{0}s_{[1/2]}x = s_{pred}s_{[1/2]}c_{0}x.

In * we used c_{0}s_{[1/0]}s_{suc}x =^{Cl.3.17} c_{1}s_{[0/1]}s_{suc}x =^{Ax} c_{1}s_{suc}s_{pred}s_{suc}x =^{Ax}

=^{Ax} c_{1}s_{suc}x =^{Cl.3.18} s_{suc}c_{0}x.

Proof of Theorem 2.7 (1) Using the result of the previous subsection stated in Corollary 3.6 we need to prove only that Ax_{G} ⊢(*1)–(*7) and Ax_{G} ⊢ c_{i}x = s_{[0,i]}c_{0}s_{[0,i]}x.

(*2) is a trivial consequence of (2).

(3) and (4) together imply (*3) and (*4) since if A is an algebra of IGwdf_{G} and A^{∗} is the semigroup of all polynomials of A, expanded with the constant symbols [i/j], suc, pred evaluated into the polynomials s_{[i/j]}, s_{suc}, s_{pred} then A^{∗} is a model of (3.1)–(3.6) ((3) and (4) is the relevant part of the set of equations (3.1)–(3.7) — see Claim 3.9–3.13 — written in the language of A^{∗}) and so \underline{τ} = \underline{ν} forces A^{∗} ⊧ τ = ν and that is s_{τ} x = s_{ν}x.

(*7) is included in (6).

To prove (*5), suppose τ and ν are in G^{∗} and \underline{τ} and \underline{ν} agree everywhere but in i. Then \underline{τ} ∘ \underline{[i/i + 1]} and \underline{ν} ∘ \underline{[i/i + 1]} are equal everywhere.

s_{τ} c_{i}x =^{6} s_{τ} s_{[i/i+1]}c_{i}x = s_{τ[i/i+1]}c_{i}x =
= s_{ν[i/i+1]}c_{i}x = s_{ν}s_{[i/i+1]}c_{i}x =^{6} s_{ν}c_{i}x

In (*1) x ≤ c_{i}x, c_{i}(x ∨ y) = c_{i}x ∨ c_{i}y follow from (2) and (5). c_{i}c_{i}x = c_{i}x and c_{i}(−c_{i}x) = −c_{i}x is a consequence of (2) and (6): c_{i}c_{i}x = c_{i}s_{[i/i+1]}c_{i}x = s_{[i/i+1]}c_{i}x = c_{i}x and c_{i}(−c_{i}x) = c_{i}(−s_{[i/i+1]}c_{i}x) = c_{i}s_{[i/i+1]}(−c_{i}x) = = s_{[i/i+1]}(−c_{i}x) = −s_{[i/i+1]}c_{i}x = −c_{i}x

To prove (*6) we will need the following observation: If T_{0} = \{f ∈ [\underline{G}] | f^{−1}(0) = {0}} and G_{0} = {[i/j] | i, j ≥ 1} ∪ {[1/0]suc, pred[1/2]} then T_{0} is generated by the meanings of the elements of G_{0}. To verify this statement define the function ′ mapping [\underline{G}] into itself

f′ = (\underline{suc} ∘ f ∘ \underline{pred})[0/0]

(Since [\underline{G}] is rich f′ ∈ [\underline{G}].) It is easy to check that ′ is a homomorphism ((f ∘ g)′ = f′ ∘ g′), furthermore, the ′ image of [\underline{G}] is T_{0} (if f ∈ [\underline{G}] then f^{′−1}(0) = \{0\} so f′ ∈ T_{0} and if g ∈ T_{0} then (\underline{pred} ∘ g ∘ \underline{suc})′ = g). Finally, we note that the set of transformations named by the elements of G_{0} coincide with the ′ image of the set of those transformations that are named by the elements of G.

We note that for any τ ∈ G_{0}, s_{τ} c_{0}x = c_{0}s_{τ} x. This follows from Lemma 3.14 since all the extra equations listed in the formulation of the lemma are consequences of Ax_{G}, as it was proved up till this point. In passing, we mention that the same reasoning shows that Claim 3.16 proves that the definition of c_{i} (i > 0) is implied by Ax_{G}. Turning our attention again to (*6), suppose τ ∈ G^{∗}, \underline{τ}^{−1}(j) = \{i\}. Then f = \underline{[j, 0]} ∘ \underline{τ} ∘ \underline{[i, 0]} ∈ T_{0}. Using the previous observation, f is a composition of functions named by elements of G_{0} say, f = \underline{ν_{1}} ∘ … ∘ \underline{ν_{n}}. (3), (4) and (6) imply that

s_{[j,0]τ[i,0]}c_{0}x = s_{ν_{1}...ν_{n}}c_{0}x = s_{ν_{1}} … s_{ν_{n}}c_{0}x = c_{0}s_{ν_{1}} … s_{ν_{n}}x = c_{0}s_{[j,0]τ[i,0]}x.

Finally we derive

s_{τ} c_{i}x † = s_{τ} s_{[i,0]}c_{0}s_{[i,0]}x = s_{[j,0]}s_{[j,0]τ[i,0]}c_{0}s_{[i,0]}x =
= s_{[j,0]}c_{0}s_{[j,0]τ[i,0]}s_{[i,0]}x † = c_{j}s_{τ} x.

(In † we used that the definition of c_{i} and c_{j} is already proven from Ax_{G}.)

It is left to prove c_{i}c_{j}x = c_{j}c_{i}x in (*1). For that we need x ≤ y ⇒ c_{i}x ≤ c_{i}y

and c_{i}c_{j}c_{i}x = c_{j}c_{i}x. c_{i}c_{j}c_{i}x =^{6} c_{i}c_{j}s_{[i/k]}c_{i}x =^{∗6} c_{i}s_{[i/k]}c_{j}c_{i}x =^{6} s_{[i/k]}c_{j}c_{i}x =^{∗6}

c_{j}s_{[i/k]}c_{i}x =^{6} c_{j}c_{i}x.

Now c_{i}c_{j}x ≤ c_{i}c_{j}c_{i}x = c_{j}c_{i}x and symmetrically c_{j}c_{i}x ≤ c_{i}c_{j}x giving c_{j}c_{i}x = c_{i}c_{j}x.

In the previous two subsections we distinguished the symbol τ from the transformation \underline{τ} denoted by it. This distinction is not necessary anymore since axioms (*3), (*4) of Definition 3.3 hold in all algebras studied hereafter. So we return to the original notation where τ denotes both the symbol and the corresponding transformation hoping that context will help.

3.3 Theorem 2.11: compressing the unit element

Proof of Theorem 2.11 (ii) IGwdf_{H}^{cm} = HCdf_{H} can be verified as follows. Suppose that A ∈ Gwdf_{H}^{cm}. Put V to be the unit element, A the universe of A. Since V is a compressed Gws_{ω}–unit, every weak space in V has the same base,

say U. Put B = {x ⊆ ^{ω}U : x ∩ V ∈ A}. Clearly, B =^{def} ⟨B, ∪, −, s_{τ} , c_{k}⟩_{τ∈H,k∈ω}

is in Cdf_{H} and the relativization of B with the set V is a homomorphism from B to A. This gives that A ∈ HCdf_{H}.

We need to show that IGwdf_{H}^{nm} = IGwdf_{H}^{cm}. The IGwdf_{H}^{nm} ⊇ IGwdf_{H}^{cm} part is obvious so it is left to check that IGwdf_{H}^{nm} ⊆ IGwdf_{H}^{cm}.

Let A be an algebra from Gwdf_{H}^{nm}. The unit element V of A is a normal Gws_{ω}–unit therefore it is a disjoint union of weak spaces. Denote the set of weak spaces building V by Λ. We put U to be the union of the bases of elements of Λ. We define an accessibility relation R on Λ as: for any λ_{1}, λ_{2} ∈ Λ

λ_{1}Rλ_{2} iff (∃q ∈ λ_{1})(∃σ ∈ H) q ∘ σ ∈ λ_{2}.

It follows that λ_{1}Rλ_{2} ⇒ base(λ_{1}) = base(λ_{2}). (Here we used that V is a normal Gws_{ω}–unit.) Let R^{∗} be the transitive, symmetric, reflexive closure of R. Clearly, R^{∗} is an equivalence relation. We have that λ_{1}R^{∗}λ_{2} ⇒ base(λ_{1}) = base(λ_{2}).

For each χ ∈ Λ/R^{∗} we put U_{χ} to be base(λ) for some λ ∈ χ, and we fix a function f_{χ} : U → U_{χ} that is the identity on U_{χ}. Now we can map the sequences of V into subsets of ^{ω}U in a following way. For any q ∈ λ ∈ χ ∈ Λ/R^{∗}

m(q) =^{def} {s ∈ ^{ω}U | f_{χ} ∘ s = q, s ≈ q}.

                                                                    cll1

Claim 3.19 The statements below hold. For all q, q′, s ∈ V

(i). m(q) and m(q′) are disjoint if q and q′ are distinct.

(ii). s ∈ m(q) ⇒ s[i/u] ∈ m(q[i/f_{χ}(u)]) if u ∈ U.

(iii). s ∈ m(q) ⇒ s ∘ σ ∈ m(q ∘ σ) if σ ∈ H.

Proof (i): Suppose that s ∈ m(q) ∩ m(q′). Then q ≈ s ≈ q′ so q and q′ are in the same weak space of V, say in λ. Since λ ∈ χ for some χ ∈ Λ/R^{∗} we infer that q = f_{χ} ∘ s = q′.

(ii): Suppose that s ∈ m(q), q ∈ λ ∈ χ ∈ Λ/R^{∗}. Since q ≈ q[i/f_{χ}(u)] we have q[i/f_{χ}(u)] ∈ λ ∈ χ. Now f_{χ} ∘ s[i/u] = q[i/f_{χ}(u)], s[i/u] ≈ s ≈ q ≈ q[i/f_{χ}(u)] shows that (ii) holds.

(iii): Suppose that s ∈ m(q), q ∈ λ ∈ χ ∈ Λ/R^{∗}. If λ′ is the weak space of q ∘ σ then λRλ′ and so λR^{∗}λ′, λ′ ∈ χ. We have s ≈ q, f_{χ} ∘ s = q and therefore f_{χ} ∘ s ∘ σ = q ∘ σ and s ∘ σ ≈ q ∘ σ (we used that σ is bounded).

We put V^{∗} = ⋃_{q∈V} m(q). (ii) of the previous claim shows that V^{∗} is a com-

pressed Cartesian space, (iii) gives that s_{σ}(V^{∗}) = V^{∗} whenever σ ∈ H.

                                                                    cll2

Claim 3.20 The statements below hold.

(i). {s ∈ V^{∗} | ∃u ∈ U s[i/u] ∈ m(q)} = ⋃_{q′∈c_{i}{q}} m(q′).

(ii). {s ∈ V^{∗} | s ∘ σ ∈ m(q)} = ⋃_{q′∈s_{σ}{q}} m(q′).

Proof (i): If s[i/u] ∈ m(q) then s = s[i/u][i/s(i)] ∈^{3.19(ii)} m(q[i/f_{χ}(s(i))]) ⊆

⋃_{q′∈c_{i}{q}} m(q′). On the other hand, if s ∈ m(q′) for some q′ ∈ c_{i}{q} then

s[i/q(i)] ∈^{3.19(ii)} m(q′[i/f_{χ}(q(i))]) = m(q) since f_{χ}(q(i)) = q(i), q′[i/q(i)] = q.

(ii): If s ∈ V^{∗}, s ∘ σ ∈ m(q) then s ∈ m(q′) for some q′ ∈ V. By Claim 3.19 (iii), s ∘ σ ∈ m(q ∘ σ). Claim 3.19 (i) implies m(q) ∩ m(q′ ∘ σ) ≠ ∅ ⇒ q′ ∘ σ = q.

So q′ ∈ s_{σ}{q}. On the other hand, if s ∈ m(q′) for some q′ ∈ s_{σ}{q} then s ∘ σ ∈ m(q′ ∘ σ) = m(q).

We arrived to the point when the algebra in which A is embeddable and the representation function rep can be defined:

A′ = \underline{P}(V^{∗}) ∈ Gwdf_{H}^{cm},
for any a ∈ A, rep(a) = ⋃_{q∈a} m(q).

Clearly, rep is a Boolean embedding of A into A′ since m(q) is not empty (q ∈ m(q)), and m(q) and m(q′) are disjoint when q and q′ are distinct (see Claim 3.19(i)).

To see that rep preserves the extra Boolean operations we compute:

c_{i}rep(a) = c_{i} ⋃_{q∈a} m(q) = ⋃_{q∈a} c_{i}m(q) =^{3.20(i)} ⋃_{q∈a} ⋃_{q′∈c_{i}{q}} m(q′) = ⋃_{q′∈c_{i}a} m(q′) =

rep(c_{i}a).

s_{σ}rep(a) = s_{σ} ⋃_{q∈a} m(q) = ⋃_{q∈a} s_{σ}m(q) =^{3.20(ii)} ⋃_{q∈a} ⋃_{q′∈s_{σ}{q}} m(q′) = ⋃_{q′∈s_{σ}a} m(q′) =

rep(s_{σ}a).

Before proving Theorem 2.11 (iii) we state an important result.

                                                                    l-qb

Lemma 3.21 Let H be a set of quasi-bounded transformations, A be a Gwdf_{H}, λ_{1} and λ_{2} be weak spaces of A. If (∃q ∈ λ_{1})(∃σ ∈ H) q∘σ ∈ λ_{2}, then base(λ_{1}) ⊆ base(λ_{2}).

Proof Suppose that u ∈ base(λ_{1}), q ∈ λ_{1}, σ ∈ H, |σ^{−1}(σ(k))| < ω (there is a proper k ∈ ω while σ is quasi-bounded), q ∘ σ ∈ λ_{2}. Since λ_{1} is a weak space, q[σ(k)/u] ∈ λ_{1}. But then {i ∈ ω | q[σ(k)/u] ∘ σ(i) ≠ q ∘ σ(i)} ⊆ σ^{−1}(σ(k)) is finite so q[σ(k)/u] ∘ σ ≈ q ∘ σ ∈ λ_{2}. The sequence q[σ(k)/u] ∘ σ of λ_{2} takes the value u at k so u ∈ base(λ_{2}).

Proof of Theorem 2.11 (iii) We need to show that under the conditions formulated in the theorem Gwdf_{H} ⊆ IGwdf_{H}^{nm}.

Let A be an algebra from Gwdf_{H}. As we did in the proof of (ii) we put V to be the unit element of A, Λ to be the set of weak spaces of A, R to be the accessibility relation on Λ, R^{∗} to be the equivalence relation generated by R.

We show that λRλ_{0} ⇒ base(λ) = base(λ_{0}) (and so λR^{∗}λ_{0} ⇒ base(λ) = base(λ_{0})). Suppose that λRλ_{0}. Then (∃q ∈ λ)(∃σ_{0} ∈ H) q ∘ σ_{0} ∈ λ_{0}. We know that σ_{0} has a quasi-inverse in [H], say σ_{1} ∘ … ∘ σ_{n}. For any i ∈ n + 1 we put λ_{i} to be the weak space of q ∘ σ_{0} ∘ … ∘ σ_{i}. Lemma 3.21 implies that base(λ_{i}) ⊆ base(λ_{i+1}) (i ∈ n). If we note that σ_{0}∘σ_{1}∘…∘σ_{n} ≈ Id, and so λ = λ_{n} then we have base(λ) ⊆ base(λ_{0}) ⊆ base(λ_{1}) ⊆ … ⊆ base(λ_{n}) = base(λ).

Now we can define the set U_{χ} to be base(λ) for some λ ∈ χ ∈ Λ/R^{∗}. Surely, the definition is independent from the choice of λ. We put f_{χ} : U_{χ} → U_{χ} × {χ} to be the natural embedding (f_{χ}(u) = ⟨u, χ⟩), and χ : V → Λ/R^{∗} to be the function that associates the R^{∗} class of the weak space of q to a q ∈ V. We define

for any a ∈ A, rep(a) = {f_{χ(q)} ∘ q | q ∈ a}
A′ = {rep(a) | a ∈ A}
A′ = ⟨A′, ∪, −, s_{τ} , c_{k}⟩_{τ∈H,k∈ω}

It is straightforward to verify that A′ ∈ Gwdf_{H}^{nm} and rep is an isomorphism between A and A′.

3.4 Quasi-axiomatizing ICdf_{H}

To find a proof to Theorem 2.15, we examine the situation described in Example 2.13. The key idea is that the presence of a constant sequence can be captured by a quasi-equation. Among those Gwdf_{G}’s that have constant sequences in their universes, the simplest in structure are the ones with unit elements of the form ^{ω}U^{(q)} for some set U and constant sequence q. A unit element of this form will be called horizontal. (It is easy to see that s_{τ} (^{ω}U^{(q)}) = ^{ω}U^{(q)}.)

Any algebra from Gwdf_{H} that has a constant sequence q in it’s universe can be homomorphically mapped into a Gwdf_{H} with horizontal unit element. (Indeed, the relativization with ^{ω}U^{(q)} — the function that maps the element x of the algebra into x ∩^{ω}U^{(q)} — will be a satisfactory homomorphism.) So any Gwdf_{H} that is isomorphic to a Cdf_{H} has a homomorphism into some Gwdf_{H} with horizontal unit element. The next theorem states that this requirement is not only necessary but also sufficient to force a Gwdf_{H} to be isomorphic to a H–cylindric set algebra.

                                                                    th-csg

Theorem 3.22 Let H be an arbitrary subset of ^{ω}ω with the property that for any σ ∈ H, σ is bounded and has a right quasi-inverse in ^{ω}ω. Then any algebra A ∈ Gwdf_{H}, that has a homomorphism into some Gwdf_{H} with horizontal unit element, is isomorphic to a H–cylindric set algebra. That is,

(∃ set U)(∃u_{0} ∈ U)(∃h : A → \underline{P}(^{ω}U^{(⟨u_{0},u_{0},...⟩)})) ⇒ A ∈ ICdf_{H}.

Before the proof of the Theorem above we present an important lemma.

                                                                    lm-d->s

Lemma 3.23 Suppose U is a set, u_{0} ∈ U. There is a cardinal κ for that if \underline{P}(W′) is a full compressed H–cylindric set algebra with base U′ of cardinality bigger than κ then there is a homomorphism h′ : \underline{P}(^{ω}U^{(⟨u_{0},u_{0},...⟩)}) → \underline{P}(W′).

Proof Let κ be a cardinal bigger than ω, the cardinality of U and that of H.

For the algebra \underline{P}(W′), we define the set Λ of weak spaces, the accessibility relations R and R^{∗} on Λ as we defined in the proof of Theorem 2.11 (ii). For each weak space λ ∈ Λ we fix a sequence q_{λ} in λ. We put U′_{χ} (χ ∈ Λ/R^{∗}) to be the set {q_{λ}(i) | λ ∈ χ, i ∈ ω}.

                                                                    cl-card

Claim 3.24 The cardinality of |U′_{χ}| + |U| is less than κ.

Proof For a given λ_{1} ∈ Λ and σ ∈ H there is exactly one λ_{2} ∈ Λ with λ_{1}Rλ_{2}. This can verified by noting that from q ∘ σ ∈ λ_{2}, q ∈ λ_{1} we can infer q′ ∘ σ ∈ λ_{2} when q′ ∈ λ_{1} (σ is bounded so q ≈ q′ ⇒ q ∘ σ ≈ q′ ∘ σ and q ∘ σ ∈ λ_{2} ∩ λ′_{2} ⇒ λ_{2} = λ′_{2}).

For any σ ∈ H, σ is right quasi-invertible in ^{ω}ω so there is a transformation f_{σ} ∈ ^{ω}ω with σ ∘ f_{σ} ≈ Id. Suppose for contradiction that there is a k ∈ ω for that |f_{σ}^{−1}(k)| = ω. Then the transformation σ ∘ f_{σ} takes the value σ(k) on any coordinate of the infinite set f_{σ}^{−1}(k). But this is impossible since σ ∘ f_{σ} takes the value i on coordinate i for all but finitely many i ∈ ω. This reasoning shows that f_{σ} is bounded.

For a given λ_{2} ∈ Λ and σ ∈ H there is exactly one λ_{1} ∈ Λ with λ_{1}Rλ_{2}. Suppose that λ_{1}, λ′_{1} ∈ Λ, q ∈ λ_{1}, q′ ∈ λ′_{1} and q ∘ σ ∈ λ_{2} ∋ q′ ∘ σ. Then q ∘ σ ≈ q′ ∘ σ and q ∘ σ ∘ f_{σ} ≈ q′ ∘ σ ∘ f_{σ} since f_{σ} is bounded. But this implies that q ≈ q ∘ σ ∘ f_{σ} ≈ q′ ∘ σ ∘ f_{σ} ≈ q′, q ∈ λ_{1} ∩ λ′_{1} so λ_{1} = λ′_{1}.

For a given λ ∈ Λ, |{λ′ ∈ Λ | λRλ′ or λ′Rλ}| ≤ 2 · |H|. For a given λ ∈ Λ, we have that λ′ ∈ Λ and λ sit in the same R^{∗} class if and only if there is a finite series λ_{0}, … λ_{n} of weak spaces with λ_{0} = λ, λ_{n} = λ′ and i ∈ n ⇒ (λ_{i}Rλ_{i+1} or λ_{i+1}Rλ_{i}). Therefore, the size of a R^{∗} class is less than 1 + 2 · |H| + (2 · |H|)^{2} + … ≤ ω · |H|. Finally, |U′_{χ}| ≤ ω · |χ| ≤ ω · ω · |H| = ω · |H|, |U′_{χ}| + |U| < κ.

Let f_{χ} (χ ∈ Λ/R^{∗}) be any function mapping U′ onto U with the property

(∀i ∈ ω)(∀λ ∈ χ) f_{χ}(q_{λ}(i)) = u_{0}.

Such an f_{χ} exists since not more than |U′_{χ}|-many elements of U′ are to be mapped on u_{0} so there are enough elements left to cover the set U − {u_{0}}.

With the help of f_{χ}, for each sequence q of ^{ω}U^{(⟨u_{0},u_{0},...⟩)} a subset of W′ can be associated.

m(q) = {s ∈ W′ | f_{χ} ∘ s = q, s ∈ λ ∈ χ ∈ Λ/R^{∗}}.

As it was presented in the more complicated situation in the proof of Theorem 2.11 (ii) the function h′(a) = ⋃_{q∈a} m(q) is a homomorphism. (Claims 3.19 and

3.20 hold here as well since the original proofs can be adapted to the present situation. )

Proof of Theorem 3.22 In Theorem 2.11 (ii) and (iii) IGwdf_{H} = IGwdf_{H}^{cm} was proved under the conditions that for any σ ∈ H, σ is quasi-bounded and it has a quasi-inverse in [H]. This holds in our situation so we may assume that A ∈ Gwdf_{H}^{cm}. The unit element of A is V ⊆ ^{ω}U^{∗} for some set U^{∗}. Let U′ be a set with cardinality bigger than the cardinality of U^{∗} and the cardinal that corresponds to the set U according to Lemma 3.23.

Let f be a function mapping U′ onto U^{∗}. With the help of f, for each sequence q of ^{ω}U^{∗} a subset of ^{ω}U′ can be associated.

m(q) = {s ∈ ^{ω}U′ | f ∘ s = q}.

Let V′ = ⋃_{q∈V} m(q). As it was presented in the proof of Theorem 2.11 (ii) the

function r_{1} : A → \underline{P}(V′), r_{1}(a) = ⋃_{q∈a} m(q) is an embedding.

Let W′ = ^{ω}U′ \ V′. Just like V′, W′ is a Gws_{ω}–unit and s_{σ}(W′) = W′ for any σ ∈ H. So W′ can be a unit element of a Gwdf_{H}^{cm}. According to Lemma 3.23 there is a homomorphism h′ mapping \underline{P}(^{ω}U^{(⟨u_{0},u_{0},...⟩)}) into \underline{P}(W′). Let r_{2} be the composition of the homomorphisms h′ and h (r_{2} = h′ ∘ h) mapping A into \underline{P}(W′). Since \underline{P}(^{ω}U′) = \underline{P}(V′) × \underline{P}(W′) the function rep defined as rep(a) = r_{1}(a) ∪ r_{2}(a) is an embedding and it demonstrates that A ∈ ICdf_{H}.

In the second part of this subsection we show that if an algebra in Gwdf_{H} satisfies Qx then it has a homomorphism to Gwdf_{H} with horizontal unit element. We assume that H satisfies the assumption stated in Theorem 2.19.

                                                                    ll1

Lemma 3.25 If A ∈ Gwdf_{H} and A ⊧ Qx then there is an ultrafilter U of A with the property that −c_{(Γ)}x ∈ U holds whenever x ∩ s_{τ} x = 0 for some Γ ⊆_{ω} ω τ ∈ [H] with τ⌈Γ = Id⌈Γ.

                                                                    clll1

Claim 3.26 ∀σ, τ_{1}, …, τ_{n} ∈ [H] ∃σ′, τ′_{1}, …, τ′_{n} ∈ [H] : ⋀_{i≤n} σ′ ∘ τ_{i} = τ′_{i} ∘ σ.

Furthermore, if σ⌈Γ = τ_{1}⌈Γ = ⋯ = τ_{n}⌈Γ = Id⌈Γ then the same holds to σ′, τ′_{1}, …, τ′_{n} (Γ ⊆_{ω} ω).

Proof We prove by induction. If n = 0 then σ′ = σ. Suppose that the statement holds for n − 1. Let σ′′, τ′′_{1}, …, τ′′_{n−1} be associated to σ, τ_{1}, …, τ_{n−1}. Let σ^{∗} and τ_{n}^{∗} be the left quasi-inverse of σ′′ ∘ τ_{n} and σ respectively. Since [H] contains all finite transformations we can assume that σ^{∗} ∘ σ′′ ∘ τ_{n}(k) =

\{ \begin{matrix}k & ∈ Γ \\ 0 & k ∈ m_{0} − Γ \\ k & m_{0} ≤ k \end{matrix} \} = τ′_{n} ∘ σ(k) for some m_{0} ∈ ω. Setting σ′ = σ^{∗} ∘ σ′′,

τ′_{i} = σ^{∗} ∘ τ′′_{i} (i = 1, …, n) gives the required result.

Proof of Lemma 3.25 Let B^{∗} = {−c_{(Γ)}x : Γ ⊆_{ω} ω, ∃K ⊆_{ω} [H] (τ ∈ K → τ⌈Γ = Id⌈Γ), ⋂_{τ∈K} s_{τ} x = 0}. Qx states that B^{∗} has the finite intersection

property. We put B to be B^{∗}’s filter closure, that is, B = {y ∈ A : ∃X ⊆_{ω} B^{∗} y ≥ ⋂ X}.

                                                                    clll2

Claim 3.27 B is closed under s_{ν} for all ν ∈ [H].

Proof Suppose −c_{(Γ)}x ∈ B^{∗}, ⋂_{τ∈K} s_{τ} x = 0 for some Γ ⊆_{ω} ω, K ⊆_{ω} [H],

τ ∈ K → τ⌈Γ = Id⌈Γ. Let Γ′ = {i ∈ ω − Γ : ν(i) ∈ Γ, ∀j ∈ i − Γ (ν(i) ≠ ν(j))}. ν is bounded so Γ′ is finite. If Γ′ = {γ_{1}, …, γ_{n}} then let ν_{0} = [γ_{1}, ν(γ_{1})] ∘ … ∘ [γ_{n}, ν(γ_{n})]. Let Γ′′ = Γ′∪(Γ−{ν(γ) : γ ∈ Γ′}), ν_{1} = (ν_{0}∘ν)[Γ/Id]. Now we have that ν_{0} ∘ ν_{1}⌈ω − Γ = ν⌈ω − Γ and for all i ∈ Γ ν_{1}^{−1}(i) = {i}. Using Claim 3.26, we pick corresponding transformations ν′_{1} and τ′ to ν and τ (τ ∈ K). Then 0 =

s_{ν_{0}}s_{ν′_{1}} ⋂_{τ∈K} s_{τ} x = ⋂_{τ∈K} s_{ν_{0}}s_{ν′_{1}}s_{τ} x = ⋂_{τ∈K} s_{ν_{0}}s_{τ′}s_{ν_{1}}x = ⋂_{τ∈K} s_{ν_{0}∘τ′∘ν_{0}}s_{ν_{0}}s_{ν_{1}}x. Not-

ing that ν_{0}∘τ′∘ν_{0}⌈Γ′′ = Id⌈Γ′′ we have −c_{(Γ′′)}s_{ν_{0}}s_{ν_{1}}x ∈ B^{∗}. So −c_{(Γ′′)}s_{ν_{0}}s_{ν_{1}}x =^{∗6}

−s_{ν_{0}}c_{(Γ)}s_{ν_{1}}x =^{∗6} −s_{ν_{0}}s_{ν_{1}}c_{(Γ)}x =^{∗5} −s_{ν}c_{(Γ)}x = s_{ν}(−c_{(Γ)}x) gives s_{ν}(−c_{(Γ)}x) ∈ B^{∗}.

Finally, suppose that x ∈ B. Then there are x_{1}, …, x_{n} ∈ B^{∗} with x ≥ ⋂_{1}^{n} x_{i}.

So s_{ν}x ≥ s_{ν} ⋂_{1}^{n} x_{i} = ⋂_{1}^{n} s_{ν}x_{i} ∈ B giving s_{ν}x ∈ B.

Let U be a maximal filter extending B with the property that it is closed under s_{ν} for all ν ∈ [H]. We can use Zorn’s lemma to construct such a filter. We show that U is indeed an ultrafilter. Suppose not. Then there is a y such that neither y nor −y is in U. y cannot be added to U so there are z ∈ U, K ⊆_{ω} [H] such that z ∩ ⋂_{τ∈K} s_{τ} y = 0. Then 0 = z ∩ ⋂_{τ∈K} s_{τ} y ⊇ ⋂_{τ∈K} s_{τ} (z ∩ y) giving

−(y ∩z) ∈ B. Similarly, −(−y ∩z′) ∈ B. Therefore U ∋ −(−y ∩z′)∩−(y ∩z) = −((y ∪ z′) ∩ (z ∪ z′) ∩ (z ∪ −y)). But all the three terms in the last expression are in U so their intersection is in U giving that U contains an element and its complement.

Our algebra A ∈ Gwdf_{H} is a normal Boolean algebra with operators. (Cf. e.g. [HMTI] Definition 2.7.1.) We can define its canonical embedding algebra or ultrafilter extension A^{∗} as follows (see Definition 2.7.4. in [HMTI]). Let V be the set of ultrafilters of A. If O is any of the operators {s_{τ} : τ ∈ H}∪{c_{i} : i ∈ ω} and X ⊆ V then we define

OX = {U ∈ V : (∃S ∈ X)(∀x ∈ U) Ox ∈ S}.

Then A^{∗} is ⟨P(V), ∪, −, s_{τ} , c_{i}⟩_{τ∈H,i∈ω}.

As stated in Corollary 3.5, IGwdf_{H}^{nm} is axiomatized by (*1)–(*7) (defined in Definition 3.3) together with the definition of c_{i} (i ∈ ω). All that axioms but c_{i}(−c_{i}x) = −c_{i}x and s_{σ}(−x) = −s_{σ}x are positive, that is, they do not contain any occurance of the symbol − for complementation. But the two exceptions are equivalent (in the presence of the others) with some positive formulas:

c_{i}(−c_{i}x) = −c_{i}x iff c_{i}0 = 0, c_{i}(x ∧ c_{i}y) = c_{i}x ∧ c_{i}y
s_{σ}(−x) = −s_{σ}x iff s_{σ}(x ∧ y) = s_{σ}x ∧ s_{σ}y.

Since positive equations valid in a Boolean algebra with operators still hold in the ultrafilter extension of the algebra, (see e.g. [HMTI] Remark 2.7.15) we can conclude that the ultrafilter extension A^{∗} of A ∈ Gwdf_{H}^{nm} is in Gwdf_{H}^{nm}. Furthermore, under the hypothesis of Theorem 2.19, IGwdf_{H} = IGwdf_{H}^{nm} holds, so the conclusion stated above holds to the class Gwdf_{H} as well.

Finally, we note that every Boolean algebra with operators is embeddable into its ultrafilter extension. (The map that associates {U ∈ V : x ∈ U} to an element x in A will suffice.)

                                                                    ll2

Lemma 3.28 If A ∈ Gwdf_{H} and A^{∗} is its ultrafilter extension then the atom a = {U} has the property x∩c_{(Γ)}a ⊆ s_{τ} x (Γ ⊆_{ω} ω, τ ∈ [H], τ⌈Γ = Id⌈Γ, x ∈ A^{∗}) provided that U is an ultrafilter of A that satisfies the property stated in Lemma 3.25.

Proof It is enough to show that the condition x ∩ c_{(Γ)}a ⊆ s_{τ} x holds for all atoms of A^{∗}. Suppose x = {F }. If F ∉ c_{(Γ)}a then there is nothing to show. If F ∈ c_{(Γ)}a then ∀y ∈ F c_{(Γ)}y ∈ U. Suppose for contradiction that x ⊈ s_{τ} x, that is, ∃y ∈ F s_{τ} y ∉ F. Then −s_{τ} y ∈ F, w = y ∩ −s_{τ} y ∈ F. We can conclude that c_{(Γ)}w ∈ U. On the other hand, w ∩ s_{τ} w = 0 gives −c_{(Γ)}w ∈ U and that is a contradiction.

                                                                    ll3

Lemma 3.29 If A^{∗} ∈ Gwdf_{H}^{cm} and A^{∗} has an atom a with x ∩ c_{(Γ)}a ⊆ s_{τ} x whenever Γ ⊆_{ω} ω, τ ∈ [H], τ⌈Γ = Id⌈Γ, x ∈ A^{∗} then A^{∗} has a homomorphism to a Gwdf_{H} with horizontal unit element.

Proof We denote the base of A^{∗} by U′ and the universe of A^{∗} by A^{∗}. Let q be a sequence in a, V = {q ∘ τ : τ ∈ [H]}, V^{∗} = ⋃_{m∈ω} c_{(m)}V. Put U_{0} to be the

range of q. Fix an arbitrary element u ∈ U_{0}. Denote U′ − U_{0} ∪ {u} by U. Let f be the function that is the identity on U′ − U_{0} and the constant u on U_{0}.

                                                                    clll3

Claim 3.30 x ∈ A^{∗}, s, s′ ∈ V^{∗}, s ∈ x, f ∘ s = f ∘ s′ → s′ ∈ x.

Proof Let Γ = {i ∈ ω : s(i) ∉ U_{0}}. Since s ≈ q ∘ τ for some τ ∈ [H], Γ is finite. Clearly, Γ = {i ∈ ω : s′(i) ∉ U_{0}} so s⌈Γ = s′⌈Γ. We have that s′ ≈ q∘τ′ for some τ′ ∈ [H]. s = q ∘τ[Γ/s], s′ = q ∘τ′[Γ/s]. Let ν and ν′ be the right quasi-inverses of τ and τ′. Since all the finite transformations are in [H], we can choose ν and ν′ that they satisfy the following additional properties: ν⌈Γ = ν′⌈Γ = Id⌈Γ, τ ∘ ν⌈ω − Γ = τ′ ∘ ν′⌈ω − Γ. Then s ∘ ν = (q ∘ τ[Γ/s]) ∘ ν = q ∘ τ ∘ ν[Γ/s] = q ∘ τ′ ∘ ν′[Γ/s] = (q ∘ τ′[Γ/s]) ∘ ν′ = s′ ∘ ν′. Since s ∈ x ∩ c_{(Γ)}a ⊆ s_{ν}x, we get that s′ ∘ ν′ = s ∘ ν ∈ x. (We used that a ⊆ s_{τ} a and so q ∘ τ ∈ a.) If we suppose for contradiction that s′ ∉ x then s′ ∈ −x ∩ c_{(Γ)}a ⊆ s_{ν′} − x and so s′ ∘ ν′ ∈ −x but that cannot be the case.

Now we can define a homomorphism that maps A into \underline{P}(^{ω}U^{(⟨u,u,...⟩)}):

h(x) = {f ∘ s : s ∈ x ∩ V^{∗}}.

It is straightforward to verify that h preserves ∩, while Claim 3.30 proves that it preserves complementation. The following two claims prove that h preserves the extra Boolean operations.

                                                                    clll4

Claim 3.31 c_{i}h(x) = h(c_{i}x).

Proof r ∈ c_{i}h(x) ⇒ r = (f ∘ s)[i/r(i)] for some s ∈ x. But r = (f ∘ s)[i/r(i)] = f ∘ (s[i/r(i)]) ∈ h(c_{i}x) since s[i/r(i)] ∈ c_{i}x.

On the other hand, r ∈ h(c_{i}x) ⇒ r = f ∘s for some s ∈ c_{i}x. So there is s′ ∈ x with s′[i/s(i)] = s. But r = f ∘ s = f ∘ (s′[i/s(i)]) = (f ∘ s′)[i/f(s(i))]) ∈ c_{i}h(x)

                                                                    clll5

Claim 3.32 s_{τ} h(x) = h(s_{τ} x).

Proof r ∈ s_{τ} h(x) ⇔ r ∘ τ ∈ h(x) ⇔ ∃s′ ∈ x f ∘ s′ = r ∘ τ. r = f ∘ s for some s ∈ V^{∗} so f ∘ s′ = r ∘ τ = f ∘ s ∘ τ. Using Claim 3.30 we have that s′ ∈ x ⇔ s ∘ τ ∈ x. But s ∘ τ ∈ x ⇔ s ∈ s_{τ} x ⇔ r = f ∘ s ∈ h(s_{τ} x) completes the proof.

Summarizing the results of this subsection, we prove Theorem 2.19. Proof of Theorem 2.19 Suppose that the algebra A is a model of Qx ∪ Eq(IGwdf_{H}). Lemmas 3.25 and 3.28 state that the ultrafilter extension A^{∗} of A has an atom with certain properties. Since the ultrafilter extension satisfies all the positive equations valid in the algebra, we have that A^{∗} ⊧ Eq(IGwdf_{H}). Using Theorem 2.11 we conclude that A^{∗} is isomorphic to an algebra B ∈ Gwdf_{H}^{cm}. Lemma 3.29 implies that B has a homomorphism to a Gwdf_{H} with horizontal unit element. Since A is embeddable into its ultrafilter extension and, in that way, into B, A also has a homomorphism to a Gwdf_{H} with horizontal unit element.

Finally, Theorem 3.22 states that the above mentioned result is sufficient to show that A ∈ ICdf_{H}.

3.5 Theorem 2.30: the cylindric reduct of Mod(H1, H2)

The proof will have the following structure. Any model of H1 is actually an extension of a model of EqGwdf nm ; H̄. But Theorem 2.11 (i) imply that a model of EqGwdf nm ; H̄ is isomorphic to a Gwdf nm ; H̄ We will examine the extra abstract constant d_{01}. (In the presence of the substitutions the other d_{ij}’s are term definable so it is enough to concentrate on d_{01}.) Finally, the proper behaviour of d_{01} will lead us to a representation function that proves our theorem.

Recall from Notation 2.8 that if q_{1} are q_{2} sequences then q_{1} ≈ q_{2} indicates that they agree on all but finitely many coordinates.

                                                                    nt-stau

Notation 3.33 Let H be a set of transformations of ω. Suppose that τ = ⟨σ_{1} … σ_{n}⟩ ∈ H^{∗}. We introduce the notation s_{τ} x for the term s_{σ_{1}} … s_{σ_{n}}x.

                                                                    rm-H4

Remark 3.34 Let H be a set of transformations of ω with the property that [H̄] is rich. (Recall that [H̄] is the subsemigroup of ⟨^{ω}ω, ∘⟩ generated by H ∪ {[i/j] | i, j ∈ ω}.)

In the definition of a rich semigroup the existence of two special elements ŝ and p̂ were stated. We fix two elements of [H̄] with the required property and denote them by ŝ and p̂. We also fix sŝ and sp̂ to stand for the terms s_{τ_{1}} and s_{τ_{2}} respectively where τ_{1} = ŝ, τ_{2} = p̂, and τ_{1}, τ_{2} ∈ H̄^{∗}. It is provable from H1 that for any choice of τ_{1} ∈ H̄^{∗} with τ_{1} = ŝ, s_{τ_{1}} is the same operation of the algebra so sŝ (and similarly sp̂) is well defined.

ŝ(i) ≠ ŝ(j) if i ≠ j since p̂∘ ŝ = Id. There is a permutation f of ω that takes ŝ(0) to 0 and ŝ(1) to 1 and fixes all the elements of ω − {0, 1, ŝ(0), ŝ(1)}. (f is one of [0, ŝ(0)] ∘ [1, ŝ(1)], [1, ŝ(1)] ∘ [0, ŝ(0)] or [0, 1] depending on whether any of ŝ(0) = 0, ŝ(0) = 1, ŝ(1) = 0 or ŝ(1) = 1 hold.) Since f is finite f ∈ [H̄]. So there is a τ_{H} ∈ H̄^{∗} for that τ_{H} = f.

We formalize a set of equations that are all consequences of H1,H2.

s_{[0/1]}x = c_{0}(d_{01} ∧ x),
s_{[1/0]}x = c_{1}(d_{01} ∧ x),
c_{i}d_{01} = d_{01} whenever i ≥ 2,
s_{[0,1]}d_{01} = d_{01},
s_{τ_{H}} sŝd_{01} = d_{01}.

(H4)

Here s_{[i,j]}x stands for the term s_{τ} x where τ ∈ H̄^{∗} and τ = [i, j]. Since [H̄] is rich, all the finite transformations (including [i, j]) belong to [H̄].

                                                                    lm-2

Lemma 3.35 Let H be a set of transformations of ω with the property that [H̄] is rich. Suppose that A is a GwdfH̄ extended with the abstract^{18} constant d_{01} that satisfies H4. If x is an element of A and ⟨u_{0}, u_{1}, u_{2}, …⟩ is a sequence from

18Here the adjective “abstract” means that this constant is NOT necessarily the set theoretically definable diagonal element, but any constant that satisfies the required equations. It will be shown that this “abstract” constant need to have a nice structure similar to that of the set theoretic diagonal element.

the universe of A then ⟨u_{0}, u_{1}, u_{2}, …⟩ ∈ d_{01}∧x implies \begin{aligned}⟨u_{0}, u_{0}, u_{2}, …⟩ & ∈ & x, \\ ⟨u_{1}, u_{0}, u_{2}, …⟩ & ∈ & x, \\ ⟨u_{1}, u_{1}, u_{2}, …⟩ & ∈ & x. \end{aligned}

Proof Suppose that ⟨u_{0}, u_{1}, u_{2}, …⟩ satisfies the premise of the lemma. Then

⟨u_{0}, u_{1}, u_{2}, …⟩ ∈ c_{0}(d_{01} ∧ x) =^{H4} s_{[0/1]}x. This implies ⟨u_{0}, u_{1}, u_{2}, …⟩ ∘ [0/1] =

⟨u_{1}, u_{1}, u_{2}, …⟩ ∈ x.

Using s_{[1/0]}x =^{H4} c_{1}(d_{01} ∧ x) we can get ⟨u_{0}, u_{0}, u_{2}, …⟩ ∈ x.

s_{[0,1]}d_{01} =^{H4} d_{01} implies ⟨u_{1}, u_{0}, u_{2}, …⟩ ∈ d_{01}. If we suppose for contradiction that ⟨u_{1}, u_{0}, u_{2}, …⟩ ∉ x then ⟨u_{1}, u_{0}, u_{2}, …⟩ ∈ −x and according to the previous observation we can conclude that ⟨u_{1}, u_{1}, u_{2}, …⟩ ∈ −x and that is impossible.

                                                                    lm-3

Lemma 3.36 Let H, A and d_{01} be as in Lemma 3.35. If u and v are the first two elements of a sequence q of d_{01} then any sequence r of an arbitrary x ∈ A can be modified in any of its positions from u to v provided that q and r are in the same weak space. In other words, if q ∈ d_{01}, r ∈ x for some x ∈ A, q ≈ r, r(k) = q(0) = u for some k ∈ ω and q(1) = v then r[k/v] ∈ x.

Proof First suppose that k ≠ 1. Let q^{∗} = (r ∘ [0, k])[1/v]. Clearly, q^{∗} is in the weak space of q (and of r). Therefore, q^{∗} ∈ c_{i_{1}} … c_{i_{n}}d_{01} where Γ = {i_{1}, … i_{n}} is the set where q and q^{∗} do not agree (it is finite). Now q^{∗}(0) = (r ∘ [0, k])(0) = r(k) = u and q^{∗}(1) = v so 0, 1 ∉ Γ and c_{i}d_{01} =^{H4} d_{01} whenever i ≥ 2. We can conclude that q^{∗} ∈ d_{01}.

We put z to be an element of ω − Rng(ŝ). [H̄] is rich so ω − Rng(ŝ) is not empty. (q^{∗} ∘ p̂)[z/r(1)] ∘ ŝ = q^{∗} ∈ d_{01} implies that (q^{∗} ∘ p̂)[z/r(1)] ∈ sŝd_{01}. (q^{∗} ∘ p̂)[z/v][ŝ(1)/r(1)] ∘ ŝ = r ∘ [0, k] ∈ s_{[0,k]}x, (q^{∗} ∘ p̂)[z/v][ŝ(1)/r(1)] ∈ sŝs_{[0,k]}x.

Furthermore, (q^{∗} ∘ p̂)[z/r(1)] = (q^{∗} ∘ p̂)[z/v][ŝ(1)/r(1)] ∘ [z, ŝ(1)]. We put r^{∗} =^{def} (q^{∗} ∘ p̂)[z/r(1)] ∘ τ_{H}^{−1}.

Summarizing all the results we get that r^{∗} ∈ s_{τ_{H}} sŝd_{01} =^{H4} d_{01} and r^{∗} ∈ s_{τ_{H}} s_{[z,ŝ(1)]}sŝs_{[0,k]}x, r^{∗}(0) = q^{∗}(0) = u, r^{∗}(1) = q^{∗}(1) = v. Using Lemma 3.35 we conclude that r^{∗}[0/v] ∈ s_{τ_{H}} s_{[z,ŝ(1)]}sŝs_{[0,k]}x. This means that r^{∗}[0/v] ∘ τ_{H} ∘ [z, ŝ(1)] ∘ ŝ∘ [0, k] ∈ x. Then r^{∗}[0/v] ∘ τ_{H} ∘ [z, ŝ(1)] ∘ ŝ∘ [0, k] = ((q^{∗} ∘ p̂)[z/r(1)] ∘ τ_{H}^{−1} ∘ τ_{H})[ŝ(0)/v] ∘ [z, ŝ(1)] ∘ ŝ ∘ [0, k] = (q^{∗} ∘ p̂∘ [z, ŝ(1)])[ŝ(1)/r(1)][ŝ(0)/v] ∘ ŝ ∘ [0, k] = (q^{∗} ∘ p̂ ∘ ŝ)[1/r(1)][0/v] ∘ [0, k] = ((r ∘ [0, k])[1/v][1/r(1)] ∘ [0, k])[k/v] = (r ∘ [0, k] ∘ [0, k])[k/v] = r[k/v] ∈ x.

If k = 1 then r ∈ x ⇒ r ∘ [1, 2] ∈ s_{[1,2]}x ⇒ (r ∘ [1, 2])[2/v] ∈ s_{[1,2]}x ⇒ (r ∘ [1, 2])[2/v] ∘ [1, 2] = r[1/v] ∈ x.

Proof of Theorem 2.27 (1) Surely, any representable cylindric set algebra is a subalgebra of a reduct of a model of H1,H2.

To see the other direction, suppose that A′ is a model of H1,H2. A′ ⊧ H1 means that all the valid equations of Gwdf nm ; H̄ hold in A′. Naturally, some operations of tH̄ are term functions in Gws_{H}. Since IGwdf nm ; H̄ is a variety, the tH̄–reduct of A′ is isomorphic to a Gwdf nm ; H̄, say to A. We will use only that A ∈ IGwdfH̄. The image of d_{01} under the isomorphism is an element of A not necessary the set theoretic (0,1)–diagonal. The image of any other diagonal constant can be computed from the image of d_{01} since d_{ij} is term definable from d_{01} in GwdfH̄. This shows that to represent A′, it is enough to represent A that is to find a isomorphism rep mapping the cylindric reduct of A into a RCA_{ω}.

The universe V of A is a Gws_{ω}–unit therefore it is a (disjoint) union of weak spaces. Denote the set of weak spaces building A by Λ. For any weak space λ from Λ, base(λ) is the base set of λ. d_{01} defines an equivalence relation on base(λ) in a following way: for any u, u′ ∈ base(λ)

u ∼_{λ} u′ iff (∃q ∈ d_{01} ∩ λ) q(0) = u, q(1) = u′

                                                                    cl-1

Claim 3.37 ∼_{λ} is reflexive.

Proof Suppose u ∈ base(λ). Let ⟨u_{0}, u_{1}, u_{2}, …⟩ ∈ λ arbitrary. It is obvious that ⟨u, u, u_{2}, …⟩ ∈ λ. Now ⟨u, u, u_{2}, …⟩ ∈ V = c_{1}d_{01}. So (∃v ∈ base(λ)) ⟨u, v, u_{2}, …⟩ ∈ d_{01}. Applying Lemma 3.35 to the case when x = d_{01} it gives that ⟨u, u, u_{2}, …⟩ ∈ d_{01}

                                                                    cl-2

Claim 3.38 ∼_{λ} is symmetric.

Proof Follows from Lemma 3.35 when applied to the case x = d_{01}.

                                                                    cl-3

Claim 3.39 ∼_{λ} is transitive.

Proof Follows from Lemma 3.36 when applied to the case x = d_{01}, k = 0.

Our aim is to embed the cylindric reduct of the not fully represented algebra A into a Gws_{ω}. For saving energy and not losing what we have already achieved, we are looking for a representation function rep that acts not only on the algebra level but deeper, on the sequence level hiding in the elements of A. In other words,

rep(x) = {f(q) | q ∈ x}

where f if the sequence level function mapping V into the universe V^{∗} of some algebra A^{∗}. To ensure that f(d_{01}) is the set theoretic constant we want for any q, q′ ∈ λ ∈ Λ that (∀i ∈ ω) q(i) ∼_{λ} q′(i) should imply f(q) = f(q′). This observation gives us a hint for an adequate definition of f.

For every λ ∈ Λ, we define U_{λ} to be the set (base(λ)/∼_{λ}) × {λ}. U_{λ} corresponds to the ∼_{λ} classes of base(λ). Clearly, if λ and λ′ are distinct then U_{λ} and U_{λ′} are disjoint. For every q ∈ λ, we define

f(q) = ⟨⟨q(0)/∼_{λ}, λ⟩, ⟨q(1)/∼_{λ}, λ⟩, ⟨q(2)/∼_{λ}, λ⟩, …⟩

The f image of a λ ∈ Λ is also a weak space in ^{ω}U_{λ}. Let it be denoted by λ^{∗}. Now we can define the image algebra A^{∗} ∈ Gws_{ω}:

V^{∗} = ⋃_{λ∈Λ} λ^{∗},
A^{∗} = {rep(x) | x ∈ A},
A^{∗} = ⟨A^{∗}, ∩, −, c_{i}, d_{ij}⟩.

One can easily verify that the above defined rep is an isomorphism between the cylindric reduct of A and a generalised weak cylindric set algebra. Finally, the result IGws_{ω} ⊆ IGs_{ω} = RCA_{ω} published in [HMTII] Theorem 3.1.103. completes the proof.

3.6 Further observations on Mod(H1, H2)

We have seen that a model A′ of H1,H2 is isomorphic to an algebra A whose tH̄ reduct is a GwdfH̄. In the previous proof another isomorphism rep was defined that mapped the cylindric reduct of A into A^{∗} ∈ Gws_{ω}. A^{∗} can be expanded with the abstract operations s_{σ} (σ ∈ H) as follows

s_{σ}y =^{def} rep s_{σ}rep^{−1}y.

The expanded algebra is denoted by A^{∗} as well.

We examine the behaviour of the new, abstract operations. In this subsection we collect plenty of the characteristic features that will be useful in the proof of Theorem 2.30 (3). All the notations (A, A^{∗}, Λ, ∼_{λ}, f, rep) that were introduced in the previous subsection are kept. The set of weak spaces of A^{∗} is denoted by Λ^{∗}. Λ and Λ^{∗} is in a one-to-one correspondence in a natural way. We have that base(λ^{∗}) = (base(λ)/∼_{λ}) × {λ}.

¿From now we suppose that all the elements of H are bounded transformations of ω.

                                                                    cl-bound

Claim 3.40 If σ ∈ H (and so σ is bounded) and λ_{1}, λ_{2} ∈ Λ then the statements below hold.

• s_{σ}λ_{1} ⊇ λ_{2} or s_{σ}λ_{1} ∩ λ_{2} = ∅.

• s_{σ}λ_{1} ⊇ λ_{2} iff (∃q ∈ λ_{2})(q ∘ σ ∈ λ_{1}).

• (∀λ_{2} ∈ Λ)(∃!λ_{1} ∈ Λ)(s_{σ}λ_{1} ⊇ λ_{2}). (Here ∃! stands for ‘there exists exactly one’.)

Proof Suppose that q ∈ s_{σ}λ_{1} ∩ λ_{2}. For all q′ ∈ λ_{2}, q′ ∘ σ ∈ λ_{1} since q ∘ σ ∈ λ_{1} and {i ∈ ω | q ∘ σ(i) ≠ q′ ∘ σ(i)} ⊆ σ^{−1}{i ∈ ω | q(i) ≠ q′(i)} is finite. So λ_{2} ⊆ s_{σ}λ_{1}.

To prove the last statement suppose that q ∈ λ_{2} ∈ Λ. Put λ_{1} to be the weak space of q ∘ σ. Clearly, q ∘ σ ∈ λ_{1} and so λ_{2} ⊆ s_{σ}λ_{1}. If λ′ ∈ Λ and λ_{2} ⊆ s_{σ}λ′ then s_{σ}λ_{1} ∩ s_{σ}λ′ = s_{σ}(λ_{1} ∩ λ′) ⊇ λ_{2} shows that λ_{1} ∩ λ′ ≠ 0 and so λ_{1} = λ′.

That claim shows that the following definition is explicit.

                                                                    d-sonL

Definition 3.41 For each σ ∈ H, we define a transformation σ̂ of Λ:

σ̂(λ_{2}) = λ_{1} if λ_{2} ⊆ s_{σ}λ_{1}.

Since Λ and Λ^{∗} are in one-to-one correspondence, σ̂ can be viewed as a transformation of Λ^{∗}: λ_{1}, λ_{2} ∈ Λ, σ̂(λ_{2}^{∗}) = λ_{1}^{∗} if σ̂(λ_{2}) = λ_{1}.

We present an important property of these transformations.

                                                                    cl-hatjo

Claim 3.42 Suppose that σ_{1}, …, σ_{n} and σ′_{1}, …, σ′_{m} are elements of H. If σ_{n} ∘ … ∘ σ_{1} ≈ σ′_{m} ∘ … ∘ σ′_{1} then σ̂_{1} ∘ … ∘ σ̂_{n} and σ̂′_{1} ∘ … ∘ σ̂′_{m} are the same transformations of Λ (and of Λ^{∗} as well).

Proof Suppose that λ ∈ Λ. σ̂_{1} ∘ … ∘ σ̂_{n}(λ) = λ′ if λ ⊆ s_{σ_{n}} … s_{σ_{1}}λ′. Then for any q ∈ λ, q ∘ σ_{n} ∘ … ∘ σ_{1} ∈ λ′. Since σ_{n} ∘ … ∘ σ_{1} ≈ σ′_{m} ∘ … ∘ σ′_{1} and they are bounded, q ∘ σ_{n} ∘ … ∘ σ_{1} ≈ q ∘ σ′_{m} ∘ … ∘ σ′_{1}. Then q ∘ σ′_{m} ∘ … ∘ σ′_{1} ∈ λ′, λ ⊆ s_{σ′_{m}} … s_{σ′_{1}}λ′, σ̂′_{1} ∘ … ∘ σ̂′_{m}(λ) = λ′ and this was to prove.

                                                                    r-ph

Remark 3.43 The domain of the functionˆ defined in Definition 3.41 is H. The previous claim implies thatˆ can be defined on [H̄] as well. If ν ∈ [H̄] ⊆ ^{ω}ω then we set

ν̂ =^{def} σ̂_{1} ∘ … ∘ σ̂_{n}

where ν ≈ σ_{n} ∘ … ∘ σ_{1}. Clearly, ν̂ does not depend on the choice of σ_{1}, …, σ_{n}. The newˆ : [H̄] → ^{Λ^{∗}}Λ^{∗} has the following properties:

• If ν, μ ∈ [H̄], ν ≈ μ then ν̂ = μ̂.

• If ν, μ ∈ [H̄] then ν̂ ∘ μ = μ̂ ∘ ν̂.

                                                                    cl-base

Claim 3.44 When σ̂(λ_{2}) = λ_{1} for some σ ∈ H, λ_{1}, λ_{2} ∈ Λ then

• base(λ_{2}) ⊆ base(λ_{1}),

• ∼_{λ_{2}} = ∼_{λ_{1}} ∩ ^{2}base(λ_{2}).

Proof Suppose that λ_{2} ⊆ s_{σ}λ_{1}, q ∈ λ_{2}. For all u ∈ base(λ_{2}), q[σ(0)/u] ∈ λ_{2} and so q[σ(0)/u] ∘ σ ∈ λ_{1}. But (q[σ(0)/u] ∘ σ)(0) = u ∈ base(λ_{1}). It shows that base(λ_{2}) ⊆ base(λ_{1}).

To prove the second statement suppose that u, u′ ∈ base(λ_{2}), u ∼_{λ_{2}} u′. There is a q_{2} ∈ d_{01} ∩ λ_{2} for that q_{2}(0) = u, q_{2}(1) = u′. We fix a k ∈ ω for that σ(0) ≠ σ(k) and a finite transformation h of ω that maps σ(0) to 0 and σ(k) to 1. Since [H̄] is rich h ∈ [H̄] and so there is τ ∈ H̄^{∗} for that τ = h. We put

q_{1} =^{def} q_{2} ∘ h ∘ σ ∘ [1, k]. q_{2} ∈ d_{01} and s_{τ} s_{σ}s_{[1,k]}d_{01} = d_{h(σ([1,k](0))),h(σ([1,k](1)))} =

d_{01} implies that q_{1} ∈ d_{01}. q_{2} ∈ λ_{2} and λ_{2} ⊆ s_{σ}λ_{1} gives that q_{1} ∈ λ_{1}. Finally, q_{1}(0) = u, q_{1}(1) = u′ shows that u ∼_{λ_{1}} u′.

For the other direction suppose that u, u′ ∈ base(λ_{2}), u ∼_{λ_{1}} u′. There is a q ∈ λ_{1} ∩ d_{01} for that q(0) = u, q(1) = u′. Pick any q_{2} ∈ λ_{2} with q_{2}(0) = u, q_{2}(1) = u′. We put q_{1} =^{def} q_{2} ∘ h ∘ σ ∘ [1, k]. As in the previous case q_{1} ∈ λ_{1}. q ≈ q_{1} so they disagree on a finite set Γ = {i_{1}, …, i_{n}}. 0, 1 ∉ Γ. We conclude that q_{1} ∈ c_{i_{1}} … c_{i_{n}}d_{01} = d_{01}. Using again s_{τ} s_{σ}s_{[1,k]}d_{01} = d_{01} and q_{1} ∈ d_{01} we get that q_{2} ∈ d_{01}. This proves that u ∼_{λ_{2}} u′.

                                                                    d-em

Definition 3.45 We define the function

b : ⋃_{σ ∈ H, λ^{∗} ∈ Λ^{∗}} {⟨σ, λ^{∗}⟩} × base(λ^{∗}) → ⋃_{λ^{∗}∈Λ^{∗}} base(λ^{∗})

as follows. b_{σ,λ^{∗}}(⟨α, λ⟩) = ⟨α′, σ̂(λ)⟩ if α′ ∈ base(σ̂(λ))/∼_{σ̂(λ)} and α ⊆ α′ holds. The previous claim proved that b is well defined.

We collect some properties of the function b defined above.

                                                                    cl-propb

Claim 3.46 (1). q ∈ λ^{∗} ∈ Λ^{∗} ⇒ b_{σ,λ^{∗}} ∘ q ∘ σ ∈ V^{∗}.

(2). q, q′ ∈ λ^{∗} ∈ Λ^{∗} ⇒ b_{σ,λ^{∗}} ∘ q ∘ σ ≈ b_{σ,λ^{∗}} ∘ q′ ∘ σ.

(3). b_{σ,λ^{∗}} is injective.

(4). (∀λ ∈ Λ^{∗})(∃!λ′ ∈ Λ^{∗})(∀q ∈ λ) b_{σ,λ} ∘ q ∘ σ ∈ λ′.

Proof (1): Since q ∈ V^{∗}, there is a s ∈ V for that f(s) = q. The weak space of s in A is λ, and that of q in A^{∗} is λ^{∗}. We show that b_{σ,λ^{∗}} ∘ q ∘ σ = f(s ∘ σ) ∈ V^{∗} by checking that they take the same value on an arbitrary i ∈ ω. (b_{σ,λ^{∗}} ∘ q ∘ σ)(i) = b_{σ,λ^{∗}}(q(σ(i))) = b_{σ,λ^{∗}}(f(s)(σ(i))) = b_{σ,λ^{∗}}(⟨s(σ(i))/∼_{λ}, λ⟩) = ⟨s(σ(i))/∼_{σ̂(λ)}, σ̂(λ)⟩ = f(s ∘ σ)(i)

To prove (2) we need only that σ is bounded. (3) follows from the definition, and (4) from (2).

                                                                    rm-sigmab

Remark 3.47 If a function g satisfies condition (4) of Claim 3.46 then for each σ ∈ H, a transformation σ̂_{g} of Λ^{∗} can be defined:

σ̂_{g}(λ) = λ′ iff (∀q ∈ λ) g_{σ,λ} ∘ q ∘ σ ∈ λ′.

When g coincides with b then we get back σ̂, that is σ̂_{b} = σ̂.

                                                                    cl-prop5

Claim 3.48 Let λ^{∗} ∈ Λ^{∗}, σ_{1}, …, σ_{n} and σ′_{1}, …, σ′_{m} be elements of H.

(5). If σ̂_{1}∘…∘σ̂_{n}(λ^{∗}) = λ^{∗} then b_{σ_{1},σ̂_{2}(...σ̂_{n}(λ^{∗})...)}∘b_{σ_{2},σ̂_{3}(...σ̂_{n}(λ^{∗})...)}∘…∘b_{σ_{n},λ^{∗}} is the identity mapping of base(λ^{∗}).

(6). If σ̂_{1} ∘ … ∘ σ̂_{n}(λ^{∗}) = σ̂′_{1} ∘ … ∘ σ̂′_{m}(λ^{∗}) then

b_{σ_{1},σ̂_{2}(...σ̂_{n}(λ^{∗})...)} ∘ b_{σ_{2},σ̂_{3}(...σ̂_{n}(λ^{∗})...)} ∘ … ∘ b_{σ_{n},λ^{∗}} = = b_{σ′_{1},σ̂′_{2}(...σ̂′_{m}(λ^{∗})...)} ∘ b_{σ′_{2},σ̂′_{3}(...σ̂_{m}(λ^{∗})...)} ∘ … ∘ b_{σ′_{m},λ^{∗}}

Proof First we note that the expression formulated above is correct. The range of b_{σ_{i},σ̂_{i+1}(...σ̂_{n}(λ)...)} is contained in base(σ̂_{i}(… σ̂_{n}(λ) …)) and that is the domain of b_{σ_{i+1},σ̂_{i}(...σ̂_{n}(λ)...)}.

To check the validity of the expression in (6) we evaluate the two sides of the equation on an arbitrary element of base(λ^{∗}), say an ⟨u/∼_{λ}, λ⟩. When the left side of the equation is applied to that element we get ⟨u/∼_{(σ̂_{1}∘...∘σ̂_{n})(λ)}, (σ̂_{1} ∘ … ∘ σ̂_{n})(λ)⟩ and that is the same point as the image of ⟨u/∼_{λ}, λ⟩ under the function that appear on the right side of the equation.

(5) follows from the definition.

                                                                    nt-circ

Notation 3.49 We define a new composition operation • mapping V^{∗} ×H into V^{∗}:

q • σ =^{def} b_{σ,[q]} ∘ q ∘ σ

where [q] is the weak space of q in A^{∗}.

Now a direct definition can be given to s_{σ} (σ ∈ H).

                                                                    cl-newd2

Claim 3.50 For all σ ∈ H, y ∈ A^{∗}

s_{σ}y = {q ∈ V^{∗} | q • σ ∈ y}

Proof As a side result, in the proof of Claim 3.46 (1) we showed that if s ∈ V, q ∈ V^{∗}, f(s) = q then f(s ∘ σ) = q • σ.

Now we can compute that q ∈ s_{σ}y ⇔ s ∈ s_{σ}rep^{−1}y ⇔ s ∘ σ ∈ rep^{−1}y ⇔ f(s ∘ σ) ∈ y ⇔ q • σ ∈ y.

We arrived to the point when a new class of set algebras can be introduced. A new algebra has a deeper structure than a Gws_{H} does and its operations are computable from the structure of the algebra.

                                                                    df-nonst

Definition 3.51 An algebra A = ⟨A, ∪, −, c_{k}, d_{kl}, s_{σ}⟩_{k,l∈ω,σ∈H} is called a nonstandard generalised weak H–cylindric set algebra with equality (or briefly a nstGws_{H}) if ⟨A, ∪, −, c_{k}, d_{kl}⟩_{k,l∈ω} is a generalised weak cylindric set algebra and there is a function b with the following properties:

• Let V be the unit element of A. We put Λ to be the set of weak spaces building V. The domain of b is ⋃_{σ∈H,λ∈Λ}{σ, λ} × base(λ), the range is a

subset of ⋃_{λ∈Λ} base(λ).

• b satisfies the properties (1)-(6) listed in Claim 3.46 and Claim 3.48 where σ̂ = σ̂_{b} is defined as in Remark 3.47.

• We put • : V × H → V to be the function q • σ =^{def} b_{σ,[q]} ∘ q ∘ σ. Clearly, the properties of b gives that b_{σ,[q]} ∘ q ∘ σ is an element of V. Then s_{σ}y = {q ∈ V | q • σ ∈ y}.

If A is a nstGws_{H} and b is a function with the required properties then b is called a base transformation function of A. Note that the base transformation function is not uniquely determined.

The theorem below is a summary of the results that have achieved so far in this subsection.

                                                                    th-nonst

Theorem 3.52 Any model of H1,H2 is isomorphic to a nstGws_{H}.

                                                                    th-st-nst

Theorem 3.53 Gws_{H} ⊆ nstGws_{H}.

Proof Any Gws_{H} is a nstGws_{H} with the identity as base transformation function. (∀σ ∈ H)(λ ∈ Λ)(∀u ∈ base(λ)) b_{σ,λ}(u) =^{def} u.

                                                                    cl-hatjo2

Claim 3.54 Suppose that A ∈ nstGws_{H}. Then Claim 3.42 is true in A.

Proof As usual, Λ is the set of weak spaces of A. Pick an arbitrary element of Λ, say λ, and an arbitrary sequence q in λ. Using the definition of σ̂ in Remark 3.47 we have that σ̂_{1} ∘ … ∘ σ̂_{n}(λ) and σ̂′_{1} ∘ … ∘ σ̂′_{m}(λ) are the weak spaces of b_{σ_{1},σ̂_{2}(...σ̂_{n}(λ)...)} ∘b_{σ_{2},σ̂_{3}(...σ̂_{n}(λ)...)} ∘…∘b_{σ_{n},λ} ∘q ∘σ_{n} ∘…∘σ_{1} = q •σ_{n} •…•σ_{1} and b_{σ′_{1},σ̂′_{2}(...σ̂′_{m}(λ)...)} ∘ b_{σ′_{2},σ̂′_{3}(...σ̂_{m}(λ)...)} ∘ … ∘ b_{σ′_{m},λ} ∘ q ∘ σ′_{m} ∘ … ∘ σ′_{1} = q • σ′_{m} • … • σ′_{1} each respectively. Since σ_{n} ∘…∘σ_{1} ≈ σ′_{m} ∘…∘σ′_{1}, we have that q∘σ_{n} ∘…∘σ_{1} ≈ q∘σ′_{m}∘…∘σ′_{1}. This fact and Claim 3.48 implies that q•σ_{n}•…•σ_{1} ≈ q•σ′_{m}•…•σ′_{1} and so they are in the same weak space, that is σ̂_{1} ∘…∘σ̂_{n}(λ) = σ̂′_{1} ∘…∘σ̂′_{m}(λ).

                                                                    r-pb

Remark 3.55 As we did in Remark 3.43, we can introduce the function ˆ :

[H̄] → ^{Λ}Λ as ν̂ =^{def} σ̂_{1} ∘…∘σ̂_{n} when ν ∈ [H̄], σ_{1}, …, σ_{n} ∈ H and ν ≈ σ_{n} ∘…∘σ_{1}.

In the same sense, the domain of b can be expanded

b : ⋃_{ν∈[H̄],λ∈Λ}{ν, λ} × base(λ) → ⋃_{λ∈Λ} base(λ)

b_{ν,λ} =^{def} b_{σ_{1},σ̂_{2}(...σ̂_{n}(λ)...)} ∘ b_{σ_{2},σ̂_{3}(...σ̂_{n}(λ)...)} ∘ … ∘ b_{σ_{n},λ}

where ν ∈ [H̄], σ_{1}, …, σ_{n} ∈ H, λ ∈ Λ and ν ≈ σ_{n} ∘ … ∘ σ_{1}. If σ′_{1}, …, σ′_{m} ∈ H and ν ≈ σ′_{m} ∘ … ∘ σ′_{1} then σ̂_{1} ∘ … ∘ σ̂_{n} = ν̂ = σ̂′_{1} ∘ … ∘ σ̂′_{m} so σ̂_{1} ∘ … ∘ σ̂_{n}(λ) = σ̂′_{1} ∘ … ∘ σ̂′_{m}(λ). This gives that (6) of Claim 3.48 is applicable showing that the above definition of b does not depend on the choice of σ_{1}, …, σ_{n}.

We collect some properties of our newˆ functions. ν, μ ∈ [H̄], λ ∈ Λ.

(1). ν ≈ μ implies ν̂ = μ̂.

(2). ν̂ ∘ μ = μ̂ ∘ ν̂.

(3). ν ≈ Id implies that b_{ν,λ} is the identity mapping of base(λ).

(4). b_{ν∘μ,λ} = b_{μ,ν̂(λ)} ∘ b_{ν,λ}.

(5). ν̂(λ) = μ̂(λ) implies b_{ν,λ} = b_{μ,λ}.

(1) and (2) can be found in Remark 3.43, (3) and (5) are only reformulations of (5) and (6) of Claim 3.48, and (4) is a consequence of (6) of Claim 3.48.

                                                                    th-subd

Lemma 3.56 Let A be a subdirect irreducible model of H1,H2,H3. Then either −c_{0}(−d_{01}) = 1 or −c_{0}(−d_{01}) = 0.

Proof Suppose that in a model A of H1,H2,H3 neither −c_{0}(−d_{01}) = 0 nor c_{0}(−d_{01}) = 0 holds. We show that the relativizations with −c_{0}(−d_{01}) and c_{0}(−d_{01}) are homomorphisms, but not isomorphisms, and A is a subdirect product of the two image algebras. This proves that A cannot be subdirectly irreducible.

A relativization with some element R is a homomorphism if and only if R is closed under the operations of the algebra. H3 implies that −c_{0}(−d_{01}) and c_{0}(−d_{01}) are closed. In the image algebras −c_{0}(−d_{01}) = 1 or c_{0}(−d_{01}) = 1 will hold showing that they cannot be isomorphic to A. Finally, an element of A is solely determined by its two image under the two relativizations.

                                                                    l-extr

Lemma 3.57 If −c_{0}(−d_{01}) = 1 holds in A ∈ nstGws_{H} then A is a Gs_{H}.

Proof Let A be the universe, V the unit element, Λ the set of weak spaces of A. −c_{0}(−d_{01}) = 1 shows that for all λ ∈ Λ, |base(λ)| = 1.

Introduce the set theoretical operations on A:

s̃_{σ}x =^{def} {q ∈ V | q ∘ σ ∈ x}.

Then A′ =^{def} ⟨A, ∪ −, c_{k}, d_{kl}, s̃_{σ}⟩_{k,l∈ω,σ∈H} ∈ Gs_{H}. We show that s̃_{σ} = s_{σ} and so A = A′ ∈ Gs_{H}.

s_{σ}x = x since the axiom s_{σ}(x − c_{0}(−d_{01})) = x − c_{0}(−d_{01}) in H3 can be reduced to that form using −c_{0}(−d_{01}) = 1. On the other hand, s̃_{σ}x = x is a result of that fact that in V all the sequences are of the form ⟨u, u, u, …⟩ for some u.

3.7 The witness tree method

In this subsection we build a machinery called the witness tree method to prove Theorem 2.30. The essence of the method is the following. The failure of an equation in a given algebra can be captured by a tree structure that reflects the local nature of the algebra. This tree can be cut out from the algebra and moved to another one with better properties to testify the failure of the same equation therein. In our case we will show that an equation that is not satisfied in a nstGws_{H} cannot hold in all the Gws_{H}s.

                                                                    d-wt

Definition 3.58 Let H be a set of transformations of ω. We say that Ω = ⟨V, E, r, U, τ, ε, l⟩ is a witness tree of type H if the following requirements are fulfilled.

(i). ⟨V, E⟩ is a directed tree. r ∈ V. The edges are directed from the root r towards the leaves.

(ii). U, τ and ε are functions with domain V. If v ∈ V then U_{v} is a set, τ_{v} is a term of type t_{H}^{=}, and ε_{v} is either ∋ or ∌. (Note that we used the less conventional notation U_{v} instead of U(v).)

(iii). l is a function with domain E. If e = v⃗v′ ∈ E is an edge then l_{e} is one of ’=’, ’[k/u]’ or ’σ’ where k ∈ ω, u ∈ U_{v}, σ ∈ H. We will call l_{e} the label of

the edge e.

(iv). If e = v⃗v′ ∈ E is an edge then U_{v} ⊆ U_{v′}. Furthermore, if l_{e} is not ’σ’ for some σ ∈ H then U_{v} = U_{v′}.

(v). For every vertex v, τ_{v}, ε_{v}, the number of children of v, the labels of the edges pointing to the children of v, and the value of τ and ε on of the children vertexes of v are in a connection indicated in the following table.

τ_{v}, ε_{v}  The number of children The label of an edge pointing to a child The value ; of τ, ε on ; a child ; vertex

(−ϱ), ∋  1  =  ϱ, ∌
(−ϱ), ∌  1  =  ϱ, ∋
(ϱ_{1} ∪ ϱ_{2}), ∋  1  =  ϱ_{i}, ∋  where i is 1 or 2
(ϱ_{1} ∪ ϱ_{2}), ∌  2  =  ϱ_{i}, ∌  for i ∈ {1, 2}
c_{k}ϱ, ∋  1  [k/u]  ϱ, ∋  where u ∈ U_{v}
c_{k}ϱ, ∌  |U_{v}|  [k/u]  ϱ, ∌  for each u ∈ U_{v}
s_{σ}ϱ, ∋  1  σ  ϱ, ∋
s_{σ}ϱ, ∌  1  σ  ϱ, ∌
X, ∋  0  −  −
X, ∌  0  −  −
d_{kl}, ∋  0  −  −
d_{kl}, ∌  0  −  −

                                                                    d-nuv

Definition 3.59 Let Ω be a witness tree. We define a function ν : V → ^{ω}ω by recursion. For the root r, ν_{r} = Id. If e = v⃗_{1}v_{2} ∈ E and ν_{v_{1}} is already defined then ν_{v_{2}} is set to ν_{v_{1}} when l_{e} is ’=’ or ’[k/u]’ for some k ∈ ω, u ∈ U_{v_{1}} and to ν_{v_{1}} ∘ σ when l_{e} is ’σ’.

                                                                    d-Mr

Definition 3.60 Let ϱ be a term. Then M_{ϱ} denotes the set of those transformations f of ω for that exist σ_{1}, …, σ_{n} ∈ H with the property that f = σ_{1} ∘ … σ_{n} and s_{σ_{1}}, …, s_{σ_{n}} are letters of ϱ. We allow σ_{i} to be equal with σ_{j} (i ≠ j) but in that case s_{σ_{i}} and s_{σ_{j}} refer to the multiple occurrence of the same letter in ϱ. Clearly, n is smaller than or equal to the length of term ϱ.

                                                                    cl-Mfin

Claim 3.61 The set M_{ϱ} defined in the previous definition is finite.

Proof The term ϱ has only finite number of letters so there is only finitely many possible choices of σ_{1}, …, σ_{n}.

                                                                    d-M

Definition 3.62 Let Ω be a witness tree. Then M_{Ω} denotes M_{τ_{r}}.

                                                                    cl-nuM

Claim 3.63 For each vertex v of Ω, ν_{v} ∈ M_{Ω}.

                                                                    d-M=

Definition 3.64 M_{Ω}^{=}, M_{Ω}^{≠} denotes the following subsets of M_{Ω} × M_{Ω}.

M_{Ω}^{=} =^{def} {⟨ν, ν′⟩ | ν ≈ ν ∧ (∃ vertex v, v′)(ν = ν_{v} ∧ ν′ = ν_{v′})}
M_{Ω}^{≠} =^{def} {⟨ν, ν′⟩ | ν ≉ ν′ ∧ (∃ vertex v, v′)(ν = ν_{v} ∧ ν′ = ν_{v′})}

Both M_{Ω}^{=} and M_{Ω}^{≠} are finite.

                                                                    d-degen

Definition 3.65 Let Ω be a witness tree. We say the Ω is not degenerated if

(∀ vertex v_{1}, v_{2})(∀μ ∈ [H̄]) ν_{v_{1}} ∘ μ ≈ ν_{v_{2}} ⇒ U_{v_{1}} ⊆ U_{v_{2}}  (‡)

holds.

                                                                    d-validq

Definition 3.66 Let Ω be a witness tree. We say that a function Q is a valuation of the vertex set of Ω if the conditions below hold.

(1). The domain of Q is the vertex set of Ω.

(2). For all vertex v, Q_{v} is an ω-sequence over U_{v}.

(3). If v_{1} and v_{2} are two adjacent vertexes of Ω then the connection between Q_{v_{1}} and Q_{v_{2}} is determined by the label of the edge that joins v_{1} and v_{2}.

• If the label is ’=’ then Q_{v_{2}} = Q_{v_{1}}.
• If the label is ’[k/u]’ then Q_{v_{2}} = Q_{v_{1}}[k/u].
• If the label is ’σ’ then Q_{v_{2}} = Q_{v_{1}} ∘ σ.

                                                                    cl-vq

Claim 3.67 A valuation Q of the vertex set of a witness tree Ω and the value of Q on the root of Ω uniquely determine each other.

Proof If we know the value of Q on the root then we can compute the values of Q on other vertexes going step-by-step towards the leaves using (3) of Definition 3.66. To verify (2), we need only that U_{v_{1}} ⊆ U_{v_{2}} whenever v⃗_{1}v_{2} is an edge. (See the table in Definition 3.58.)

                                                                    cl-c1

Claim 3.68 Let Ω be a witness tree with root r, Q be a valuation of the vertex set. Then

(∃c_{1} ∈ ω)(∀ vertex v)(∀i ∈ ω) Q_{v}(i) ≠ (Q_{r} ∘ ν_{v})(i) ⇒ i ≤ c_{1}.

Proof To get an insight into the relation of Q_{v} and Q_{r} ∘ν_{v}, we take an example first. Suppose that we find the sequence σ_{1}, [k_{1}/u_{1}], σ_{2}, [k_{2}/u_{2}], σ_{3}, σ_{4}, [k_{3}/u_{3}], σ_{5} of labels on the r → v path. Then

Q_{v}(i) = \{ \begin{matrix}u_{3} & if i ∈ σ_{5}^{−1}(k_{3}), \\ u_{2} & if i ∈ (σ_{3} ∘ σ_{4} ∘ σ_{5})^{−1}(k_{2}) − σ_{5}^{−1}(k_{3}), \\ u_{1} & if i ∈ (σ_{2} ∘ σ_{3} ∘ σ_{4} ∘ σ_{5})^{−1}(k_{1}) − B, \\ Q_{r} ∘ ν_{v}(i) & otherwise \end{matrix}

where B = (σ_{3} ∘ σ_{4} ∘ σ_{5})^{−1}(k_{2}) ∪ σ_{5}^{−1}(k_{3}).

This example shows that for any v, Q_{v} and Q_{r} ∘ ν_{v} are equal everywhere but on the union of finitely many sets of the form (σ_{1} ∘ … ∘ σ_{n})^{−1}(k) where s_{σ_{1}}, …, s_{σ_{n}}, c_{k} are letters of the root term. In that case (σ_{1} ∘ … ∘ σ_{n})^{−1}(k) is finite since σ_{i} is bounded (i ≤ n) and σ_{1} ∘ … ∘ σ_{n} ∈ M_{Ω}. We can conclude that the set ⋃_{ν ∈ M_{Ω}, ck is a letter of the root term} ν^{−1}(k) is finite and c_{1} can be set to be its maximum.

                                                                    cl-c2

Claim 3.69 Let Ω be a witness tree with root r, Q be a valuation of the vertex set. Then

(∃c_{2} ∈ ω)(∀ vertex v, v′)(∀i ∈ ω) ν_{v} ≈ ν_{v′} ∧(Q_{r} ∘ν_{v})(i) ≠ (Q_{r} ∘ν_{v′})(i) ⇒ i ≤ c_{2}.

Proof Put c_{2} =^{def} max ⋃_{⟨ν,ν′⟩∈M_{Ω}^{=}}{i ∈ ω | ν(i) ≠ ν′(i)}. This definition is

transparent since the set, we have to take the maximum of is finite. (M_{Ω}^{=} is finite, {i ∈ ω | ν(i) ≠ ν′(i)} is finite if ν ≈ ν′.)

                                                                    l-c

Lemma 3.70 Let Ω be a witness tree with root r, Q be a valuation of the vertex set. Then

(∃c ∈ ω)(∀ vertex v, v′)(∀i ∈ ω) ν_{v} ≈ ν_{v′} ∧ Q_{v}(i) ≠ Q_{v′}(i) ⇒ i < c.

Proof Put c = max{c_{1}, c_{2}} + 1. Claims 3.68 and 3.69 will prove the statement.

                                                                    l-S

Lemma 3.71 Suppose that U_{r} is a set with cardinality bigger than 2. Then there is a sequence S ∈ ^{ω}U_{r} with the property that for all μ, ν ∈ [H̄]

μ ≉ ν ⇒ S_{r} ∘ μ ≉ S_{r} ∘ ν

To prove this lemma we will need the following claim.

                                                                    cl-h1

Claim 3.72 There is a set D ⊆ P(ω) for that

• α ∈ D ⇒ |α| = 2,

• α, β ∈ D ∧ α ≠ β ⇒ α ∩ β = ∅,

• μ, ν ∈ [H̄], μ ≉ ν ⇒ |D ∩ {{μ(i), ν(i)} | i ∈ ω}| = ω.

Proof Let ⟨μ_{i}, ν_{i}⟩ (i ∈ ω) be a series of pairs of transformations of ω with the property that for any μ, ν ∈ [H] with μ ≉ ν we have that ⟨μ_{i}, ν_{i}⟩ = ⟨μ, ν⟩ for infinitely many i ∈ ω. A series of that kind exists since |H| ≤ ω, |H̄| ≤ ω, |[H̄]| ≤ |H̄^{∗}| ≤ ω, |[H̄] × [H̄]| ≤ ω.

For all k ∈ ω we define the set α_{k} recursively:

• α_{0} = {μ_{0}(i), ν_{0}(i)} for an i ∈ ω with μ_{0}(i) ≠ ν_{0}(i).

• α_{k} = {μ_{k}(i), ν_{k}(i)} for an i ∈ ω with μ_{k}(i) ≠ ν_{k}(i) and i ∉ μ_{k}^{−1}( ⋃_{j<k} α_{j}) ∪

ν_{k}^{−1}( ⋃_{j<k} α_{j}).

α_{0} exists since μ_{0}(i) ≠ ν_{0}(i) for all but finitely many i ∈ ω. α_{k} can be chosen

since |{i ∈ ω | μ_{k}(i) ≠ ν_{k}(i)}| = ω and |μ_{k}^{−1}( ⋃_{j<k} α_{j}) ∪ ν_{k}^{−1}( ⋃_{j<k} α_{j})| < ω (both

μ_{k} and ν_{k} are bounded). Finally, we put D to be {α_{k} | k ∈ ω}.

Proof of Lemma 3.71 Suppose that D is a subset of P(ω) with the properties listed in Claim 3.72, u_{1} and u_{2} are distinct elements of U_{r}. We put S_{r} ∈ ω{u_{1}, u_{2}} to be

S_{r}(i) = \{ \begin{matrix}u_{1} & (∃j ∈ ω) \{i, j\} ∈ D ∧ i < j, \\ u_{2} & otherwise. \end{matrix}

Clearly, for all {i, j} ∈ D, S_{r}(i) ≠ S_{r}(j). If μ, ν ∈ [H̄], μ ≉ ν then there is infinitely many i ∈ ω for that {μ(i), ν(i)} ∈ D and so S_{r}(μ(i)) ≠ S_{r}(ν(i)) and this is what we stated in the formulation of the lemma.

                                                                    d-cons

Definition 3.73 Let Ω be a witness tree of type H with root r, Q be a valuation of the vertex set of Ω. We say that Q is consistent if (1), (2), (3) below hold.

(1). If v is a leaf, τ_{v} = d_{ij} and ε_{v} =∋ (or ε_{v} =∌) then Q_{v}(i) = Q_{v}(j) (or Q_{v}(i) ≠ Q_{v}(j) respectively).

(2). If v_{1} and v_{2} is a pair of leaves, τ_{v_{1}} = X = τ_{v_{2}} and ε_{v_{1}} ≠ ε_{v_{2}} then Q_{v_{1}} ≠ Q_{v_{2}}.

(3). If v_{1}, v_{2} are two vertexes of Ω, μ ∈ [H̄] and Q_{r} ∘ ν_{v_{1}} ∘ μ ≈ Q_{r} ∘ ν_{v_{2}} then U_{v_{1}} ⊆ U_{v_{2}}.

We say that Q is semi–consistent if (1) above and (2’), (3’) below hold.

(2’). If for a pair of leaves v_{1} and v_{2}, we have that τ_{v_{1}} = X = τ_{v_{2}}, ε_{v_{1}} ≠ ε_{v_{2}} and ν_{v_{1}} ≈ ν_{v_{2}} then Q_{v_{1}} ≠ Q_{v_{2}}.

(3’). Ω is not degenerated.

Note that if Q is consistent then it is semi–consistent but it does not hold the other way round.

                                                                    l-P

Lemma 3.74 Let Ω be a witness tree with root r, Q be a semi–consistent valuation of the vertex set of Ω. Suppose that |U_{r}| ≥ 2. Then there is a consistent valuation P of the vertex set.

Proof Since Q is semi–consistent, we have that Ω is not degenerated. Lemma 3.71 is applicable, therefore there is a sequence S_{r} with the property that (∀μ, ν ∈ [H̄]) μ ≉ ν ⇒ S_{r} ∘ μ ≉ S_{r} ∘ ν. S_{r} uniquely determines a valuation S of the vertex set of Ω (Claim 3.67).

With the help of a merge function m ∈ ^{ω}{0, 1} the merge P of Q and S can be defined: for all i ∈ ω, vertex v

P_{v}(i) =^{def} \{ \begin{matrix}S_{v}(i) & if & m ∘ ν_{v}(i) = 0 \\ Q_{v}(i) & if & m ∘ ν_{v}(i) = 1. \end{matrix}

We show that there is a merge function, such that P is a consistent valuation of the vertex set.

For any merge function m, P is a valuation of the vertex set. We check the conditions formulated in Definition 3.66. The domain of P is the vertex set of Ω, P_{v} is an ω-sequence over U_{v}.

If vertexes v_{1} and v_{2} are connected with an edge labelled by ’=’ (or ’[k/u]’) then m ∘ ν_{v_{1}} = m ∘ ν_{v_{2}} so P_{v_{2}} = P_{v_{1}} (or P_{v_{2}} = P_{v_{1}}[k/u]). If the edge is labelled

by ’σ’ then P_{v_{2}}(i) = \{ \begin{matrix}S_{v_{2}}(i) & if & m ∘ ν_{v_{2}}(i) = 0, \\ Q_{v_{2}}(i) & if & m ∘ ν_{v_{2}}(i) = 1. \end{matrix} Since S_{v_{2}} = S_{v_{1}} ∘ σ, Q_{v_{2}} =

Q_{v_{1}}∘σ and ν_{v_{2}} = ν_{v_{1}}∘σ we get P_{v_{2}}(i) = \{ \begin{matrix}S_{v_{1}}(σ(i)) & if & m ∘ ν_{v_{1}}(σ(i)) = 0, \\ Q_{v_{1}}(σ(i)) & if & m ∘ ν_{v_{1}}(σ(i)) = 1 \end{matrix} =

P_{v_{1}}(σ(i)) = P_{v_{1}} ∘ σ(i).

The following claims give sufficient conditions on m to ensure that P is consistent.

                                                                    cl-s1

Claim 3.75 There is a finite set D_{1} ⊆ ω with the property that if m(i) = 1 for all i ∈ D_{1} then P satisfies (1) of the definition of consistency.

Proof Put D_{1} =^{def} {ν(i), ν(j) | ν ∈ M_{Ω}, d_{ij} is in one of the leaves}. Since there are only finitely many d_{ij}’s that appear as leaf label term, D_{1} is finite.

Suppose that a for a leaf v τ_{v} = d_{ij}. Since ν_{v}(i), ν_{v}(j) ∈ D_{1}, m ∘ ν_{v}(i) = m ∘ ν_{v}(j) = 1, P_{v}(i) = Q_{v}(i), P_{v}(j) = Q_{v}(j). Now P_{v}(i) = P_{v}(j) if and only if Q_{v}(i) = Q_{v}(j), but this holds exactly when ε_{v} is ’∋’.

                                                                    cl-s2

Claim 3.76 There is a finite set D_{2} ⊆ ω with the property that if m(i) = 1 for all i ∈ D_{1} and m ≈ ⟨0, 0, 0, …⟩ then P satisfies (2) of the definition of consistency.

Proof Put D_{2} =^{def} {ν(i) | ν ∈ M_{Ω}, i < c} where c is the constant defined in Lemma 3.70. Suppose that for a pair of leaves v_{1} and v_{2} we have that τ_{v_{1}} = X = τ_{v_{2}} and ε_{v_{1}} ≠ ε_{v_{2}}.

If ν_{v_{1}} ≉ ν_{v_{2}} then S_{v_{1}} ≉ S_{v_{2}} since S_{v_{1}} ≈ S_{r} ∘ ν_{v_{1}} ≉ S_{r} ∘ ν_{v_{2}} ≈ S_{v_{2}}. Furthermore, from the facts that m ≈ ⟨0, 0, 0, …⟩ and ν_{v_{1}} and ν_{v_{2}} are bounded we can infer that m ∘ ν_{v_{1}} ≈ ⟨0, 0, 0, …⟩ ≈ m ∘ ν_{v_{2}}. It gives that P_{v_{1}} ≈ S_{v_{1}} and P_{v_{2}} ≈ S_{v_{2}} and so P_{v_{1}} ≉ P_{v_{2}}. But then P_{v_{1}} ≠ P_{v_{2}}.

Now suppose that ν_{v_{1}} ≈ ν_{v_{2}}. In that case there is an i ∈ ω for that Q_{v_{1}}(i) ≠ Q_{v_{2}}(i) since Q was semi–consistent and (2’) was applicable. Lemma 3.70 implies that i < c. Since ν_{v_{1}}, ν_{v_{2}} ∈ M_{Ω} we have that ν_{v_{1}}(i), ν_{v_{2}}(i) ∈ D_{2} and so m ∘ ν_{v_{1}}(i) = m ∘ ν_{v_{2}}(i) = 1. This gives P_{v_{1}}(i) = Q_{v_{1}}(i) ≠ Q_{v_{2}}(i) = P_{v_{2}}(i). But then P_{v_{1}} ≠ P_{v_{2}}.

                                                                    cl-s3

Claim 3.77 If m ≈ ⟨0, 0, 0, …⟩ then P satisfies (3) of the definition of consistency.

Proof Suppose that v_{1}, v_{2} are two vertexes of Ω, μ ∈ [H̄] and P_{r} ∘ ν_{v_{1}} ∘ μ ≈ P_{r} ∘ ν_{v_{2}}. m ≈ ⟨0, 0, 0, …⟩ implies that P_{r} ≈ S_{r}. Using the fact that ν_{v_{1}} ∘ μ and ν_{v_{2}} are bounded, we conclude that S_{r} ∘ ν_{v_{1}} ∘ μ ≈ S_{r} ∘ ν_{v_{2}}. Referring to the property of S, we infer that ν_{v_{1}} ∘ μ ≈ ν_{v_{2}}. Ω is not degenerated so we derive that U_{v_{1}} ⊆ U_{v_{2}}.

If we put m(i) =^{def} \{ \begin{matrix}1 & if & i ∈ D_{1} ∪ D_{2} \\ 0 & if & i ∉ D_{1} ∪ D_{2} \end{matrix} then m satisfies the conditions

described in the previous claims so P is consistent.

                                                                    d-adapt

Definition 3.78 Let Ω be a witness tree of type H, A be a nstGws_{H} with base transformation function b. Let Λ be the set of weak spaces building A. We say that a function a : ⋃_{vertex v}{v} × U_{v} → ⋃_{λ∈Λ} base(λ) is an adaptation of Ω in ⟨A, b⟩

if

• (∃λ ∈ Λ)(∀ vertex v) a_{v} is a bijection between U_{v} and base(ν̂_{v}(λ)),

• for any pair of vertexes v_{1}, v_{2}, and μ ∈ [H̄] we have that ν_{v_{1}} ∘ μ ≈ ν_{v_{2}} ⇒ a_{v_{2}}⌈U_{v_{1}} = b_{μ,ν̂_{v_{1}} (λ)} ∘ a_{v_{1}}.

                                                                    d-validw

Definition 3.79 Let Ω be a witness tree of type H, A be a nstGws_{H}, b be a base transformation function of A, Q be a valuation of the vertex set of Ω, and a be an adaptation of Ω in ⟨A, b⟩. Suppose that w is a function mapping the set of those variables that occur in a term of a vertex label into the universe of A.

• ⟨Q, w, a, b⟩ is said to be a valuation of Ω into A if for all vertex v, a_{v} ∘ Q_{v} is a sequence from the unit element of A, a_{v} is a bijection between U_{v} and the base of that weak space of A that contains a_{v} ∘ Q_{v}.

• We say that a valuation ⟨Q, w, a, b⟩ of Ω into A makes the label of a vertex v true (or satisfies v) if τ_{v}[w] ε_{v} a_{v} ∘ Q_{v} holds in A. (Depending on ε_{v}, it is τ_{v}[w] ∋ a_{v} ∘ Q_{v} or τ_{v}[w] ∌ a_{v} ∘ Q_{v}.)

• And finally, a valuation ⟨Q, w, a, b⟩ of Ω into A is valid if it makes all the vertex labels of Ω true.

In the special situation, when A ∈ Gws_{H} we say that ⟨Q, w⟩ is a (valid) valuation of Ω into A if ⟨Q, w, a, b⟩ is a (valid) valuation, where a and b are the identity mappings.

                                                                    cl-leaves

Claim 3.80 A valuation ⟨Q, w, a, b⟩ of Ω into A is valid if and only if it makes all the leaf labels of Ω true.

Proof The requirements formulated in Definition 3.58 and 3.66 were designed to ensure that the validity of a vertex label could be proved from the validity of the labels of the children of that vertex.

                                                                    cl-sound

Claim 3.81 If ⟨Q, w, a, b⟩ is a valid valuation of the witness tree Ω into some algebra A ∈ nstGws_{H} then Q is semi–consistent.

Proof To prove (1) we pick an arbitrary leaf v with τ_{v} = d_{ij}, ε_{v} =∋. ⟨Q, w, a, b⟩ satisfies this vertex so d_{ij} ∋ a_{v} ∘ Q_{v} and that is a_{v} ∘ Q_{v}(i) = a_{v} ∘ Q_{v}(j). Since a_{v} is a bijection, it is implied that Q_{v}(i) = Q_{v}(j). In a similar way, we can infer that Q_{v}(i) ≠ Q_{v}(j) whenever τ_{v} = d_{ij}, ε_{v} =∌.

To verify (2’) we suppose that v_{1} and v_{2} are vertexes with τ_{v_{1}} = X = τ_{v_{2}}, ε_{v_{1}} ≠ ε_{v_{2}} and ν_{v_{1}} ≈ ν_{v_{2}}. Using the property (3) of the base transformation (Remark 3.55) and that of the adaptation we get that a_{v_{1}} = a_{v_{2}}. Since ⟨Q, w, a, b⟩ satisfies v_{1} and v_{2} we have that w(X) ∋ a_{v_{1}} ∘ Q_{v_{1}}, w(X) ∌ a_{v_{2}} ∘ Q_{v_{2}} and so a_{v_{1}} ∘Q_{v_{1}} ≠ a_{v_{2}} ∘Q_{v_{2}}. Now using that a_{v_{1}}(= a_{v_{2}}) is a bijection, we get Q_{v_{1}} ≠ Q_{v_{2}} as desired.

Finally, (3’) is an immediate consequence of the last property of the adaptation. Suppose that for a pair of vertexes v_{1}, v_{2}, and μ ∈ [H̄] we have that ν_{v_{1}} ∘ μ ≈ ν_{v_{2}}. Then a_{v_{2}}⌈U_{v_{1}} = b_{μ,ν̂_{v_{1}} (λ)} ∘ a_{v_{1}}. This shows that the domain of

a_{v_{1}}, that is U_{v_{1}}, is contained in that of a_{v_{2}} so U_{v_{1}} ⊆ U_{v_{2}}.

                                                                    cl-compl

Claim 3.82 Let Ω be witness tree with root r, P be a consistent valuation of the vertex set of Ω. Then there is an A ∈ Gws_{H} and a function w for that ⟨P, w⟩ is a valid valuation of Ω into A.

Proof For all vertex v, U_{r} ⊆ U_{v} and so s ∈ ^{ω}U_{r} ⇒ s ∈ ^{ω}U_{v}. Furthermore, s ∈ ^{ω}U_{r} ⇒ s ∘ f ∈ ^{ω}U_{v}, where f is any transformation of ω.

We define the set U_{s} for all s ∈ ^{ω}U_{r} as follows.

U_{s} =^{def} ⋃{U_{v} | v is vertex of Ω, (∃μ ∈ [H̄]) P_{v} ∘ μ ≈ s}

If no vertex satisfies the condition, then U_{s} is set to the empty set. We put V to be ⋃{^{ω}U_{s}^{(s)} | s ∈ ^{ω}U_{r}}, A to be the full generalised weak H–cylindric set algebra with equality over V.

To see that V is a Gws_{ω}–unit we need to show that (∀s_{1}, s_{2} ∈ ^{ω}U_{r})(^{ω}U_{s_{1}}^{(s_{1})} ∩ ωU_{s_{2}}^{(s_{2})} ≠ ∅ ⇒ ^{ω}U_{s_{1}}^{(s_{1})} = ^{ω}U_{s_{2}}^{(s_{2})}). Suppose that q ∈ ^{ω}U_{s_{1}}^{(s_{1})} ∩ ^{ω}U_{s_{2}}^{(s_{2})}. Then s_{1} ≈ q ≈ s_{2}. This gives that (∀ vertex v)(∀μ ∈ [H̄])P_{v} ∘ μ ≈ s_{1} ⇔ P_{v} ∘ μ ≈ s_{2} and so U_{s_{1}} = U_{s_{2}}, ^{ω}U_{s_{1}}^{(s_{1})} = ^{ω}U_{s_{2}}^{(s_{2})}.

To ensure that V can be a unit element of a Gws_{H} we need that (∀σ ∈ H) s_{σ}V = V, that is (∀σ ∈ H)(∀q ∈ V) q ∘ σ ∈ V. Suppose that q ∈ ^{ω}U_{s}^{(s)} ⊆ V, σ ∈ H. U_{s∘σ} ⊇ U_{s} since for any vertex v, μ ∈ [H̄], P_{v} ∘ μ ≈ s ⇒ P_{v} ∘ μ ∘ σ ≈ s ∘ σ. (We used that σ is bounded.) Now q ∘ σ ∈ ^{ω}U_{s}^{(s∘σ)} ⊆ ^{ω}U_{s∘σ}^{(s∘σ)} ⊆ V.

An important result is that for any vertex v, U_{v} = U_{P_{r}∘ν_{v}}. Clearly, P_{v} ∘Id = P_{v} ≈ P_{r} ∘ ν_{v} so U_{v} ⊆ U_{P_{r}∘ν_{v}}. On the other hand, if for some vertex v′, μ ∈ [H̄], P_{v′} ∘ μ ≈ P_{r} ∘ ν_{v} holds then P_{r} ∘ ν_{v′} ∘ μ ≈ P_{r} ∘ ν_{v} and so U_{v′} ⊆ U_{v}. (Property (3) of consistency.) This gives that U_{v} ⊇ U_{P_{r}∘ν_{v}}.

We have that for every vertex v, P_{v} ∈ V since P_{v} ∈ ^{ω}U_{P_{r}∘ν_{v}}^{(P_{r}∘ν_{v})} ⊆ V.

Finally we can define function w. For any variable X that appear in τ_{v} for some vertex v, we set

w(X) =^{def} {P_{v} | v is a vertex, τ_{v} = X, ε_{v} =∋}.

The previous observations shows that ⟨P, w⟩ is a valuation of Ω into A. To see that ⟨P, w⟩ is valid we need to check that it satisfies the leaves. Property (1) of consistency can be used to verify that a leaf v with τ_{v} = d_{ij} is satisfied. If τ_{v} = X, ε_{v} =∋ then P_{v} ∈ X[w] = w(X). Finally, if τ_{v} = X, ε_{v} =∌ then there is no other vertex v′ with τ_{v′} = X, ε_{v′} =∋ and have P_{v} = P_{v′} in the same time. (Property (2) of consistency.) Therefore we have that P_{v} ∉ X[w] = w(X).

In the following corollary we collect all the results we have achieved so far.

                                                                    cr-help

Corollary 3.83 Let Ω be a witness tree with root r. Suppose that the cardinality of U_{r} is bigger than 1 and Ω has a valid valuation into a nstGws_{H}. Then Ω has a valid valuation into a Gws_{H}.

Proof If Ω has a valid valuation, say ⟨Q, w, a, b⟩ to a nstGws_{H} then Q is semi– consistent (Claim 3.81). Lemma 3.74 proves that in that situation, there is a consistent valuation of the vertex set. Finally, using Claim 3.82 we conclude that Ω has a valid valuation into a Gws_{H}.

                                                                    d-wing

Definition 3.84 We say that a witness tree Ω with root r witnesses the fact that the equation ϱ = 0 does not hold in an algebra A ∈ nstGws_{H} if τ_{r} = ϱ, ε_{r} =∋ and Ω has a valid valuation into A.

                                                                    l-wing

Lemma 3.85 Let A be a nstGws_{H}, ϱ be a term. Then A |̸= ϱ = 0 if and only if there is a witness tree Ω that witnesses that fact.

Proof If Ω witnesses that ϱ = 0 does not hold in A, then there is a valid valuation ⟨Q, w, a, b⟩ that makes all the labels true. Concentrating on the root label we have that ϱ[w] ∋ a_{r} ∘ Q_{r}, and so A |̸= ϱ = 0[w], A |̸= ϱ = 0.

To prove the other direction suppose that A ∈ nstGws_{H}, A |̸= ϱ = 0. Let b be a base transformation function of A. There is a valuation w of the variables of ϱ for that ϱ[w] is not empty. We fix w and a sequence q in ϱ[w]. We denote the weak space of q by λ.

                                                                    c-w1

Claim 3.86 (∃ξ ∈ [H̄])(∀ν ∈ M_{ϱ})(∃ν^{∗} ∈ [H̄]) ν ∘ ν^{∗} ≈ ξ, that is, M_{ϱ} has an upper bound. (M_{ϱ} is defined in Definition 3.60).

Proof We prove that the statement holds for an arbitrary, but finite M ⊆ [H̄]. We prove it by induction on the size of M. If |M| = 1 then there is nothing to verify.

Suppose that M ⊆ [H̄] is finite, ν_{0}, ξ ∈ [H̄], ν_{0} ∉ M and (∀ν ∈ M)(∃ν^{∗} ∈ [H̄]) ν ∘ ν^{∗} ≈ ξ. Using the property of [H̄] formulated in Theorem 2.30 (3), we get that there are transformations ν_{0}^{∗}, ξ^{∗} with ν_{0} ∘ ν_{0}^{∗} ≈ ξ ∘ ξ^{∗}. Now for the set H′ = H ∪ {ν_{0}}, ξ ∘ ξ^{∗} is an appropriate choice to be its upper bound. Indeed, (∀ν ∈ M) ν ∘ ν^{∗} ∘ ξ^{∗} ≈ ξ ∘ ξ^{∗}. (We used that ξ^{∗} is bounded.)

For every ν ∈ M_{ϱ} we set

U_{ν} = {b_{ν^{∗},ν̂(λ)}(u) | u ∈ base(ν̂(λ))},
a_{ν} = b_{ν^{∗},ν̂(λ)}^{−1}.

Clearly, a_{ν} is a bijection between U_{ν} and base(ν̂(λ)).

                                                                    c-w2

Claim 3.87 If ν_{1} ≈ ν_{2} ∘ μ then a_{ν_{1}}⌈U_{ν_{2}} = b_{μ,ν̂_{2}(λ)} ∘ a_{ν_{2}} (ν_{1}, ν_{2} ∈ M_{ϱ}, μ ∈ [H̄]).

Proof ν_{1} ≈ ν_{2} ∘ μ and ν_{2} ∘ ν_{2}^{∗} ≈ ξ ≈ ν_{1} ∘ ν_{1}^{∗} gives that ν_{2} ∘ ν_{2}^{∗} ≈ ν_{2} ∘ μ ∘ ν_{1}^{∗} and so ν̂_{2}^{∗} ∘ ν̂_{2} = μ̂ ∘ ν_{1}^{∗} ∘ ν̂_{2}, ν̂_{2}^{∗}(ν̂_{2}(λ)) = μ̂ ∘ ν_{1}^{∗}(ν̂_{2}(λ)). Property (5) of Remark 3.55 and then (4) gives that b_{ν_{2}^{∗},ν̂_{2}(λ)} = b_{μ∘ν_{1}^{∗},ν̂_{2}(λ)} = b_{ν_{1}^{∗},μ̂∘ν̂_{2}(λ)} ∘ b_{μ,ν̂_{2}(λ)}. Using property (2), from ν_{1} ≈ ν_{2}∘μ we can infer that μ̂∘ν̂_{2} = ν̂_{1}. This gives b_{ν_{2}^{∗},ν̂_{2}(λ)} = b_{ν_{1}^{∗},ν̂_{1}(λ)} ∘ b_{μ,ν̂_{2}(λ)} so a_{ν_{2}}^{−1} = a_{ν_{1}}^{−1} ∘ b_{μ,ν̂_{2}(λ)}. But then a_{ν_{1}}⌈U_{ν_{2}} = b_{μ,ν̂_{2}(λ)} ∘ a_{ν_{2}}.

We construct a witness tree Ω that witnesses A ⊧ ϱ ≠ 0 together with an adaptation a and a valid valuation Q of the vertex set by induction. To give name to the interior stages of the construction we introduce the notion of a unsaturated witness tree and that of an unsaturated system.

Ω is an unsaturated witness tree if it satisfies all but the last requirement listed in Definition 3.58 \underline{and} it satisfies the following one.

(v’). For every vertex v, \underline{that is not a leaf}, τ_{v}, ε_{v}, the number of children of v, the labels of the edges pointing to the children of v, and the value of τ and ε on of the children vertexes of v are in a connection indicated in the table given in Definition 3.58.

The level (or depth) of saturation is the minimal length of a path in the tree that joins the root with a vertex that does not satisfy (v) of Definition 3.58. The level of saturation is set to ω if every vertex satisfies (v), that is, the tree is a witness tree. We also call a tree with that property saturated. If the saturation level is bigger than the length of the root term then the tree is saturated i.e. it is a witness tree. Clearly, on a path starting form the root every term written on a vertex is a subterm of the previous one and so the length of a path cannot be longer than the length of the root term.

An unsaturated system is a triple ⟨Ω, Q, a⟩ where Ω is an unsaturated witness tree, Q is a valuation of the vertex set of Ω, a is an adaptation of Ω in ⟨A, b⟩ and ⟨Q, w, a, b⟩ is a valid valuation.

We construct a series of unsaturated systems. Every system is an extension of the previous one, that is, V^{n+1} ⊇ V^{n}, E^{n+1} ⊇ E^{n}, r^{n+1} = r^{n}, the functions U^{n+1}, τ^{n+1}, ε^{n+1}, l^{n+1}, Q^{n+1}, a^{n+1} are extensions of the corresponding functions of the n-th system. The root term of the first system, and so that of all systems, is ϱ. The saturation level of the witness trees in the series is strictly increasing. This proves that after a certain index, say n_{0} all the systems are saturated in the series. So Ω^{n_{0}} is a witness tree and ⟨Q^{n_{0}}, w, a^{n_{0}}, b⟩ proves that Ω^{n_{0}} witnesses the fact that A |̸= ϱ = 0 as desired.

Construction of the first system: Let r be any point. Then we set

V^{1} =^{def} {r}, E^{1} =^{def} ∅, U_{r}^{1} =^{def} U_{Id}, τ_{r}^{1} =^{def} ϱ, ε_{r}^{1} =∋, a_{r}^{1} =^{def} a_{Id}, Q_{r}^{1} =^{def} a_{Id}^{−1} ∘ q.

Construction of the n-th system from the (n−1)-th: We add children vertexes to those leaves of Ω^{n−1} that do not satisfy (v). If leaf v ∈ V^{n−1} does not satisfy (v) and τ_{v}^{n−1}, ε_{v}^{n−1} has the value indicated in column C1 then we add as many children vertexes as given in column C2, we label the edges pointing to the new vertexes according to column C3, and we set the values of τ^{n}, ε^{n}, Q^{n}, a^{n} on the new vertexes as indicated in column C4.

C1  C2 C3 C4
τ_{v}^{n−1}, ε_{v}^{n−1}  l^{n} U^{n}, τ^{n}, ε^{n}, Q^{n}, a^{n}
(−ϱ), ∋  1  = U_{v}^{n−1}, ϱ, ∌, Q_{v}^{n−1}, a_{v}^{n−1}
(−ϱ), ∌  1  = U_{v}^{n−1}, ϱ, ∋, Q_{v}^{n−1}, a_{v}^{n−1}
(ϱ_{1} ∪ ϱ_{2}), ∋ 1  = U_{v}^{n−1}, ϱ_{i}, ∋, Q_{v}^{n−1}, a_{v}^{n−1}  (*) where

i ∈ {1, 2} and ϱ_{i}[w] ∌ a_{v} ∘ Q_{v}

(ϱ_{1} ∪ ϱ_{2}), ∌ 2 = U_{v}^{n−1}, ϱ_{i}, ∌, Q_{v}^{n−1}, a_{v}^{n−1} for i ∈ {1, 2}

c_{k}ϱ, ∋ 1 [k/u] U_{v}^{n−1}, ϱ, ∋, Q_{v}^{n−1}[k/u], a_{v}^{n−1} (*) where u ∈ U_{v} and ϱ ∋ a_{v} ∘ (Q_{v}[k/u])

c_{k}ϱ, ∌  |U_{v}| [k/u] U_{v}^{n−1}, ϱ, ∌, Q_{v}^{n−1}[k/u]_{v}, a_{v}^{n−1} for each u ∈ U_{v}
s_{σ}ϱ, ∋  1  σ U_{ν_{v}∘σ}, ϱ, ∋, Q_{v}^{n−1} ∘ σ, a_{ν_{v}∘σ} (**)
s_{σ}ϱ, ∌  1  σ U_{ν_{v}∘σ}, ϱ, ∌, Q_{v}^{n−1} ∘ σ, a_{ν_{v}∘σ} (**)

In (*) we used that ϱ_{1} ∪ ϱ_{2}[w] ∌ a_{v} ∘ Q_{v} implies that there is an i ∈ {1, 2} with that property. Similarly, if c_{k}ϱ[w] ∋ a_{v} ∘ Q_{v} then there is an u ∈ U_{v} with ϱ ∋ a_{v} ∘ (Q_{v}[k/u]). To see (**) we note that ν_{v} ∘ σ ∈ [H̄] so a_{ν_{v}∘σ} and U_{ν_{v}∘σ} is defined some pages before.

The verification of the facts that the newly defined Q^{n} is indeed a valuation of the vertex set of the expanded tree, a^{n} is an adaptation and ⟨Q^{n}, w, a^{n}, b⟩ is a valid valuation is straightforward. We need to examine the table above, the definitions of the notions in question and to note that for every vertex v a_{v}^{n} = a_{ν_{v}}, U_{v}^{n} = U_{ν_{v}}.

Before turning to prove Theorem 2.30 (3) we state a final corollary of the previous lemma.

                                                                    cr-fo

Corollary 3.88 Suppose that the equation ϱ = 0 fails in an algebra A ∈ nstGws_{H}, and A ⊧ −c_{0}(−d_{01}) = 0. Then Gws_{H} |̸= ϱ = 0.

Proof If A ⊧ −c_{0}(−d_{01}) = 0 then none of the weak spaces of A can have a base of cardinality 1.

If ϱ = 0 fails in A, then there is a witness tree Ω with root r that witnesses that fact. Ω has a valid valuation into A. |U_{r}| > 1. Corollary 3.83 is applicable, therefore Ω has a valid valuation into a Gws_{H}. Using again Lemma 3.85 we get that ϱ = 0 fails in that algebra of Gws_{H}.

Proof of Theorem 2.30 (3) Since both HGws_{H} and Mod(H1, H2, H3) are varieties, we need to show that they satisfy the same set of equations.

First we show that Gws_{H} ⊧ H1, H2, H3. The only equation that needs explanation is the first one in H3. First suppose that q ∈ x − c_{0}(−d_{01}). Then the weak space of q has a base of cardinality 1, so q = ⟨u, u, u, …⟩. But in that case q = q ∘ σ, q ∈ s_{σ}(x − c_{0}(−d_{01})). Now suppose that q ∈ s_{σ}(x − c_{0}(−d_{01})). Then q ∘ σ ∈ x − c_{0}(−d_{01}), so the weak space of q ∘ σ has a base of cardinality 1. Referring to Claim 3.44 we have that the base of the weak space of q is contained in that of q ∘ σ so it is of cardinality 1 as well. Hence, q = q ∘ σ, q ∈ x − c_{0}(−d_{01}).

For the other direction we show that any equation e that fails in an A ∈ Mod(H1, H2, H3) also fails in some B ∈ Gws_{H}. First we simplify the situation by putting assumptions on A and e and then we will apply Corollary 3.88 or Lemma 3.57 to prove the theorem.

If e is of the form τ = τ′ then the equation τ ⊕ τ′ = 0 is satisfied in exactly those algebras where e (⊕ is the symmetric difference operator). For that reason, without loss of generality we may assume that e of the form ϱ = 0.

Every algebra is a subalgebra of a product of subdirect irreducible algebras. If an equation fails in a subdirect product, then it fails in some of the factors. So we may assume that A is a subdirectly irreducible algebra.

Furthermore, referring to Theorem 3.52 we may put the assumption that A is a nstGws_{H}. According to Theorem 3.56 either −c_{0}(−d_{01}) = 1 or −c_{0}(−d_{01}) = 0 holds in A. In the first case Lemma 3.57, in the second Corollary 3.88 provides the required B in which ϱ = 0 fails.

Proof of Theorem 2.30 (4) The proof of Theorem 2.30 (3) is applicable with some adjustments. We present the required modifications here.

Theorem 3.56 remains valid.

In the proof of Lemma 3.57 one can note that the algebra A′ defined therein is a direct product of some two element algebras. (Clearly, any weak space with a base of cardinality 1 is a H-cylindric set algebra with equality in itself.) Hence, this lemma can be reformalized as: If −c_{0}(−d_{01}) = 1 holds in A ∈ nstGws_{H} then A is a PCs_{H}.

Under the conditions listed in Theorem 2.30 (4), we have that: If Ω is a not degenerated witness tree then for every vertex v we have that U_{v} = U_{r}. Suppose that v is a vertex. Put ν_{v}^{∗} and ν_{r}^{∗} to be the right quasi-inverse of ν_{v} and ν_{r} respectively. Then ν_{v} ∘ ν_{v}^{∗} ∘ ν_{r} ≈ ν_{r} and ν_{r} ∘ ν_{r}^{∗} ∘ ν_{v} ≈ ν_{v} shows that U_{v} ⊇ U_{r} and U_{r} ⊇ U_{v} giving U_{v} = U_{r}. (We used that ν_{r} and ν_{v} are bounded transformations.)

Claim 3.82 can be modified to: Let Ω be witness tree with root r, P be a consistent valuation of the vertex set of Ω. Then there is a function w for that ⟨P, w⟩ is a valid valuation of Ω into the full H–cylindric set algebra with equality over the base set U_{r}. To prove that statement we need to skip the argumentation about the algebra itself in the original proof and start reading from the point where w is defined.

Using that modified Claim we get: Suppose that the equation ϱ = 0 fails in an algebra A ∈ nstGws_{H}, and A ⊧ −c_{0}(−d_{01}) = 0. Then Cs_{H} |̸= ϱ = 0.

Following the argument described in the proof of Theorem 2.30 (3) and inserting the modifications listed above we get that the statement in Theorem 2.30 (4) holds.

Historical remark

The early versions of the ideas presented in this work can be found in [Sa87] but the investigations here go much further than the ones therein. Many of our results for the special choice H = G are already stated in [Sa87] in less developed form. The case without equality is fully proved there, but our axiom system Ax is considerably simpler than the one in [Sa87]. (Cf. around the end of Part I and beginning of Part II of [Sa87].) The Tarski–Givant style part of the case with equality is implicit in [Sa87a]. These research directions are not investigated in [Sa93].

The works of Sándor Csizmazia (e.g. [Cs93], [Cs95]) were based on the early version [Sa87] of the present ideas.

Acknowledgement

The authors are grateful to W.Craig, L.Henkin, J.D.Monk and I.Németi for encouragement, valuable discussions and suggestions concerning the topic of this paper. Thanks are due to S.Csizmazia for pointing out the data written in the Historical remark section above.

References

                                                                           diszi

[A91] Andréka,H. Complexity of the Equations Valid in Algebras of Relations PhD thesis, Hungarian Academy of Sciences, Budapest, Budapest, 1991. (Thesis for D.Sc — a post–habilitation degree).

                                                                           amast

[ANS93] Andréka,H. Németi,I. and Sain,I. Applying Algebraic Logic to Logic In: Algebraic Methodology and Software Technology (AMAST ’93) (Proceedings of the Third International Conference on Algebraic Methodology and Software Technology, University of Twente, The Netherlands, 21–25 June 1993.) eds.: Nivat,M. Rattray,C. Rus,T. and Scollo,G., Springer-Verlag, London, Workshops in Computing series.

                                                                           ansk

[ANSK] Andréka,H. Kurucz,Á. Németi,I. and Sain,I. Methodology of applying algebraic logic to logic Course material of the Summer School “Algebraic Logic and the Methodology of Applying it”, Budapest, 1994. 67pp. Preprint of Math. Inst. Hungarian Academy of Sciences, Budapest, 1994. A short version of this appeared as [ANS93].

                                                                           benthem

[vB91] van Benthem,J. Language in Action North–Holland, Amsterdam, 1991.

                                                                  vb96

[vB96] van Benthem,J. Exploring Logical Dynamics CSLI Publications & Cam-

bridge Univ. Press, 1996.

                                                                  biro

[Bi89] Biró,B. Non-finite Axiomatizability Results in Algebraic Logic Journal of

Symbolic Logic, vol.57, 1992, p832–843.

                                                                  memoirs

[BP89] Blok,W.J. and Pigozzi,D. Algebraizable Logics Memoirs of American Math.

Society, vol.77, 396pp, 1989.

                                                                  craig

[Cr74] Craig,W. Logic in Algebraic Form North–Holland, Amsterdam, 1974.

                                                                  Cs93

[Cs93] Csizmazia,S. Databases and Cylindric Algebras PhD dissertation Hungarian

Academy of Sciences, Budapest, 1993.

                                                                  Cs95

[Cs95] Csizmazia,S. Additions to “Databases and Cylindric Algebras” PhD disser-

tation Hungarian Academy of Sciences, Budapest, 1995.

                                                                  philos

[GG85] Handbook of Philosophical Logic Eds: Gabbay,D. and Guenthner,F.

D. Reidel Publ. Co., Dordrecht, 1985.

                                                                  hm74

[HM74] Henkin,L. and Monk,J.D. Cylindric Algebras and Related Structures Proc.

Tarski Symp., American Math. Society, vol.25, 1974, p105–121.

                                                                  hmti

[HMTI] Henkin,L. Monk,J.D. and Tarski,A. Cylindric Algebras Part I. North–

Holland, Amsterdam, 1971.

                                                                  hmtii

[HMTII] Henkin,L. Monk,J.D. and Tarski,A. Cylindric Algebras Part II. North–

Holland, Amsterdam, 1985.

                                                                  ht

[HT61] Henkin,L. and Tarski,A. Cylindric Algebras In Proceedings of Symp. Pure Math. Vol II. Lattice Theory, American Math. Society, 1961, p83–113. North–Holland, Amsterdam, 1971.

                                                                  jj

[Jo69] Johnson,J.S. Nonfinitizability of Classes of Representable Polyadic Algebras

Journal of Symbolic Logic, vol.34, 1969, p344–352.

                                                                  jo86

[Jó86] Jónsson,B. On Binary Relations In: Proceedings of the NIH Conference on Universal Algebra and Lattice Theory (ed.:Hutchinson,G.) Laboratory of Computer Research and Technology, National Institute of Health, Bethesda, Maryland, 1986, p2–5.

                                                                  lt

[LT36] Lindenbaum,A. and Tarski,A. Über die Beschränktheit der Ausdrucksmittel

deduktiven Theorien Ergeb. Math. Kolloq. vol.7, 1936, p15–22.

                                                                  mo70

[M70] Monk,J.D. On an Algebra of Sets of Finite Sequences Journal of Symbolic

Logic, vol.35, 1970, p19–28.

                                                                  nean

[NA93] Németi,I. and Andréka,H. General Algebraic Logic: A Perspective on What is Logic. In: What is a logical system (ed.:Gabbay,D.) Oxford University Press. To appear.

                                                                  Ne91

[N91] Németi,I. Algebraizations of Quantifier Logics: An Introductory Overview Shortened version in Studia Logica, vol.5(3–4) (a special issue devoted to Algebraic Logic, eds.: Blok,W.J. and Pigozzi,D.L.) 1991, p485–569. Expanded version (with proofs etc.) is Preprint of Math. Inst. Hungarian Academy of Sciences, Budapest, 1996.

                                                                  ne93

[N93] Németi,I. Algebras of Relations of Various Ranks with Applications to Logics Technical Report No.50/1993, Math. Inst. Hungarian Academy of Sciences, Budapest, November 1993. (A much shorter version of this is [N91].)

                                                                  SagNe95

[NS95] Németi,I. and Sági,G. Polyadic Equality Algebras, Their Axiomatizability Issues Preprint of Math. Inst. Hungarian Academy of Sciences, Budapest, November 1995.

                                                                  P

[P73] Pinter,C.C. A Simple Algebra of First Order Logic Notre Dame Journal of

Formal Logic, vol.14(3), 1973.

                                                                  sagi

[Sá95] Sági,G. A Warning on Schemas in Completeness Theorems Manuscript of

Math. Inst. Hungarian Academy of Sciences, Budapest, 1995.

                                                                  SaFIN

[Sa87] Sain,I. On the Search for a Finitizable (w.r.t. the Representables) Algebraization of First Order Logic, Parts i–ii Technical Report No.53/1987, Math. Inst. Hungarian Academy of Sciences, Budapest, 1987. 58pp.

                                                                  S87

[Sa87a] Sain,I. Positive Results Related to the Jónsson, Tarski–Givant Representa-

tion Problem Expanded version of [Sa87], 1987.

                                                                  gabbay

[Sa92] Sain,I. On the Problem of Finitizing First Order Logic and its Algebraic Counterpart (A survey of results and methods) In: Proceedings of Logic Colloquium’92, (eds.: Csirmaz,L. and Gabbay,D.) To appear.

                                                                  S9

[Sa93] Sain,I. On the Search for a Finitizable Algebraization of First Order Logic (Shortened Version A) Preprint of Math. Inst. Hungarian Academy of Sciences, Budapest, 1988, revised in April 1993.

                                                                  bull

[Sa94] Sain,I. On Finitizing First Order Logic Bull. Section of Logic (Wroclaw)

1994. vol.23(2).

                                                                  st

[SaT91] Sain,I. and Thompson,R.J. Strictly Finite Schema Axiomatization of Quasipolyadic Algebras Algebraic Logic, Proc. Conf. Budapest 1988, (eds.: Andréka,H. Monk,J.D. and Németi,I.) Colloq. Math. Soc. J. Bolyai vol.54, North-Holland, Amsterdam, 1991, p539–571.

                                                                  sher

[Sh91] Sher,G. The Bounds of Logic MIT Press, Cambridge, Mass., 1991.

                                                                  whatnot

[Si93] Simon,A. What the Finitization Problem is Not In: Algebraic Methods in Logic and in Computer Science, Proc. Banach Semester Fall 1991, (ed.: Rauscher,C.) Institute of Mathematics, Polish Academy of Sciences, Banach Center Publications vol.28, 1993, p95–116. (Improved version available from author.)

                                                                  tarski

[Ta87] Tarski,A. What are logical notions? In: History and philosophy of logic

(ed.:Corcoran,J.) vol.7 1986, p143-154.

                                                                  tg87

[TaG87] Tarski,A. and Givant,S. A Formalization of Set Theory without Variables

AMS Colloquium publications, vol.41, 1987, Providence, Rhode Island.

                                                                  T

[To93] Thompson,R.J. Complete Description of Substitutions in Cylindric Algebras and other Algebraic Logics Institute of Mathematics, Polish Academy of Sciences, Banach Center Publications, vol.28, 1993, p327–341.

                                                                  wojcicki

[W88] Wójcicki,R. Theory of Logical Calculi (Basic Theory of Consequence Operations) Kluwer Academic Publishers, Dordrecht, 1988.