ON AMALGAMATION OF REDUCTS OF POLYADIC ALGEBRAS

TAREK SAYED AHMED

Abstract. Following research initiated by Tarski,Craig and Nemeti, and further pursued by Sain, we show that for certain subsets G of ^{ω}ω, G polyadic algebras have the strong amalgamation property. G polyadic algebras are obtained by restricting (the similarity type) and axiomatization of ω-dimensional polyadic algebras to finite quantifiers and substitutions in G. Using algebraic logic, we infer that for certain proper extensions of first order logic without equality, the theorems of Beth, Craig and Robinson hold.

Introduction

In this paper we are concerned with proving amalgamation for classes of algebras relevant to algebraic logic. Amalgamation is interesting from a purely algebraic point of view, and in algebraic logic it is proved that amalgamation in classes of algebras corresponds to interpolation properties (like Craig interpolation) in the corresponding logics.

As is often the case in algebraic investigations in general, (and in particular, in algebraic logic), we distinguish between abstract and concrete (or set) algebras. The abstract class of algebras is defined by a simple axiomatization, (usually by equations or quasiequations) in the first order language of a certain fixed similarity type. The concrete class, on the other hand, is given by specifying the universes of the algebras in this class, as sets of certain sets endowed with “set theoretic operations” as interpretations of the symbols in the similarity type of the abstract class. Thus in the concrete case the algebras are completely determined by specifying their universes. In the ideal case, the abstract and concrete classes coincide, in which case we say that we have a Strong Representation Theorem. This is the case for e.g. in boolean algebras, summarised in the celebrated result of Stone:

Every abstract boolean algebra (defined by a set of finite equations) is isomomorphic to a set boolean algebra, equivalently, boolean set algebras are finitely axiomatizable.

Strong Representation Theorems (like Stone’s Theorem) , is proved in algebraic logic, to be equivalent to completeness results in the corresponding logics. In particular, Stone’s theorem, is equivalent to the completeness of proposional logic.

The algebras we deal with are boolean algebras with extra operations, in fact they will be (normal) boolean algebras with operators. These algebras, appropraite for algebraizations of first order logic, are reducts (in the universal algebraic sense) of Halmos’ polyadic algebras

The concrete version of polyadic algebras is defined as follows:

Let U be a set, and α an ordinal. The full polyadic set algebra of dimension α with base U is the algebra

⟨B(^{α}U), S_{τ} , C_{Γ}⟩_{Γ⊆α,τ∈^{α}α}

where B(^{α}U) is the boolean set algebra with unit (greatest element) ^{α}U, and for Γ ⊆ α and τ ∈ ^{α}α, C_{(Γ)} and S_{τ} are unary operations on B(^{α}U) defined (for each X ⊆ ^{α}U) as follows:

C_{(Γ)}X = {s ∈ ^{α}U : there exists z in X such that s_{j} = z_{j} for all j ∉ Γ}

S_{τ} X = {s ∈ ^{α}U : s ∘ τ ∈ X}.

The concrete class of the so called representable algebras of dimension α, α an ordinal, is defined as the class of all subdirect products of full polyadic set algebras of dimension α.

This class is a variety. When α is infinite the class of representable algebras of dimension α can be defined abstractly by a finite schema of equations. This schema is due to Halmos. So for (Halmos’) polyadic algebras of infinite dimension, we have a strong representation Theorem, too.

As indicated in the title, we will be concerned with proving amalgamation for certain reducts of Halmos’ polyadic algebras of infinite dimension, for which the notion of abstract and concrete also coincide, i.e for which a Stone-like Strong Representation Theorem is available. These algebras were introduced by Sain, as one possible solution to the so called finitization problem in algebraic logic.

History and Background

Unless otherwise specified, algebra(s) is short for algebra(s) of infinite dimension.

Polyadic algebras were introduced by Halmos to provide an algebraic reflection of the study of first order logic without equality. Later the algebras were enriched by diagonal elements to permit the discussion of equality. That the notion is indeed an adequate reflection of first order logic was demonstrated by Halmos’ representation theorem for locally finite polyadic algebras (with and without eqaulity). Daigneault and Monk [DM63], proved a strong extension of Halmos’ theorem, namely, every polyadic algebra (without equality) is representable. The latter a typical Stone-like representation theorem , shows that the notion of polyadic algebra is an adequate reflection of Kiesler’s predicate logic (KL).

KL is a proper extension of first order logic without equality, obtained when the bound on the number of variables in formulas is relaxed; and, accordingly, allowing the following as extra operations on formulas: Quantification on infinitely many variables and simultaneous substitutions of (infinitely many) variables for variables. Adding equality to KL, proved problematic as illustrated algebraically by J.S Johnson in [Jo69]. In this paper, Johnson showed that the class of representable polyadic algebras with equality is not closed under ultraproducts, i.e is not even first order axiomatisable. A subtle recent result in this direction is Nemeti- Sagi’s: In sharp contrast to KL , the validities of KL with equality cannot be recaptured by any any set of schemes analogous to Halmos’ schemes , let alone a finite one (cf. [NS98]). In particular, the variety generated by the class of representable polyadic algebras is not finite schema axiomatisable. The latter answers a question of Craig.

It is interesting (and natural) to ask for algebraic versions of model theoretic results, other than completeness, reflected algebraically by Stone-like representability results. A. Diagneault [D63] succeeded in stating and proving versions of Beth’s and Craig’s Theorems. This was done by proving the algebraic analogue of Robinsons consistancy Theorem: Locally finite polyadic algebras (with and without equality) have the amalgamation property. Later Johnson removed the condition of local finiteness, proving that polyadic algebras without equality have the strong amalgamation property [J73].^{1} With this stronger result, Robinson’s, Beth’s and Craig’s theorems hold for KL. It is open whether any of the above (interpolation) properties still hold when we add equality to KL.

KL, though, has negative properties, due to its enormous expressive power. A pecularity of KL proved by Sagi [Sagi 98] is: Though the set of validities can be recaptured by a finite schema, namely Halmos’ schemes, this set is not recursively enumerable.^{2}

1In locally finite algebras, amalgamation is equivalent to strong amalgamation. In the general case, strong amalgamation, is stronger than amalgamation, see below)

The above deep results of Nemeti and Sagi point in the direction of the limited relevance of polyadic theory for “finitary” extensions of first order logic. Tarski’s cylindric algebras, and for that matter Halmos’ quasipolyadic algebras , it seems, are more appropriate for studying such extensions. We will not give a precise definition of finitary, but we think the following is sharp enough to give an intuitive idea. A finitary extension of first order logic, should be structural in the sense of [BP89]. This is necessary to admit algebraic treatment. Probably more important, is that in a finitary extension of first order logic completeness should imply recursive enumerability of the validities; an implication that breaks down for KL for non trivail reasons as shown by Sagi in [Sa98].

Finitary logics of infinitary relations was the name given by Andreka and Nemeti cf. [AN78] to the logics corresponding to the class of representable cylindric algebras and variants thereof like Halmos’ quasipolyadic algebras. In these logics formulas of infinite length are allowed (recall that a formula is a sequence of symbols), the operations though of quantification and substitutions are only restricted to finitely many variables at a time. These logics are refered to as typless logics in [HMT2] sec 4.3, the adjective typeless referring to abstracting away the arity of atomic relation symbols in the formalism. That the set of validities of such logics is recursively enumerable, was proved by Andreka, Gregory and Nemeti in [AGN77]. Unfortunately, the set of validities of these logics cannot be captured by a finite schema in the sense of Monk [M69]. This follows from Monk’s celebrated result: The class of representable cylindric algebras is not finite schema axiomatizable. Monk’s result was generalized to Halmos quasipolyadic algebras (with and without equqality) by I.Sain and J.Thompson [ST91]. These results were considerably sharpened by Andreka [An97] when she showed that any axiomatization of several variants and extensions of the above classes, besides bieng “essentially infinite”, has to be extremely complex.

Also the theorems of Robinson, Beth and Craig fail for such logics. This was proved much earlier, though by Pigozzi [Pi71], when he showed that: Any class of cylindric algebras , containing the representable ones, fail to have the amalgamation property.

The above (both positive and negative) results prompted the search for classes of algebras that lie somewhere between the cylindric paradigm and the polyadic one, so to speak, and at the same time enjoy the positive properties of both.

This problem is one instance of the, so called finitization problem^{3} in Algebraic logic which very roughly states: Find a structural extension of first order logic where the class of algebras associated to this logic is axiomatizable by a nice (simple, mathematically elegant, preferably finite) schema of equations or quasiequations. A harder version of the problem which appeared in Henkin-Monk [74] asks for a strictly finite axiomatization. We quote Henkin-Monk’s formulation of this problem.

Devise an algebraic version of predicate logic in which the class of representable algebras form a finitely based variety.

A Research direction initiated by Craig [Cr74], and further pursued by Sain, Thompson and others, cf.[ST91] and [Sa98] is the following:

2Here of course, one has to be careful as to what “recursively enumerable” means in languages with uncountably many operation symbols. In this connection we refer the reader to [Sagi 98].

3The finitization problem can be traced back to the works of Pierce and Schroder in the last century. Tarski put it on a modern footing in the 40’s. The book [TG86] carries out the project of finitizing set theory by building it in relation algebras (RA). Nemeti carried out a similar task for (SA), the class of semi-associative relation algebras. The finitization problem is the attempt rather to “finitize first order logic”, not only set theory.

Search for these algebras among the continuim many reducts of Polyadic algebras of dimension α, α an infinite ordinal.

Let us be more concrete. Craig observed that for any subset G^{4} of transformations on α, we have a potentially interesting reduct of α dimensional polyadic algebras obtained by restricting the similarity type of the latter to substitutions indexed by elements in G, and to finite quantifiers on α. Such algebras are called α-dimensional G polyadic algebras. (See below, for precise definitions)

Here the ordinal α specifies the length of the sequence of variables available in the corresponding logic. Let it be the least infinite, i.e assume that the sequence of variables in our logic is of order type ω. Fixing the dimension at ω, such algebras will be refered to simply as G algebras. Sain showed in [Sa98], that the Diagneault-Monk representation theorem still holds for various G algebras, pending on the structure of [G], the semigroup generated by G. Abstracting away such properties, Sain called such semigroups rich. An example of a rich semigroup is the full semigroup ^{ω}ω. But ^{ω}ω algebras are amenable to Sagi’s negative results. Another far more interesting example, at least in so far as it survives Sagi’s negative results, is the semigroup generated by the set of finite transformations on ω together with the successor and predecessor functions.

Sain showed that Halmos’ finite shemes restricted to the similarity type of G algebras , does capture the infinity of the validities of the corresponding logic, as long as [G] is rich. Like KL, the corresponding logic, referred to as KL_{G} (KL restricted to G), is a proper extension of first order logic without equality. In this logic, formulas can be of length ω. In addition, to the boolean connectives and usual quantification, (i.e quantification on finitely many variables), the additional (possibly infinitary)^{5} operations of simultaneous substitutions of variables for variables corresponding to the transformations in [G], is allowed. A novel interpretation of [G] algebras, as algebras of sentences in languages with ω individual constants, will be given below. (cf. Remarks 1.12-13, below).

Moreover Sain proved that when [G] happens to be also finitely presented, then Halmos’ schemes can be cut to be strictly finite.

The problem of truly “finitising” first order logic without equality, thus reduces to the following problem in semigroups:

Find a “simple” rich finitely presented semigroup on ω.

In [Sa98] a rich finitely presented semigroup is given, and the question to find simpler such semigroups is posed.

The main results

In this paper, we show when [G] is rich, then G algebras, also have the strong amalgamation property. The main result though will be formulated and proved for the specific rich semigroup, namely the one generated by all finite transformations together with the successor and predecessor functions on ω. This semigroup is rich, but not finitely presented. The proof however easily adapts to arbitrary rich semigroups. (see item (b) in the Concluding Remarks ). Thus for a given set of transformations G as long as [G] is rich , the theorems of Craig Beth and Robinson follow for KL_{G}. Also, for “good” choices of G, KL_{G} can be chosen to be a finitary extension of first order logic as well as an algorithmic reduct of KL. Compactness and (strong) completeness of KL_{G} was already proved by Sain.^{6} We do not know whether any of the above interpolation properties hold when we enrich our language with equality.

4Craig considered semigroups of transformations; for any G he considered the semigroup generated by G. His approach therefore, is often refered to in the literature as the semigroup approach.

5We note that at least one infinitary substitution should exist in our language, for else the logic considered reduces to first order logic without equality.

In preparation of formulating our main result algebraically, we review the basic notions to be used in the sequel. Our notation is mostly standard (see e.g [HMT]or [BS]). Less usual notations will be introduced at their first occurrence in the text. Let X be a set. Then P (X) denotes the set of all subsets (the powerset) of X and B(X) denotes the boolean set algebra with universe P (X). That is B(X) = ⟨P (X), ∩, ∪, −, ∅, X⟩. Let α be an ordinal. Then ^{α}U denotes the set of all U termed sequences of length α. Elements in ^{α}α will be referred to as transformations on α.

Let V ⊆ ^{α}U, i < α and τ ∈ ^{α}α. Then C_{i}^{V} and S_{τ}^{V} are functions from P (V) into itself defined for X ⊆ V as follows:

C_{i}^{V} (X) = {s ∈ V : there exists t ∈ X such that s(j) = t(j) for all j ≠ i};

and

S_{τ}^{V} (X) = {s ∈ V : s ∘ τ ∈ X}.

Here, and elsewhere throughout the paper, composition of functions is defined so that the righthand most function acts first. In particular, s ∘ τ(x) = s(τ(x)). Superscripts are usually omitted. For i ∈ α, C_{i} is called the i-th cylindrification. For τ ∈ ^{α}α, S_{τ} is called the substitution operation corresponding to τ, or simply a substitution.

Let U be a set and p ∈ ^{α}U. Then ^{α}U^{(p)} denotes the set

{s ∈ ^{α}U : {i ∈ α : s_{i} ≠ p_{i}} is finite }.

