Finite algebras of relations are representable on finite sets

H. Andréka, I. Hodkinson, I. Németi^{∗}

13 December 1996

Abstract

Using a combinatorial theorem of Herwig on extending partial isomorphisms of relational structures, we give a simple proof that certain classes of algebras, including Crs, polyadic Crs, and WA, have the ‘finite base property’ and have decidable universal theories, and that any finite algebra in each class is representable on a finite set.

1 Introduction

In this paper, we give a simple proof that certain classes K of algebras have the ‘finite base property’. This will imply decidability of the universal theory of K, and that any finite algebra in K is representable on a finite set. Examples of such K include the relativized cylindric set algebras in dimension n (Crs_{n}), polyadic Crs, and the weakly associative relation algebras WA. Most of these results were first established in the paper [ABN2]; the original proofs were substantially longer than the present one.

What is the finite base property?

Say that we are given a class K of concrete algebras. This is to say that the algebras in K have the form A = ⟨A, f, g, …⟩, where A is the domain of A, and f, g, … are functions defined on A. However, the domain A is not merely an abstract set, but has intrinsic structure; and f, g, … are defined in terms of this structure, uniformly over K. In fact, A will typically be a subset of ℘(W), the power set of some set W of sequences of elements of another set, U. All the sequences will have the same finite length, n, so in symbols we have W ⊆ ^{n}U. The definitions of the functions f, g then utilise the form of the elements of A as sets of sequences. For example, for a, b ∈ A, f(a, b) might be a ∩ b, while g(a) might be the set of reverses of the sequences in a (the reverse of ⟨s_{0}, …, s_{n−1}⟩ being ⟨s_{n−1}, …, s_{0}⟩), and so on.

∗Andréka and Németi were supported by the Hungarian National Foundation for Scientific Research, grant numbers T16448, T7255. We thank Szabolcs Mikulás for helpful comments on drafts of this paper.

The sets W and U associated with A are not unique — any larger sets will do too — but there will be unique smallest such sets for each A. The smallest W, obtainable as the union of all elements of A, is called the unit of A. The smallest U, obtainable as the set of all elements occurring in sequences in the unit, is called the base of A.

The class K is now said to have the finite base property if any universal sentence in the signature of K that is not valid in K is not valid in some A ∈ K with finite base. This property implies that a finite algebra (in finite similarity type) is isomorphic to one with a finite base (by taking the negation of the diagram of the algebra as our universal sentence: see the proof of theorem 4). It is formally stronger than what we may call the ‘finite algebra property’, which says that a non-valid universal sentence may be falsified in some finite A ∈ K (i.e., with finite domain). An algebra in K could be finite and yet have infinite base.

Why is the finite base property of interest? For one thing, it suggests that K is in some way a ‘nice’ class. For example, the algebras in K with finite base can often be enumerated recursively — certainly, this is true for the classes K we consider here. So if the universal theory Σ of K is recursively axiomatisable, the finite base property implies decidability of Σ. (In fact, we will show that there is a recursive bound on the size of the base of the algebra witnessing non-validity of a universal sentence ϕ, in terms of the syntactic size of ϕ. This yields decidability of Σ whether or not Σ is known to be recursively axiomatisable.) Notice that the finite algebra property is not sufficient in this regard, for as a finite algebra can have infinite base, it is not clear that we can recursively enumerate all finite algebras in K. For more information see [N92].

Further, given A = ⟨℘(W), f, g, …⟩ ∈ K, we may view W in a modal-logical way. We consider the modal formulas formed using a (k-ary) connective ♯_{f} for each (k-ary) function f of A. We evaluate them at sequences in W — so W is the set of possible worlds of our model. The intended semantics is that if (inductively) the sets of sequences in W at which formulas φ_{1}, …, φ_{k} hold are a_{1}, …, a_{k}, respectively, then the formula ♯_{f}(φ_{1}, …, φ_{k}) will hold precisely at the sequences in f(a_{1}, …, a_{k}). If f happens to be ‘normal and completely additive’ (in the current context, this means f(a_{1}, …, a_{k}) = ⋃_{s_{i}∈a_{i}, i≤k} f({s_{1}}, …, {s_{k}}) for all a_{1}, …, a_{k} ⊆ W), the connective ♯_{f} has a genuinely modal (Kripke) semantics, via the (k + 1)-ary accessibility relation R_{f} defined in the following standard way: for all s_{0}, …, s_{k} ∈ W, R_{f}(s_{0}, …, s_{k}) holds iff s_{0} ∈ f({s_{1}}, …, {s_{k}}). This justifies our calling the logic ‘modal’, as many of the functions usually considered (including those in this paper) are indeed normal and completely additive. The exceptions are the boolean operations (for example, W ∨ ∅ = W, while ⋃_{s_{1}∈W,s_{2}∈∅} s_{1} ∨ s_{2} = ∅) and, here, the counting quantifiers.

In this setting the modal formulas will correspond to algebraic terms, and validity of formulas in W to validity of equations in A. So the logic is decidable iff the equational theory of K is. The finite base property for equations only now corresponds to a strong n-dimensional form of the modal finite model property familiar to modal logicians.

Modalizing the classes of algebras studied here yields variants of the n-variable fragment of first-order logic, with semantics differing from the classical Tarskian view because W need not be of the form ^{n}U. These ‘mutant’ logics are under intensive study at the present time, and we cite [ABN1, VM] as sources. They frequently have desirable properties that nvariable first-order logic lacks (such as decidability, Craig interpolation, Beth definability).

The finite base property can also be useful in obtaining other theorems. For example: by the finite base property for cylindric-relativized set algebras (Crs_{n}), any finite Crs_{n} can be obtained by relativizing a finite cylindric set algebra (Cs_{n}). This was used by A. Simon [S] to prove that every finite cylindric algebra of dimension 3 can be obtained by twisting and relativization from a finite Cs_{3}. The finite base property for our classes K also can be seen as a combinatorial principle that we formalize roughly as ‘any finite pattern of n-ary relations can be realized also with finite n-ary relations’.

We will prove the finite base property for several classes of algebras, including the classes Crs, polyadic Crs, WA, and locally cubic n-dimensional relativized cylindric set algebras augmented with substitution operators. For definitions of these see section 3 and example 22, or [HMT,Madd]; but they all fit the framework described above, varying only in what functions are present and what properties of W are assumed. We actually prove a single result (theorem 4) that gives most of these as corollaries, and then extend it (theorem 23) to give the rest.

The proof of theorem 4 starts off similarly to modal filtration, which is entirely natural, as the finite base property is analogous to the modal finite model property. However, this does not necessarily yield an algebra whose elements are sets of sequences and with the functions defined in terms of this internal structure. So our proof must involve more work. The chief extra argument used is the following combinatorial theorem of Herwig. Theorem 23 is proved similarly, using a stronger version (theorem 16 below, from [He2]), and it establishes the finite base property for further classes of algebras, including the weakly associative algebras — a new result, we believe.

Theorem 1 (Herwig, [He1]) Let 𝔎 be a finite structure in a finite relational language L. There is a finite L-structure 𝔎^{+} ⊇ 𝔎 such that any partial isomorphism of 𝔎 is induced by an automorphism of 𝔎^{+}.

Herwig’s proof generalizes arguments of Hrushovski [Hr]. A primitive recursive upper bound on the cardinality |𝔎^{+}| of the domain of 𝔎^{+} in terms of k = |𝔎| and L may be extracted from the proof. The existence of a recursive bound follows from the theorem itself, as for each of the finitely many L-structures 𝔎 with domain of size k, we may enumerate all finite L-structures extending 𝔎, stopping when we find one with the property of the theorem. Lascar has a simpler proof of theorem 1, which may give a better bound. This will appear in a joint paper with Herwig, which places the result in the setting of free groups.

We will also borrow an idea from [MM] when dealing with counting quantifiers.

The ideas presented here will also yield a completeness theorem for the associated modal logic, without using ‘step-by-step’ arguments — see [VM,HHMMR].

The layout of the paper is as follows. In section 2 we prove the finite base property for a fairly general class of algebras, and in section 3 we use this result and the notion of subreducts to get the property for more classes. In section 4 we extend the results of section 2 to classes such as WA. In the final section we discuss some of the implications of these results.

Notation

Our notation is mostly standard, but the following list may help.

Sets. If X is a set, |X| denotes the cardinality of X, and ℘X the set of all subsets (the power set) of X. Id_{X} is the identity map on X. The ordinal n < ω is identified with {0, 1, …, n − 1}. If θ : X → Y is a map, and X′ ⊆ X, we write θ⌈X′ for the restriction of θ to X′.

Sequences. Let X be a set, and n < ω. An (n-)sequence (or n-tuple) of elements of X is a map from n into X. The set of all such sequences is denoted by ^{n}X. We use s, t, … to denote sequences of elements, and x̄, ȳ to denote sequences (or tuples) of variables. The length of x̄ is denoted by len(x̄). For i < n, the ith element of a sequence s is written as s_{i}, and we can write s as ⟨s_{0}, …, s_{n−1}⟩. If σ : n → n, then s ∘ σ is just the composition of the maps σ, s: so (s ∘ σ)_{i} = s_{σ(i)} for each i < n. If α : X → Y and s ∈ ^{n}X, then sα denotes the sequence ⟨s_{0}α, …, s_{n−1}α⟩ ∈ ^{n}Y. (Maps are often written on the right.) Thus s ∘ σ is the sequence ‘rearranged’ according to σ, while sα is the sequence where the ‘letters’ occurring in s are replaced according to α.

If Γ = {i_{0}, …, i_{k−1}} ⊆ n, where i_{0} < ⋯ < i_{k−1}, then for s ∈ ^{n}X, s⌈Γ denotes the sequence ⟨s_{i_{0}}, …, s_{i_{k−1}}⟩ ∈ ^{k}X. s ≡_{Γ} t will mean that s⌈(n \ Γ) = t⌈(n \ Γ), or equivalently, s_{i} = t_{i} for all i ∈ n \ Γ.

Rng(s) denotes the range of s: i.e., Rng(s) = {s_{i} : i < n}. The concatenation st of sequences s ∈ ^{n}X, t ∈ ^{m}X is the sequence u ∈ ^{n+m}X given by

