On the equational theory of representable polyadic equality algebras (Extended abstract) ^{∗}

István Németi Gábor Sági^{†}

21 Jun, 1997

Abstract

Among others we will see that the equational theory of ω dimensional representable polyadic equality algebras (RP EA_{ω}’s) is not schema axiomatizable. This result is in interesting contrast with the Daigneault-Monk representation theorem, which states that the class of representable polyadic algebras is finite schema-axiomatizable (and hence the equational theory of this class is finite schema-axiomatizable, as well). We will also see that the complexity of the equational theory of RP EA_{ω} is also extremely high in the recursion theoretic sense. Finally, comparing the present negative results with the positive results of Ildikó Sain and Viktor Gyuris [10], the following methodological conclusions will be drawn: the negative properties of polyadic (equality) algebras can be removed by switching from what we call the “polyadic algebraic paradigm” to the “cylindric algebraic paradigm”.

1 Introduction

It is well known that the class RP EA_{ω} of (ω dimensional) representable polyadic equality algebras is not closed under taking of ultraproducts, and hence this class is not axiomatizable. This result leaves open the question of axiomatizability of the equational theory of RP EA_{ω}. The equational theory of RP EA_{ω} (Eq(RP EA_{ω}) for short) is not finitely axiomatizable, simply because the language of RP EA_{ω} contains uncountable many operation symbols. So the next interesting question is axiomatizability by some kind of schemas. Indeed, “schema axiomatization” has been the traditional approach in polyadic algebra theory, namely, Halmos’s axiom schemas, which appeared in 1960’s constitute a typical example for schema axiomatization (see [3]). In section 3 we will see that the equational theory of RP EA_{ω} is not axiomatizable by schemas similar to the usual defining schemas of (abstract) polyadic equality algebras. This result is in interesting contrast with the theorem of Daigneault and Monk [6], which states that the class of representable polyadic algebras RP A_{ω} (without equality) is finite schema axiomatizable. (Independently from Daigneault and Monk, Keisler proved the logical version of this representation theorem.)

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

†Supported by Hungarian National Foundation for Scientific Research grants T16448,F17452.

Before turning to the goal of section 3, let us look briefly to the goal of section 4. (The notational system will be recalled from the textbooks [4], [5] in section 2, till then we try to use as little notation as we can.) In section 4 we look at the equational theory of RP EA_{ω} from the point of view of recursion theoretic degrees of unsolvability. We have two aims with this:

(i) To shed some more light on the possibility or impossibility of finding some notion of a schema with which Eq(RP EA_{ω}) and related theories would be axiomatizable.

(ii) To study the complexity properties of theories like Eq(RP EA_{ω}) and its finite reducts on their own right.

We will see that Eq(RP EA_{ω}) is highly non-computable, and even its restrictions to finite sublanguages are very far from being recursively enumerable. More concretely, in Theorem 4.1 we will claim that

Eq(RP EA_{ω}) is Π_{1}^{1} hard (in the recursion theoretic sense).

This means the following: let N denote the standard model of arithmetic. There is a computable function (e.g. by a Turing machine)

T r : (Π_{1}^{1} formulas ^{1} of arithmetic) → (equations of RP EA_{ω})

such that for any Π_{1}^{1} sentence of arithmetic φ:

N ⊧ φ ⇔ RP EA_{ω} ⊧ T r(φ).

We will see that the above is meaningful because the range of T r contains only finitely many operation symbols (so the cardinality of Eq(RP EA_{ω}) causes no problem from the point of view of computability of T r).

1Π_{1}^{1} formulas are second order formulas in which the second order variables are quantified universally (in prenex form). For precise definitions we refer to [9]. We note that Π_{1}^{1} hardness automatically implies non-recursive-enumerability, but Π_{1}^{1} hardness is a much stronger negative property than this.

On the intuitive consequences of Theorem 4.1:

If Eq(RP EA_{ω}) were finitely axiomatizable by some kind of schemas, then the equational consequences of these schemas would form a Π_{1}^{1} hard set (by Theorem 4.1). Usually, finite (schema) axiomatizability of some theory implies recursive enumerability of this theory. So we conclude that Eq(RP EA_{ω}) can not be finitely (or recursively) axiomatizable by any kind of reasonable schemas. Further investigations and discussions in this line are in section 4.