αU^{(p)} is more commonly referred to in the literature as the weak space of dimension α, determined by p. U is called its base (cf. [HMT1] Def. 3.1.5).

Now we turn to defining certain expansions of boolean set algebras, that are also reducts of Halmos’ polyadic algebras. The units of such algebras are unions of weak spaces of dimension α, and their elements are α-ary relations. The operations, besides the familiar boolean set operations, are the extra operations of cylindrifications and substitutions indexed by a fixed set G of transformations on α. In our subsequent discussion we will impose further restrictions on α and G.

Definition 0.1 Concrete G algebras

Let α be an ordinal and G ⊆ ^{α}α.^{7}By a G polyadic set algebra of dimension α, a GP SA_{α} for short, we understand a subalgebra:

A ⊆ ⟨B(V), C_{i}, S_{τ} ⟩_{i∈α,τ∈G}

6Other model theoretic properties of such logics like omitting types is investigated in [S99].

7When G is empty then the class of G set algebras reduces to the case of the so called diagonal free cylindric algebras, the theory of which is well developed, see e.g. [HMT2]. We will be primarily concerned with the case when α = ω (the least infinite ordinal) and a specific set of transformations G on ω, to be specified shortly. We should mention that Definition 0.1, in this general form, covers almost all CA-like diagonal free algebras of relations, where CA abbreviates cylindric algebras. These include Pinter’s algebras and Halmos’ quasipolyadic algebras, cf. [Sa91].

where V, the unit of A, is a union of weak spaces having a common base U, i.e. V is of the form ∪_{i∈I}^{α}U^{(p_{i})}, for a non-empty set I, and U termed sequences p_{i} (i ∈ I). V as indicated above, is one instance of a compressed space in the sense of [HMT2] Def. 3.1.5.^{8}

Following the conventions of the monograph [HMT], GP SA_{α} also stands for the class of all GP SA_{α}’s. When α is clear from context, we refer to GP SA_{α}’s as G set algebras or concrete G algebras. Here “concrete” refers to the facts that elements of the algebras are real α-ary relations and the operations are set theoretic ones.^{9}

We will show that for a particular G ⊆ ^{ω}ω, the class GP SA_{ω} has the strong amalgamation property.

To formulate our main result, we recall from [Pi71] the notion of strong amalgamation, then we specify the set G (of transformations on ω) that we shall be exclusively dealing with.

Definition 0.2

Let K be a class of algebras. Then K is said to have the amalgamation property, if for any A, B, C ∈ K, and any monomorphisms f, g of A into B, C respectively, there exists D and a monomorphism m from B into D and a monomorphism n from C into D such that m ∘ f = n ∘ g. If, in addition m(B) ∩ n(C) = mof(A), then K is said to have the strong amalgamation property.

Notation. Let α be an ordinal and i, j ∈ α. Then [i|j] denotes the replacement that maps i to j and leaves the rest of the elements of α fixed. suc is short for the successor function on ω. That is suc(i) = i + 1, for every i ∈ ω. pred is short for the predecessor function on ω, i.e. pred(0) = 0 and pred(i) = i − 1 for i ∈ ω ∖ {0}.

For a class K of algebras IK stands for the class obtained by taking all isomorphic copies of K. Now we are ready to formulate our main result:

Theorem 1 (Main Theorem). Let G = {[i|j] : i, j ∈ ω} ∪ {suc, pred}. Then IGP SA_{ω} has the strong amalgamation property.

Unless specified to the contrary, G is as specified in Theorem 1. To prove Theorem 1, we shall show that the countable IGP SA_{ω} free algebras satisfy the algebraic version of Craig’s interpolation property. To formulate (and justify) the latter we further need:

Notation. Given a class K and a set X F r_{X}K, denotes the K algebra freely generated by X. Recall that F r_{X}K is determined up to isomorphism by |X| and K. Henceafter, however, when we write F r_{X}K, we shall be tacitly assuming that X ⊆ F r_{X}K.

Let A be an algebra and X ⊆ A. Then Sg^{A}X or simply SgX, when A is clear from context, denotes the subalgebra of A generated by X.

8The choice of units in this form is not haphazard. The reader is referred to [Sa98] for a fuller discussion of the reasons of this choice. One important reason, but not the only one, is that this choice of units makes our algebras boolean algebras with operators, or BAOs, for short.

9Later we will define abstract G algebras. These will be defined by a set of equations valid in the (more)

concrete ones.

Definition 0.3

Let K be a class of algebras with a boolean reduct^{10} and X be a set. Then F r_{X}K is said to have the interpolation property if whenever X_{1}, X_{2} ⊆ X, a ∈ SgX_{1} and c ∈ SgX_{2} are such that a ≤ c, then there exists b ∈ Sg(X_{1} ∩ X_{2}) such that a ≤ b ≤ c. Here ≤ is the usual boolean ordering.

As previously noted, the above is the algebraic counterpart of the Craig interpolation property in logic. Accordingly we refer to b as an interpolant of a and c

The following fact, essentially due to [Maksimova], is the cornerstone on which our proof relies.

Fact 0.4. Let K be a variety with a countable signature. Suppose further that every A ∈ K is a normal boolean algebra with unary operators, briefly a BAO . Then the following two conditions are equivalent:

(i) F r_{X}K has the interpolation property, for every countable X

(ii) K has the super amalgamation property.

The notion of super amalgamation introduced by Maksimova is actually stronger than strong amalgamation. The fact that IGP SA_{ω} is a variety was proved by Sain in [Sa98]. In fact in Definition 1.2 below we shall exhibit a set of equations (also due to Sain) axiomatizing IGP SA_{ω}, asserting among other things that every A ∈ IGP SA_{ω} is a BAO. To show that IGP SA_{ω} has the strong (and indeed the super) amalgamation property it is enough, in view of fact 0.4, to prove:

Proposition 1

Let X be countable. Then F r_{X}(IGP SA_{ω}) has the interpolation property.

Organization.

Section 1 is devoted to proving proposition 1 (and Theorem 1). The proof of proposition 1, is preceded by an informal outline stressing on its metalogical source, as an instance of Robinson’s methods of finite forcing in Model Theory. The proof, proper, is purely algebraic.

In section 2 (Concluding remarks) we discuss the scope of the applicability of our proof (for other Gs, i.e. other reducts of polyadic algebras). Since the story was often told elsewhere (see e.g. [Pi72],[Sa89],[Marx98] and [Mad98]), we only briefly hint on the logical implications mentioned in the abstract. Finally in item (c) we highlight a property^{11}) that played an essentail role in the proof of Theorem 1. We also work out a context in which such a property seems to be equivalent to strong amalgamation. In the present (more restrictive) framework, this property implies strong amalgamation.

10The greatest and least elements are explicit in the similarity type of boolean algebras. In particular, SgX containing at least these elements, is not empty for any X.

11This property is abbreviated by (*) in the informal outline of the proof , and proved in claim 1.15 below.

It reflects the fact that neat reducts commute with forming subalgebras.

Section 1.

In this section we prove Proposition 1. First we define an abstract class of G algebras satisfying a set of equations denoted by (P_{1} −P_{10}) below which are valid in the corresponding class of concrete G algebras. When G is as specified in Theorem 1, then this set of equations is an adequate axiomatisation of IGP SA_{ω}, in the sense that if A ⊧ (P_{1} − P_{10}), then A is isomorphic to a G set algebra. The latter, a typical Stone-like representability result, was proved by Sain [Sa98]. Actaully, the proof of Proposition 1 will be carried out for the variety Mod(P_{1} − P_{10}).^{12}

In our formulation of abstract G algebras of dimension α, we allow as extra (yet term definable) operations those substitutions which are indexed by transformations in the subsemigroup of ⟨^{α}α, ∘⟩ generated by G. So before postulating (P_{1} − P_{10}), we recall from [Sa98] some basic semigroup theoretic notation.

In the following notation, and Definition 1.1 no conditions whatsoever are assumed on α nor on G. Restrictions on G will be imposed in due time. In harmony with the notation of [HMT], we use +, ., −, 0, 1, c_{i}, s_{τ} (τ ∈ G) to denote the function symbols of the similarity type of G set algebras.

Notation. Let X be a set. Then Id_{X}, or simply Id when X is clear from context denotes the identity function on X. Let α be an ordinal and G ⊆ ^{α}α. Then ⟨[G], ∘⟩, or simply [G] denotes the subsemigroup of ⟨^{α}α, ∘⟩ generated by G.

G^{∗} denotes the set of all finite words on G, i.e. G^{∗} = ∪_{n∈ω}^{n}G. For u, w ∈ G^{∗}, u^{∩}w, or simply uw, denotes the concatenation of u and w. Recall that G^{∗} is the free semigroup generated by G. We let ˆ : G^{∗} → [G] denote the unique anti-homomorphism extending Id : G → [G].

Definition 1.1

Let w ∈ G^{∗}. Suppose that w = ⟨w_{0}, ⋯, w_{n−1}⟩, with w_{i} ∈ G. Then s_{w}(x) denotes the unary term s_{w_{n−1}}(⋯ (s_{w_{0}}(x)) ⋯) of the language of GP SA_{α}.

Σ_{G} denotes the following set of equations (easily seen) to be valid in GP SA_{α}:

Σ_{G} := {s_{u}(x) = s_{w}(x) : u, w ∈ G^{∗} and uˆ = wˆ }.

When Σ_{G} holds in a class K of algebras similar to GP SA_{α}, then for any A ∈ K and τ ∈ [G], we can correlate a unary operation s_{τ} on A determined by the following stipulation:

If τ = τ_{0} ∘ ⋯ ∘ τ_{n−1}, with τ_{i} ∈ G, then

s_{τ}^{A}(x) = s_{τ_{0}}^{A}(⋯ (s_{τ_{n−1}}^{A}(x)) ⋯).

By Σ_{G} holding in K and A ∈ K, s_{τ}^{A}(x) is well defined.

Convention

12Here Mod is short for “the class of all models of”.

Accordingly we do not distinguish between an algebra in the class IGP SA_{α}, and its expansion obtained by allowing substitutions corresponding to elements in [G] − G which are, as indicated above, term definable.

Now we turn to defining the abstract class of G algebras. In Definition 1.2 we assume that α is an arbitrary infinite countable ordinal and G is a set

of transformations on α containing all replacements. That is {[i|j] : i, j ∈ α} ⊆ G.^{13}

Definition 1.2 Abstract G algebras

By an abstract G polyadic algebra of dimension α, a GP A_{α} for short, we understand an algebra of the form

A = ⟨A, +, ., −, 0, 1, c_{i}, s_{τ} ⟩_{i∈α,τ∈[G]}

where c_{i} (i ∈ α) and s_{τ} (τ ∈ [G]) are unary operations on A such that postulates (P_{1} − P_{10}) below hold for τ, σ ∈ [G] and all i, j, k, ∈ α.

(P_{1}) ⟨A, +, ., −, 0, 1⟩ is a boolean algebra, henceafter denoted by BlA. (P_{2}) 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. In other words c_{i} is an additive closure operator, and c_{i}, c_{j} commute. (P_{3}) s_{τ} is a boolean endomorphism. (P_{4})Σ_{G}. In particular s_{τ} s_{σ}x = s_{τ∘σ}x and s_{Id}x = x. (P_{5})s_{τ} c_{i}x = s_{τ[i|j]}c_{i}x. Here τ[i|j] is the transformation that agrees with τ on α − {i} and τ[i|j](i) = j. (P_{6}) s_{τ} c_{i}x = c_{j}s_{τ} x if τ^{−1}(j) = {i}. (P_{7}) c_{i}s_{[i|j]}x = s_{[i|j]}x. (P_{8}) s_{[i|j]}c_{i}x = c_{i}x. (P_{9}) s_{[i|j]}c_{k}x = c_{k}s_{[i|j]}x whenever k ∉ {i, j}. (P_{10}) c_{i}s_{[i|j]}x = c_{j}s_{[j|i]}x.

We often write s_{i}^{j}x instead of s_{[i|j]}x. Also, for better readability, , or if there is likelihood of confusion, we write s_{τ} (x) instead of s_{τ} x.

Remarks on Definition 1.2

a. We should point out that (P_{1} − P_{10}) are not independent. In fact, (P_{8} − P_{10}) are easily derivable from the rest, as the reader is invited to show. Also note that Σ_{G} is in fact an infinite set of equations. When G consists only of replacements, or G consists of finite transformations, then Σ_{G} can be, and is indeed considerably simplified in [ST91]. There G algebras are also presented as systems of varieties definable by Monk’s schemes. (See also [HMT2] p.260-263.)

b. Algebras satisfying (P_{1} − P_{10}) will be henceafter referred to as abstract G algebras, being abstractions from the more concrete GP SA_{α}’s. That is if A ∈ IGP SA_{α}, then A ⊧ (P_{1} − P_{10}).^{14} (P_{1} − P_{10}), loosely speaking, the restriction of Halmos’ schemes (cf. [HMT2] Def.5.4.1) to finite quantifiers and substitutions indexed by transformations in G, are actually designed to force algebras satisfying them to be representable as concrete G algebras. Pending on G of course, it turns out that the relation of the abstract to the concrete is unfortunately not as close as we wish. A result of Sain and Thompson (cf. [ST91]) (extending a result of Johnson [J69]) is that when G consists of finite transformatons only, then G set algebras are not even finite schema axiomatisable in the sense of [M69] over Σ_{G}. In particular, there are abstract G algebras that are not representable.

13We chose to restrict ourselves to infinite α, because we are only interested in infinite dimensional algebras.

Nevertheless, Definition 1.2 makes perfect sense for finite α. For e.g. when G consists only of replacements on α, then the G algebras coincide with Pinter’s algebras. When G consists of replacements and transpositions then the G algebras coincide with Halmos’ quasipolyadic algebras. Such equivalences are worked out systimatically for e.g.in [Sa91], for finite as well as infinite α.

However when we start putting infinitary substitutions in G, switching to the polyadic paradighm so to speak, we get strong representability results as shown by Sain in [Sa98].