u_{i} = \{ \begin{matrix}s_{i}, & if i < n \\ t_{i−n}, & if n ≤ i < n + m. \end{matrix}

Model theory. Classical model-theoretic (first-order) structures will be denoted by gothic letters. The domain (or universe) of the structure 𝔎 will be written as K; it is always non-empty. A relational signature (or similarity type) is one with no function symbols or constants. Apart from algebras (below), we will only consider relational structures (structures in a relational signature), or at worst structures whose signature L has no function symbols except possibly constants. If 𝔎 is an L-structure and R is an m-ary relation symbol in L, we write R^{𝔎} for the interpretation of R in 𝔎. So R^{𝔎} ⊆ ^{m}K. An L-structure 𝔍 is said to be a substructure of 𝔎 — in symbols, 𝔍 ⊆ 𝔎 — if J ⊆ K and 𝔍 ⊧ R(s) iff 𝔎 ⊧ R(s) for each R ∈ L (m-ary) and s ∈ ^{m}J. If X ⊆ K, 𝔎⌈X denotes the substructure of 𝔎 with domain X. We say that L-structures 𝔍, 𝔎 are isomorphic (written 𝔍 ≅ 𝔎) if there is a bijection between their domains that preserves all atomic L-formulas in both directions.

A partial isomorphism of 𝔎 is a partial one-to-one map α on K such that for each atomic L-formula φ(x_{0}, …, x_{m−1}) and s ∈ ^{m}(dom(α)), 𝔎 ⊧ φ(s) ↔ φ(sα). Note that partial isomorphisms will be written as acting on the right. An automorphism of 𝔎 is a partial isomorphism of 𝔎 that is a permutation of K (a bijection : K → K). The set Aut(𝔎) of all automorphisms of 𝔎 forms a group under composition and inverse of permutations, with identity element Id_{K}.

Algebras. These are structures whose signature has no relation symbols, but only function symbols and constants. They play a different role from the classical structures here, so we will write them differently, as A, B, …, with domains A, B, …. Note that the domain of an algebra may have pertinent intrinsic structure, as we saw. If u is an assignment of variables to elements of the domain of A, we write τ^{(A,u)} for the value of the term τ in A under this assignment. So τ^{(A,u)} ∈ A. If τ has no variables, we may write τ^{A} instead. In the same way, if f is a function symbol of the signature of A, we write f^{A} for its interpretation in A as a function on A. For terms τ, σ, we write A ⊧ τ = σ[u] if τ^{(A,u)} = σ^{(A,u)}.

Up to isomorphism there is a unique algebra in any signature with domain of size 1.

Conventions. n will be the algebra dimension; i, j will denote ordinals < n; σ will denote a map : n → n; and Γ will denote a subset of n.

2 Proving the finite base property

We wish to prove the finite base property for various classes of algebras, which are defined in section 3 below. Rather than prove many similar theorems, we will show that the following class C of algebras has the finite base property, and then derive the particular results as corollaries using the notion of subreducts (definition 9). Some classes (such as WA) that do not succumb to this will be dealt with later, in theorem 23.

Recall that n, the dimension, is fixed throughout and satisfies 2 ≤ n < ω.

2.1 Definitions

Definition 2 Define C to be the class of all algebras A of the following form. The signature or vocabulary of A consists of the following function symbols:

binary: · (used in infix form)

unary: −, c_{(Γ)}, s_{σ}, and e_{r}, for each Γ ⊆ n, σ : n → n, r < ω. We may write c_{i} instead of c_{({i})}, for i < n.

constant symbols: 0, 1, and d_{ij}, for each i, j < n.

The domain or universe of A is a subset A of ℘(W), where W ⊆ ^{n}U for some arbitrary set U. It is mandatory that A contains the interpretations of the constant symbols and is closed under the interpretations of the function symbols. These are:

• ‘·’ is interpreted as intersection, and ‘−’ as complement relative to W (that is, a · b = a ∩ b and −a = W \ a, for all a, b ∈ A).

• 0 and 1 are interpreted as ∅ and W, respectively. W is called the unit of the algebra.

• d_{ij} is interpreted as the ‘diagonal’ {s ∈ W : s_{i} = s_{j}}.

• s_{σ} is interpreted as substitution via the map σ: for each a ∈ A, s_{σ}^{A}a = {s ∈ W : s ∘ σ ∈ a}.

• c_{(Γ)} is interpreted as cylindrification along all components in Γ: for each a ∈ A, c_{(Γ)}^{A}a = {s ∈ W : s ≡_{Γ} t for some t ∈ a}.

• e_{r} is a counting quantifier. For each r < ω, e_{r}a is interpreted as W if |a| ≥ r, and ∅ otherwise, for each a ∈ A. That is, e_{r}^{A}a = {s ∈ W : |a| ≥ r}. The e_{r} are sometimes called ‘graded modalities’.

See the previous section for notation used here. Thus, A has the form

⟨A, ·, −, 0, 1, d_{ij}, s_{σ}, c_{(Γ)}, e_{r}⟩_{i,j<n, σ:n→n, Γ⊆n, r<ω}.

Definition 3 The base of an algebra A ∈ C is the smallest set U such that 1^{A} ⊆ ^{n}U.

2.2 Finite base property for C

Theorem 4 Any universal sentence that is not valid in C is falsifiable in an algebra A ∈ C with finite base. In fact, from the universal sentence we can compute an upper bound for the size of this finite base.

Hence, the universal theory of C is decidable; and if C’ is the class of reducts of algebras in C to any finite signature, then any finite algebra in C’ is isomorphic to an algebra in C’ with finite base.

Proof.

Let T be any finite set of terms in the language of C that is closed under taking subterms, let A ∈ C, and let u be an assignment of the variables in T to elements of A. We will construct an algebra B ∈ C with finite base and an assignment v of the same variables to elements of B such that for all τ, σ ∈ T ,

(∗) A ⊧ τ = σ[u] iff B ⊧ τ = σ[v].

This will imply the first part of theorem 4 because of the following. Let ∀x̄ψ be a universal sentence that is not valid in C, where ψ is quantifier-free. Let T be the set of terms occurring in ψ, and let A ∈ C and u be such that A |̸= ψ[u]. Take B ∈ C with finite base and v for which (∗) holds. Then clearly, B |̸= ψ[v], and so ∀x̄ψ fails in a member of C with finite base.

So let T , A and u as above be given. We may assume that 1 ∈ T . Let the base of A be U, and let Q be an arbitrary finite subset of U. (We will use Q to handle the counting operations e_{r}; in this we borrow an idea from [MM]. So at the moment Q is arbitrary, but later we will make a restriction on it.)

Form a first-order relational signature \overline{T} as follows. For each term τ ∈ T , \overline{T} contains a relation symbol \overline{τ}. If τ does not begin with c_{(Γ)} for some Γ, then the arity of \overline{τ} is n. Otherwise, τ begins with c_{(Γ)}, so is of form c_{(Γ)}τ′ for some τ′, and in this case the arity of \overline{τ} is n − |Γ|. (This is so even if τ′ is itself of the form c_{Δ}τ′′.)

Now create a classical first-order \overline{T} -structure 𝔘 as follows. The domain of 𝔘 is U. The relation symbol \overline{τ} is interpreted in 𝔘 as τ^{(A,u)} if the arity of \overline{τ} is n. Otherwise, τ is of the form c_{(Γ)}τ′, and then we interpret \overline{τ} in 𝔘 as \{s⌈(n \ Γ) : s ∈ τ′^{(A,u)}\}. For example, if Γ = n then \overline{τ}^{𝔘} is either the set containing the empty tuple, if τ′^{(A,u)} ≠ ∅, or the empty set, otherwise. (Notice that we define \overline{τ}^{𝔘} in terms of τ′^{(A,u)}, and not \overline{τ′}^{𝔘}, which may have lower arity than n.)

For any s ∈ ^{n}U we define the structure 𝔘(s) to be the finite substructure of 𝔘 with domain Q∪Rng(s), expanded by additional constants naming s_{0}, …, s_{n−1} and the elements of Q. More precisely, we introduce new constants a_{q} and a_{i} for each q ∈ Q and i < n. (We may assume that Q ∩ n = ∅.) The signature of each 𝔘(s) is always the same, namely \overline{T} ∪ \{a_{q}, a_{i} : q ∈ Q, i < n\}. In 𝔘(s), the interpretation of a_{q} is q, and the interpretation of a_{i} is s_{i}, for each q ∈ Q and i < n, while with regard to relation symbols in \overline{T} , 𝔘(s) is a substructure of 𝔘.

Lemma 5 If s, t ∈ ^{n}U and 𝔘(s) ≅ 𝔘(t), then s ∈ τ^{(A,u)} iff t ∈ τ^{(A,u)} for all τ ∈ T .

Proof.

Indeed, assume that 𝔘(s) ≅ 𝔘(t). The unique isomorphism between 𝔘(s) and 𝔘(t) takes s to t. First let τ ∈ T be any term which does not begin with any c_{(Γ)}. Then s ∈ τ^{(A,u)} iff 𝔘(s) ⊧ \overline{τ}(s) iff 𝔘(t) ⊧ \overline{τ}(t) iff t ∈ τ^{(A,u)}. In particular, s ∈ 1^{A} iff t ∈ 1^{A}, since 1 ∈ T . Assume now that τ is of form c_{(Γ)}τ′. If s ∉ 1^{A}, then as t ∉ 1^{A}

too, s, t ∉ τ^{(A,u)}. So we may assume that s, t ∈ 1^{A}. Then

(†) s ∈ τ^{(A,u)} iff 𝔘(s) ⊧ \overline{τ}(s⌈(n \ Γ)),

and the same for t, because of the following. By the definition of \overline{τ}^{𝔘(s)} we have that 𝔘(s) ⊧ \overline{τ}(s⌈(n\Γ)) iff there is z ∈ τ′^{(A,u)} such that s ≡_{Γ} z, which by s ∈ 1^{A} holds iff s ∈ c_{(Γ)}^{A}τ′^{(A,u)} = τ^{(A,u)}.

Now (†) together with 𝔘(s) ≅ 𝔘(t) implies that s ∈ τ^{(A,u)} iff t ∈ τ^{(A,u)}, as required. ♣

The structures 𝔘(s) (s ∈ ^{n}U) have at most |Q| + n elements and their language is finite, so that there are only finitely many isomorphism types of them. Choose a finite subset K ⊆ U such that for all s ∈ ^{n}U there is t ∈ ^{n}K with 𝔘(t) ≅ 𝔘(s). Necessarily, Q ⊆ K (though of course, if this were not true we could simply add Q to K). For, if q ∈ Q, then q ∈ U, so there are s ∈ 1^{A} and j < n with s_{j} = q. Let t ∈ ^{n}K with 𝔘(t) ≅ 𝔘(s). Then t_{j} = q since by s_{j} = q we have that 𝔘(s) ⊧ a_{j} = a_{q}, so the same holds in 𝔘(t). Then q ∈ K by t ∈ ^{n}K.

Let 𝔎 be the substructure of 𝔘 with domain K. It has a finite relational signature, so we may use Herwig’s theorem (theorem 1) to obtain a finite \overline{T} - structure 𝔎^{+} ⊇ 𝔎 such that any partial isomorphism of 𝔎 is induced by an automorphism of 𝔎^{+}. Let G be the group consisting of all automorphisms of 𝔎^{+} that fix Q pointwise — that is,

G = {g ∈ Aut(𝔎^{+}) : xg = x for all x ∈ Q}.

Let

H = \{sg : s ∈ \overline{1}^{𝔎}, g ∈ G\} ⊆ ^{n}K^{+}.

We now obtain an algebra

B = ⟨℘(H), ·, −, ∅, H, d_{ij}, s_{σ}, c_{(Γ)}, e_{r}⟩_{i,j<n, σ:n→n, Γ⊆n, r<ω} ∈ C.

The base of B is a subset of K^{+}, and so is finite.

Define an assignment v of the variables in T to elements of the domain of B, by: v(y) = \{s ∈ H : 𝔎^{+} ⊧ \overline{y}(s)\}.

Lemma 6 For any g ∈ G, τ ∈ T , and s ∈ τ^{(B,v)}, we have sg ∈ τ^{(B,v)} also.

Proof.

A simple induction on τ. We want to prove that τ^{(B,v)} is preserved by G. Note that 1^{B} = H is preserved under G since G is a group (closed under multiplication). Also, y^{(B,v)} = v(y) is preserved by G, since each element of G is an automorphism of 𝔎^{+} and H is preserved under G. The rest follows from the fact that each operation of B is permutation-invariant, so if all the arguments are preserved by G then the result of the operation is also preserved by G. ♣

We can now prove the main lemma, analogous to the ‘truth lemma’ in modal filtration.

Lemma 7 For all τ ∈ T , we have s ∈ τ^{(A,u)} iff s ∈ τ^{(B,v)} for every s ∈ ^{n}K.

Proof.

By induction on the structure of τ. Let s ∈ ^{n}K be arbitrary.

The case τ = 0. Trivial. The case τ = 1. Then s ∈ 1^{B} iff s ∈ H, iff sg ∈ ^{n}K and 𝔎 ⊧ \overline{1}(sg)

for some g ∈ G, iff sg ∈ ^{n}K and 𝔎^{+} ⊧ \overline{1}(sg) for some g ∈ G (because 𝔎 ⊆ 𝔎^{+}). This holds iff 𝔎^{+} ⊧ \overline{1}(s) — ‘⇒’ because G ⊆ Aut(𝔎^{+}), and ‘⇐’ because s ∈ ^{n}K already. This is equivalent to 𝔎 ⊧ \overline{1}(s) (since s ∈ ^{n}K and 𝔎 ⊆ 𝔎^{+}), i.e., to s ∈ 1^{A}, by definition of 𝔎.

The case where τ is a variable. We have s ∈ v(τ) iff s ∈ H = 1^{B} and 𝔎^{+} ⊧ \overline{τ}(s). By the preceding case, τ = 1, and the fact that 𝔎 ⊆ 𝔎^{+}, this is iff s ∈ 1^{A} and 𝔎 ⊧ \overline{τ}(s), which holds iff s ∈ 1^{A} and s ∈ u(τ), by definition of 𝔎. This is iff s ∈ u(τ), as required.

The case τ = d_{ij}. Clear, since s ∈ d_{ij}^{A} iff s ∈ 1^{A} and s_{i} = s_{j}, iff

s ∈ 1^{B} and s_{i} = s_{j} (by the case τ = 1 above), iff s ∈ d_{ij}^{B}. The case −τ. Assume the lemma for τ. We have s ∈ −τ^{(A,u)} iff

s ∈ 1^{A} and s ∉ τ^{(A,u)}, iff s ∈ 1^{B} and s ∉ τ^{(B,v)} (by the case τ = 1 and the inductive hypothesis), iff s ∈ −τ^{(B,v)}.

The case τ · τ′. The proof is obvious. The case s_{σ}τ. Assume the lemma for τ. Then s ∈ (s_{σ}τ)^{(A,u)} iff

s ∈ 1^{A} and s ∘ σ ∈ τ^{(A,u)}. Note that s ∘ σ ∈ ^{n}K, also. So by the case τ = 1 and the inductive hypothesis, this is equivalent to s ∈ 1^{B} and s ∘ σ ∈ τ^{(B,v)}, i.e., s ∈ (s_{σ}τ)^{(B,v)}.

The case c_{(Γ)}τ. This is where the real work starts. Assume the lemma for τ. Suppose first that s ∈ (c_{(Γ)}τ)^{(B,v)}. Then there is t ∈ τ^{(B,v)} with t ≡_{Γ} s. Choose g ∈ G such that tg ∈ ^{n}K; g exists because t ∈ τ^{(B,v)} ⊆ 1^{B} = H. Now by lemma 6, tg ∈ τ^{(B,v)} also; by the inductive hypothesis, tg ∈ τ^{(A,u)}. So certainly, tg ∈ (c_{(Γ)}τ)^{(A,u)}. By definition of 𝔎, it follows that 𝔎 ⊧ \overline{c_{(Γ)}τ}(tg⌈(n \ Γ)). As g^{−1} is an automorphism of 𝔎^{+}, of which 𝔎 is a substructure, and t⌈(n \ Γ) = s⌈(n \ Γ) ∈ ^{n−|Γ|}K, we can apply g^{−1} to this and get 𝔎 ⊧ \overline{c_{(Γ)}τ}(s⌈(n \ Γ)). So by definition of 𝔎, there is s′ ∈ τ^{(A,u)} with s′ ≡_{Γ} s. Hence, s ∈ (c_{(Γ)}τ)^{(A,u)}. Note that for this last step we need to know that s ∈ 1^{A}; but s ∈ (c_{(Γ)}τ)^{(B,v)} ⊆ 1^{B}, so by the case τ = 1, s ∈ 1^{A}. See figure 1.

[figure: 𝔘; 𝔎; 𝔎^{+}; s; t ∈ τ^{(B,v)}; tg; \overline{c_{(Γ)}τ} holds here; ; ; ⇒; 𝔘; 𝔎; 𝔎^{+}; s ∈ c_{(Γ)}τ^{(A,u)}; s′ ∈ τ^{(A,u)}]

Figure 1.

Conversely, assume that s ∈ (c_{(Γ)}τ)^{(A,u)}. So there is t ∈ τ^{(A,u)} with t ≡_{Γ} s. We may not have t ∈ ^{n}K, but by choice of K there does exist t′ ∈ ^{n}K with 𝔘(t′) ≅ 𝔘(t). Let α : 𝔘(t′) → 𝔘(t) be the unique isomorphism. Then as t_{i} = s_{i} for all i ∈ n\Γ, the domain and range of the map

β = α⌈(Q ∪ {t′_{i} : i ∈ n \ Γ})

are contained in K, so β is a partial isomorphism of 𝔎. Using the properties of 𝔎^{+} given by Herwig’s theorem, let g be an automorphism of 𝔎^{+} extending β. Now by lemma 5, t′ ∈ τ^{(A,u)}, so by the inductive hypothesis, t′ ∈ τ^{(B,v)}. Clearly, g ∈ G, so by lemma 6, t′g ∈ τ^{(B,v)}. But t′g ≡_{Γ} t ≡_{Γ} s. As s ∈ 1^{B} (by reversing the proof that s ∈ 1^{A}, above), we obtain s ∈ (c_{(Γ)}τ)^{(B,v)}, as required. See figure 2.

[figure: 𝔘; 𝔎; 𝔎^{+}; s; t ∈ τ^{(A,u)}; t′g ∈ τ^{(B,v)}; t′; 𝔘(t) ≅ 𝔘(t′)]

Figure 2.

The case e_{r}τ. Recall that Q has so far been an arbitrary finite subset of U, the base of A. We now require that it is large enough to ensure that for each term in T of the form e_{r}τ,

(∗∗) |τ^{(A,u)} ∩^{n}Q| ≥ min(|τ^{(A,u)}|, r).

This is easily arranged. Now let e_{r}τ ∈ T and assume the lemma for τ.

Claim. |τ^{(A,u)}| ≥ r ⟺ |τ^{(B,v)}| ≥ r. Proof of claim. Assume that |τ^{(A,u)}| ≥ r. It follows from (∗∗) that |τ^{(A,u)} ∩^{n}Q| ≥ r. Since inductively, τ^{(A,u)} ∩^{n}Q ⊆ τ^{(B,v)}, we must have |τ^{(B,v)}| ≥ r. Conversely, suppose that |τ^{(A,u)}| < r. By (∗∗), τ^{(A,u)} ⊆ ^{n}Q. Let t ∈ τ^{(B,v)} be arbitrary, and let h ∈ G be such that th ∈ ^{n}K. Then by lemma 6, th ∈ τ^{(B,v)}, so by the inductive hypothesis, th ∈ τ^{(A,u)} ⊆ ^{n}Q. But by definition of G, h fixes Q pointwise, so th = t. Thus, t ∈ τ^{(A,u)}. So τ^{(B,v)} ⊆ τ^{(A,u)}, giving |τ^{(B,v)}| ≤ |τ^{(A,u)}| < r. This proves the claim.

Now, for all s ∈ ^{n}K, s ∈ (e_{r}τ)^{(A,u)} iff s ∈ 1^{A} and |τ^{(A,u)}| ≥ r, iff s ∈ 1^{B} and |τ^{(B,v)}| ≥ r (by the case τ = 1 and the claim), iff s ∈ (e_{r}τ)^{(B,v)}.

This proves the lemma. ♣

Corollary 8 σ^{(A,u)} = τ^{(A,u)} iff σ^{(B,v)} = τ^{(B,v)}, for all σ, τ ∈ T .

Proof.

Assume that σ^{(A,u)} ≠ τ^{(A,u)}. Let, say, s ∈ τ^{(A,u)} \ σ^{(A,u)}. Let t ∈ ^{n}K be such that 𝔘(s) ≅ 𝔘(t). By lemma 5, t ∈ τ^{(A,u)} \ σ^{(A,u)}. As t ∈ ^{n}K, by lemma 7 we have t ∈ τ^{(B,v)} \ σ^{(B,v)}, so that τ^{(B,v)} ≠ σ^{(B,v)}.

In the other direction, assume s ∈ τ^{(B,v)} \ σ^{(B,v)}. Then s ∈ 1^{B} by s ∈ τ^{(B,v)}, so sg ∈ ^{n}K for some g ∈ G. Then sg ∈ τ^{(B,v)} \ σ^{(B,v)} by lemma 6, and then sg ∈ τ^{(A,u)} \ σ^{(A,u)} by sg ∈ ^{n}K and lemma 7. ♣

This says that A ⊧ σ = τ[u] iff B ⊧ σ = τ[v] for all σ, τ ∈ T , which finishes the proof of the first part of theorem 4.

Finally, we can compute an upper bound β(ϕ) for the cardinality of the base of B from our universal sentence ϕ as follows. From ϕ we can compute T , and from T we can compute an upper bound for |Q|. Then from T , |Q| we can compute an upper bound for the number of isomorphism types of the structures 𝔘(s). This gives an upper bound for |K|, from which Herwig’s theorem gives an upper bound for |K^{+}|, which bounds the size of the base of B.

It follows that the universal theory of C is decidable. For, given a universal sentence ϕ of the signature of C, we may compute β(ϕ) as above, enumerate the finitely many algebras in the reduct of C to the symbols in ϕ with base of size at most β(ϕ), and evaluate ϕ in each. If we find one in which ϕ is false, then obviously ϕ is not valid in C. If not, then ϕ is valid in C.

It also follows that any reduct to a finite signature (say Σ) of a finite algebra in C is isomorphic in this signature to an algebra in C with finite base. For if A ∈ C is finite, with domain {a_{0}, …, a_{d−1}}, say, let ϕ(x_{0}, …, x_{d−1}) be a formula representing the diagram of A in Σ. (So ϕ is the conjunction of all Σ-formulas of the form x_{i_{0}} = f(x_{i_{1}}, …, x_{i_{r}}), where f ∈ Σ, {i_{0}, …, i_{r}} ⊆ d, and a_{i_{0}} = f^{A}(a_{i_{1}}, …, a_{i_{r}}), together with ⋀_{i<j<d} x_{i} ≠ x_{j}.) Then ∀x̄¬ϕ(x̄) is not valid in C, as it is not true in A. Hence there is B ∈ C with finite base, and elements b_{0}, …, b_{d−1} ∈ B such that B ⊧ ϕ(b̄). The map (a_{i} ↦ b_{i})_{i<d} is then a Σ-embedding : A ↪ B, so the restriction of B to {b_{0}, …, b_{d−1}} is an algebra in C with finite base and isomorphic to A in signature Σ.

This completes the proof of theorem 4. ♣

3 Corollaries

Now we want to prove the finite base property for more classes of algebras. This is not so hard: quite a few familiar classes can be obtained as subreduct classes of C; and we will show (corollary 10) that taking subreducts preserves the finite base property.

3.1 Subreduct classes

First we define what we mean by a subreduct class of C. We can get one by omitting some operations, by making restrictions on the unit of the algebras, and even by adding some new operations.

Definition 9 (A subreduct class of C) Let ȳ = ⟨y_{0}, …, y_{m−1}⟩ be a sequence of variables. We will call y_{i}, i < m, parameter variables; other variables will be called nonparameter variables.

Let χ = ⟨η, τ_{1}, …, τ_{k}⟩ be a sequence, where τ_{1}, …, τ_{k} are terms in the language of C, and η(ȳ, x) is a quantifier-free formula in the language of C which contains exactly one non-parameter variable (x). The signature associated to χ consists of function symbols f_{1}, …, f_{k}, where the arity of f_{i}, 1 ≤ i ≤ k, is the number of non-parameter variables of τ_{i}. Of course, we identify a 0-ary function symbol with a constant.

Assume that for every A ∈ C and every m-tuple ā of elements (parameters) from A, the set

η^{A}(ā) =_{def.} {b ∈ A : A ⊧ η(ā, b)}

is closed under the functions on A defined by the τ_{i}^{A}(ā), for each i. Then if η^{A}(ā) is nonempty, we obtain an algebra Aā in the new signature {f_{1}, …, f_{k}}. Its domain Aā is η^{A}(ā), and the function symbols f_{i} are interpreted in it as the restrictions to Aā of the functions defined by the τ_{i}^{A}(ā), for each i (1 ≤ i ≤ k).

If η^{A}(ā) is empty, then by convention we let Aā be the one-element algebra with doamin {∅}.

1. We say that an algebra of the signature associated to χ is a χ-subreduct of A ∈ C if it is a subalgebra of Aā for some A ∈ C and parameters ā from A.

Note that its domain is a subset of the domain of A.

2. The χ-subreduct class C_{χ} of C is defined as the class of all χ-subreducts of algebras in C.

3. A subreduct class of C is a χ-subreduct class for some χ.

Corollary 10 Let C′ be a subreduct class of C. Then C′ has the finite base property: if a universal sentence fails in C′, then it fails in a member of C′ with finite base. An upper bound for the size of this finite base can be computed from the universal sentence. Thus, the set of universal formulas valid in C′ is decidable.

Proof.

Let C′ be the χ-subreduct class of C, where χ = ⟨η, τ_{1}, …, τ_{k}⟩. Let ψ(x̄) be a quantifier-free formula in the language of C′, and assume that A′ |̸= ∀x̄ψ for some A′ ∈ C′. Let A ∈ C, and ā be an m-tuple of elements of A, such that A′ = Aā. If η^{A}(ā) is empty, then A′ is the one-element algebra, which is clearly isomorphic to an algebra with base of size 0; so already ∀x̄ψ fails in an algebra with finite base. Assume not. Then

A ⊧ ∃ȳ∃x̄( ⋀_{1≤i≤len(x̄)} η(ȳ, x_{i}) ∧ ¬ψ′),

where ψ′ is the formula we get from ψ by replacing each function symbol f_{i} with its ‘definition’ τ_{i} (in the obvious way; we do not go into the detailed definition now), and ȳ are the parameter variables. By theorem 4, there is B ∈ C with finite base such that

B ⊧ ∃ȳ∃x̄(⋀_{i} η(ȳ, x_{i}) ∧ ¬ψ′).

Then ∀x̄ψ fails in the biggest χ-subreduct of B, which is in C′ and has finite base, a subset of the base of B. Also, by theorem 4, an upper bound on the size of the base of B can be computed from the formula ∃ȳ∃x̄(⋀_{i} η(ȳ, x_{i})∧¬ψ′), and hence from ψ. Thus, the universal theory of C′ is decidable. ♣

3.2 Special cases

In this section we define some special classes of algebras investigated in the literature, and then we will show that they are all subreduct classes of C. Here, n remains the dimension of C.

Definition 11 1. Crs_{n} is the class of all subalgebras of algebras of the form

⟨℘(W), ·, −, 0, 1, c_{i}, d_{ij}⟩_{i,j<n},

where W ⊆ ^{n}U for some set U. Recall that we are writing c_{i} instead of c_{({i})}.

2. Polyadic Crs_{n} is the class of all subalgebras of algebras of the form

⟨℘(W), ·, −, 0, 1, c_{i}, s_{(i,j)}, s_{[i/j]}⟩_{i,j<n},

where W ⊆ ^{n}U for some set U. Here, we write (i, j) for the transposition map σ : n → n given by σ(i) = j, σ(j) = i, and σ(k) = k for all k ∈ n \ {i, j}. We write [i/j] for the map : n → n given by: [i/j](i) = j, and [i/j](k) = k for all k < n with k ≠ i.

3. We obtain C^{+} from C by adding the combined substitution-cylindrification operations s_{σ,Γ} for all σ : n → n and Γ ⊆ n. Take an algebra A in C, let its unit be W, and let a ∈ A. Then

s_{σ,Γ}(a) = {s ∈ W : s ∘ σ ≡_{Γ} t for some t ∈ a}.

Note that in the above definition, s∘σ does not necessarily belong to W, and indeed, s_{σ,Γ} is not expressible from s_{σ} and c_{(Γ)} for arbitrary W.

We interpose a lemma on a certain ‘reflexivity’ restriction on the unit.

Lemma 12 Let A ∈ C and let W = 1^{A} be the unit of A. The following are equivalent.

1. A is locally cubic [VM] — i.e., if s ∈ W and σ : n → n then s ∘ σ ∈ W

2. A ⊧ s_{σ}1 = 1 for all σ : n → n

3. W is the union of Cartesian spaces — sets of the form ^{n}U for some set U.

Proof.

1 ⇒ 2 : Assume that A is locally cubic, and let σ : n → n be given. If s ∈ W then s ∘ σ ∈ W, so s ∈ (s_{σ}1)^{A}. That is, W ⊆ (s_{σ}1)^{A}. The converse inclusion is obvious; so A ⊧ s_{σ}1 = 1.

2 ⇒ 3 : Assume that A ⊧ s_{σ}1 = 1 for all σ : n → n. Let s ∈ W. For any σ : n → n, (2) gives s ∈ (s_{σ}1)^{A}, so s ∘ σ ∈ W. We have proved s ∈ ^{n}Rng(s) ⊆ W, from which W = ⋃_{s∈W} ^{n}Rng(s) follows, giving (3).

3 ⇒ 1 : clear. ♣

Definition 11 (continued) 4. The subclass C^{lc} of C consists of all locally cubic algebras in C.

5. A locally cubic n-dimensional relativized cylindric set algebra augmented with substitution operators is a subalgebra of a locally cubic algebra of the form

⟨℘(W), ·, −, 0, 1, c_{i}, s_{σ}, d_{ij}⟩_{i,j<n, σ:n→n}.

Note that such a subalgebra will itself be locally cubic. We write S_{n} for the class of all such algebras.

6. The classes G_{n}, D_{n} are defined as follows:

G_{n} = {A ∈ Crs_{n} : A is locally cubic}

D_{n} = {A ∈ Crs_{n} : A ⊧ c_{i}d_{ij} = 1 for all i, j < n}.

We have G_{n} ⊆ D_{n} ⊆ Crs_{n}.

The class Crs_{n} is extensively investigated in the literature, e.g. in [HMTAN, HMT (section 5.5), Monk93, ABN1]. The class S_{n} is investigated, for example, in [VM], and the classes G_{n} and D_{n} in [N86, N96, AGN]. The class C^{+} is studied in [N96].

Lemma 13 All the classes defined in definition 11 are subreduct classes of C.

Proof.

Crs_{n} and polyadic Crs_{n} are obtained from C simply by omitting some operations. We can get Crs_{n}, for example, by taking

η(x) = x = x
τ_{·}(x, z) = x · z
τ_{−}(x) = −x
τ_{c_{i}}(x) = c_{i}(x) for all i < n, etc.

C^{+} is obtained from C by adding a new operation s_{σ,Γ}. C^{+} is rendered a χ-subreduct of C by letting

η(y, x) = x ≤ y ∧ ⋀_{σ:n→n} s_{σ}1 = 1
τ_{·}(x, z) = y · (x · z)
τ_{−}(x) = y · −x, etc. (i.e., relativize C-operations to y)
τ_{s_{σ,Γ}}(x) = y · s_{σ}c_{(Γ)}(x).

Notice that η^{A}(a) is closed under the functions so defined, for all A ∈ C and parameters a from A. If A ∈ C is such that 1^{A} is not closed under all s_{σ}, then for all a ∈ A, η^{A}(a) is the empty set, giving the one-element algebra as the χ-subreduct of A. Otherwise, by lemma 12 A is locally cubic, and it follows that the meaning of s_{σ,Γ} in χ-subreducts A′ of A is as intended. It can be checked that all algebras in C^{+} arise in this way.

C^{lc} is obtained from C by making a restriction on the unit 1. We can obtain C^{lc} as a χ-subreduct class of C by letting

η(x) = (x = x) ∧ ⋀_{σ:n→n} s_{σ}1 = 1.

If A ∈ C is not locally cubic then η^{A} is again the empty set, giving the oneelement algebra as the χ-subreduct of A. In the other cases, where A is locally cubic, the χ-subreduct of A is itself.

S_{n}, D_{n}, and G_{n} are obtained by combining these methods. ♣

Corollary 14 All the classes defined in definition 11 have the finite base property. In particular, a finite algebra in them is representable on a finite set, and the universal theory of the class is the same as that of the finite members. Further, the universal theories of the above classes are decidable.

Proof.

Use corollary 10, lemma 13, and also lemma 29 below. ♣

Finally, we note that we can look at theorem 4 as stating a combinatorial principle. Namely, it states that if a ‘pattern’ is realizable by n-ary relations at all, then it is realizable by finite n-ary relations also. Here by a pattern we mean a finite partial algebra in the similarity type of C. (By a finite partial algebra we mean one with finite domain, and with finitely many operations defined only.)

4 Generalisations

We can prove the finite base property for more classes using a recent strengthening of theorem 1, done by Herwig in [He2]. This gives a structure 𝔎^{+} ⊇ 𝔎 as in theorem 1 that ‘looks locally like 𝔎’ — roughly, any substructure of 𝔎^{+} that is ‘packed together’, in that any pair of distinct elements of it can be extended to a tuple lying in a relation, can be found already in 𝔎, except that extra relations may hold on the copy in 𝔎. This means that we can handle more operators than were in the class C. We discuss the strengthened theorem first, and then we apply it to algebras. Although theorem 23 and remark 26 below can be adapted to give theorem 4, we think it valuable to present both proofs because the argument in theorem 4 uses a more elementary version of Herwig’s theorem.

4.1 Strengthening Herwig’s theorem

First, a definition.

Definition 15 Let L be a relational signature, and 𝔐, 𝔑, L-structures.

1. A tuple (a_{1}, …, a_{m}) of elements of M is said to be live in 𝔐 if 𝔐 ⊧ α(a_{1}, …, a_{m}) for some atomic L-formula α(x_{1}, …, x_{m}) in which all of x_{1}, …, x_{m} occur.

2. 𝔐 is said to be irreflexive if whenever a_{1}, …, a_{m} ∈ M, R ∈ L, and 𝔐 ⊧ R(a_{1}, …, a_{m}) then the a_{i} are pairwise distinct.

3. 𝔐 is said to be packed if for any x, y ∈ M there are m-ary R ∈ L and elements a_{1}, …, a_{m} ∈ M with x, y ∈ {a_{1}, …, a_{m}} and 𝔐 ⊧ R(a_{1}, …, a_{m}).

4. A map ν : M → N is said to be a weak homomorphism : 𝔐 → 𝔑 if whenever R ∈ L is m-ary, a_{1}, …, a_{m} ∈ M, and 𝔐 ⊧ R(a_{1}, …, a_{m}), then 𝔑 ⊧ R(a_{1}ν, …, a_{m}ν).

Example: (a, a) is always live in 𝔐, as 𝔐 ⊧ a = a. Note that ν may not be one to one, and that fewer relations may hold on a tuple in 𝔐 than on its image in 𝔑.

The following can be easily extracted from [He2].

Theorem 16 (Herwig) Let 𝔎 be a finite irreflexive structure in a finite relational signature L. There is a finite irreflexive L-structure 𝔎^{+} ⊇ 𝔎 with the following properties.

1. Any partial isomorphism of 𝔎 is induced by an automorphism of 𝔎^{+}.

2. If s is a live tuple in 𝔎^{+}, then there is g ∈ Aut(𝔎^{+}) such that sg is a tuple of elements of K.

3. For any packed irreflexive L-structure 𝔐, if there is a weak homomorphism ν^{+} : 𝔐 → 𝔎^{+}, then there is a weak homomorphism ν : 𝔐 → 𝔎.

There is also a recursive (in 𝔎) upper bound for the size of K^{+}.

It is easy to show that irreflexivity is not needed here. At the same time, we take the opportunity to put the theorem in the form we will use. For this, we need the following definition.

Definition 17 Let L be a relational signature. A first-order L-formula π(x_{1}, …, x_{m}) with free variables x_{1}, …, x_{m} is said to be packed if (a) it is a conjunction of atomic Lformulas, and (b) whenever 1 ≤ i < j ≤ m, there is a conjunct of π in which x_{i}, x_{j} both occur.

Corollary 18 Let 𝔎 be any finite structure in a finite relational signature L. There is a finite L-structure 𝔎^{+} ⊇ 𝔎 with the following properties.

1. Any partial isomorphism of 𝔎 extends to an automorphism of 𝔎^{+}.

2. If s is a live tuple in 𝔎^{+}, then there is g ∈ Aut(𝔎^{+}) such that sg is a tuple of elements of K.

3. For any packed L-formula π(x̄), if 𝔎^{+} ⊧ ∃x̄π(x̄) then 𝔎 ⊧ ∃x̄π(x̄).

Proof (sketch).

The idea is very simple: we introduce relations of lower arity that replace the original ones wherever they are reflexive. This makes 𝔎 irreflexive, and we can apply theorem 16. Then we put the original relations back.

In a little more detail, for each n, each n-ary R ∈ L, and each equivalence relation E on n, we introduce a new |n/E|-ary relation symbol R_{E}. Let L′ consist of these new symbols. We also choose a transversal T_{E} for each E: that is, T_{E} is a set of representatives, one from each E-class on n. And for an n-tuple s, we let E_{s} be the equivalence relation {(i, j) : i, j < n, s_{i} = s_{j}} on n.

Define an L′-structure 𝔎′ with domain K as follows. For R_{E} ∈ L′, we let

(R_{E})^{𝔎′} = {s⌈T_{E_{s}} : s ∈ R^{𝔎}, E_{s} = E}.

Then 𝔎′ is irreflexive. Let 𝔎^{′+} ⊇ 𝔎′ be as in theorem 16. Define an L-structure 𝔎^{+} with domain K^{′+} as follows. For R ∈ L, of arity n, say, let

R^{𝔎^{+}} = {s ∈ ^{n}K^{′+} : s⌈T_{E_{s}} ∈ (R_{E_{s}})^{𝔎^{′+}}}.

Note that Aut(𝔎^{′+}) = Aut(𝔎^{+}).

We check that 𝔎^{+} fits the bill. Evidently, 𝔎 is a substructure of it. If α is a partial isomorphism of 𝔎, it is also a partial isomorphism of 𝔎′, so it extends to an automorphism g of 𝔎^{′+}. Then g is an automorphism of 𝔎^{+} extending α. Hence (1) holds. For (2), if |Rng(s)| = 1, it is clear. If 𝔎^{+} ⊧ R(s), then 𝔎^{′+} ⊧ R_{E_{s}}(s⌈T_{E_{s}}), so s⌈T_{E_{s}} is live in 𝔎^{′+} and by theorem 16(2) is mapped into K′ by some automorphism g of 𝔎^{′+}. Then g is also an automorphism of 𝔎^{+} and maps s into K. So (2) holds.

For (3), let π(x_{1}, …, x_{m}) be a packed L-formula, let s ∈ ^{m}K^{+}, and suppose that 𝔎^{+} ⊧ π(s). Let 𝔐 be the substructure of 𝔎^{′+} with domain Rng(s). If |Rng(s)| = 1, then by (2) above, there is g ∈ Aut(𝔎^{+}) mapping s into K, so 𝔎 ⊧ ∃x̄π(x̄). Assume that |Rng(s)| > 1. As 𝔎^{′+} is irreflexive, it can be checked that 𝔐 is a packed irreflexive L′-structure. The inclusion map is clearly a weak homomorphism from 𝔐 into 𝔎^{′+}. Hence, by condition (3) for 𝔎^{′+}, there exists a weak homomorphism ν : 𝔐 → 𝔎′. Note that because 𝔐 is packed and 𝔎′ is irreflexive, ν must be one-to-one. It follows that 𝔎 ⊧ π(sν). So (3) holds. ♣

4.2 Applications

Definition 19 Let Σ be a functional signature, and let n ≥ 1.

1. We say that an algebra A of signature Σ has dimension n if there are sets U, W (called the base and unit of A, respectively) with A ⊆ ℘(W) and W ⊆ ^{n}U, W, U being as small as possible subject to this.

Clearly, if A has a dimension then its base and unit are uniquely determined.

2. Let f ∈ Σ be an r-ary function symbol, let δ(x_{0}, …, x_{n−1}) be a first-order formula of the signature \{\overline{1}, R_{1}, …, R_{r}\} (all n-ary relation symbols), and let A be an ndimensional algebra of signature Σ with base U and unit W. We say that f is defined by δ in A, and that δ is the table of f (in A), if

f^{A}(a_{1}, …, a_{r}) = {s ∈ ^{n}U : (U, W, a_{1}, …, a_{r}) ⊧ δ(s)} for all a_{1}, …, a_{r} ∈ A,

where in the structure (U, W, a_{1}, …, a_{r}), the symbol \overline{1} is interpreted as W ⊆ ^{n}U, and R_{i} is interpreted as a_{i} (where 1 ≤ i ≤ r).

3. A table δ(x̄, R_{1}, …, R_{r}) is said to be existential-packed, or ‘EP’, for short, if it is of

the form

δ(x̄, R_{1}, …, R_{r}) = μ(x̄) ∧ ∃ȳ(ε(x̄, ȳ) ∧ π(ȳ)).

Here:

• x̄ = x_{0}, …, x_{n−1}, ȳ = y_{0}, …, y_{m−1} for some m < ω, and all the x_{i}, y_{j} are distinct variables.

• ε is a (possibly empty) conjunction of equalities of the form x_{i} = y_{j}, equating elements of x̄ with elements of ȳ.

• μ and π are quantifier-free formulas of the signature \{\overline{1}, R_{1}, …, R_{r}\}; they may involve equality, too.

• μ(x̄) ⊢ α(x̄) for some atomic formula α(x̄) of signature \{\overline{1}, R_{1}, …, R_{r}\} in which all variables in x̄ occur free.

• π is packed.

Example 20 All of the operations of definition 2 are EP (i.e., definable by EP tables), except for the counting quantifiers:

• The boolean operations are EP. Their tables are

\begin{aligned}δ_{0}(x̄) & = & x_{0} ≠ x_{0} \\ δ_{1}(x̄) & = & \overline{1}(x̄) \\ δ_{−}(x̄, R) & = & \overline{1}(x̄) ∧ ¬R(x̄) \\ δ_{·}(x̄, R_{1}, R_{2}) & = & R_{1}(x̄) ∧ R_{2}(x̄). \end{aligned}

Here, ‘∃ȳ(ε(x̄, ȳ) ∧ π(ȳ))’ is the ‘empty formula’ (i.e., we choose m = 0).

• d_{ij} is a nullary function with table \overline{1}(x̄) ∧ x_{i} = x_{j}.

• For σ : n → n, s_{σ} is a unary function with table \overline{1}(x̄) ∧ R(x_{σ(0)}, …, x_{σ(n−1)}).

• For Γ ⊆ n, c_{(Γ)} is a unary function with table \overline{1}(x̄) ∧ ∃y_{0} … y_{n−1}((⋀_{i∈n\Γ} x_{i} = y_{i}) ∧ R(y_{0}, …, y_{n−1})).

Further EP operations are also possible. The simultaneous cylindrification-substitution operations s_{σ,Γ} of section 3.2 may be introduced in this way. We may also define, in the manner of Marx and Németi (see [MNS]), an EP product p(a_{0}, …, a_{n−1}) of n n-ary relations, with table of the form

\overline{1}(x̄) ∧ ∃y_{0} … y_{n}( ⋀_{i<n} x_{i} = y_{i} ∧ [ ⋀_{i<n} R_{i}(y_{0}, …, y_{i−1}, y_{i+1}, …, y_{n}) ∧ \overline{1}(y_{0}, …, y_{n−1})]).

(The final \overline{1}(y_{0}, …, y_{n−1}) is needed when n = 2, to make the ‘π’-part packed, although omitting it does not change the logical meaning of the table.) Modulo a minor permutation of variables, in the case n = 2 this yields the classical product of two binary relations, relativized to the unit. The classical converse ă of a binary relation a is also EP. See example 22 below.

A final typical example comes from [J], in which the following m^{2}-ary operation on binary relations is defined and investigated: the defining formula is

Q_{m}(x_{0}, x_{1}, ⟨R_{ij} : i, j < m⟩) = ∃y_{0} … y_{m−1}(x_{0} = y_{0} ∧ x_{1} = y_{m−1} ∧ ⋀_{i,j<m} R_{ij}(y_{i}, y_{j})).

This is an EP formula.

Definition 21 Let Σ be a a functional signature. A class K of algebras of signature Σ is said to be EP if there are a number n ≥ 1, an EP table δ_{f} associated to each f ∈ Σ, and an existential sentence ξ of the signature Σ, such that K is the class of all n-dimensional algebras A of signature Σ such that (i) each f ∈ Σ is defined in A by δ_{f}, and (ii) A ⊧ ξ.

Example 22 The class WA of weakly associative algebras, defined in [Madd], is the closure under isomorphism of an EP class. For it may be defined as the isomorphism-closure of the class of all two-dimensional algebras of signature Σ = {·, −, 0, 1, Id,^{⌣} ,; } (Id is nullary, ⌣ unary, and ; binary), where the defining sentence ξ is (1 = ˘1) ∧ (1 = Id; 1) (which is quantifier-free), and the tables are as follows:

• For the boolean functions ·, −, 0, 1 see example 20.

• δ_{Id}(x_{0}, x_{1}) = x_{0} = x_{1}

• δ_{⌣}(x_{0}, x_{1}, R) = R(x_{1}, x_{0})

• δ_{;}(x_{0}, x_{1}, R_{1}, R_{2}) = \overline{1}(x_{0}, x_{1}) ∧ ∃y_{0}y_{1}y_{2}(x_{0} = y_{0} ∧ x_{1} = y_{1} ∧ R_{1}(y_{0}, y_{2}) ∧ R_{2}(y_{2}, y_{1}) ∧ \overline{1}(y_{0}, y_{1}))

(As before, the final \overline{1}(y_{0}, y_{1}) is there to ensure packedness; its omission does not change the meaning.) The sentence ξ enforces that the unit is a reflexive and symmetric binary relation on the base. The tables enforce that Id is interpreted in WA as equality, ^{⌣} as converse, and ; as relation composition, all relativized to the unit. There are related classes in which one or both of the reflexive and symmetric restrictions on the unit are dropped, and these are also EP.

Theorem 23 Let n ≥ 1 be finite, and let K be an EP class of n-dimensional algebras. Any universal sentence that is not valid in K is falsifiable in an algebra in K with finite base. An upper bound for the size of this finite base is computable from the sentence. K has decidable universal theory. If the signature of K is finite, then any finite algebra in K is isomorphic to an algebra in K with finite base.

Proof.

The proof is much as in theorem 4, and we only mention the differences. We wish to show that any existential sentence ϕ = ∃z̄ψ satisfiable in K is in fact satisfiable in some algebra in K with finite base. We may assume that ϕ logically entails the existential sentence ξ that defines K (as in definition 21). Let T be a finite set of terms that contains all the terms occurring in ψ and is closed under subterms. Assume we are given an algebra A ∈ K, and an assignment u of the variables in T to elements of A, such that (A, u) ⊧ ψ. We will find an n-dimensional algebra B with finite base of size effectively computable from T , and an assignment v of the variables in T to elements of B, such that (B, v) ⊧ ψ. Hence, B ⊧ ϕ; and as ϕ ⊢ ξ, it follows that B ∈ K.

Let U be the base of A. We form a finite relational signature, and a structure 𝔘 with domain U, as follows. First, we introduce an n-ary relation symbol \overline{1} and interpret it in 𝔘 as the unit of A. Then, for each τ ∈ T we introduce an n-ary relation symbol \overline{τ}, and interpret it in 𝔘 as τ^{(A,u)}. But there are more operation symbols. Let τ = f(τ_{1}, …, τ_{r}) ∈ T , where f is an operation defined on the algebras in K by the EP table δ = μ(x̄) ∧ ∃ȳ(ε(x̄, ȳ) ∧ π(ȳ)). Let μ(x̄, \overline{τ_{1}}, …, \overline{τ_{r}}) be the result of substituting the relation symbol \overline{τ_{i}} for R_{i} in μ, for each i. Suppose that ε is ⋀_{l<k} x_{i_{l}} = y_{j_{l}}, where i_{0} ≤ ⋯ ≤ i_{k−1} < n. Then a k-ary relation symbol τ† is also introduced, and interpreted in 𝔘 as

(τ†)^{𝔘} = \{(s_{i_{0}}, …, s_{i_{k−1}}) : s ∈ ^{n}U \ τ^{(A,u)}, 𝔘 ⊧ μ(s, \overline{τ_{1}}, …, \overline{τ_{r}})\}.

In the case τ = c_{(Γ)}τ′, for example, τ†^{𝔘} = {s⌈n \ Γ : s ∈ (−τ)^{(A,u)}}.

Choose ℓ ≥ n such that the table of any operation occurring in T contains at most ℓ variables, and take a finite substructure 𝔎 ⊆ 𝔘 containing isomorphic representatives of each substructure of 𝔘 of size at most ℓ. Let 𝔎^{+} ⊇ 𝔎 be as in corollary 18. Let B be the algebra with domain B = ℘(\overline{1}^{𝔎^{+}}), the operations being defined by the same tables as they are in K. Certainly, the base of B is finite — in fact, we have:

Lemma 24 The base of B is K^{+}, and the unit of B is \overline{1}^{𝔎^{+}}.

Proof.

It is clear that B’s unit is \overline{1}^{𝔎^{+}}. To show that K^{+} is its base, it

suffices to take arbitrary a ∈ K^{+} and find s ∈ \overline{1}^{𝔎^{+}} with a ∈ Rng(s).

As (a, a) is a live tuple in 𝔎^{+} (see definition 15), by corollary 18(2) there is g ∈ Aut(𝔎^{+}) with ag ∈ K. So we can assume that a ∈ K. As a is (now) in the base U of A, there is t ∈ \overline{1}^{𝔘} with a ∈ Rng(t). By choice of K, there is t′ ∈ \overline{1}^{𝔎} with 𝔎⌈Rng(t′) ≅ 𝔘⌈Rng(t). Let i < n be such that t_{i} = a. Then {(t′_{i}, t_{i})} is a partial isomorphism of 𝔎 which extends by corollary 18(1) to an automorphism g of 𝔎^{+}. Let s = t′g. Then we see that a = s_{i} ∈ Rng(s) and s ∈ \overline{1}^{𝔎^{+}}. ♣

Define an assignment v of the variables in T into B by v(z) = \overline{z}^{𝔎^{+}}. We can now prove an analogue of lemma 7:

Lemma 25 For each term τ ∈ T , we have τ^{(B,v)} = \overline{τ}^{𝔎^{+}}.

Proof.

By induction on τ. If τ is a variable then the statement holds by definition of v. Let τ = f(τ_{1}, …, τ_{r}) ∈ T and assume the result for τ_{1}, …, τ_{r}. For each i we have

τ_{i}^{(A,u)} = \overline{τ_{i}}^{𝔘} and τ_{i}^{(B,v)} = \overline{τ_{i}}^{𝔎^{+}}  (1)

(the first by definition of 𝔘, the second by the inductive hypothesis). Let the EP table of f be δ(x̄, R_{1}, …, R_{r}). Substitute the relation symbol \overline{τ_{i}} for R_{i} in this, for each i, to give the formula

δ(x̄) = μ(x̄) ∧ ∃ȳ(ε(x̄, ȳ) ∧ π(ȳ)).  (2)

We stress that δ, μ, π in (2) will in general involve n-ary predicates from \{\overline{1}, \overline{τ_{1}}, …, \overline{τ_{r}}\}, though for brevity we do not show these explicitly. Then by (1), using lemma 24 for the second line,

\begin{aligned}∀s ∈ ^{n}U, & s ∈ τ^{(A,u)} & ⟺ & 𝔘 ⊧ δ(s), \\ ∀s ∈ ^{n}K^{+}, & s ∈ τ^{(B,v)} & ⟺ & 𝔎^{+} ⊧ δ(s). \end{aligned}  (3)

Now we prove the lemma for τ. By (3), it suffices to show that if s ∈ ^{n}K^{+} then

𝔎^{+} ⊧ δ(s) ↔ \overline{τ}(s).  (4)

Now if s is a counterexample then s is live in 𝔎^{+}. (‘Live’ is defined in definition 15. If 𝔎^{+} ⊧ \overline{τ}(s) then it is obviously live; and if 𝔎^{+} ⊧ δ(s) then 𝔎^{+} ⊧ μ(s), so by the assumption on μ in definition 19(3), 𝔎^{+} ⊧ α(s) for some atomic formula α(x̄) of the signature \{\overline{1}, \overline{τ_{1}}, …, \overline{τ_{r}}\} in which all variables in x̄ occur.) So by corollary 18(2), s is mapped into nK by an automorphism of 𝔎^{+}, and as this automorphism preserves both sides of (4), we see that there is a counterexample to (4) in K.

So we may assume that s ∈ ^{n}K.

Suppose first that 𝔎^{+} ⊧ \overline{τ}(s). Since s ∈ ^{n}K now, we have 𝔘 ⊧ \overline{τ}(s), and so by definition of 𝔘, s ∈ τ^{(A,u)}. Let ȳ in (2) be y_{0}, …, y_{m−1}, and using (3) let t ∈ ^{m}U be such that 𝔘 ⊧ μ(s) ∧ ε(s, t) ∧ π(t). There are s′ ∈ ^{n}K and t′ ∈ ^{m}K such that, as substructures of 𝔘, we have s′t′ ≅ st. Then 𝔎^{+} ⊧ ε(s′, t′) ∧ π(t′), as this formula is quantifier-free. Moreover, the map s′ ↦ s is a partial isomorphism of 𝔎. Using corollary 18(1), let g ∈ Aut(𝔎^{+}) extend it. Then 𝔎^{+} ⊧ ε(s, t′g) ∧ π(t′g). Since 𝔘 ⊧ μ(s), and this formula is quantifier-free, 𝔎^{+} ⊧ μ(s), proving that 𝔎^{+} ⊧ δ(s) as required.

Conversely, if 𝔎^{+} ⊧ δ(s) then there is t ∈ ^{m}K^{+} such that 𝔎^{+} ⊧ μ(s) ∧ ε(s, t) ∧ π(t). Let ε = ⋀_{l<k} x_{i_{l}} = y_{j_{l}}, where i_{0} ≤ ⋯ ≤ i_{k−1} < n and j_{0}, …, j_{k−1} < m. Let

π^{∗}(ȳ) = π(ȳ) ∧ τ†(y_{j_{0}}, …, y_{j_{k−1}}).  (5)

Claim. 𝔎^{+} |̸= π^{∗}(t). Proof of claim. Assume the contrary. Now π^{∗} is clearly packed, so by corollary 18(3) we have 𝔎 ⊧ π^{∗}(t′) for some t′ ∈ ^{m}K. As π^{∗} is quantifier-free, 𝔘 ⊧ π^{∗}(t′). In particular, 𝔘 ⊧ τ†(t′_{j_{0}}, …, t′_{j_{k−1}}). By definition of τ†^{𝔘}, we may choose s′ ∈ ^{n}U \ τ^{(A,u)} with 𝔘 ⊧ μ(s) and (s′_{i_{0}}, …, s′_{i_{k−1}}) = (t′_{j_{0}}, …, t′_{j_{k−1}}). But now, 𝔘 ⊧ ε(s′, t′) ∧ π(t′), so 𝔘 ⊧ δ(s′) and (by (3)) s′ ∈ τ^{(A,u)}, a contradiction. This proves the claim.

But we have 𝔎^{+} ⊧ π(t), so by the claim, 𝔎^{+} |̸= τ†(t_{j_{0}}, …, t_{j_{k−1}}). As 𝔎^{+} ⊧ ε(s, t), this says that 𝔎^{+} |̸= τ†(s_{i_{0}}, …, s_{i_{k−1}}). But s ∈ ^{n}U, so also, 𝔘 |̸= τ†(s_{i_{0}}, …, s_{i_{k−1}}). As 𝔎^{+} ⊧ μ(s), the same holds in 𝔘. So by definition of (τ†)^{𝔘} we obtain s ∈ τ^{(A,u)}. By definition of \overline{τ}^{𝔘}, 𝔘 ⊧ \overline{τ}(s), and as s ∈ ^{n}K we have 𝔎^{+} ⊧ \overline{τ}(s) as required. The proof of (4) is complete. ♣

It now follows that two terms σ, τ ∈ T are equal in (A, u) iff they are in (B, v). For if s ∈ σ^{(A,u)} \ τ^{(A,u)} then 𝔘 ⊧ (\overline{σ} ∧ ¬\overline{τ})(s). By choice of K, there is s′ ∈ ^{n}K with the same property. By the lemma, s′ ∈ σ^{(B,v)} \ τ^{(B,v)}. Conversely, if s ∈ σ^{(B,v)} \ τ^{(B,v)} then the lemma yields 𝔎^{+} ⊧ (\overline{σ} ∧ ¬\overline{τ})(s). Hence s is live in 𝔎^{+}, and by corollary 18(2) we may suppose without loss of generality that s ∈ ^{n}K. So 𝔘 ⊧ (\overline{σ} ∧ ¬\overline{τ})(s), giving s ∈ σ^{(A,u)} \ τ^{(A,u)}.

It clearly follows that (B, v) ⊧ ψ; so as we said, B ⊧ ϕ, B ⊧ ξ, and B ∈ K. The rest of the proof is as in theorem 4. ♣

Remark 26 Recall that theorem 4 contained some additional arguments (borrowed from [MM]) to handle the counting quantifiers. These can be included in theorem 23, too, but for simplicity we omitted them. The same idea gives the following. Let K be as in the theorem. Take any finite set T of terms in the language of K, any A ∈ K, and any assignment u of the variables occurring in T to elements of A. Then there are B ∈ K with finite base and an assignment v of the variables to elements of B such that for all τ, σ ∈ T :

1. A ⊧ (τ = σ)[u] iff B ⊧ (τ = σ)[v].

2. If τ^{(A,u)} is finite, then τ^{(A,u)} = τ^{(B,v)}.

However, the proof does not give an effective bound on the size of the base of B in terms of T .

We indicate the modifications to the proof required to obtain this. We can assume that T is closed under taking subterms. For any τ ∈ T such that τ^{(A,u)} is finite, choose a finite subset Q_{τ} of U such that τ^{(A,u)} ⊆ ^{n}(Q_{τ}); otherwise let Q_{τ} = ∅. Set Q = ⋃{Q_{τ} : τ ∈ T } ⊆ U. Then Q is finite. Include in the signature of 𝔘 additional constant symbols to denote the elements of Q.

Note that any substructure of 𝔘 contains Q. Corollary 18 can be adapted in the style of theorem 4 to signatures with finitely many constant symbols, and lemma 25 can still be proved.

To show τ^{(A,u)} = τ^{(B,v)} when the former is finite, assume it is, and let s ∈ τ^{(A,u)}. Then s ∈ ^{n}Q ⊆ ^{n}K, so 𝔎^{+} ⊧ \overline{τ}[s] since 𝔘 ⊧ \overline{τ}[s], hence s ∈ τ^{(B,v)} by lemma 25. Conversely, assume s ∈ τ^{(B,v)}, i.e., 𝔎^{+} ⊧ \overline{τ}[s]. Then s is live in 𝔎^{+}, so s = s′g for some s′ ∈ ^{n}K and automorphism g of 𝔎^{+}. Then 𝔎^{+} ⊧ \overline{τ}[s′], hence 𝔘 ⊧ \overline{τ}[s′], i.e., s′ ∈ τ^{(A,u)}, and hence s′ ∈ ^{n}Q. But each automorphism of 𝔎^{+} is the identity on Q, so s = s′ and s ∈ τ^{(A,u)}.

Notice that we obtain as a special case of theorem 23:

Corollary 27 The class WA of weakly associative algebras is the closure under isomorphism of a class with the properties cited in theorem 23. The same holds for the related classes in which the unit is not required to be reflexive/symmetric.

Proof.

Example 22 shows that WA is the isomorphism-closure of an EP class, so that theorem 23 applies. ♣

5 Discussion

In this section we investigate the notion of finite base property a little more, and then we explore the possible improvements of our theorem 4. The class C is as in definition 2.

Definition 28 1. Let K ⊆ C, or more generally, K ⊆ C′ for some subreduct class C′ of C. Let S be a set of sentences. We say that K has the finite algebra property (respectively, finite base property) with respect to S if whenever a sentence in S fails in some algebra in K, it also fails in a finite algebra (respectively, in an algebra with finite base) in K.

Thus, K has the finite algebra property of the introduction if it has the finite algebra property with respect to the set of all universal sentences; and similarly for the finite base property.

2. We say that K has the finite algebra on finite base property if each finite member of K can be represented on a finite base (i.e., is isomorphic to an algebra in K with finite base).

In other words, K has the finite algebra property with respect to S means that the S-theory of K is the same as the S-theory of the class of all finite members of K.

We state the following simple lemma without proof.

Lemma 29 Let K ⊆ C, possibly with some C-operations dropped. The following are with respect to arbitrary S.

1. Suppose that the similarity type of K is finite. If K has both the finite algebra property and the finite algebra on finite base property then it has the finite base property. The converse holds if S contains all universal sentences.

2. K has the finite algebra (respectively, base) property iff every reduct of an algebra in K to a finite signature Σ is isomorphic to a reduct (to Σ) of a finite algebra (respectively, of an algebra with finite base) in K.

Using the terminology of definition 28, our theorem 4, corollary 14, and theorem 23 state that the classes C, C^{lc}, Crs_{n}, polyadic Crs_{n}, etc., all have the finite base property with respect to universal sentences. We now begin to discuss the possible improvements of these statements.

1. Let Cs_{n} = {A ∈ Crs_{n} : 1^{A} is a Cartesian space}, and Gs_{n} = {A ∈ Crs_{n} : 1^{A} is a disjoint union of Cartesian spaces}. Then Cs_{2}, Gs_{2} have the finite base property by [HMT, 4.2.8, 3.2.66], while for n ≥ 3, Cs_{n} has neither the finite algebra property with respect to equations, nor the finite algebra on finite base property. The same holds for Gs_{n}, cf. [N84] and [Monk91, status of Problem 4.15].

2. Crs_{n} for n ≥ 2 does not have the finite algebra property with respect to existential sentences. This follows from work of Mikulás [Mi], in which an equation e with free variable x is given such that A ⊧ e for some A ∈ Crs_{n} while for all A ∈ Crs_{n}, A ⊧ e implies that A is infinite. That is, the existential sentence ∃x¬e fails in Crs_{n} and it can fail only in infinite algebras in Crs_{n}. Roughly, the idea in [Mi] is to express with ∀x e that the unit ‘contains’ an injective but non-surjective function on (part of) the base.

3. Here we briefly summarize what is known about the finite base property in the theory of relation algebras. Let RA, SA, WA, Rs respectively denote the classes of all relation algebras, semi-associative relation algebras, weakly associative relation algebras, and set algebras. For definitions see [HMT, chapter 5.3] and [Madd], for example. Now, RA, SA, Rs do not have the finite algebra property for equations. Rs does not have the finite algebra on finite base property. The proofs for these are adaptations of the ones for the cylindric cases. It is proved in [N87] that WA has the finite algebra property. We proved above (corollary 27) that WA has the finite algebra on finite base property. (This was stated in [N96], but the proof therein contains an error.)

4. It is a useful general question to characterise the operators for which the finite base property holds — that is, what kind of tables, as in definition 19, are allowed?

First, one might consider adding to the signature of C some more interesting counting quantifiers, of the form e_{Γ}^{r} for arbitrary Γ ⊆ n, with semantics

e_{Γ}^{r}a = {s ∈ 1^{A} : |{t ∈ a : t ≡_{Γ} s}| ≥ r}

for an algebra A and a ∈ A. However, Mikulás proved in [Mi] that the resulting class does not have the finite algebra property with respect to equations, and indeed, for n ≥ 3 it has undecidable equational theory. But it still can have, in principle, the finite algebra on finite base property. It would be interesting to know whether it does or not.

5. The preceding point shows that we cannot be too liberal with what operators we include in the signature of C. On the other hand, we can be slightly more general and add any unary operators of the form f_{ψ}, where ψ(ȳ_{0}, …, ȳ_{r−1}) may be any quantifierfree first-order formula written with equality only, and ȳ_{0}, …, ȳ_{r−1} are n-tuples of distinct variables. The table δ(x̄, R) of the function f_{ψ} is

∃ȳ_{0} … ȳ_{r−1}(ψ(ȳ_{0}, …, ȳ_{r−1}) ∧ ⋀_{i<r} R(ȳ_{i})).

See definition 19. As x̄ does not occur in δ, the value of f_{ψ} is always empty or the unit. It is required of ψ that in any algebra, if a is infinite then f_{ψ}a is the unit. We can then adapt the proof of lemma 7, in particular, to handle these operators. The set Q should be chosen so that for each f_{ψ}τ ∈ T , ^{n}Q contains some s_{0}, …, s_{r−1} in τ^{(A,u)} such that U ⊧ ψ(s_{0}, …, s_{r−1}), if there are any (i.e., if (A, u) ⊧ f_{ψ}τ = 1), and the whole of τ^{(A,u)}, if not. Thus, the finite base property still holds.

Here are some examples of such ψ. (We write y_{ij} for the jth variable in the tuple ȳ_{i}.)

• ⋀_{i<j<r} ⋁_{k<n} y_{ik} ≠ y_{jk}, for which f_{ψ}a = e_{r}a, for all a. The counting quantifiers are therefore expressible by the operators f_{ψ}.

• ⋁_{η:r→n} ⋀_{i<j<r} y_{i,η(i)} ≠ y_{j,η(j)}, for which f_{ψ}a = 1 says that the ‘base’ of a, defined in the obvious way, has at least r elements.

Notice in each case that if a is infinite then there are s_{0}, …, s_{r−1} ∈ a such that U ⊧ ψ(s_{0}, …, s_{r−1}), as required. A non-example is February 10, 1997 27

• ⋀_{i<j<r, k,l<n} y_{ik} ≠ y_{jl}, for which f_{ψ}a = W expresses that the argument a has at least r pairwise disjoint sequences.

Here, a may be infinite and yet all its sequences may intersect. We wonder whether adding such an operator destroys the finite base property.

References

ABN1 H. Andréka, J. van Benthem, I. Németi. Modal languages and bounded fragments of predicate logic. J. Philosophical Logic, to appear.

ABN2 H. Andréka, J. van Benthem, I. Németi. Finite model property of bounded fragment of first-order logic and cylindric-relativized set algebras. Budapest, 1995, manuscript.

AGN H. Andréka, R. Goldblatt, I. Németi. Relativised quantification: some canonical varieties of sequence-set algebras. J. Symbolic Logic, to appear.

HMT L. Henkin, J. D. Monk, A. Tarski. Cylindric Algebras, Part I (1971), Part II (1985). North-Holland.

HMTAN L. Henkin, J. D. Monk, A. Tarski, H. Andréka, I. Németi. Cylindric set algebras. Lecture Notes in Mathematics Vol. 883, Springer–Verlag, Berlin, 1981.

He1 B. Herwig. Extending partial isomorphisms on finite structures. Combinatorica 15 (1995) 365–371.

He2 B. Herwig. Extending partial isomorphisms for the small index property of many ω–categorical structures. Israel J. Math., 1996, submitted.

HHMMR R. Hirsch, I. Hodkinson, M. Marx, S. Mikulás, M. Reynolds. Mosaics and step-by-step. Studia Logica, 1996, submitted.

Hr E. Hrushovski. Extending partial isomorphisms of graphs. Combinatorica 12 (1992) 411–416.

J B. Jónsson The theory of binary relations. In: Algebraic Logic (Proc. Conf. Budapest, 1988) Colloq. Math. Soc. J. Bolyai Vol. 54, North-Holland, Amsterdam, 1991. pp. 245–292.

Madd R. Maddux. Some varieties containing relation algebras. Trans. Amer. Math. Soc. 272 (2), 1982, 501–526.

MM M. Marx, S. Mikulás. Decidability and complexity of classical Cs_{2}. Imperial College, London, 1996, in preparation.

MNS M. Marx, I. Németi, I. Sain. Conjugated Boolean algebras with operators. Manuscript, in preparation.

Mi S. Mikulás. A note on expressing infinity in cylindric-relativized set algebras. King’s College London, preprint, 1996.

Monk91 J. D. Monk. Remarks on the problems in the books Cylindric Algebras, Part I and Part II and Cylindric Set Algebras. In: Algebraic Logic, Coll. Soc. J. Bolyai Vol. 54, North-Holland, Amsterdam, 1991. pp.719–722.

Monk93 J. D. Monk. Lectures on cylindric set algebras. In: Algebraic Methods in Logic and in Computer Science (Proc. Banach Semester, Fall 1991, ed. C. Rauszer). Banach Center Publications Vol. 28, Institute of Mathematics, Polish Academy of Sciences, Warsaw 1993, pp. 253–290.

N84 I. Németi. Neither the variety of cylindric algebras nor the variety of representable cylindric algebras is generated by its finite members for dimensions greater than 2. Preprint, Mathematical Institute, Budapest, 1984.

February 10, 1997 28

N86 I. Németi. Free algebras and decidability in algebraic logic. Doctoral Dissertation with the Academy, Budapest, 1986.

N87 I. Németi. Decidability of relation algebras with weakened associativity. Proc. Amer. Math. Soc. 100 no. 2 (1987) 340–344.

N92 I. Németi. Decidable versions of first-order logic. In: Logic Colloquium ’92, ed. L. Csirmaz, D. Gabbay, M. de Rijke, CSLI Publications & FoLLI, 1995, pp. 177–241.

N96 I. Németi. Fine structure analysis of first order logic. In: Arrow Logic and Multi-Modal Logic, M. Marx, L. Pólos and M. Masuch (eds.), CSLI Publications, 1996, pp. 221–247.

S A. Simon. Nonrepresentable algebras of relations. PhD Dissertation, in preparation. Budapest, 1996.

VM Y. Venema, M. Marx. A Modal Logic of Relations. Studia Logica, to appear (Report no. IR-396, Faculteit der Wiskunde en Informatica, Vrije Universiteit Amsterdam, 1995).

Andréka, Németi:  Hodkinson:
Mathematical Institute of  Department of Computing
Hungarian Academy of Sciences  Imperial College
Pf. 127  180 Queen’s Gate
1364 Budapest  London SW7 2BZ
Hungary  UK