It is interesting to contrast non-computability of Eq(RP EA_{ω}) (i.e. Theorem 4.1) with the fact that Eq(RCA_{ω}) and Eq(RQP EA_{ω}) are recursively enumerable (cf. e.g. Németi, [7]). Here, RCA_{ω} and RQP EA_{ω} denote the class of representable cylindric algebras and the class of representable quasi-polyadic algebras, respectively. For more on this contrast, cf. the end of section 5 herein. For completeness, we note that the main results of this paper are Theorems 3.7 and 4.1.

2 Notation

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

Sets: Throughout ω denotes the set of natural numbers. If A, B are sets then ^{A}B denotes the set of functions from A to B. If A is a set, then | A | denotes the cardinality of A. If A is a set then P(A) denotes the power set of A, that is, P(A) consists of all subsets of A.

Algebras: If K is a class of algebras, then HK, SK, PK denote the classes of homomorphic images, subalgebras and direct products of members of K, respectively.

Throughout we use function composition in such a way that the rightmost factor acts first. That is, for functions f, g we define f ∘ g(x) = f(g(x)).

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

⟨P(^{α}U), ∩, −, C_{(Γ)}, S_{τ}, D_{i,j}⟩_{Γ⊆α, τ∈^{α}α, i,j∈α}

where ∩ and − are intersection and complementation (wrt the top element ^{α}U), and for X ⊆ ^{α}U, Γ ⊆ α, τ ∈ ^{α}α and i, j ∈ α

C_{(Γ)}(X) = {s ∈ ^{α}U : (∃z ∈ X)(∀j ∉ Γ)(s_{j} = z_{j})}, C_{i}(X) = C_{({i})}(X), S_{τ}(X) = {s ∈ ^{α}U : s ∘ τ ∈ X}, D_{i,j} = {s ∈ ^{α}U : s_{i} = s_{j}}.

SP EA_{α} := S{A : A is a full polyadic equality set algebra of dimension α with base U, for some set U}.

SP EA_{α} is called the class of \underline{s}et \underline{p}olyadic \underline{e}quality \underline{a}lgebras of dimension α.

RP EA_{α} := SP{A : A is a full polyadic equality set algebra of dimension α with base U, for some set U}.

RP EA_{α} is called the class of \underline{r}epresentable \underline{p}olyadic \underline{e}quality \underline{a}lgebras of dimension α.

The class RP A_{α} of \underline{r}epresentable \underline{p}olyadic \underline{a}lgebras of dimension α is defined to be the class of D_{i,j} free subreducts of members of RP EA_{α}; in symbols:

RP A_{α} = SRd(RP EA_{α}).

For details see [5].

Definition 2.1 Throughout, α is an ordinal. L_{P EA_{α}} denotes the language of RP EA_{α}. For completeness we note that a detailed discussion is in [5], p.225.

We will denote the polyadic operations by ∩, −, C_{(Γ)}, S_{τ} and D_{i,j}. The corresponding operation symbols (in L_{P EA_{α}}) are ∧, −, c_{(Γ)}, s_{τ} and d_{i,j}, respectively.

3 Non schema-axiomatizability results

Definition 3.1 The class P EA_{ω} of \underline{p}olyadic \underline{e}quality \underline{a}lgebras of dimension ω is an abstract class defined by equation schemas (P_{0} − P_{11}, E_{1} − E_{3}) originating from Halmos. Cf. [3],[5] and the Appendix herein.

Let us turn to the difference (or distance) between P EA_{ω} and HSP(RP EA_{ω}). We will construct an equation that separates the two classes hence P EA_{ω} ≠ HSP(RP EA_{ω}). One could hope that adding new, similar schemas to P_{0} − E_{3} might lead to an axiomatization of HSP(RP EA_{ω}). We will see below that this cannot be done.

Motivating Example Consider the axiom schema of polyadic algebras s_{τ}s_{σ}(x) = s_{τ∘σ}(x) as an example. For simplicity let us write this as s_{τ}s_{σ} = s_{τ∘σ}. Let us notice that τ, σ (and ϱ below) are “meta-variables” ranging over ^{ω}ω. We can write the same schema in the form

(∗) τ ∘ σ = ϱ ⇒ s_{τ}s_{σ} = s_{ϱ}.

When studying schemas like (∗), sometimes it will be convenient to treat τ, σ and ϱ in (∗) as function symbols of some first order language L_{T}. At other times we will treat τ, σ and ϱ as second order variables ranging over functions.

Definition 3.2 L_{T} is the first order language that consists of countably many unary relational symbols, countably many unary function symbols and countably many constants (and nothing more), which are r_{1}, r_{2}, ... and f_{1}, f_{2}, ... and n_{1}, n_{2}, ... respectively.