In fact our research was inspired by the following strong representability result of Sain [SaG96]. When G = {[i|j] : i, j ∈ α} ∪ {suc, pred}, then every abstract G algebra is representable, i.e. isomorphic to a set algebra. There a simpler set of axioms is also given.^{15}

Sain’s proof in [Sa98] appeals to a Neat Embedding Theorem (cf. [HMT1]) and has a wide range of applicability, certainly wider than the G as specified in our Theorem 1. The techniques of Sain will be used and further elaborated upon in the proof of proposition 1. In Section 2 we show that our theorem remains valid, for those Gs for which G abstract algebras are representable. More concisely, we show that when [G] happens to be rich in the sense of [Sa98], then G algebras have the strong amalgamation property. In particular, our result also applies to those G’s for which [G] is rich and finitely presented over G (cf. [Sa98]). For these algebras (the similarity type) and axiomatisation in Definition 1.1 can be cut to be strictly finite. As mentioned in the introduction, this provides a solution to one version of the so called finitization problem in algebraic logic. We refer the reader to [Ne96] for an extensive survey of the finitization problem. [Sagi 98] is devoted to this problem alone.

We first give an informal outline of the idea of the proof, stressing on its metalogical source. A novelty that occurs here is the likening of the neat embedding Theorem to Henkin’s methods of constructing models from constants.

To emphasize on the strong tie with logic, we borrow terminology and concepts from Model Theory. We start off with the algebraic counterpart of the notion of satisfiability. This is folklore (see [HMT2] sec 4.3) in algebraic logic.

Definition 1.3

Let A be an abstract G algebra, and a a non-zero element in A. A model of (A, a) is a homomorphism h from A into a G set algebra such that h(a) is non-empty.

Note that an abstract A is representable, i.e isomorphic to a set algebra, iff for every non-zero a ∈ A, (A, a) has a model.

Definition 1.4 Let A be an abstract G algebra.

14This is a soundness condition expressed algebraically for logics corresponding to GP A_{α} in the sense of [ANKS]. If the units of the algebras in Definition 0.1 were broadened to allow any α-ary relations (better known in the literature as Crs units), then it is easy to construct examples violating the above set of axioms.

We refer to [Sa98] for a fuller discussion on this particular choice of units.

15The logical implications, being a strong completeness (and compactness) for the corresponding logic, is also worked out. This logic, as noted in the introduction, is a proper extension of first order logic without equality.

Theorem 1, will show that for this logic the famous theorems of Beth, Craig and Robinson also hold.

(a) Let a ∈ A. Then Δa, referred to as the dimension set of a, (cf. [HMT1]) is the set {i ∈ α : c_{i}a ≠ a}. Let β ≤ α, then a is β-dimensional if Δa ⊆ β.

The following Definition singles out certain boolean ultrafilters in G algebras. These ultrafilters correspond to the notion of Henkin’s complete rich theories (cf. [CK91]), hence the notation.

(b) Let F be a boolean ultrafilter of A. Then F is called a Henkin ultrafilter^{16} if whenever c_{i}a ∈ F, then there exists j ∉ Δa such that s_{[i|j]}a ∈ F.

Now we are ready to give an informal outline of the idea of the proof. It is a typical Henkin construction, or rather the algebraisation thereof. It is otherwise and also better known in Model Theory as the method of constructing models out of constants.

An outline of the proof of Proposition 1

As is standard practice, from now on we do not distinguish between an algebra A and its universe A, and denote both of them by latin letters.

Let X be a countable set. For brevity set A = F r_{X}(GP A_{ω}). Let X_{1}, X_{2} ⊆ X. Let a ∈ SgX_{1} and c ∈ SgX_{2} be such that A ⊧ a ≤ c. We must show that there exists an interpolant of a and c, i.e. some b ∈ Sg(X_{1} ∩ X_{2}) such that A ⊧ a ≤ b ≤ c.

The proof goes by contradiction. We assume no such b exists. Then we construct a model of a − c. This contradicts A ⊧ a ≤ c. We devide the proof into three parts (i), (ii) and (iii). Using Hodges terminology [Ho85], in parts (i) and (ii) we force with A, preparing for constructing the model. This is done by adding enough supply of witnesses, in preparation of defining a notion of forcing. Algebraically we neatly embed A into ω extra dimensions. The neat embedding part is done in part (i). In part (ii) we define a notion of forcing and construct appropriate Henkin ultrafilters. In part (iii) we construct the desired model out of these ultrafilters.

Part (i) Adding witnesses

In this part we follow [Sa98]. We neatly embed A into ω extra dimensions. That is we view A as “living” in a bigger ω + ω -dimensional algebra A^{+}, in the sense that A can be embedded in an appropriate subreduct of A^{+}. This subreduct, referred to below as Rd_{ω}A^{+}, is loosely speaking obtained by restricting the similarity type of A^{+} to the first ω dimensions. Moreover A can be neatly embedded into A^{+}, or A is embeddable in the neat ω-reduct of A^{+}, referred to below as Nr_{ω}A^{+}. A novelty that occurs here is that we show that A^{+} is a minimal extension of A in the following sense: No new ω-dimensional elements of A^{+} are definable from A even in the presence of the ω extra operations of A^{+}. Formally: (*)

A ⊆ Nr_{ω}A^{+} and for all X ⊆ A we have Sg^{A}X = Nr_{ω}Sg^{A^{+}}X.

16Such ultrafilters, never in this name though, have appeared frequently in the literature in the context of proving representability result. To mention a few, see for e.g.[AN75], [AGN77], [Pi71], [DM63]. More recent references include the mongraph [HMT] ,[S97], [F98], and [Sa98]. This is hardly surprising, since representability corresponds to completeness in algebraic logic (cf. [ANKG])

Here Nr_{ω} is an operator, which when applied to subsets of A^{+} only keeps the ω-dimensional ones, and throws away the rest. We point out that (*) is crucial. By (*) we are sure that no interpolant of a and c exists even in Sg^{A+}(X_{1} ∩ X_{2}). This will be the base of defining a notion of forcing in part (ii). (*) will be further elaborated upon in the conclusion. Also the algebraic process of neat embeddability will be compared to the metalogical process of adding constants (or witnesses) in Remark below.

Part (ii) Defining a notion of forcing

Using the omega extra dimensions, we extend a and −c to Henkin ultrafilters F_{1} and F_{2} of the bigger algebra A^{+}. In forcing terminology such ultrafilters are called generic. F_{1} and F_{2} are constructed in a step-by-step fashion to agree on Sg^{A^{+}}(X_{1}∩X_{2}), with (*) providing a base of this construction. That is for all x ∈ Sg^{A^{+}}(X_{1} ∩ X_{2}) we have x ∈ F_{1} if and only if x ∈ F_{2}. Borrowing terminology from [CK91], F_{1} and F_{2}, so constructed, may be called inseparable Henkin extensions of a and −c. In this part of the proof we closely follow [Pi71].^{17}

Part (iii) Forming a model of a − c

In this part we build a model of a − c. We assume that X_{1} ∪ X_{2} = X. Again following [Sa98], we form a model of (Sg^{A}X_{1}, a) corresponding to F_{1} and another of (Sg^{A}X_{2}, −c) corresponding to F_{2}. In the construction of such models, we make explicit use of the extra ω dimensions, or the ω new operations of A^{+}. This consists of forming the so called canonical models of the rich complete theories corresponding to F_{1} and F_{2}. This is standard practice in Model Theory. Now the freeness of A comes in. Together with the fact that F_{1} and F_{2} agree on Sg^{A^{+}}(X_{1} ∩ X_{2}), we are able to paste these models, constructing a model of (Sg^{A}(X_{1} ∪ X_{2}), a − c) = (A, a − c).

17As a matter of fact, our proof on the whole is very similar to Pigozzi’s proof that the class of the so called Dimension complemented cylindric algebras have strong amalgamation w.r.t. the representables. (cf. [Pi71] for Definitions) . Both proofs can be traced back to Henkin’s proof of Craig’s classical interpolation Theorem for F OL, proved earlier by Craig. This is a typical example of the fruitfulness of the algebraization of a metalogical proof, so that the algebraization has a broader application than the proof it had originated from.

Needless to say, this says something about Henkin’s deep method of constructing models from constants.

Details of the proof

Throughout the proof G stands for the set {[i|j] : i, j ∈ ω} ∪ {suc, pred}. In parts (i) and (ii) A is an arbitrary countable G abstract algebra. It is only in part (iii) that we assume that A is the free algebra on some countable set.

The following notation will be used extensively in the proof: Let f : B → C, be a function from B into C. Let X ⊆ B. Then f ↾ X denotes the restriction of f to X. f(X) denotes the image of X under f, i.e f(X) = {f(x) : x ∈ X}. We let Rngf denote f(B), the range of f. Let Y ⊆ C. Then f^{−1}Y = {x ∈ B : f(x) ∈ Y }. We write f^{−1}y instead of f^{−1}{y}. Assume that B = C. Then f^{n} stands for the function f ∘ f ⋯ ∘ f, n times. Recall that for a set X, Id_{X} or simply Id , when X is clear from context, denotes the identity function on X. |X| stands for the cardinality of X.

Details of part (i)

In part (i) we follow almost literally [Sa98] sec 2.2. The strategy is: We neatly embed A into arbitrary finite extra dimensions, then using ultraproducts we neatly embed A into ω extra dimensions. We should warn the reader, though, that we deliberately chose to devaite from [Sa98] in two respects:

(1) We consider a specific semigroup namely the one generated by G. While In [Sa98], the proof is carried out for any rich semigroup^{18} in the sense of [Sa98]. The proof adopted herein, however adapts easily to the more general context of rich semigroups.

(2) Sain was concerned with choosing a minimal set of operations generating all the rest. However in our formulation of G algebras we allow term definable operations (like substitutions indexed by transformations in [G] − G) as basic ones.

By this the proofs, which we include in some detail - even when easily recovered from those available in [Sa98] - are usually simpler and sometimes even slightly different. Proofs that have appeared in [Sa98] in the more general context of rich semigroups, will of course be credited to Sain.

By doing this, we hope that the present paper is self contained and that the reader with no access to [Sa98], should have no difficulty figuring out what is going on.

We start off by fixing some notation:

Notation. T denotes [G] the semigroup generated by G. Let n ≤ ω. Then α_{n} = ω + n and M_{n} = α_{n} ∖ ω. Note that when n ∈ ω, then M_{n} = {ω, ⋯, ω + n − 1}. Let τ ∈ T. Then τ_{n} = τ ∪ Id_{M_{n}}. T_{n} denotes the subsemigroup of ⟨^{α_{n}}α_{n}, ∘⟩ generated by {τ_{n} : τ ∈ T } ∪ ∪_{i,j∈α_{n}}{[i|j], [i, j]}. For n ∈ ω, we let ρ_{n} : α_{n} → ω be the bijection defined by ρ_{n} ↾ ω = suc^{n} and ρ_{n}(ω + i) = i for all i < n.

Claim 1.1. (a) Let n ∈ ω. For v ∈ T_{n} let v′ = ρ_{n} ∘ v ∘ ρ_{n}^{−1}. Then v′ ∈ T.

(b)For τ ∈ T_{ω}, let D_{τ} = {m ∈ M_{ω} : τ^{−1}(m) = {m} = {τ(m)}}. Then |D_{τ} | < ω.

The proofs of (a) and (b) are given in [Sa98] sec2.2, in the more general context of rich semigroups. (a) and (b) are also straightforward to check from the definitions. Here we give a sketch of (a). Let n ∈ ω. Since (vou)′ = v′ou′, it suffices to check that v′ ∈ T for every v in a generating set of T_{n}. Let i, j ∈ α_{n}. Then [i|j]′ = [ρ_{n}(i)|ρ_{n}(j)]. Similarly for replacements. Let v = suc^{n}oId_{M_{n}}. Let x ∈ ω. Then it is not hard to check that v′(x) = x if x < n and v′(x) = suc^{n}(x) otherwise. Thus v′ = [n + n|n] ∘ ⋯ ∘ [n|0] ∘ suc^{n} ∈ T. The case when v = pred^{n} ∪ Id_{M_{n}} is similar.

18We’d rather not burden the reader with the definition of a rich semigroup. For all that matters, a rich semigroup is basically one that contains all finite transformations together with a suc-like element, and its quasi-inverse, a pred-like one.

From now on, unless specified to the contrary, n is a fixed finite ordinal, α_{n}, M_{n}, T_{n}, ρ_{n} are as indicated above, and A is an arbitrary countable G algebra.

Now let A_{n} be the algebra defined as follows:

A_{n} = ⟨A, +, ., −, 0, 1, c_{i}^{A_{n}}, s_{v}^{A_{n}}⟩_{i∈α_{n},v∈T_{n}}

where for each i ∈ α_{n} and v ∈ T_{n},

c_{i}^{A_{n}} := c_{ρ_{n}(i)}^{A} and s_{v}^{A_{n}} := s_{v′}^{A}.

Note that A_{n} has the same universe as A. In fact BlA_{n} = BlA. Each non boolean operation of A_{n}, though, is obtained by renaming an operation of A. For e.g (for n > 0) we have c_{ω}^{A_{n}} = c_{0}^{A}. Following terminology of [HMT1] Def. 2.6.1 for cylindric algebras, A_{n} may be called the ρ_{n} − reduct of A. It is tedious but absolutely straightforward to show that A_{n}, so defined, satisfies (P_{1} − P_{10}) of Defintion 1.1 by replacing G by T_{n} and α by α_{n}. Let Rd_{ω}A_{n} be the following reduct of A_{n} obtained by restricting the type of A_{n} to the first ω dimensions:

Rd_{ω}A_{n} = ⟨A_{n}, +, ., −, 0, 1, c_{i}^{A_{n}}, s_{τ_{n}}^{A_{n}}⟩_{i∈ω,τ∈T} .