Definition 3.3 Throughout L_{P T} denotes the similarity type (in the algebraic sense): of Boolean algebras with extra unary operation symbols c_{r_{1}}, c_{r_{2}}, ... and s_{f_{1}}, s_{f_{2}}, ... and constants d_{n_{1},n_{1}}, d_{n_{1},n_{2}}, d_{n_{2},n_{1}}.... Here, the indices of the symbols c, s and d are the same as the corresponding relation, function and constant symbols in the previous definition.

Definition 3.4 By a Halmos schema we mean a pair ⟨s, e⟩ where s is a first-order sentence in the language L_{T}, and e is an equation in L_{P T}.

We will denote ⟨s, e⟩ as s ⇒ e in order to keep the notation closer to intuition.

Motivating Example, Continued The form (∗) will help us in making certain things explicit about these kinds of schemas. Now let f_{1}, f_{2}, f_{3} ∈ ^{ω}ω. Then the equation s_{f_{1}}s_{f_{2}}(x) = s_{f_{3}}(x) will be called an instance of (∗) iff indeed f_{1} ∘ f_{2} = f_{3}. Thus, the single schema (∗) has continuum many instances (if the meta-variables τ, σ and ϱ are ranging over ^{ω}ω).

Definition 3.5 Let s ⇒ e be a Halmos schema, let g be an equation in L_{P EA_{α}}. We say that g is an (α dimensional) instance of s ⇒ e iff there exist sets, functions and constants

r_{1}^{M}, r_{2}^{M}, ..., ⊆ α, f_{1}^{M}, f_{2}^{M}, ... ∈ ^{α}α and n_{1}^{M}, n_{2}^{M}, ... ∈ α such that

M = ⟨α; r_{1}^{M}, r_{2}^{M}, ..., f_{1}^{M}, f_{2}^{M}, ...n_{1}^{M}, n_{2}^{M}, ...⟩ ⊧ s;

and g is obtained from e by replacing r_{i}, f_{i} and n_{i} by r_{i}^{M}, f_{i}^{M} and n_{i}^{M} respectively. In this case we say that g is an instance of e with respect to M.

Definition 3.6 Let A be an L_{P EA_{α}} type algebra. A Halmos schema h is valid in A iff every α dimensional instance of h is valid in A.

We note that one can easily translate the usual defining schemas of polyadic (equality) algebras into Halmos schemas. Consider for example s_{σ∘τ}(x) = s_{σ}s_{τ}(x), where σ, τ ∈ ^{α}α. This schema is axiom P_{7} in [5] on page 225, which is a typical example of the usual defining schemas of polyadic algebras. Let h be the following Halmos schema:

(∀x)(f_{1}(f_{2}(x)) = f_{3}(x)) ⇒ s_{f_{3}}(y) = s_{f_{1}}s_{f_{2}}(y).

Now one can easily see that the instances of P_{7} and the α dimensional instances of h are the same. In the Appendix we give Halmos schemas which correspond to the usual definition of P EA_{α}. That is, we give a complete list of the translations of the usual defining schemas of polyadic (equality) algebras. Now we can state our first main result.

Theorem 3.7

(i) The set Eq(RP EA_{ω}) of equations valid in RP EA_{ω} is not axiomatizable by any set of Halmos schemas. More formally:

(ii) Let Σ be a set of Halmos schemas valid in RP EA_{ω}. Then for the class Mod(Σ) of all models of all ω dimensional instances of Σ we have

Mod(Σ) ≠ HSP(RP EA_{ω}) or, equivalently, Ded(Σ) ≠ Eq(RP EA_{ω})

where Ded(Σ) denotes the set of equational consequences of Σ.

Unless otherwise specified, the proofs of theorems announced are found in [8]. Theorem 3.7 is a corollary of Theorem 3.15 at the end of section 3 below. Now we formulate an equivalent version of Theorem 3.7.

Definition 3.8 P EA_{α}^{+} denotes the class of all models of all α dimensional instances of those Halmos schemas which are valid in RP EA_{α}.

Note that P EA_{α}^{+} is the smallest variety which contains RP EA_{α} and is defined by Halmos schemas. The previous theorem stated that the variety generated by RP EA_{ω} is not axiomatizable by Halmos schemas, which is equivalent to the following.

Theorem 3.7^{∗} P EA_{ω}^{+} ≠ HSP(RP EA_{ω}).

To show this, we will construct an equation e_{CM} which is valid in RP EA_{ω} but not in P EA_{ω}^{+}. This equation is based on the method of W. Craig and R. McKenzie (cf. [2]), hence the notation.

First we introduce some notation. Throughout, t_{j}^{i}(x) abbreviates the term d_{i,j} ∧ c_{j}(x). As usual, [i, j] ∈ ^{ω}ω denotes the transposition which interchanges i and j and leaves every other element fixed. Here i and j are distinct elements of ω. The symbol suc denotes the successor function on ω. To build e_{CM}, we will introduce some simpler equations (see Definitions 3.9 and 3.13 below).

Definition 3.9 Throughout, e_{1}, e_{2}, e_{3} denote the following equations: e_{0} is x = c_{1}x, e_{1} is x − d_{3,4} ≤ d_{2,3}, e_{2} is (x ∧ d_{3,4} − c_{0}c_{1}t_{3}^{4}t_{2}^{3}s_{suc}(x)) ∧ (c_{0}c_{2}s_{[1,2]}(x) − c_{0}c_{2}t_{3}^{4}t_{1}^{3}s_{suc}(x)) ≤ d_{1,2}, e_{3} is x ∧ d_{3,4} ≤ c_{0}c_{1}c_{2}(x ∧ d_{3,4} − c_{0}c_{1}t_{3}^{4}t_{2}^{3}s_{suc}(x)).

The intuitive content of these equations will be illustrated in Theorem 3.11.

If s is a finite sequence, and h is another (possibly infinite) sequence, then s^{⌢}h denotes the concatenation of s and h.

Definition 3.10 Let A ∈ SP EA_{ω}, with base U, let a ∈ A, and let h ∈ ^{ω}U. Then (a)_{h} denotes the “projection” of a with respect to h to the second coordinate, that is, (a)_{h} = {u ∈ U : (∃v_{0}, v_{1} ∈ U) ⟨v_{0}, v_{1}, u⟩^{⌢}h ∈ a}.

Theorem 3.11 Suppose A ∈ SP EA_{ω}, with base U, and a ∈ A such that e_{0}, e_{1}, e_{2} and e_{3} hold for a. Then (∀h ∈ ^{ω}U)(| (a)_{h} | < ℵ_{0}).

Definition 3.12 Suppose A ∈ SP EA_{ω}, with base U, a ∈ A and h ∈ ^{ω}U. Then f_{a,h} denotes the following binary relation:

f_{a,h} = {⟨x, y⟩ ∈ ^{2}U : (∃z)(⟨y, z, x⟩^{⌢}h ∈ a)}.

Of course, dom(f_{a,h}) = (a)_{h}; where dom(f_{a,h}) is the domain of f_{a,h} in the usual sense (similarly, range(f_{a,h}) denotes the range of f_{a,h} ).

Definition 3.13 Throughout, e_{4}, e_{5}, e_{6}, e_{7} denote the following equations: e_{4} is s_{[0,1]}(x) ∧ x ≤ d_{0,1}, e_{5} is s_{[1,2]}(x) ∧ x ≤ d_{1,2}, e_{6} is s_{[0,2]}(x) ≤ c_{0}(x), e_{7} is s_{[0,2]}(x) ≤ c_{2}(x).

Suppose A ∈ SP EA_{ω}, with base U, a ∈ A, h ∈ ^{ω}U and C_{1}^{A}(a) = a. Let us notice that

e_{4}(a) expresses that f_{a,h} is a function, e_{5}(a) expresses that f_{a,h} is an injective relation, e_{6}(a) expresses that range(f_{a,h}) ⊆ dom(f_{a,h}), e_{7}(a) expresses that dom(f_{a,h}) ⊆ range(f_{a,h}).

The variety P EA_{ω}^{+} is a discriminator variety because c_{(ω)} is a complemented normal closure operator which majorizes all other extra-boolean operation. These properties are expressible by Halmos schemas. It is well known from the theory of discriminator varieties that the quasi-equations over a discriminator variety are translatable into equivalent equations. That is, for any discriminator variety V, and for any quasi-equation q over V, there is a translation tr(q) which is an equation and V ⊧ q iff tr(q) ∈ Eq(V). So below we will write quasi-equations and will refer to them as equations.

Definition 3.14 Throughout, e_{CM} is defined as follows:

e_{CM} is the (quasi-)equation e_{0}&e_{1}&...&e_{6} ⇒ e_{7}.

Theorem 3.15