Now Rd_{ω}A_{n} has the same similarity type and universe of A. The boolean operations are the same. The extra non boolean ones, though are ρ_{n} shifted, so to speak.

For x ∈ A, let e_{n}(x) = s_{suc^{n}}^{A}(x). Then e_{n} : A → A_{n}.

Claim 1.2. (Sain) e_{n} is an isomorphism from A into Rd_{ω}A_{n}.

(i) e_{n} preserves the boolean operations because by (P_{3}) we have s_{suc^{n}}^{A} is a BA endomorphism, and BlA = BlA_{n}.

(ii)We check that e_{n} preserves cylindrifications.

Let x ∈ A and i ∈ ω. Then, by definition, we have e_{n}(c_{i}^{A}x) = s_{suc^{n}}^{A}c_{i}^{A}x.

Let j = suc^{n}(i). Then j = suc^{n}(k) iff k = i, because suc, hence suc^{n}, is one to one. Applying (P_{6}) we get e_{n}(c_{i}^{A}x) = s_{suc^{n}}^{A}c_{i}^{A}x = c_{j}^{A}s_{suc^{n}}^{A}x. By ρ_{n} ↾ ω = suc^{n} and i ∈ ω we have ρ(i) = suc^{n}(i) = j. Thus by the definition of e_{n} and the above we get

e_{n}(c_{i}^{A}x) = c_{j}^{A}s_{suc^{n}}^{A}x = c_{ρ_{n}(i)}^{A}e_{n}(x) = c_{i}^{A_{n}}e_{n}(x) = c_{i}^{Rd_{ω}A_{n}}e_{n}(x).

(iii) We check that e_{n} preserves substitutions.

First of all note that suc^{n}oτ = τ′_{n}osuc^{n} for all τ ∈ T. Indeed let x ∈ ω. Then suc^{n} ∘τ(x) = τ(x) + n. On the other hand, a direct computaton gives:

(τ_{n})′ ∘ suc^{n}(x) = ρ_{n} ∘ τ_{n} ∘ ρ_{n}^{−1} ∘ suc^{n}(x) = ρ_{n} ∘ τ_{n}(x) = ρ_{n} ∘ τ(x) = suc^{n}(τ(x)) = τ(x) + n.

Now let τ ∈ T and x ∈ A. Computing we get by the definition of e_{n}, (P_{4}) and the above that e_{n}(s_{τ}^{A}x) = s_{suc^{n}}^{A}(s_{τ}^{A}x) = s_{suc^{n}∘τ}^{A} (x) = s_{τ′_{n}∘suc^{n}}^{A}(x) = s_{τ′_{n}}^{A}(s_{suc^{n}}^{A}x) = s_{τ}^{Rd_{ω}A_{n}}e_{n}(x)

We have proved that e_{n} preserves substitutions. (iv) e_{n} is one to one. Let x ∈ A. Assume that e_{n}(x) = 0. We will show that x = 0. By (P_{3}), and (P_{4}) upon noting that pred^{n} ∘ suc^{n} = Id, we get 0 = s_{pred^{n}}^{A}e_{n}(x) =

s_{pred^{n}}^{A}s_{suc^{n}}^{A}(x) = s_{pred^{n}∘suc^{n}}^{A}(x) = s_{Id}x = x.

Notation. For Y ⊆ A_{n} = A, we let Nr_{ω}Y denote the set of all ω dimensional elements in Y, that is Nr_{ω}Y = {a ∈ Y : c_{i}^{A_{n}}a = a for all ω ≤ i < ω + n}. Since c_{ω+i}^{A_{n}}a = c_{i}^{A}a for all i < n and a ∈ A, it follows that Nr_{ω}Y = {a ∈ Y : c_{i}^{A}a = a for all i < n}.

Claim 1.3. e_{n}(Sg^{A}Y) = Nr_{ω}(Sg^{A_{n}}e_{n}(Y)) for all Y ⊆ A.

Proof: Let Y ⊆ A. We first show that e_{n}(Sg^{A}Y) ⊆ Nr_{ω}(Sg^{A_{n}}e_{n}(Y)). This part of the proof is due to Sain.^{19} Towards this let y ∈ e_{n}(Sg^{A}Y). Then y = e_{n}(a) say with a ∈ Sg^{A}(Y). We will show that y ∈ Nr_{ω}A_{n}, i.e c_{m}^{A_{n}}y = y for all m ∈ M_{n}, by which we will be done, since Nr_{ω}A_{n} ∩ e_{n}(Sg^{A}Y) = Nr_{ω}e_{n}(Sg^{A}Y). So let m ∈ M_{n} = {ω, .., ω + n − 1}. From ρ_{n}(m) ∈ {0, ...n − 1}, i.e ρ_{n}(m) ∉ Rng(suc^{n}), it follows that [ρ_{n}(m)|j] ∘ suc^{n} = suc^{n}, for any j ∈ ω. Together with (P_{4}) and (P_{7}) we get for any j ∈ ω:

c_{m}^{A_{n}}y = c_{ρ_{n}(m)}^{A}s_{suc^{n}}^{A}(a) = c_{ρ_{n}(m)}^{A}s_{[ρ_{n}(m)|j]∘suc^{n}}^{A}(a) = s_{[ρ_{n}(m)|j]osuc^{n}}^{A}(a) = s_{suc^{n}}^{A}(a) = e_{n}(a) = y. We have shown that c_{m}^{A_{n}}y = y for each m ∈ M_{n}, thus y is as desired. Now we prove the other inclusion, namely that, Nr_{ω}(Sg^{A_{n}}e_{n}(Y)) ⊆ e_{n}(Sg^{A}Y). This part

of the proof is new.

Let y ∈ Nr_{ω}Sg^{A_{n}}e_{n}(Y). Then y ∈ Sg^{A_{n}}e_{n}(Y). Let a = s_{pred^{n}}^{A}(y). We will show that e_{n}(a) = y and that a ∈ Sg^{A}Y by which we will be done. We start by showing that e_{n}(y) = a.

For brevity, let c_{(n)}x abbreviate c_{0} ⋯ c_{n−1}x. Since y ∈ Nr_{ω}Sg^{A_{n}}e_{n}(Y), we get c_{i}^{A}y = y for all i < n, i.e. c_{(n)}^{A}y = y. Together with the definition of e_{n} and (P_{4}) we obtain

e_{n}(a) = s_{suc^{n}}^{A}(s_{pred^{n}}^{A}y) = s_{suc^{n}∘pred^{n}}^{A}c_{(n)}^{A}y.

Note that suc ∘ pred = [0|1]. Also suc ∘ [i|j] = [i + 1|j + 1] ∘ suc for all i, j ∈ ω. This is absolutely straightforward. It then follows, implementing a straightforward induction, that

suc^{n} ∘ pred^{n} = [n − 1|n] ∘ ⋯ ∘ [0|1].