(i) RP EA_{ω} ⊧ e_{CM}. (ii) P EA_{ω}^{+} |̸= e_{CM}.

It is easy to see that Theorems 3.7 and 3.7^{∗} indeed follow from Theorem 3.15.

Sketch of the proof of Theorem 3.15 Recall that (a)_{h} is the 2-th projection of the element a with respect to tail h. By Theorem 3.11, e_{0}&e_{1}&e_{2}&e_{3}(a) imply that (a)_{h} is finite. The equation e_{CM} formulates a combinatorial consequence of (a)_{h} being finite (injective selfmaps are surjective). Now, e_{CM} is true in the representable algebras simply because it formulates a true combinatorial principle. The proof of the second part consists of showing that the combinatorial principle coded by e_{CM} cannot be derived from the axioms of P EA_{ω}^{+}.

4 Complexity of the equational theories

As we mentioned in the introduction, in [6] Daigneault and Monk proved a representation theorem for (ω dimensional) polyadic algebras (P A_{ω} for short). However, this result does not imply that the equational theory of P A_{ω} is recursively enumerable. One simple reason for this is that the language of P A_{ω} contains a continuum of operation symbols. Actually, in [12] it is proved that intuitively, the set Eq(P A_{ω}) is not recursively enumerable for any reasonable generalization (to non-enumerable sets) of the notion of recursive enumerability. ^{2} More formally this is stated in Theorem 5.1 below.

In this section we will see that the set Eq(RP EA_{ω}), i.e., the equational theory of RP EA_{ω} is complex in the recursion theoretic sense as well. That is, Eq(RP EA_{ω}) is strictly more complex than the full first order theory of standard arithmetic.

To see this, we will recursively reduce the second order universal theory of standard arithmetic to Eq(RP EA_{ω}). By a Π_{1}^{1} formula of arithmetic we mean a second order formula of arithmetic in which every second order variable is quantified universally (in prenex form). This subject will be further discussed below the formulation of the next theorem. Recall that N is the standard model of arithmetic.

Theorem 4.1 Eq(RP EA_{ω}) is Π_{1}^{1} hard, by which we mean the following: there is a strictly finite reduct L of the language of RP EA_{ω} and a recursive function T r such that T r maps the Π_{1}^{1} formulas of arithmetic to equations written in L, and for any Π_{1}^{1} sentence σ of arithmetic

N ⊧ σ ⇔ RP EA_{ω} ⊧ T r(σ).

(For the second order logical and recursion theoretic details see the next remark and [9].)

Remark We say that a set A of natural numbers is Π_{1}^{1}, iff A is definable by a Π_{1}^{1} formula in arithmetic. The set S of all (Gödel numbers of) true Π_{1}^{1} sentences of arithmetic is not Π_{1}^{1}, by Tarski’s theorem of undefinability of truth. That is, S is more complex than any Π_{1}^{1} set. So Theorem 4.1 means that Eq(RP EA_{ω}) is more complex than any Π_{1}^{1} set, this property is called Π_{1}^{1} hardness.

Sketch of proof of Theorem 4.1 The proof is based on a systematic translation of the Π_{1}^{1} formulas of arithmetic into polyadic equations. For all n ∈ ω we can construct a polyadic equation e_{8} with one variable such that if an element y satisfies it (i.e. if e_{8}(y) holds), then one can identify (or simulate) ω with the first n projections (“columns”) of y. A further equation e_{9}(z) ensures that the element z codes the successor function “suc” on this ω. Then, using this y and z, we construct a translation mapping which associates to each arithmetical term τ the number theoretic meaning of τ in terms of y, z and the polyadic operations. This translation of τ is a polyadic term of y and z and the translation procedure can be generalize to translate even the Π_{1}^{1} formulas of arithmetic. The so obtained translation of Π_{1}^{1} arithmetic into the equational language of RP EA_{ω} (in some sense) is used to prove the theorem.

2The reason for this intuitive interpretation was given above Definition 4.2 for an analogous situation.

As we explained close to the end of section 1, Theorem 4.1 implies that Eq(RP EA_{ω}) can not be finitely (or recursively) axiomatizable by any kind of reasonable schemas. (From the point of view of certain applications this seems to be an inconvenient feature.)

An intuitive consequence of the above considerations is that Eq(RP EA_{ω}) is not computable. This is not a precise mathematical statement because the cardinality of this set is the continuum. But suppose one generalizes the concept of computability in a meaningful way to continuum big sets. Cf. the figure.