Thus by (P_{4}) we have e_{n}(a) = s_{[n|n−1]}^{A}(⋯ (s_{[0|1]}^{A}(c_{(n)}^{A}y) ⋯). Now appealing to (P_{8}) and (P_{9}) we get that e_{n}(a) = c_{(n)}^{A}y = y.

It thus remains to show that a = s_{pred^{n}}y ∈ Sg^{A}Y. Towards this end, we define inductively the sequence ⟨Y_{k} : k ∈ ω⟩ as follows: Y_{0} = e_{n}(Y) ∪ {0, 1} and for k ≥ 0, we set Y_{k+1} = Y_{k} ∪ {f^{A_{n}}(x): f is an i-ary operation of A_{n}, i ∈ {1, 2} and a ∈ ^{i}A}.

19The formulation in [Sa98] is slightly different, though. For eg, there the notation Nr_{ω} which we borrow from cylindric algebras, cf [HMT1] Def.2.6.28, is never used. Other than this formal distinction the proof is the same.

Case (i). y ∈ Y_{0}, then either y = e_{n}(y′) for some y′ ∈ Y or y ∈ {0, 1}. If y ∈ {0, 1}, then by (P_{3}) we have a = s_{pred^{n}}^{A}y ∈ {0, 1}, hence a ∈ Sg^{A}Y. If y = e_{n}(y′) for some y′ ∈ Y, then by (P_{4}), upon noting that pred^{n} ∘ suc^{n} = Id, we get

a = s_{pred^{n}}^{A}e_{n}(y′) = s_{pred^{n}∘suc^{n}}^{A}(y′) = s_{Id}y′ = y′ ∈ Y ⊆ Sg^{A}Y.

Case (ii). y ∈ Y_{k+1} for some k ∈ ω. If y ∈ Y_{k}, then y ∈ Sg^{A}(Y) by induction hypothesis, and so a = s_{pred^{n}}^{A}y ∈ Sg^{A}Y, as well.

Assume thus that y = f^{A_{n}}(x), where x ∈ ^{i}Y and i ∈ {1, 2}. If f is a BA operation of A_{n} then a = s_{pred^{n}}^{A}f^{A_{n}}(x) = s_{pred^{n}}^{A}f^{A}(x) since BlA = BlA_{n}. The latter is in Sg^{A}Y since, by the induction hypothesis, we have f^{A}(x) ∈ Sg^{A}(Y).

We are thus left with the case when f is a unary non boolean operation of A_{n}. We only check the case when f is a cylindrification. The case when f is a substitution is entirely analogous, the idea bieng that in both cases, the operations of A_{n} are obtained by renaming those of A.

Towards this end, assume y = c_{i}^{A_{n}}x, i < ω + n. Then y = c_{ρ_{n}(i)}^{A}x. A direct application of the definitions give:

a = s_{pred^{n}}^{A}y = s_{pred^{n}}^{A}c_{ρ_{n}(i)}^{A}x. By the induction hypothesis we have x ∈ Sg^{A}Y, thus a ∈ Sg^{A}(Y) as well. By this claim 1.3 is proved. Taking Y = A we get e_{n}(A) = Nr_{ω}A_{n}.

In accordance with [HMT1] Def.2.6.28, we refer to Nr_{ω}A_{n}, as the neat − ω reduct of A_{n}. Like in the cylindric case, we have proved that Nr_{ω}A_{n} is a subalgebra of Rd_{ω}A_{n}.

Having done so, claim 1.3 can be written in the form:

e_{n}(Sg^{A}Y) = Sg^{Nr_{ω}A_{n}}e_{n}Y = Nr_{ω}Sg^{A_{n}}e_{n}Y.

20 Remark 1.4. We have shown that A has the so called neat embedding property in [HMT1], Remark 2.6.26. That is for every n ∈ ω, there exists an ω + n dimensional algebra A_{n} such that A can be embedded into the set of ω dimensional elements of A_{n}. Using polyadic terminology, cf [DM63], A_{n} may be called an n − dilation of A.

In fact, we have proved more namely: A can be embedded onto the set of ω dimensional elements of A_{n}, for each n. This follows from the yet stronger: A_{n} is a minimal n dilation of A; expressed more succintly in claim 1.3. Usually neat embeddability into finite extra dimensions, imply neat embeddability into ω extra dimensions. Fortunately, this is the case with G algebras, as we proceed to show.

Using ultraproducts, we paste the A_{n}’s forming an epansion and extension A^{+} of A. A^{+} is an ω + ω dimensional algebra, in which A is neatly embedded. We construct A^{+} as a limit of the A_{n}’s, (n ∈ ω).^{21}

First we expand the A_{n}’s to be all of the same similarity type, then we form an ultraproduct of the resulting expanded algebras. This is standard practice in algebraic logic (see for eg [HMT1], Thms 2.6.7 and 2.6.35)

For brevity let α = α_{ω} = ω + ω. Recall that T_{ω} is the semigroup generated by the set {τ_{ω} : τ ∈ T } ∪_{i,j∈α} {[i|j], [i, j]}

20Note that this is the finite version of the property abbreviated by (*) in the informal outline of the proof.

(*) will be proved in claim 1.9 below.

21In category theory such a construction is better known as an upward limit.

For σ ∈ T_{ω}, and n ∈ ω, let [σ]_{n} = σ ↾ ω + n. Note that for fixed n, [σ]_{n} is not necessarily in T_{n}, however by claim 1.1.(b) there exists l ∈ ω such that for all n ≥ l [σ]_{n} ∈ T_{n}.

For each n ∈ ω let

A_{n}^{+} = ⟨A, +, −, 0, 1, c_{i}^{A_{n}^{+}}, s_{σ}^{A_{n}^{+}}⟩_{i∈α,σ∈T_{ω}}

be an expansion of A_{n} such that BlA_{n}^{+} := BlA(= BlA_{n}) and for each σ ∈ T_{ω} and i ∈ α set s_{σ}^{A_{n}^{+}} := s_{[σ]_{n}}^{A_{n}} iff σ_{n} ∈ T_{n} , and c_{i}^{A_{n}^{+}} := c_{i}^{A_{n}} iff i < ω + n. This means that if σ_{n} ∉ T_{n}

(i ≥ ω + n), and a ∈ A, then s_{σ}^{A_{n}^{+}}a (c_{i}^{A_{n}^{+}}a) is an arbitary but fixed element of A.

Let F be the cofinite ultrafilter on ω. Now forming the ultraproduct of the A_{n}^{+}’s relative to F, let

A^{+} = P_{n∈ω}A_{n}^{+}/F

A^{+} is often referred to in the literature as the F rechet limit of the A_{n}^{+}’s. Henceafter though, we more often refer to A^{+} as an ω dilation of A. This is, as previously

noted, a term we borrow from polyadic algebras (cf, [DM63]).

We point out that, given n ∈ ω, A_{n}^{+} may (and actually does) not satisfy (P_{1} − P_{10}). But, by taking T_{ω} for G in Definition 1.2, the F rechet limit A^{+} does.

This will be partially justified in Remark 1.10 below and afterwards used without any further notice. A proof of this though, can be easily recovered from fact 0.5.15 (ii) in [HMT1], formulated for ultraproducts of general algebras.

For x ∈ A, let e(x) = ⟨e_{n}(x) : n ∈ ω⟩/F. Then e : A → A^{+}. Also e is one to one since every e_{n} is one to one.

Let Rd_{ω}A^{+} be the following reduct of A^{+}, obtained by restricting its similarity type to the first ω dimensions:

Rd_{ω}A^{+} = ⟨A^{+}, +, ., −, 0, 1, c_{i}^{A^{+}}, s_{τ_{ω}}^{A^{+}}⟩_{i<ω,τ∈T}

Recall that for τ ∈ T, τ_{ω} = τ ∪ Id_{α∖ω} ∈ T_{ω}. In particular, s_{τ_{ω}}^{A^{+}} is meaningful. Now that Rd_{ω}A^{+} has the same similarity type as A , we can compare the two algebras.

And indeed we have:

Claim 1.5. (Sain) e is an isomorphism from A into Rd_{ω}A^{+}.

Though the proof follows directly from the basic properties of ultraproducts, we include it for the sake of completeness.

First of all e is a boolean homomorphism since every e_{n} is. Also e is one to one since every e_{n} is one to one. Next we check cylindrifications. Let x ∈ A and i ∈ ω. Then e(c_{i}^{A}x) = ⟨e_{n}(c_{i}^{A}x) : n ∈ ω⟩/F = ⟨c_{i}^{Rd_{ω}}e_{n}(x) : n ∈ ω⟩/F (by e_{n} preserving cylindrifications for all n) = ⟨c_{i}^{A_{n}}e_{n}(x) : n ∈ ω⟩/F (by definition) = ⟨c_{i}^{A_{n}^{+}}e_{n}(x) : n ∈ ω⟩/F (by i < ω < ω + n and by definition of A_{n}^{+}) = c_{i}^{A^{+}}⟨e_{n}(x) : n ∈ ω⟩/F (by definition of ultraproducts) = c_{i}^{A^{+}}e(x) e preserves substitutions: Let x ∈ A and τ ∈ T. Then e(s_{τ}^{A}x) = ⟨e_{n}(s_{τ}^{A}x) : n ∈ ω⟩/F (by definition)

= ⟨s_{τ}^{Rd_{ω}A_{n}}e_{n}(x) : n ∈ ω⟩/F (by e_{n} preserving substitutions for all n ∈ ω)

= ⟨s_{τ_{n}}^{A_{n}}e_{n}(x) : n ∈ ω⟩/F (by definition)

= ⟨s_{[τ_{ω}]_{n}}^{A_{n}^{+}}e_{n}(x) : n ∈ ω⟩/F (Since [τ_{ω}]_{n} = τ_{n} = τ ∪ Id_{M_{n}} ∈ T_{n} for all τ ∈ T)

= ⟨s_{τ_{ω}}^{A_{n}^{+}}e_{n}(x) : n ∈ ω⟩/F (by definition of A_{n}^{+})

= s_{τ_{ω}}^{A^{+}}⟨e_{n}(x) : n ∈ ω⟩/F (by definition of ultraproducts)

= s_{τ_{ω}}^{Rd_{ω}A^{+}}e(x) (by definition)

By this the proof of claim 1.5 is complete.

Next we show that A^{+} so constructed is also a minimal dilation of A. This means that A can be embedded into the set of ω dimensional elements of A^{+}, via e, and that A^{+} satisfies claim 1.6 below, obtained by taking the limit as n tends to infinity, in claim 1.3. First an expected piece of notation.

Notation. For Z ⊆ A^{+}, Nr_{ω}Z consists of the ω dimensional elements in Z. That is Nr_{ω}Z = {z ∈ Z : Δz ⊆ ω} = {z ∈ Z : c_{i}^{A^{+}}z = z for all ω ≤ i < α}.

Claim 1.6. e(Sg^{A}Y) = Nr_{ω}Sg^{A^{+}}Y for all Y ⊆ A

Let Y ⊆ A. We first show that e(Sg^{A}Y) ⊆ Nr_{ω}Sg^{A^{+}}e(Y). This part of the proof is the same as that of Sain. (cf [Sa98]). Let y ∈ Sg^{A}(Y) and m ∈ α ∖ ω. We have to show that c_{m}^{A^{+}}e(x) = e(x). Computing we get

c_{m}^{A^{+}}e(x) = c_{m}^{A^{+}}⟨e_{n}(x) : n ∈ ω⟩/F = ⟨e_{n}(x) : n ∈ ω⟩/F, since c_{m}^{A_{n}^{+}}e_{n}(x) = c_{m}^{A_{n}}e_{n}x = e_{n}(x) for all n for which m ∈ ω + n and since J = {n ∈ ω : m ∈ ω + n} ∈ F, the latter being the cofinite ultrafilter. We have shown that c_{m}^{A^{+}}e(x) = e(x) for each m ∈ α ∖ ω, i,e e(x) ∈ Nr_{ω}(A^{+}). Since e(x) is clearly in Sg^{A^{+}}e(Y) we get the desired.

Before proving the other inclusion, namely Nr_{ω}Sg^{A^{+}}e(Y) ⊆ e(Sg^{A}Y), we shall need:

Claim 1.7. (i) (Sain) For brevity, let M = α ∖ ω. Let Y ⊆ Nr_{ω}A^{+} = {x ∈ A^{+} : Δx ⊆ ω}. Then for all x ∈ Sg^{A^{+}}Y we have |M ∩ Δx| < ω.

(ii) Let 0 ≤ j < ω. For σ ∈ T_{j} let σ_{ω} = σ ∪ Id_{α∖α_{j}}, i.e for x ∈ α, σ_{ω}(x) = σ(x) if x ∈ ω + j and σ_{ω}x = x, otherwise. Then σ_{ω} ∈ T_{ω}. Now let Rd_{ω+j}A^{+} be the following reduct of A^{+} having the same type as A_{j}:

Rd_{ω+j}A^{+} = ⟨A, +, ., −, c_{i}^{A^{+}}, s_{σ_{ω}}^{A^{+}}⟩_{i∈ω+j,σ∈T_{j}}

.

Then Sg^{A^{+}}Y = ∪{Sg^{Rd_{ω+j}A^{+}}Y : j ∈ ω}.

Proof of (i): Since all operations are evaluated in A^{+} we omit the superscript A^{+}. Let Y ⊆ Nr_{ω}A^{+}. For brevity, let R = Sg^{A^{+}}Y. Since for all y ∈ Y we have Δy ⊆ ω, i.e M ∩ Δx = ∅, it suffices to show that for any x ∈ R and any (unary) non boolean operation f of A^{+}, the following holds:

If |M ∩ Δx| < ω, then |M ∩ Δ(fx)| < ω.

Of course we have to check that the above holds for the boolean operations as well, but this is straightforward.

This time we start with the case when f is a substitution. So let τ ∈ T_{ω}. Let D_{τ} be as defined in claim 1.1, i.e D_{τ} = {m ∈ M : τ^{−1}(m) = {m} = {τ(m)}}. Then |D_{τ} | < ω. By |M ∩Δx| < ω, we have |(M ∩Δx)∪D_{τ} | < ω. We will show that M ∩Δ(s_{τ} x) ⊆ (M ∩Δx)∪D_{τ} by which we will be done. So assume that i ∈ M ∖ ω, and that i ∉ (M ∩ Δx) ∪ D_{τ}. Then i ∈ (M ∖ D_{τ}) ∖ Δx, so {τ(i)} = {i} = τ^{−1}(i). Then by (P_{6}) holding in A^{+}, we get that c_{i}s_{τ} x = s_{τ} c_{i}x, proving that i ∉ M ∩ Δs_{τ} x.

Now assume that f = c_{j} with j ∈ α. If i ∈ M and i ∉ Δx then by (P_{2}) holding in A^{+} , we have c_{i}c_{j}x = c_{j}c_{i}x = c_{j}x^{22}, i.e i ∉ Δx.

Note that, we have actually proved the following (only implicit in [Sa98]):

Fact 1.8. Given any finite subset X of R, then α ∖ ∪{Δx : x ∈ X} is infinite.

Proof. Indeed, let X = {x_{0}, ..x_{n−1}}. Then for every i < n there exists l_{i} ∈ ω such that {m ∈ M : ω + l_{i} ≤ ω + m} ⊆ M ∩ Δx_{i}. From α ∖ ∪{Δx_{i} : i < n} ⊆ ∩_{i<n}(M ∩ Δx_{i}) , we immediately get the desired.

Fact 1.8 will be used in part (ii) of the proof.

Remark 1.9

Fact 1.8 says that the ω + ω dimensional algebra R is dimension complemented, a term used for cylindric algebras satisfying fact 1.8 (cf [HMT1] Def 1.11.1 (ii) and Thm 1.11.4 (iii)). Dimension complemented cylindric algebras are generalizations of the locally finite ones. While in locally finite algebras the dimension sets of elements are finite, in dimension complemented ones, this need not be the case. What they share with locally finite algebras is rather: The complement (relative to the dimension) of dimension sets is infinite. Here, of course we are speaking of infinite dimensional algebras.

Remark 1.10

In the above proof we have assumed that the “cylindrifications commute” part of (P_{2}) and (P_{6}) hold in A^{+}. This follows from the basic properties of ultraproducts. However for the sake of completeness we give a self contained justification of this. The non-sceptical reader can skip this remark, and go on with the proof of Claim 1.7.

We put back superscripts. Let i, j ∈ α and x = ⟨x_{n} : n ∈ ω⟩/F ∈ A^{+}. That c_{i}^{A^{+}}c_{j}^{A^{+}}x = c_{j}^{A^{+}}c_{i}^{A^{+}}x can be proved as follows:

Let J_{i} = {n ∈ ω : i ∈ ω + n}, J_{j} = {n ∈ ω : j ∈ ω + n} and J_{ij} = J_{i} ∩ J_{j}. Since F is closed under finite intersections, it follows that J_{ij} ∈ F, because J_{i} and J_{j} are clearly in F.

Let n ∈ J_{ij}. Then c_{i}^{A_{n}^{+}}c_{j}^{A_{n}^{+}}x_{n} = c_{i}^{A_{n}}c_{j}^{A_{n}}x_{n} = c_{ρ_{n}(i)}^{A}c_{ρ_{n}(j)}^{A}x_{n} = c_{ρ_{n}(j)}^{A}c_{ρ_{n}(i)}^{A}x_{n} = c_{j}^{A_{n}}c_{i}^{A_{n}}x_{n} =

c_{j}^{A_{n}^{+}}c_{i}^{A_{n}^{+}}x_{n}. It then follows that c_{i}^{A^{+}}c_{j}^{A^{+}}x = c_{j}^{A^{+}}c_{i}^{A^{+}}x.

Now we now justify (P_{6}) holding in A^{+}. Let τ ∈ T_{ω}, x and D_{τ} be as above and i ∈ (M ∖ D_{τ}) ∖ Δx.

Then by claim 1.1 (a) there exists l ∈ ω such that for all n ≥ l we have [τ]_{n} ∈ T_{n}. We can obviously assume that i ∈ ω + l. Let J_{l} = {n ∈ ω : n ≥ l}. Then J_{l} ∈ F. Also for any n ∈ J_{l} we have s_{[τ]_{n}}^{A_{n}^{+}}c_{i}^{A_{n}^{+}}x_{n} = s_{[τ]_{n}}^{A_{n}}c_{i}^{A_{n}}x_{n} = c_{i}^{A_{n}}s_{[τ]_{n}}^{A_{n}}x_{n} = c_{i}^{A_{n}^{+}}s_{[τ]_{n}}^{A_{n}^{+}}x_{n}. This proves that

c_{i}^{A^{+}}s_{τ}^{A^{+}}x = s_{τ}^{A^{+}}c_{i}^{A^{+}}x.

In parts (ii) and (iii) of the proof, we shall be extensively using the fact that (P_{1} − P_{10}) hold in the algebra A^{+}, by takig T_{ω} for G. As previously noted, this is routine, following the same reasoning as above.

22Here we only use that cylindrifications commute.

We go back to proving Claim 1.7:

Proof of Claim 1.7 (ii). Let everything be as in the hypothesis.

We define inductively the sequence ⟨Y_{k} : k ∈ ω⟩ as follows:

Y_{0} = Y ∪ {0, 1} and

Y_{k+1} = Y_{k} ∪ {f^{A^{+}}y : y ∈ ^{i}Y : i ∈ {1, 2} and f is an i ary operation of A^{+}}.

Then of course Sg^{A^{+}}Y = ∪{Y_{k} : k ∈ ω}.

We will show, by induction on k, that for all y ∈ Y_{k} there exists j ∈ ω, such that x ∈ Sg^{Rd_{ω+j}A^{+}}Y, by which we will be done.

The case when k = 0 is trivial. Ignoring the booleans as usual, assume then that y = f(x), where f is a non boolean (hence unary) operation, and inductively that x ∈ Sg^{Rd_{ω+j}A^{+}}Y for some j ∈ ω.

Assume that f = τ is a substitution. Let D_{τ} be as above. Let n ≥ j be such that (M ∩ Δx) ∪ D_{τ} ⊆ ω + n Then x ∈ Sg^{Rd_{ω+n}A^{+}}Y. Let σ = τ ↾ ω + n. Then σ ∈ T_{n} and σ_{ω} = τ. Also y = s_{τ}^{A^{+}}x = s_{σ_{ω}}^{A^{+}}x = s_{σ}^{Rd_{ω+n}A^{+}}x, proving that y is as desired. The case when f is a cylindrification is completely analogous, and is left to the reader.

Now we are ready to prove the remaining inclusion of claim 1.6, namely that Nr_{ω}Sg^{A^{+}}Y ⊆ e(Sg^{A}Y).

We write f ∈ Ism(A, B)(Is(A, B)) to abbreviate that f is an isomorphism from A into (onto) B.

Let y ∈ Nr_{ω}Sg^{A^{+}}e(Y). Then y ∈ Sg^{A}e(Y) and Δy ⊆ ω. By e(Y) ⊆ Nr_{ω}A^{+}, we have by claim 1.7 (ii) that there exists j ∈ ω such that y ∈ Sg^{Rd_{ω+j}A^{+}}e(Y). Fix any such j among the infinitely many. Let F_{j} = {Γ ∩ (ω − j) : Γ ∈ F }. Then F_{j} is the cofinite ultrafilter on ω − j. For x ∈ A_{j} = A, let e^{j}(x) = ⟨e_{n}(x) : j ≤ n < ω⟩/F_{j}. Let A_{j}^{+} = P_{j≤n<ω}A_{n}/F_{j}. Then it is not hard to see that e^{j} ∈ Ism(A_{j}, A_{j}^{+}). For x = ⟨x_{n} : n ∈ ω⟩/F ∈ A^{+}, let f(x) = ⟨x_{n} : j ≤ n < ω⟩/F_{j}. Then clearly f ∈ Is(A^{+}, A_{j}^{+}). Let g be the inverse of f. Then goe^{j} ∈ Ism(A_{j}, Rd_{ω+j}A^{+}). Moreover for any a ∈ A we have e(a) = goe^{j}oe_{j}(a). Now y ∈ Sg^{Rd_{ω+j}A^{+}}e(Y) = Sg^{Rd_{ω+j}A^{+}}(goe^{j}oe_{j}(Y)). Let y′ = f(y). Then g(y′) = y, and Δy′ ⊆ ω because Δy ⊆ ω and g is an isomorphism.

Also y′ ∈ f(Sg^{Rd_{ω+j}A^{+}}(goe^{j}oe_{j}(Y)) = Sg^{Rd_{ω+j}A_{j}^{+}}(e^{j}oe_{j}(Y)).

Recall that e^{j} : A_{j} → e^{j}(A_{j}) is an isomorphism. Let h : e^{j}(A_{j}) → A_{j} denote its inverse. Note that y′ ∈ e^{j}(A_{j}), since Sg^{Rd_{ω+j}A_{j}^{+}}(e^{j}oe_{j}(Y)) ⊆ e^{j}(A_{j}). Now let a′ = h(a). Then e^{j}(a′) = y′ and a′ ∈ h(Sg^{Rd_{ω+j}A_{j}^{+}}(e^{j}oe_{j})(Y)) = Sg^{A_{j}}e_{j}(Y). Also, by the same reasoning as above, Δa′ ⊆ ω, i.e a ∈ Nr_{ω}Sg^{A_{j}}e_{j}(Y). By Claim 1.3 we get a ∈ Sg^{A}Y such that e_{j}(a) = a′. Thus e(a) = goe^{j}oe_{j}(a′) = goe^{j}(a) = g(y′) = y. By this the proof of claim 1.5 is complete.

From now on we assume that A is a subalgebra of Rd_{ω}A^{+}, i.e we identify A with e(A), regarding e : A → Rd_{ω}A^{+} as the inclusion map. In particular, we have A ⊆ Nr_{ω}A^{+} and for all Y ⊆ A we have (*)

Sg^{A}Y = Sg^{Nr_{ω}A^{+}}Y = Nr_{ω}Sg^{A^{+}}Y.

Also we fix sets X,X_{1} and X_{2} such that X generates A, and X_{1}, X_{2} ⊆ X.

Claim 1.11. Let a ∈ Sg^{A}X_{1}, b ∈ Sg^{A}X_{2} such that a ≤ c. Assume that there exists no b ∈ Sg^{A}(X_{1} ∩ X_{2}) such that A ⊧ a ≤ b ≤ c. Then there is no b ∈ Sg^{A^{+}}(X_{1} ∩ X_{2}) such that A^{+} ⊧ a ≤ b ≤ c.

First a piece of notation. Let Γ be a finite subset of α, Γ = {j_{0}, ⋯, j_{n−1}} say, and x ∈ A^{+}. If n = 0, i.e Γ = ∅ then c_{∅}x = x. Else n > 0, in which case we set c_{(Γ)}x = c_{j_{0}} ⋯ c_{j(n−1)}x. c_{(Γ)} as defined above is referred to as generalised cylindrification (cf., [HMT1], Def 1.7.1).

Now for the proof:

Assume, seeking a contradiction, that there exists b ∈ Sg^{A^{+}}(X_{1} ∩ X_{2}) such that A^{+} ⊧ a ≤ b ≤ c. By claim 1.7 (i) we have Δb − ω = Γ, say, is finite. Set b′ = c_{(Γ)}b. Then A^{+} ⊧ a ≤ b ≤ c_{(Γ)}b = b′. Since c ∈ Sg^{A}X_{2} ⊆ Nr_{ω}Sg^{A^{+}}X_{2}, we get that c_{(Γ)}c = c, hence A^{+} ⊧ a ≤ b′ ≤ c. Since b′ ∈ Nr_{ω}Sg^{A^{+}}(X_{1} ∩ X_{2}), it then follows by claim 1.6 , that b′ ∈ Sg^{A}(X_{1} ∩ X_{2}). This contradicts our assumption that no interpolant of a and −c exists in Sg^{A}(X_{1} ∩ X_{2}).

Remark 1.12

We have mentioned in the informal outline of proof that the process of neatly embedding can be viewed as adding constants. Let us dwell on this a little longer. We illustrate this by an example:

Let L be an ordinary first order language with two propositional constants T,F, and a list ⟨c_{k}⟩ of individual constants of type α. L has no operation symbols, but as usual, the list of variables is of type ω. Denote by Sn^{L} the set of all L sentences. For ϕ ∈ Sn^{L} and k < α let ∃_{k}ϕ := ∃xϕ(c_{k}|x) where x is the first variable not occuring in ϕ. Here ϕ(c_{k}|x) is the formula obtained from ϕ by replacing all occurances of c_{k}, if any, in ϕ by x. For τ ∈ ^{α}α, and ϕ = ϕ(c_{0}, ⋯ c_{n−1}) ∈ Sn^{L} we let s_{τ} ϕ be the sentence obtained from ϕ by the simultaneous substitution of the constants c_{τ(0)}, ⋯, c_{τ_{n−1}} for the constants c_{0}, ⋯ c_{n−1} respectively. Let Σ be a set of sentences in which no constants occur. Define the equivalence relation ≡_{Σ} on 2Sn^{L} as follows

ϕ ≡_{Σ} ψ iff Σ ⊧ ϕ ≡ ψ.

Then, as easily checked, for any G ⊆ ^{α}α, ≡_{Σ} is a congruence relation on

Sn = ⟨Sn, ∧, ∨, ¬, T, F, ∃_{k}, s_{τ} ⟩_{k<α,τ∈G}

We let Sn^{L}/Σ denote the qutient algebra. For the sake of defenitness, we let α be infinite and fix G to be the set of all finite transformations on α. In this case, Sn^{L}/Σ is a locally finite polyadic algebra of dimension α. Here locally finite means that the dimension set of any element is finite. This follows from the simple observation that the constants occuring in a sentence are finite.

(b) Let L be as described in (a) above. But now we denote it L_{α}, the subsript α indicating that we have α individaul constants. Now enrich L_{α} with constants (and nothing else) obtaining L_{β}, with β > α. Recall that both languages have a list of ω variables. Let Σ be a set of sentences with no constants. For κ ∈ {α, β} let A_{κ} = Sn^{L_{k}}/Σ. (Here we are also assming that G is the set of all finite transformations on κ). For ϕ ∈ Sn^{L_{α}}, let f(ϕ/Σ) = ϕ/Σ. Then, as easily checked f is an embedding of A_{α} into A_{β}. Moreover f has the additional property that it maps A_{α}, into (and onto) the neat − α reduct of A_{β}, (i,e the set of α dimensional elements of A_{β}). In short, A_{α} ≅ Nr_{α}A_{β}.

Remark 1.13

Let A be a countable Sains algebra. In preparation of representing A (as a concrete algebra), Sain proved that A has the the neat embedding property. This, we mimmicked in our construction of the ω dilation A^{+} of A, which was constructed in a step-by-step fashion. First we neatly embedded A into A_{n}, for every n, then we neatly embedded A into an ultraproduct of (expansions) of the A_{n}’s. We delay defining the representation for a while. This will be done in part (iii). We point out that the novelty that occurs here is that A^{+} is a minimal extension of A. This was expressed in claim 1.6. With remark 1.12 at hand, we see that the process of neatly embedding A into A^{+}, step-by-step corresponds to the following metalogical fact: The process of adding ω new constants, can be broken into infinitely many steps, or tasks, each of which consists of adding one new constant. Neatly embedding A into A_{n} means we are adding n new constants. Claim 1.6 expresses the rather simple (and expected) fact that when we add constants and nothing else then we do not add to the expressive power of our logics. No “new elements” are defined from old ones; borrowing yet another concept from model theory: A^{+} is a conservative extension of A, so to speak.

Details of Part (ii)

From now on let everything be as in the hypothesis of Claim 1.11

That is X is a generating set of A, and X_{1}, X_{2} ⊆ X. Further fix a ∈ Sg^{A}(X_{1}) and c ∈ Sg^{A}(X_{2}), for which no interpolant exists in Sg^{A}(X_{1} ∩ X_{2}) (equivalently (in light of claim 1.11) in Sg^{A^{+}}(X_{1} ∩ X_{2}).)

We work with the big algebra A^{+}. Using the supply of witnesses (the extra ω dimensions of A^{+}), we extend a and −c to Henkin ultrafilters. In preparation of defining the desired model, which will be done in part (iii) , we make sure that these ultrafilters, constructed in a step-by-step manner agree on Sg^{A^{+}}(X_{1} ∩ X_{2}). The first step is already taken care of by claim 1.11. Now for the details.

Recall that α = ω + ω. For Y ⊆ A, Let A^{+}(Y) stand for Sg^{A^{+}}Y. Recall that we assumed that A ⊆ A^{+}, that A is generated by X (not freely yet) and that X_{1}, X_{2} ⊆ X.

Now arrange α × A^{+}(X_{1}) and α × A^{+}(X_{2}) into ω termed sequences:

⟨(k_{i}, x_{i}) : i ∈ ω⟩ and ⟨(l_{i}, y_{i}) : i ∈ ω⟩ respectively. This is possible since both A^{+}(X_{1}) and A^{+}(X_{2}) are countable and |α| = ω.

Using fact 1.8, we can define by recursion (or step by step) ω termed sequences of witnesses:

⟨u_{i} : i ∈ ω⟩ and ⟨v_{i} : i ∈ ω⟩

such that for all i ∈ ω we have:

u_{i} ∈ α ∖ (Δa ∪ Δc) ∪ ∪_{j≤i}(Δx_{j} ∪ Δy_{j}) ∪ {u_{j} : j < i} ∪ {v_{j} : j < i}

and

v_{i} ∈ α ∖ (Δa ∪ Δc) ∪ ∪_{j≤i}(Δx_{j} ∪ Δy_{j}) ∪ {u_{j} : j ≤ i} ∪ {v_{j} : j < i}

Notation. Let B be a boolean algebra and Y ⊆ B. Then fl^{A}B denotes the (boolean) filter generated by B

Let Y_{1} = {a} ∪ {−c_{k_{i}}x_{i} + s_{u_{i}}^{k_{i}}x_{i} : i ∈ ω}, Y_{2} = {−c} ∪ {−c_{l_{i}}y_{i} + s_{v_{i}}^{l_{i}}y_{i} : i ∈ ω}, H_{1} = fl^{BlA^{+}(X_{1})}Y_{1}, H_{2} = fl^{BlA^{+}(X_{2})}Y_{2} and H = fl^{BlA^{+}(X_{1}∩X_{2})}[(H_{1} ∩ A^{+}(X_{1} ∩ X_{2}) ∪ (H_{2} ∩ A^{+}(X_{1} ∩ X_{2})]

Claim 1.14. H is a proper filter of A^{+}(X_{1} ∩ X_{2})

To do this it is sufficient to consider any pair of finite, strictly increasing sequences of finite ordinals

η(0) < η(1).... < η(n − 1) < ω, and ξ(0) < ξ(1) < .. < ξ(m − 1) < ω and to prove that the following condition holds:

(1) For any b_{0}, b_{1} ∈ A^{+}(X_{1} ∩ X_{2}) such that

a.Π_{i<n}(−c_{k_{η(i)}}x_{η(i)} + s_{u_{η(i)}}^{k_{η(i)}}x_{η(i)}) ≤ b_{0}

and

(−c).Π_{i<m}(−c_{l_{ξ(i)}}y_{ξ(i)} + s_{v_{ξ(i)}}^{l_{ξ(i)}}y_{ξ(i)}) ≤ b_{1}

we have

b_{0}.b_{1} ≠ 0.

We do this by induction on n + m. If n + m = 0, then (1) simply expresses the fact that no interpolant of a and c exists in A^{+}(X_{1} ∩ X_{2}) already proved in claim 1.11. In more detail; if n + m = 0, then a_{0} ≤ b_{0} and −c ≤ b_{1}. So if b_{0}.b_{1} = 0, we get a ≤ b_{0} ≤ −b_{1} ≤ c which is absurd by claim 1.11. Now assume that n + m > 0.

Assume for the time being that η(n − 1) > ξ(m − 1). Apply c_{u_{η(n−1)}} to both sides of the first inclusion of (1). By u_{η(n−1)} ∉ Δa, i.e c_{u_{η(n−1)}}a = a, and by noting that c_{i}(c_{i}x.y) = c_{i}x.c_{i}y, we get (2)

a.c_{u_{η(n−1)}}Π_{i<n}(−c_{k_{η(i)}}x_{η(i)} + s_{u_{η(i)}}^{k_{η(i)}}x_{η(i)}) ≤ c_{u_{η(n−1)}}b_{0}

Let c_{i}∗ = −c_{i}−^{23}. Now apply c_{u_{η(n−1)}}∗ to the second inclusion of (1). By noting that c_{i}∗, the dual of c_{i}, distributes over meets, and by u_{η(n−1)} ∉ Δc = Δ(−c)

we get (3)

(−c).Π_{i<m}(c_{u_{η(n−1)}} ∗ (−c_{l_{ξ(i)}}y_{ξ(i)} + s_{v_{ξ(i)}}^{l_{ξ(i)}}y_{ξ(i)}) ≤ c_{u_{η(n−1)}} ∗ b_{1}

Before going on, we formulate a claim that will enable us to eliminate the quantifier c_{u_{η(n−1)}} (and its dual) from (2) (and (3)).

23c_{i}∗ is the algebraic counterpart of the universal quantifier ∀x_{i}

Not to interrupt the main stream, we assume that the claim is true, proceed with proving that H as claimed in 1.14, is indeed a proper filter, and then return to proving the claim.

Claim 1.15. For brevity set for each i < n and each i < m

z_{i} = −c_{k_{η(i)}}x_{η(i)} + s_{u_{η(i)}}^{k_{η(i)}}x_{η(i)})

and

t_{i} = c_{l_{ξ(i)}}y_{ξ(i)} + s_{v_{ξ(i)}}^{l_{ξ(i)}}y_{ξ(i)}.

Then (i) and (ii) below hold:

(i) c_{u_{η(n−1)}}z_{i} = z_{i} for i < n − 1 and c_{u_{η(n−1)}}z_{n−1} = 1. (ii) c_{u_{η(n−1)}} ∗ t_{i} = t_{i} for all i < m.

Assume that claim 1.15 is true. Then c_{u_{η(n−1)}}Π_{i<n}z_{i} = c_{u_{η(n−1)}}Π_{i<n−1}z_{i}.c_{u_{η(n−1)}}z_{n−1} = Π_{i<n−1}z_{i}. Combined with (2) we obtain

a.Π_{i<n−1}(−c_{k_{η(i)}}x_{η(i)} + s_{u_{η(i)}}^{k_{η(i)}}x_{η(i)}) ≤ c_{u_{η(n−1)}}b_{0}

On the other hand, from claim 1.15 (iii) and (3) it follows that

(−c).Π_{i<m}(−c_{l_{ξ(i)}}y_{ξ(i)} + s_{v_{ξ(i)}}^{l_{ξ(i)}}y_{ξ(i)}) ≤ c_{u_{η(n−1)}} ∗ b_{1}

Now making use of the induction hypothesis we get c_{u_{η(n−1)}}b_{0}.c_{u_{η(n−1)}} ∗ b_{1} ≠ 0, and hence b_{0}.c_{u_{η(n−1)}} ∗ b_{1} ≠ 0.

By b_{0}.b_{1} ≤ b_{0}.c_{u_{η(n−1)}} ∗ b_{1} we get the desired. The other case, when η(n−1) ≤ ξ(m−1) can be treated similarly. and is left to the reader. We have proved that H is a proper filter, modulu claim 1.15. To finish the proof of claim

1.14, we now prove claim 1.15.

Proof of (i): Proof of c_{u_{η_{n−1}}} z_{i} = z_{i} for i < n − 1. Let i < n − 1. Then by the choice of witnesses we have u_{η(n−1)} ≠ u_{η(i)}. Also it is easy to

see that Δc_{j}x ⊆ Δx and that Δs_{j}^{i}x ⊆ Δx − {i} ∪ {j}, for all j, i ∈ α.

In particular, u_{η_{n−1}} ∉ Δc_{k_{η_{i}}} x_{η_{i}} and u_{η_{n−1}} ∉ Δ(s_{u_{η_{i}}}^{k_{η_{i}}} x_{η_{i}}).

Thus c_{u_{η_{n−1}}} (−c_{k_{η_{i}}} x_{η_{i}}) = −c_{k_{η_{i}}} x_{η_{i}} and c_{u_{η_{(}n−1)}}(s_{u_{η_{i}}}^{k_{η_{i}}} x_{η_{i}}) = s_{u_{η_{i}}}^{k_{η_{i}}} x_{η_{i}}. Finally by c_{u_{η_{n−1}}} distributing over joins we get c_{u_{η_{n−1}}} z_{i} = z_{i} for i < n − 1 Proof of c_{u_{η_{n−1}}} z_{n−1} = 1 Computing we get by u_{η(n−1)} ∉ Δc_{k_{ξ(n−1)}} and (P_{7})

c_{u_{η(n−1)}}(−c_{k_{η(n−1)}}x_{η(n−1)} + s_{u_{η(n−1)}}^{k_{η_{n−1}}}x_{η_{n−1}})

= c_{u_{η_{n−1}}} − c_{k_{η_{n−1}}} x_{η_{n−1}} + c_{u_{η_{n−1}}} s_{u_{η_{n−1}}}^{k_{η_{n−1}}} x_{η_{n−1}}

= −c_{k_{η_{n−1}}} x_{η_{n−1}} + c_{u_{η_{n−1}}} s_{u_{η_{n−1}}}^{k_{η_{n−1}}} x_{η_{n−1}} = −c_{k_{η_{n−1}}} x_{η_{n−1}} + c_{u_{η_{n−1}}} s_{u_{η_{n−1}}}^{k_{η_{n−1}}} c_{u_{η_{n−1}}} x_{η_{n−1}}

= −c_{k_{η_{n−1}}} x_{η_{n−1}} + c_{k_{η_{n−1}}} s_{k_{η_{n−1}}}^{u_{η_{n−1}}} c_{u_{η_{n−1}}} x_{η_{n−1}} = −c_{k_{η_{n−1}}} x_{η_{n−1}} + c_{k_{η_{n−1}}} c_{u_{η_{n−1}}} x_{η_{n−1}} = −c_{k_{η_{n−1}}} x_{η_{n−1}} + c_{k_{η_{n−1}}} x_{η_{n−1}} = 1

Proof of (ii)

Let i < m . Then we have c_{u_{η_{n−1}}}^{∗} (−c_{l_{ξ(i)}}y_{ξ_{i}}) = −c_{l_{ξ(i)}}y_{ξ_{i}} and c_{u_{η_{n−1}}}^{∗} (s_{v_{ξ_{i}}}^{l_{ξ_{i}}} y_{ξ_{i}}) = s_{v_{ξ_{i}}}^{l_{ξ_{i}}} y_{ξ_{i}}. Indeed, computing we get c_{u_{η_{n−1}}}^{∗} (−c_{l_{ξ(i)}}y_{ξ_{i}}) = −c_{u_{η_{n−1}}} − (−c_{l_{ξ(i)}}y_{ξ_{i}}). = −c_{u_{η_{n−1}}} c_{l_{ξ(i)}}y_{ξ_{i}} = −c_{l_{ξ(i)}}y_{ξ_{i}}

Similarly we have c_{u_{η_{n−1}}}^{∗} (s_{v_{ξ_{i}}}^{l_{ξ_{i}}} y_{ξ_{i}}) = −c_{u_{η_{n−1}}} −(s_{v_{ξ_{i}}}^{l_{ξ_{i}}} y_{ξ_{i}}) = −c_{u_{η_{n−1}}} (s_{v_{ξ_{i}}}^{l_{ξ_{i}}} −y_{ξ_{i}}) = −s_{v_{ξ_{i}}}^{l_{ξ_{i}}} −y_{ξ_{i}}

= s_{v_{ξ_{i}}}^{l_{ξ_{i}}} y_{ξ_{i}}

By this the proof of claim 1.15 is complete. Therefore H is a proper filter of A^{+}(X_{1} ∩ X_{2}).

Let H^{∗} be an ultrafilter of A^{+}(X_{1} ∩ X_{2}) containing H. From BA theory we get ultrafilters F_{1} and F_{2} of A^{+}(X_{1}) and A^{+}(X_{2}) respectively such

that

H^{∗} ⊆ F_{1}, H^{∗} ⊆ F_{2}

and

F_{1} ∩ A^{+}(X_{1} ∩ X_{2}) = F_{2} ∩ A^{+}(X_{1} ∩ X_{2})

Then by construction F_{1} and F_{2} are Henkin ultrafilters and for all x ∈ A^{+}(X_{1} ∩ X_{2}) we have x ∈ F_{1} iff x ∈ F_{2}.

Now we are not too far away from defining the desired model. We try to make it even closer by drawing another analogy from model theory

Remark 1.16

Let L and Σ be as described in Remark 1.12, except that we now assume that everything is countable. For simplicity we further assume that α = ω. Let F be an ultrafiter of Sn^{L_{ω}}/Σ. Then it not hard to check that F is Henkin iff ∪F is a complete rich extension of Σ in the sense of [CK].

It is known how canonical models corresponding to Henkin theories are defined. This is precisely what we do next:

Details of Part(iii)

In this last part of the proof we form the desired model of (A, a. − c) First we define models of (Sg^{A}X_{1}, a) and (Sg^{A}X_{2}, −c) Then using the freeness of A, we

amalgamate these models, to get the desired one.

Claim 1.17. (Sain) (i)Let V = ∪_{τ∈T}^{ω}α^{τ}. For v ∈ V, let v^{∗} = v ∪ Id ↾ (α − ω). Then v^{∗} ∈ T_{ω}.

(ii)For i ∈ {1, 2}, let f_{i} be the function with domain Sg^{A}(X_{i}) such that

f_{i}(a) = {v ∈ V : s_{v}^{A^{+}(X_{i})}a ∈ F_{i}}.

Then f_{i} is a homorphism from A into ⟨B(V), C_{i}, S_{τ} ⟩_{i∈ω,τ∈T}. Also Id ∈ f_{1}(a) ∩ f_{2}(−c).

Proof of (i). Follows from the definitions (see also [Sa98]). Proof of (ii). That Id ∈ f_{1}(a) ∩ f_{2}(−c) follows from a ∈ F_{1} and −c ∈ F_{2}. It is easy to check that f_{i} is a boolean homomorphism for i ∈ {0, 1}. It is clearly enough, by total symmetry in the definition to show that f_{1} preserves the extra non boolean operations. This is proved in [Sa98], but for the sake of completeness, we include Sains proof.

For the sake of brevity let f = f_{1}, F = F_{1} and B = Sg^{A}X_{1}. Then in view of the identification A ⊆ Nr_{ω}A^{+}, we have B ⊆ Nr_{ω}A^{+} and for all b ∈ B and τ ∈ T we have s_{τ}^{B}b = s_{τ_{ω}}^{A^{+}}b. Also for all σ ∈ T_{ω} and b ∈ B, since A^{+}(X_{1}0 ⊆ A^{+} we have s_{σ}^{A^{(+)}X_{1}}b = s_{σ}^{A^{+}}b.

(i) f preserves cylindrifications

Let b ∈ B and i ∈ ω. We want to show that c_{i}f(b) = f(c_{i}b). We first show that c_{i}f(b) ⊆ f(c_{i}b). Let τ ∈ c_{i}f(b). Then τ_{j}^{i} ∈ f(b) for some j ∈ α, where τ_{j}^{i}(x) = τ(x) if x ≠ i and τ_{j}^{i}(i) = j. Let v = τ_{j}^{i}. Then, by definition, we have s_{v∗}^{A^{+}}b ∈ F. By s_{v^{∗}}^{A^{+}}b ≤ s_{v^{∗}}^{A^{+}}c_{i}^{A^{+}}b = s_{v^{∗}}^{A^{+}}c_{i}^{B}b, and F is a filter we get s_{v^{∗}}^{A^{+}}(c_{i}^{B}b) ∈ F. Hence v ∈ f(c_{i}b) Thus τ differing from v in at most the ith place is also in f(c_{i}b). We have shown that c_{i}f(b) ⊆ f(c_{i}b).

Now for the opposit inclusion, namely that f(c_{i}b) ⊆ c_{i}fb.

Let v ∈ f(c_{i}b). Let τ = v^{∗}. Then s_{τ} c_{i}b ∈ F.

We will show that there exists j ∈ α such that s_{τ[i|j]}^{A^{+}}b ∈ F, by which we will be done, because of the following:

v[i|j]∗ = τ[i|j], and so v[i|j] ∈ f(b) thus v ∈ c_{i}f(b).

Let m ∈ α such that c_{m}b = b and τ^{−1}m = m = τ(m). Such an m exists by |M ∩ Δx| < ω and |D_{τ} | < ω. Let l ∈ α∖{i, m}. Let k = τ(l). Then k ≠ m, for else we would have τ(l) = m, i.e l ∈ τ^{−1}m, contradicting that τ^{−1}m = {m} since l ≠ m. Recall that τ[i|m](x) = τ(x) if x ≠ i and τ[i|m](i) = m. By the choice of m we have τ[i|m] = τo[i|m]. Now by (P_{5}) and the above we have s_{τ} c_{i}b = s_{τ[i|m]}c_{i}b = s_{τo[i|m]}c_{i}b. By c_{m}b = b and s_{l}^{m}c_{m}b = c_{m}b and commutivity of cylindrifications the latter is equal to s_{τo[i|m]}s_{l}^{m}c_{m}c_{i}b which in turn is equal to s_{τo[i|m]o[m|l]}c_{i}b. Let σ = τo[i|m]o[m|l]. Then it is not hard to check that σ(x) = m iff x = i. By (P_{6}), we have s_{σ}c_{i}b = c_{m}s_{σ}b. We have shown that s_{τ} c_{i}b = c_{m}s_{σ}b, thus c_{m}s_{σ}b ∈ F. Since F is Henkin, there exists j ∈ α such that s_{j}^{m}s_{σ}b ∈ F. Let σ′ = [m|j]oσ. Then it is not hard to check that σ′(x) = τ[i|j]x for all x ∈ α − {m}. By the above we get s_{j}^{m}s_{σ}b = s_{j}^{m}s_{σ}c_{m}b = s_{[m|j]oσ}c_{m}b = s_{τ[i|j]}c_{m}b = s_{τ[i|j]}b.

(ii) f preserves substitutions

v ∈ f(s_{τ}^{B}b) iff s_{v^{∗}}^{A^{+}}(s_{τ}^{B}b) ∈ F iff s_{v^{∗}}^{A^{+}}s_{τ_{ω}}^{A^{+}}b ∈ F iff s_{v^{∗}oτ_{ω}}^{A^{+}}b ∈ F. By (voτ)^{∗} = v^{∗}oτ_{ω}, this is equivalent to voτ ∈ f(b), i.e v ∈ s_{τ} (f(b)).

Now assume that A is freely generated on X. Assume further, without any loss of generality, that X_{1} ∪ X_{2} = X.

Claim 1.17. Let g = f_{1} ∪ f_{2} ↾ X. Then g is a function. Moreover g extends to a homomorphism from A into ⟨B(V), ∪, ∩, −, c_{i}, s_{τ} ⟩_{i∈ω,τ∈T}. In particular, we have g(a. − c) ≠ 0.

Proof: To prove that g is a function, we have to show that f_{1} and f_{2} agree on X_{1} ∩ X_{2}. But this is immeadiate from how f_{1} and f_{2} are defined, by noting that F_{1} and F_{2} agree on A^{+}(X_{1} ∩ X_{2}) Since A is freely generated on X = X_{1} ∪ X_{2}, it follows that g extends to a homomorphism on A. Also by g(a. − c) = g(a) ∩ g(−c) = f_{1}(a) ∩ f_{2}(−c), we get that Id ∈ g(a. − c), i.e g(a. − c) ≠ 0. Thus g defines a model of (A, a. − c). By this the proof is complete of proposition 1 is complete.

Section 2. Concluding Remarks.

(a) When we have a neat embedding Theorem to the effect that algebras having the neat embedding property are representable then we have a completeness theorem in the corresponding logics.

Sain showed that G algebras, with G rich enjoy a neat embedding Theorem. The interpretation of G algebras as algebras of sentences in languages with constants underlines the similarity with Henkins celebrated completeness proof. Henkins methods of constructing models from constants, have a potentaility of applications, proving a diversity of results, like interpolation theorems and omitting types. So when we have extensions of first order logic (like logics corresponding to Sains algebras), for which the neat embedding applies on the algebra side, it is natural to ask the reverse question: How far can we use Henkins methods (already available, in a disguised form as a neat embedding Theorem) to prove other model theoretic results like interpolation and omitting types, which we already know can be proved using a Henkin construction for first order logic?. This paper shows that the algebraisation of Henkins methods, (outlined in the sketch of proof), works for G algebras to prove interpolation results, namely Beth Craig’s properties and Robinson’s Joint consistancy Theorem. Other metaogical properties, also proved in first order logic, using Henkins methods, like omitting types is investigated in [S99d].

b. To see how our proof adapts to the more general case of rich semigroups, we first recall the notion of a rich semigroup (of ^{ω}ω from [Sa98] p.13.)

Let T ⊆ ⟨^{ω}ω, ∘⟩. Then T is said to be rich if it satisfies conditions (1) and (2) below:

(1) For all i, j ∈ ω, for all τ ∈ T, we have τ[i|j] ∈ T.

(2) There are σ, π in T, such that

π ∘ σ = Id, Rng(σ) ≠ ω, and for all τ ∈ T we have

σ ∘ τ ∘ π)[(ω ∖ Rng(σ))/Id] ∈ T

Here for functions f and g and a set H, f[H/g] is the function that agrees on g if x ∈ H, and is otherwise equal to f.

If we examine Sains proof in [Sa98], then the neat embedding part is done by s_{σ}, and s_{τ} where σ and τ act like suc and pred, respectively. To make sure that the property expressed in (*) goes through, we stipulate an extra axiom namely: s_{σ∘τ} c_{(n)}x = x. This, is of course consistent with the other axioms (since the new axioms have a model, namely the one in which we proved proposition 1) . We leave it to the reader to check that our proof goes through.

(c) The following Theorem (using a neat embedding theorem) was proved by Sain:

Theorem. . Assume that T ⊆ ⟨^{ω}ω, o⟩ is a finitely presented rich semigroup. Let G ⊆ T denote a finite generator set of T. Then (i) and (ii) below hold:

(i) IGP SA_{ω} is a finitely based variety.

(ii) The subalgebras of the quasi-polyadic reducts of IGP SA_{ω} coincide with the representable quasi-polyadic algebras.

In this paper (also using Henkin’s methods), we also proved:

(iii) IGP SA_{ω} has the strong amalgamation property.

3. We highlight a property that played an essentail role in proving (iii) above, i.e showing that G (set) algebras have the strong amalgamation property. We start by a somewhat ambigious, too broad a definition, to be made hopefully narrower in a forthcoming paper. Let K = ⟨K_{α} : ω ≤ β ≤ ω + ω⟩ be a system of varieties , not necessarily definable by schemes in the sense of [HMT2] Def 5.6.11, but definable by some “uniform” schema all the same. We also assume that the notion of neat embeddings make sense, so that for example we can talk about the class SNr_{ω}K_{ω+ω}. Here S denotes the operation of forming subalgebras. For a “concrete” K, and in the presence of a neat embedding Theorem, this class is just the class of representable ω dimensional algebras. Examples of such K include the most well known variants of cylindric algebras, like Pinters algebras and Halmos quasipolyadic algebras. which as previously indicated can be formulated as G algebras, for certain fixed choices of G.

These, with cylindric algebras, are also systems of varieties definable by schemes in the sense of [AN80]. However Sains algebras and Halmos polyadic algebras are not systems of varieties definable by schemes.

Now let us focus on similarities, rather than on differences.

For all these algebras, we have a uniform schema Σ_{α} axiomatising the abstract α dimensional algebras. We can speak about neat embeddings and dilations. Moreover, a neat embedding Theorem, to the effect that algebras having an ω dilation, equivalently having the neat embedding property are representable, is at our disposal.

Baring this in mind, we abstract the property (expressed as (*)) in the outline of the proof of proposition 1.

Let K be as indicated above. RK_{ω} stands for SNr_{ω}K_{ω+ω}. Let L ⊆ RK_{ω} such that SL = L.

We say that L has the S − neat − reduct property or SNR for short, if for all A ∈ L, there exists an ω dilation A^{+} of A (here the NET is used), such that:

A ⊆ Nr_{ω}A^{+}, and for all X ⊆ A we have:

Sg^{A}X = Nr_{ω}Sg^{A^{+}}X

.

SC, CA, QP A and QP EA, stand for Pinter’s algebras, cylindric algebras, quasipolyadic algebras, and quaipolyadic equality algebras, respectively. In [S99a], it was shown that for K ∈ {SC, CA, QP A, QP EA}, the class of the so called weak set algebras of dimension ω, or W Ks_{ω} for short, does not have the SNR property. This was used in [S99b] to show that any L (that has AP) such that W Ks_{ω} ⊆ L ⊆ RK_{ω} fail to have SAP even w.r.t RK_{ω}.

In the proof of proposition 1, we used the SNR property (expressed by (*)) in showing that G algebras have SAP.

While Sain proved that the richness of G is essential as far as representability is concerned, this paper seem to confirm that the same property is also essential for proving strong amlgamation, in so far as richness imply the SNR property.

It is known that if K is a quasivariety that has AP then K has SAP if and only if in K (regarded as a concrete category, with homomorphisms representing morphisms) epimorphisms, or epis for short, in the categorial sense are surjective.

Here we have replaced the “epis are surjective” condition by the SNR property, which very loosely speaking says: ”terms definable in ω extra dimensions are term definable”.

d. Using the ideas in (a) and (c) above, it is proved in [SS99] that Nemeti’s directed cylindric algebras, (cf [Sagi99] chapter 5) which is another solution to a different version of the finitization problem (in non well founded set theories), have SAP. This follows from the fact that in these algebras, (like Sains algebras) representability is defined via a neat embedding theorem, and neat reducts commute with forming subalgebras.

References

1. [A93] Amer,M., Cylindric algebras of sentences. Abstract. Journal of Symbolic logic 58,2.p.743.1993

2. [AHS] Adamek,J.,Herrlich,H. and Strecker,G.,Abstract and concrete categories, or the joy of cats. John Wiley and sons (1990)

3. [An97] Andreka,H., Complexity of equations valid in algebras of relations. Annals of Pure and Applied logic, 89, pp 149-209. 1997

4.[AKNS] Andreka.H.,Kurucz.A.,Nemeti,I.,Sain.,I Applying algebraic logic; a general methodology Preprint Math.Inst., Budapest, 1994, 72 pages.

5. [AGN77] Andreka,H., Gregely,T., and Nemeti,I., On universal algebraic constructions of logics Studia Logica , vol 36, p.9-47. 1977.

6.[AMN91] Andreka,H, Monk., J.D., Nemeti,I. (editors) Algebraic Logic North- Holland Amsterdam, 1991.

7.[AN75] Andreka,H., Nemeti,I., A simple purely algebraic proof of the completeness of some first order logics Algebra Universalis. vol 5,p. 8-15b 1975

8.[AN78] Andreka,H., Nemeti,I., Neat reducts of varieties Studia. Sci. Math. Hungarica. vol 13, p.47-51 1978

9. [ANS96] Andreka,H., Nemeti,I., and Sayed Ahmed,T., On neat reducts of algebras of logic. Presented in Logic Colloquium 1996. Abstract appeared in the Bulletin of Journal of Symbolic Logic.

10.[ANS98] Andreka.,H, Nemeti.,I, and Sayed Ahmed,T.,Amalgamation in algebras of logic. Presented in the “Universal Algebra and Lattice Theory” conference held in Szeged , Hungary 1998. In preparation.

11. [AS98] Andreka,H., and Sayed Ahmed,T., Omitting types in logics with finitely many variables. In preparation. Presented in the Logic Colloquium 1998. An abstract appeared in the Bulletin of the Journal of Symbolic Logic.

[BP89] Block.W.J., and Pigozzi.D. Algebraizable logics. Memoirs of Amer.Math.Soc., vol 77., no 396 1989

[BS] S.Burris and H.P. Sankappanavar. A Course in Universal Algebra. Graduate Texts in Mathematics. Springer-Verlag, New York, 1981.

[C74] Craig. Logic in algebraic form North Holland Amsterdam (1974) 204 pages. 10. [CK] Chang, Keisler Model Theory. North Holland, 1994.

[D63] Freedom in polyadic algebras and two theorems of Beth and Craig. Michigan Math.J.11 (1964) 129-135.

11. [DM63] Diagneault,A., and Monk,J.D., Representation Theory for Polyadic algebras. Fund.Math. Vol 52 p.151-176, 1963

12.[J69] Nonfinitizability of classes of representable polyadic algebras, J.Symbolic Logic 34 (1964)]

13.[F98] Ferenczi M., On representability of neatly embeddable cylindric algebras. Journal of applied non-classical logics. To appear.

14. [HMT1] Henkin,L., Monk,J.D., and Tarski, A., Cylindric Algebras Part I. North Holland, 1971.

15. [HMT2] Henkin,L., Monk,J.D., and Tarski,A., Cylindric Algebras Part II. North Holland, 1985.

16. [HMTAN] Henkin,L., Monk,J.D., Tarski,A., Andreka,H., and Nemeti,I., Cylindric Set Algebras, lecture notes in Mathematics 883, Springer Verlag, 1981.

17. [HH97] Hirsch,R., and Hodkinson,I., Step by step-building representations in algebraic logic. Journal of Symbolic Logic, 62(1)p.225-279, 1997.

19. [Hod85] Hodges W. Model Theory Cambridge. University press. 1995

20. [J70] Johnson, J.S. Amalgamation of Polyadic Algebras. Trans. Amer.Math.Soc., vol 17, p.834. 1970

23. [Ma77] Maddux ,R., Relation algebras and neat embeddability of cylindric algebras. Notices American Math. Society. vol 24. p.298 1977.

24. [Ma78] Maddux,R., Topics in relation algebras P.h.D dissertation. University of California, Berkley. 1978.

25 .[M69] Monk., J.D., Non finitisability of classes of representable cylindric algebras. Journal of Symbolic Logic. vol 34 p.331-343. 1969.

26. [M91] Monk.,J.D., Remarks on the problems in the books Cylindric Algebras, Part I and Part II and Cylindric set algebras. In Algebraic Logic p.723-746, edited by Andreka, H., Nemeti.I., and Monk.J.D., North Holland, Amsterdam. 1991.

27. [N83] Nemeti,I., The Class of Neat Reducts of Cylindric Algebras is Not a Variety But is closed w.r.t. HP. Notre Dame Journal of Formal logic, Volume 24, Number 3, July 1983, pp 399-409.

28. [N96] Nemeti,I., Algebraisation of quantifier logics, an introductory overview. Math.Inst.Budapest, Preprint, No 13-1996. A shortened version appeared in Studia Logica vol 50.4 p.465-569. 1991.

[NS98] I.Nemeti,G.Sagi On the equational theory of representable polyadic algebras. Journal of Symbolic logic, to appear.

29. [Pi71] Pigozzi,D., Amalgamation, congruence extension, and interpolation properties in algebras. Algebra Universalis. Vol 1. p.269-349. 1971.

30. [Sa89] Sain I. Beth and Craigs properties via epimorphism in Algebraic Logic Manuscript. Mathematical Institute. Budapest. 1989.

31. [Sa98] Sain,I. Searching for a finitisable algebraisation of first order logic. Submitted. 32.[ST91] Sain,I. Thompson,R, Strictly finite schema axiomatization of quasi-polyadic al-

gebras. in [AMN91] p.539-571.

33.[Sagi98] Non computability of the axioms of the ω dimensional polyadic algebras. Preprint. submitted]

34.[Sagi99] Sagi, G. On the Finitization Problem of Algebraic Logic Ph.D dissertation. Budapest 1999.

35 [SS99] Sagi, G, Sayed Ahmed T. Nemeti’s directed cylindric algebras have the strong amalgamation property. Manuscript. 1999

36. [S97] Sayed Ahmed, T. Algebras of sentences of Logic. Masters Thesis, Cairo University. 1997.

37.[S99]. Sayed Ahmed, T. On neat reducts of algebras of logic Manuscript.1999 38.[TG89] Tarski,A., Givant,S. A formalization of set theory without variables AMS Collo-

quium Publications vol. 41, 1998.