[figure: L_{P EA_{ω}}; L; Eq(RP EA_{ω})]

The only thing we assume about the new, generalized concept of computability is that the intersection of two computable set is computable, and countable sets are not computable if and only if they are non-computable in the old sense. Now Eq(RP EA_{ω}) is not computable in the new, generalized sense, because its intersection with a countable decidable (in the old sense) set L forms a Π_{1}^{1} hard (hence non-computable) set, as Theorem 4.1 states.

Concluding this section we briefly summarize some of the results concerning upper bounds for the complexity of Eq(RP EA_{ω}).

Definition 4.2 If Σ is a set of Halmos schemas then

Ded(Σ) = {e : e is an equation derivable from the ω dimensional instances of Σ}.

Let us call A ⊆ ω Σ_{1}^{1} enumerable if there exists an algorithm which uses an oracle deciding the Σ_{1}^{1} theory of standard arithmetic and enumerates A. Let L be a reduct of the language of RP EA_{ω}. In [8] we show that if L is of certain form and the basic operations of L are neither too numerous nor too complicated, then the set Ded(Σ) ∩ L of the L consequences of a finite schema Σ of axioms is Σ_{1}^{1} enumerable, i.e., “of relatively low complexity”.

Remark We do not claim that the set Ded(Σ) ∩ L is Σ_{1}^{1} i.e. is definable by some Σ_{1}^{1} formula of arithmetic.

5 Related Results

Here we summarize some results about the possibility of axiomatizing of some reducts of RP EA_{ω}. The complexities of the equational theories of these reducts are also discussed.

5.1 Case of algebras without equality

By the theorem of Daigneault and Monk, every P A_{ω} is representable, therefore the “complexity” of the equational theory of P A_{ω} is the same as the “complexity” of the set of all equational consequences of the P A_{ω} axiom schemas. But this representation theorem does not imply recursive enumerability, as the following theorem claims.

Theorem 5.1 There is a strictly finite reduct L_{G} of the language of P A_{ω}, such that the set Eq(P A_{ω}) ∩ L_{G} of equations valid in P A_{ω} is not recursively enumerable. Moreover, the indices of the substitutions and cylindrifications occurring in L_{G} are recursive functions and sets, respectively.

A proof can be found in [12].

Definition 5.2 Let pred denote the usual predecessor function on ω, with pred(0) = 0. Throughout, L_{suc,pred} denotes the language that consists of the Boolean operations and c_{0}, s_{suc}, s_{pred}, s_{[0,1]}, s_{[i/j]}, i, j ∈ ω,

Note that in L_{suc,pred} the operations c_{i}, s_{[i,j]}, i, j ∈ ω are term definable. The following theorem is due to I. Sain and V. Gyuris, (see [10]) which is a possible solution of (some variant of) the finitization problem (in the sense of [7]).

Theorem 5.3 Let L_{suc,pred,ω} = L_{suc,pred} ∪ {c_{(ω)}}. Then the variety generated by the reduct of RP A_{ω} to L_{suc,pred,ω} is axiomatizable by a recursive set Σ_{suc,pred,ω} of equations. This set is explicitly given by finitely many schemas (these schemas are essentially simpler than Halmos schemas in general).

This theorem is similar to the Daigneault-Monk theorem in the sense that it is a representation theorem. But now, in addition to this, the axiom system is recursive, 3 and therefore, Eq(RP A_{ω}) ∩ L_{suc,pred,ω} = Ded(Σ_{suc,pred,ω}) ∩ L_{suc,pred,ω} is recursively enumerable.

5.2 Case of algebras with equality

The following theorem is also in [10].

Theorem 5.4 Let L_{suc,pred,D} = L_{suc,pred} ∪ {d_{0,1}}. Note that in this language all the d_{i,j}’s are term definable for i, j ∈ ω. Then the variety generated by the reduct of RP EA_{ω} to L_{suc,pred,D} is axiomatizable by a recursive set Σ_{suc,pred,D} of equations. This set is explicitly given by finitely many schemas (these schemas are essentially simpler than Halmos schemas in general).

All the remarks standing below Theorem 5.3 apply to Theorem 5.4 too. The following theorem is due to R. McKenzie.

Theorem 5.5 Let L_{suc,pred,ω,D} = L_{suc,pred} ∪ {c_{(ω)}, d_{i,j}, i, j ∈ ω}. Then the set Eq(RP EA_{ω}) ∩ L_{suc,pred,ω,D} is not recursively enumerable.

Theorems 5.3, 5.4 and 5.5 together seem to indicate that a kind of division-line has been found between the area where positive results dominate (like Theorems 5.3, 5.4) and where negative results dominate (like theorems 5.5, 4.1). More precisely, Theorem 5.5 implies that Theorems 5.3, 5.4 are best possible in the sense that adding c_{(ω)} to the language of Theorem 5.4 then it becomes false. Actually Theorems 5.3 and 5.4 do not admit a common generalization in the sense that the negative Theorem 5.5 already applies to the union of their languages.

Finally, let us turn to the complexity of the first order theory of RP EA_{ω}. One can extend the proof of Theorem 4.1 to this theory as follows: T r is extendable in such a way that T r maps the full second order theory of arithmetic into the first order theory of (a finite reduct of) RP EA_{ω}. This means that, for some finite language L, Th(RP EA_{ω}) ∩ L does not form an analytical set (so it is at least as complex as the full second order theory of standard arithmetic). Here Th(RP EA_{ω}) denotes the first order theory of RP EA_{ω}.

5.3 Methodological conclusions

Comparing the negative and positive results above, we found that there are two paradigms. In the first paradigm (called polyadic algebra oriented) the indices or names of the operation symbols have a complex and fixed structure. For example the indices of the substitutions are functions, and one can compose them. The properties and the complexity of these objects are implicitly mirrored in the equational theories that we are studying, and possibly this is the reason for our negative results.

3That is, the set of all instances of the axiom schemas is recursive.

The other paradigm (called cylindric algebra oriented) is the opposite. In this case the indices of operation symbols have basically no structure. There are neither operations nor relations defined between the names of the operation symbols. Particular examples for the cylindric paradigm are: cylindric algebras; the languages (or algebras) in Theorems 5.3 and 5.4; quasi-polyadic algebras in the sense of [11]; and SCA_{α}, QP A_{α}, QP EA_{α} in [7]. We note that all the positive results quoted in this paper follow the cylindric paradigm.

These paradigms are not rigid categories. For example, the results about quasipolyadic algebras in [11] follow the cylindric paradigm (and, indeed, these results are positive).

The main methodological conclusion is the following: suppose one wants to apply polyadic algebras to a certain area, but the negative complexity-properties of polyadic algebras are undesirable for the applications. Then it is possible to remove these properties by switching from the polyadic paradigm to the cylindric paradigm.

6 Appendix

Here we give the translations of the usual defining schemas of α dimensional polyadic (equality) algebras into Halmos schemas. First of all we recall from [5] the original defining schemas:

(P0) The Boolean Algebra axioms, (P1) c_{(Γ)}(0) = 0, (P2) x ≤ c_{(Γ)}(x), (P3) c_{(Γ)}(x ∧ c_{(Γ)}(y)) = c_{(Γ)}(x) ∧ c_{(Γ)}(y), (P4) c_{0}(x) = x, (P5) c_{(Γ)}c_{(Δ)}(x) = c_{(Γ∪Δ)}(x), (P6) s_{Id_{α}}(x) = x, (P7) s_{σ∘τ}(x) = s_{σ}s_{τ}(x), (P8) s_{σ}(x ∨ y) = s_{σ}(x) ∨ s_{σ}(y), (P9) s_{σ}(−x) = −s_{σ}(x),

(P10) If (α − Γ) | σ = (α − Γ) | τ, then s_{σ}c_{(Γ)}(x) = s_{τ}c_{(Γ)}(x), (P11) If (τ^{−1}(Γ)) | τ is one-one and Δ = τ^{−1}(Γ) then c_{(Γ)}s_{τ}(x) = s_{τ}c_{(Δ)}(x),

(E1) d_{κ,κ} = 1, (E2) x ∧ d_{κ,λ} ≤ s_{[κ/λ]}(x), (E3) s_{τ}(d_{κ,λ}) = d_{τ(κ),τ(λ)}.

Here Γ, Δ ⊆ α, σ, τ ∈ ^{α}α, κ, λ ∈ α.

The translations are: (P0’) ⟨true, The Boolean Algebra axioms ⟩, (P1’) ⟨true, c_{r_{1}}(0) = 0⟩, (P2’) ⟨true, x ≤ c_{r_{1}}(x)⟩, (P3’) ⟨true, c_{r_{1}}(x ∧ c_{r_{1}}(y)) = c_{r_{1}}(x) ∧ c_{r_{1}}(y)⟩, (P4’) ⟨(∀y)(¬r_{1}(y)), c_{r_{1}}(x) = x⟩, (P5’) ⟨(∀y)(r_{1}(y) ∨ r_{2}(y) ↔ r_{3}(y)), c_{r_{1}}c_{r_{2}}(x) = c_{r_{3}}(x)⟩, (P6’) ⟨(∀y)(f_{1}(y) = y), s_{f_{1}}(x) = x⟩, (P7’) ⟨(∀y)(f_{1}(f_{2}(y)) = f_{3}(y)), s_{f_{3}}(x) = s_{f_{1}}s_{f_{2}}(x)⟩, (P8’) ⟨true, s_{f_{1}}(x ∨ y) = s_{f_{1}}(x) ∨ s_{f_{1}}(y)⟩, (P9’) ⟨true, s_{f_{1}}(−x) = −s_{f_{1}}(x)⟩,

(P10’) ⟨(∀y)(¬r_{1}(y) → f_{1}(y) = f_{2}(y)), s_{f_{1}}c_{r_{1}}(x) = s_{f_{2}}c_{r_{1}}(x)⟩, (P11’) ⟨(∀y)((r_{2}(y) ↔ (∃z)(r_{1}(z) & y = f_{1}(z)) & (∀y, z)(r_{2}(y) & r_{2}(z) & y ≠ z →

f_{1}(y) ≠ f_{1}(z))), c_{r_{1}}s_{f_{1}}(x) = s_{f_{1}}c_{r_{2}}(x)⟩,

(E1’) ⟨true, d_{n_{1},n_{1}} = 1⟩, (E2’) ⟨(∀y)(y ≠ n_{1} → f_{1}(y) = y & f_{1}(n_{1}) = n_{2}), x ∧ d_{n_{1},n_{2}} ≤ s_{f_{1}}(x)⟩, (E3’) ⟨(f_{1}(n_{1}) = n_{3} & f_{1}(n_{2}) = n_{4}), s_{f_{1}}(d_{n_{1},n_{2}}) = d_{n_{3},n_{4}}⟩.

It is easy to see that the instances of (P0)-P(11), (E1)-(E3) are the same as the α dimensional instances of (P0’)-P(11’), (E1’)-(E3’).

References

[1] C.C. Chang, H.J. Keisler, Model Theory, North-Holland, Amsterdam (1973).

[2] W. Craig, Logic in algebraic form, North-Holland, Amsterdam (1974).

[3] P. Halmos, Algebraic Logic, Chelsea Publ. Company (1962).

[4] L. Henkin, J.D. Monk, A. Tarski, Cylindric Algebras Part 1, North-Holland, Amsterdam (1971).

[5] L. Henkin, J.D. Monk, A. Tarski, Cylindric Algebras Part 2, North-Holland, Amsterdam (1985).

[6] J.D. Monk, A. Daigneault, Representation theory for polyadic algebras, Fund. Math. Vol 52 (1963), pp 151-176.

[7] I. Németi, Algebraization of Quantifier Logics, an introductory overview 12th version. Math. Inst. Budapest, Preprint, No. 13/1996. available on the following electronic address: http://circle.math-inst.hu/pub/algebraic-logic/survey.dvi An extended abstract of this appeared in Studia Logica vol. 50, No 3/4. pp 485-569.

[8] I. Németi, G. Sági, On the Equational Theory of Representable Polyadic Algebras, Preprint, (1996), Electronic address: http://circle.math-inst.hu/pub/algebraic-logic/polyadi2.dvi

[9] P. Odifreddi, Classical Recursion Theory, North-Holland, Amsterdam (1989).

[10] I. Sain, V. Gyuris, Finite Schematizable Algebraic Logic, Bulletin of IGPL, to appear (1996).

[11] I. Sain, R. Thompson, Strictly Finite Schema Axiomatization of Quasipolyadic Algebras, in: Algebraic Logic proc. conf. Budapest (1988) (eds.: H. Andréka, J.D. Monk and I. Németi) Colloq. Math. Soc. J. Bolyai vol 54, Nort-Holland, Amsterdam, 1991, pp 539-571.

[12] G. Sági, Non-computability of the consequences of the axioms of the ω dimensional polyadic algebras, Math. Inst. Budapest, Preprint (1995). Electronic address: http://circle.math-inst.hu/pub/algebraic-logic/polyadsg.dvi

e-mail: Nemeti@circle.math-inst.hu Sagi@circle.math-inst.hu