On the equational theory of representable polyadic equality algebras

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

20 Nov, 1996

incomplete, undebugged, draft version, please comment (!)

Abstract

Among others we will prove that the equational theory of ω dimensional representable polyadic equality algebras 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, too). We will also show that the complexity of the equational theory of RP EA_{ω} is also extremely high in the recursion theoretic sense. Finally, comparing our negative results with the positive ones of Ildikó Sain and Viktor Gyuris [8], we will draw the following methodological conclusions. The negative properties of polyadic (equality) algebras can be removed by switching from the so called ”polyadic algebraic paradigm” to the ”cylindric algebraic” one.

Contents

1. Introduction 2.

2. The equational theory of RP EA_{ω} 5.

3. The equational theory of P EA_{ω}^{+} 10.

4. Complexity of the equational theories 13.

5. Related results 23.

6. Appendix 25.

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

1 Introduction

It is well known that the class of (ω dimensional) representable polyadic equality algebras ( RP EA_{ω} for short) is not closed under taking ultraproducts, and hence this class is not axiomatizable. This result leaves the question of axiomatizability of the equational theory of RP EA_{ω} open. The equational theory of RP EA_{ω} (Eq(RP EA_{ω}) for short) is not finitely axiomatizable, simply because the language of RP EA_{ω} contains continuum 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 appeared in 1960’s (see [3]). Our goal in §§2-3 is to prove 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 [5] which states, that the class of representable polyadic algebras (without equality) is finite schema axiomatizable.

Before turning to the goal of §§2-3, let us look briefly to the goal of §4. In §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 show 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 φ:

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

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).

We will prove Theorem 4.1 in §4. 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 recursively 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 §4.

It is interesting to contrast non-computability of Eq(RP EA_{ω}) (i.e. Theorem 4.1) with the facts that Eq(RCA_{ω}) and Eq(RQP EA_{ω}) are recursively enumerable (cf. e.g. Németi, [6]). 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 §5 herein. Let us now return to formulating the results of sections 2-3.

Definition 1.1 Throughout, α is an ordinal. L_{P EA_{α}} denotes the language of α dimensional polyadic equality algebras (for details see [4], p.225).

Let us turn to the difference (or distance) between P EA_{ω} and HSPRP EA_{ω}. Here, P EA_{ω} is an abstract class defined by equation schemas (P_{0} − P_{11}, E_{1} − E_{3}) originating with Halmos cf. [3], [4]. We will see that P EA_{ω} ≠ HSPRP EA_{ω} because an equation separates them. We will construct such an equation. One could hope that adding similar, new schemas to P_{0} − E_{3} might alleviate the situation. We will see below that this cannot be done.

Motivating Example 1. 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 τ, σ are ”meta-variables” ranging over ^{ω}ω. We can write the same schema into the form

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

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

Definition 1.2 L_{T} is the following first order language: L_{T} consists of countably many unary relational symbols, and 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 1.3 Let L_{P T} be the following similarity type (in the algebraic sense). In L_{P T} C_{r_{1}}, C_{r_{2}}, ..., S_{f_{1}}, S_{f_{2}}, ... are unary operation symbols, D_{n_{1},n_{1}}, D_{n_{1},n_{2}}, D_{n_{2},n_{1}}... are constants. 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. In addition L_{P T} contains a boolean (type) reduct, too.

Definition 1.4 By a Halmos schema we mean a pair ⟨s, e⟩ where s is a 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 2. The form (∗) will help us in making certain things explicit about these kinds of schemas. Let now 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 τ, σ, f are ranging over ^{ω}ω).

Definition 1.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 1.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 [4], 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 1.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_{ω}), equivalently Cons(Σ) ≠ Eq(RP EA_{ω})

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

Before proving this theorem we need some further definitions and “preparations”.

Definition 1.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 defined by Halmos schemas. Our goal is to prove that the variety generated by RP EA_{ω} is not axiomatizable by Halmos schemas, as it was stated in Theorem 1.7. For this, it is enough to prove the following equivalent form of Theorem 1.7.

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

To show this, we will prove that there is 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.

On the structure of the paper: as we mentioned, the above formulated results will be proved and elaborated sections 2-3. In section 2 we will construct an equation e_{CM} and will show RP EA_{ω} ⊧ e_{CM}. In section 3 we will show P EA_{ω}^{+} |̸= e_{CM}. In section 4 the recursion theoretic (degrees of unsolvability) results are presented, while in section 5 we will compare our negative results with the positive results occurring in [8].

2 The equational theory of RP EA_{ω}.

In this section we will construct and discuss the equation e_{CM} mentioned above. First we introduce some notation. 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 ω. We will introduce some equations (see Definitions 2.1 and 2.6 below) and will prove some properties of these equations. After this, we will construct the equation e_{CM}, and in Theorem 2.9 we will show RP EA_{ω} ⊧ e_{CM}.

Definition 2.1 Throughout e_{1}, e_{2}, e_{3} denote the following equations: 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)).

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

Definition 2.2 Let A ∈ RP 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}.

Lemma 2.2.1 Suppose A ∈ RP EA_{ω}, with a nonempty base U, and a ∈ A such that

(0) C_{1}^{A}(a) = a. Then the following hold.

(1) If A ⊧ e_{1}[a] then (∀h ∈ ^{ω}U, h_{0} ≠ h_{1})(| (a)_{h} | ≤ 1).

(2) If A ⊧ e_{2}[a] then (∀h ∈ ^{ω}U)(| (a)_{h_{0}^{⌢}h} − (a)_{h} | ≤ 1).

(3) If A ⊧ e_{3}[a] then (∀h ∈ ^{ω}U)(| (a)_{h_{0}^{⌢}h} |≠ 0 ⇒ | (a)_{h_{0}^{⌢}h} − (a)_{h} | ≥ 1).

Proof. To show (1) suppose A ⊧ e_{1}[a] and h ∈ ^{ω}U, such that h_{0} ≠ h_{1}. Suppose g ∈ (a)_{h}. That is, there exist v_{0}, v_{1} ∈ U such that ⟨v_{0}, v_{1}, g⟩^{⌢}h ∈ a. Of course, ⟨v_{0}, v_{1}, g⟩^{⌢}h ∈ −D_{3,4}^{A} and therefore by e_{1}, ⟨v_{0}, v_{1}, g⟩^{⌢}h ∈ D_{2,3}^{A} so g = h_{0}. This means that (a)_{h} ⊆ {h_{0}}, since g were chosen arbitraryly. So | (a)_{h} |≤ 1 therefore (1) is proved.

To show (2) suppose indirectly A ⊧ e_{2}[a], h ∈ ^{ω}U, v_{0}, v_{1} ∈ (a)_{h_{0}^{⌢}h}−(a)_{h} and v_{0} ≠ v_{1}. This means the following:

(a) (∃u_{0}, u_{1} ∈ U)(⟨u_{0}, u_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h ∈ a)

(b) (∃w_{0}, w_{1} ∈ U)(⟨w_{0}, w_{1}, v_{1}⟩^{⌢}h_{0}^{⌢}h ∈ a)

(c) ( ∄t_{0}, t_{1} ∈ U)(⟨t_{0}, t_{1}, v_{0}⟩^{⌢}h ∈ a)

(d) ( ∄z_{0}, z_{1} ∈ U)(⟨z_{0}, z_{1}, v_{1}⟩^{⌢}h ∈ a)

Observe ⟨u_{0}, v_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h ∉ D_{1,2}^{A}. So, to derive a contradiction we have to show that this sequence is an element of the left hand side of e_{2}[a]. To do this we need the following claim.

Claim 2.3.1 C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc}^{A}(a) = {⟨x_{0}, x_{1}, u_{2}, u_{3}, u_{3}, u_{4}, u_{5}...⟩ ∈ ^{ω}U : (∃u_{0}, u_{1} ∈ U)(⟨u_{0}, u_{1}, u_{2}, u_{3}, u_{4}, u_{5}, ...⟩ ∈ a)}.

Similarly, C_{0}^{A}C_{2}^{A}t_{3}^{4}^{A}t_{1}^{3}^{A}S_{suc}^{A}(a) = {⟨x_{0}, u_{2}, x_{2}, u_{3}, u_{3}, u_{4}, u_{5}...⟩ ∈ ^{ω}U : (∃u_{0}, u_{2} ∈ U)(⟨u_{0}, u_{1}, u_{2}, u_{3}, u_{4}, u_{5}, ...⟩ ∈ a)}.

Proof of the claim. We only show the first part of the statement, because the proof of the second part is a similar direct computation.

⟨x_{0}, x_{1}, u_{2}, u_{3}, u_{3}, u_{4}, u_{5}...⟩ ∈ C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc}^{A}(a) iff (∃u_{−1}, u_{0} ∈ U)⟨u_{−1}, u_{0}, u_{2}, u_{3}, u_{3}, u_{4}, u_{5}...⟩ ∈ t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc}^{A}(a) iff (∃u_{−1}, u_{0} ∈ U)⟨u_{−1}, u_{0}, u_{2}, u_{3}, u_{3}, u_{4}, u_{5}...⟩ ∈ C_{3}^{A}t_{2}^{3}^{A}S_{suc}^{A}(a) iff (∃u_{−1}, u_{0} ∈ U)⟨u_{−1}, u_{0}, u_{2}, u_{2}, u_{3}, u_{4}, u_{5}...⟩ ∈ C_{2}^{A}S_{suc}^{A}(a) iff (∃u_{−1}, u_{0}, u_{1} ∈ U)⟨u_{−1}, u_{0}, u_{1}, u_{2}, u_{3}, u_{4}, u_{5}...⟩ ∈ S_{suc}^{A}(a) iff (∃u_{0}, u_{1} ∈ U)⟨u_{0}, u_{1}, u_{2}, u_{3}, u_{4}, u_{5}...⟩ ∈ a.

End of proof of claim 2.3.1.

Now we are ready to show that ⟨u_{0}, v_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h is an element of the left hand side of e_{2}[a].

(i) ⟨u_{0}, v_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h ∈ D_{3,4}∧C_{1}^{A}(a) from (a). Hence from (0) ⟨u_{0}, v_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h ∈ D_{3,4}∧a.

(ii) Now we want to prove ⟨u_{0}, v_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h ∉ C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc}^{A}(a). Suppose indirectly ⟨u_{0}, v_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h ∈ C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc}^{A}(a). Then, by claim 2.3.1, (∃t_{0}, t_{1} ∈ U)(⟨t_{0}, t_{1}, v_{0}⟩^{⌢}h ∈ a which is impossible because of (c). Similarly, ⟨u_{0}, v_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h ∉ C_{0}^{A}C_{2}^{A}t_{3}^{4}^{A}t_{1}^{3}^{A}S_{suc}^{A}(a).

(iii) From (b) ⟨w_{0}, w_{1}, v_{1}⟩^{⌢}h_{0}^{⌢}h ∈ a so ⟨w_{0}, v_{1}, w_{1}⟩^{⌢}h_{0}^{⌢}h ∈ S_{[1,2]}^{A}(a) so ⟨u_{0}, v_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h ∈ C_{0}^{A}C_{2}^{A}S_{[1,2]}^{A}(a).

Computations (i)-(iii) show that ⟨u_{0}, v_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h is an element of the left hand side of e_{2}[a].

Lastly we have to show (3). Suppose A ⊧ e_{3}[a], h ∈ ^{ω}U and v_{0} ∈ (a)_{h_{0}^{⌢}h}. So there exist u_{0}, u_{1} ∈ U such that ⟨u_{0}, u_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h ∈ a ∧ D_{3,4}^{A}. By e_{3} we have

(2.3.2) ⟨u_{0}, u_{1}, v_{0}⟩^{⌢}h_{0}^{⌢}h ∈ C_{0}^{A}C_{1}^{A}C_{2}^{A}(a ∧ D_{3,4}^{A} − C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc}^{A}(a)).

Therefore there exist u_{2}, u_{3}, u_{4} ∈ U such that

(2.3.3) ⟨u_{2}, u_{3}, u_{4}⟩^{⌢}h_{0}^{⌢}h ∈ (a ∧ D_{3,4}^{A} − C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc}^{A}(a)).

Of course u_{4} ∈ (a)_{h_{0}^{⌢}h}. On the other hand, suppose u_{4} ∈ (a)_{h}, so (∃t_{0}, t_{1} ∈ U)(⟨t_{0}, t_{1}, u_{4}⟩^{⌢}h ∈ a). But then, by claim 2.3.1, ⟨u_{2}, u_{3}, u_{4}⟩^{⌢}h_{0}^{⌢}h ∈ C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc}^{A}(a). By (2.3.3), this is impossible, so u_{4} ∈ (a)_{h_{0}^{⌢}h} − (a)_{h} therefore (3) is proved.

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

Proof. First note that if U is empty, then the statement is true. Otherwise (0),(1),(2),(3) of Lemma 2.3 hold. Choose an arbitrary h ∈ ^{ω}U. If h is a constant sequence, then h_{0}^{⌢}h = h so (a)_{h_{0}^{⌢}h} = (a)_{h} hence by (3) of Lemma 2.3 | (a)_{h_{0}^{⌢}h} |=| (a)_{h} | = 0 < ℵ_{0}.

Now suppose that h is not a constant sequence, so there exists n ∈ ω such that h_{0} = h_{1} = ... = h_{n} ≠ h_{n+1} We will use induction to show that in this case

(∗) | (a)_{h} | ≤ n + 1 < ℵ_{0}.

If n = 0 then by (1) of the previous theorem we have | (a)_{h} | ≤ 1. Assume second, that (∗) holds for those sequences which are not constant on the first n natural number, and let h′ = h ∘ suc = ⟨h_{1}, h_{2}, h_{3}, ...⟩ Now | (a)_{h} | ≤ | (a)_{h} − (a)_{h′} | + | (a)_{h′} | ≤ 1 + n, by (2) of Lemma 2.3, and the induction hypothesis (∗).

Definition 2.4 Suppose A ∈ RP 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}.

Definition 2.5 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).

Lemma 2.5.1 Suppose A ∈ RP EA_{ω}, with base U, a ∈ A and h ∈ ^{ω}U. If C_{1}^{A}(a) = a then the following statements hold:

(4) If A ⊧ e_{4}[a] then f_{a,h} is a function.

(5) If A ⊧ e_{5}[a] then f_{a,h} is an injective relation.

(6) If A ⊧ e_{6}[a] then range(f_{a,h}) ⊆ dom(f_{a,h}).

(7) If A ⊧ e_{7}[a] then dom(f_{a,h}) ⊆ range(f_{a,h}).

Proof. First we want to prove (4). Suppose v_{0}, v_{1}, z ∈ U such that ⟨z, v_{0}⟩ ∈ f_{a,h}, and ⟨z, v_{1}⟩ ∈ f_{a,h}. Hence, by the definition of f_{a,h}, there exists t ∈ U such that ⟨v_{0}, t, z⟩^{⌢}h ∈ a. So ⟨v_{0}, v_{1}, z⟩^{⌢}h ∈ C_{1}^{A}(a) = a. Similarly, ⟨v_{1}, v_{0}, z⟩^{⌢}h ∈ a. But then ⟨v_{0}, v_{1}, z⟩^{⌢}h ∈ S_{[0,1]}^{A}(a). Using e_{4} we conclude ⟨v_{0}, v_{1}, z⟩^{⌢}h ∈ D_{0,1}^{A}. This means v_{0} = v_{1} so f_{a,h} is a function.

The proof of (5) is absolutely similar.

To prove (6), assume z ∈ range(f_{a,h}). That is, there exists v_{0} ∈ U such that ⟨v_{0}, z⟩ ∈ f_{a,h}, so there exists v_{1} ∈ U such that ⟨z, v_{1}, v_{0}⟩^{⌢}h ∈ a, hence ⟨v_{0}, v_{1}, z⟩^{⌢}h ∈ S_{[0,2]}^{A}(a). Using e_{6}, we conclude there exists v_{2} ∈ U such that ⟨v_{2}, v_{1}, z⟩^{⌢}h ∈ a, so ⟨z, v_{2}⟩ ∈ f_{a,h} which means z ∈ dom(f_{a,h}), as desired.

The proof of (7) is absolutely similar.

The variety P EA_{ω}^{+} is a discriminator variety because C_{(ω)} is a complemented normal closure operator which majorates 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 2.6 Throughout, e_{CM} is defined as follows:

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

Theorem 2.7 RP EA_{ω} ⊧ e_{CM}.

Proof. Let A ∈ RP EA_{ω}, with base U, let a ∈ A such that A ⊧ (e_{0}&e_{1}&...&e_{6})[a]. We want to show A ⊧ e_{7}[a] that is, ⟨v_{0}, v_{1}, v_{2}⟩^{⌢}h ∈ C_{2}^{A}(a) whenever h ∈ ^{ω}U, v_{0}, v_{1}, v_{2} ∈ U such that ⟨v_{0}, v_{1}, v_{2}⟩^{⌢}h ∈ S_{[0,2]}^{A}(a).

By the previous theorems (a)_{h} is finite, and f_{a,h} is an injective function such that range(f_{a,h}) ⊆ dom(f_{a,h}). It is easy to see that v_{0} ∈ (a)_{h} = dom(f_{a,h}). Using other terminology, we have a permutation f_{a,h} on a finite set (a)_{h}, and v_{0} is in the domain of this permutation. Of course, in this situation v_{0} ∈ range(f_{a,h}) that is, there exists z_{0} ∈ U such that ⟨z_{0}, v_{0}⟩ ∈ f_{a,h}. By the definition of f_{a,h} there exists z_{1} ∈ U such that ⟨v_{0}, z_{1}, z_{0}⟩^{⌢}h ∈ a. But then ⟨v_{0}, v_{1}, z_{0}⟩^{⌢}h ∈ C_{1}^{A}(a) = a, so ⟨v_{0}, v_{1}, v_{2}⟩^{⌢}h ∈ C_{2}^{A}(a). This means that S_{[0,2]}^{A}(a) ≤ C_{2}^{A}(a) so the conclusion of e_{CM} hold, as desired.

3 The equational theory of P EA_{ω}^{+}.

In this section we prove that e_{CM} is not valid in P EA_{ω}^{+}.

Theorem 3.1 P EA_{ω}^{+} |̸= e_{CM}.

Proof. Assume the opposite. Then there exist a proof of e_{CM} from the (ω dimensional) instances of certain Halmos schemas. Let p such a proof. Suppose that exactly the following sets, functions and numbers occur in p as indices of certain operations: r_{1}^{M}, ..., r_{k}^{M}, f_{1}^{M}, ..., f_{n}^{M}, i_{1}^{M}, ...i_{m}^{M}.

Let M = ⟨ω; ≤^{ω}, r_{1}^{M}, ..., r_{k}^{M}, f_{1}^{M}, ..., f_{n}^{M}, i_{1}^{M}, ...i_{m}^{M}⟩. Let F be a nonprincipal ultrafilter over ω. Let M′ be the ultrapower of M with respect to F, so M′ = (^{ω}M)/F. Let M′′ be an elementary part of M′ which has a countable universe, and ⟨0, 1, 2, 3, 4...⟩/F is an element of the universe of M′′. Let h be a bijection, which maps the universe of M′′ onto ω such that

h(⟨0, 0, 0...⟩/F) = 0,
h(⟨1, 1, 1...⟩/F) = 1,
h(⟨2, 2, 2...⟩/F) = 2,
h(⟨3, 3, 3...⟩/F) = 3,
h(⟨4, 4, 4...⟩/F) = 4.

Let ≤^{h}= h[≤^{M′′}], r_{i}^{h} = h[r_{i}^{M′′}], f_{j}^{h} = h ∘ f_{j}^{M′′} ∘ h^{−1} and let i_{l}^{h} = h(i_{l}^{M′′}) ( 1 ≤ i ≤ k, 1 ≤ j ≤ n, 1 ≤ l ≤ m). Finally let H = ⟨ω; ≤^{h}, r_{1}^{h}, ..., r_{k}^{h}, f_{1}^{h}, ..., f_{n}^{h}, i_{1}^{h}, ...i_{m}^{h}⟩.

Proposition 3.1.1 M and H are elementarily equivalent.

Proof. M and M′ and M′′ are elementarily equivalent, furthermore, by definition H and M′′ are isomorphic - h is an isomorphism.

Let p′ be the sequence of equations obtained from p by replacing r_{i}^{M}, f_{j}^{M}, i_{l}^{M} with r_{i}^{h}, f_{j}^{h}, i_{l}^{h} respectively. (1 ≤ i ≤ k, 1 ≤ j ≤ n, 1 ≤ l ≤ m)

Proposition 3.1.2 p′ is a proof (using Birkhoff’s calculus for equational logic).

Proof. We will use induction to show that the initial segments of p′ form a proof. We will ignore some obvious case. Suppose the k − th equation in p is g_{k}, and the k − th equation in p′ is g′_{k}.

Case (0). By the definition of the proof, we may assume that g_{1} (the first element of p) is an ω dimensional) instance of some Halmos schema s ⇒ e. That is, s is valid in M, and g_{1} is an instance of e. But then by the previous claim, s is valid in H, and g′_{1} is an instance of e with respect to H (by the definition of p′). This means, that g′_{1} is also an instance of s ⇒ e.

Now suppose that the first k − 1 elements of p′ form a proof. We have 2 cases.

Case (1). g_{k} is an (ω dimensional) instance of some Halmos schema s ⇒ e. Then, similarly to Case (0), g′_{k} is also an instance of s ⇒ e. Therefore, by the induction hypothesis, the first k element of p′ form a proof.

Case (2). g_{k} is a consequence of the preceding equations of p. One can easily see, that in this situation g′_{k} is a consequence of the preceding equations of p′. This completes the proof.

Throughout, e′_{CM} denotes the last equation of p′. This is the substituted version of e_{CM}.

Proposition 3.1.3 RP EA_{ω} |̸= e′_{CM}.

Proof. We will construct a concrete A ∈ RP EA_{ω} and a ∈ A such that A |̸= e′_{CM}[a].

Let the base of A be ω, and let a ∈ A be the following:

a = {s ∈ ^{ω}ω : (∃k, n ∈ ω)(k is even or k ≤ 2n + 1) and

s_{i} = \{ \begin{matrix}2k & if i = 0, \\ k & if i = 2, \\ 0 & if h^{−1}(3) ≤ h^{−1}(i) ≤ suc^{n}(⟨0, 1, 2, 3...⟩/F) \\ 1 & if h^{−1}(i) >^{M′′} suc^{n}(⟨0, 1, 2, 3...⟩/F)\} \end{matrix}

}, where “≤”,“>” and “suc” are understood in M′′. The same convention applies in further definitions of s_{i} or s′_{i} in this proof.

Note that e′_{1} = e_{1}, e′_{4} = e_{4}, e′_{5} = e_{5}, e′_{6} = e_{6}, e′_{7} = e_{7} (as strings of symbols) because of the construction of h. Therefore one can easily see that C_{1}^{A}(a) = a and e_{1}, e_{4}, e_{5}, e_{6} hold for a in A. On the other hand A |̸= e_{7}[a] because (∃h ∈ ^{ω}U)(1 ∈ dom(f_{a,h}), 1 ∉ range(f_{a,h})), since the range of f_{a,h} consists of even numbers. So the remaining is to prove that A ⊧ e′_{2}&e′_{3}[a].

To see A ⊧ e′_{2}[a] choose an arbitrary element s of the left hand side of e′_{2}[a]. Clearly, s ∈ a. That is, there exist k, l, n ∈ ω such that s has the following form:

s_{i} = \{ \begin{matrix}2k & if i = 0, \\ l & if i = 1, \\ k & if i = 2, \\ 0 & if h^{−1}(3) ≤ h^{−1}(i) ≤ suc^{n}(⟨0, 1, 2, 3...⟩/F) \\ 1 & if h^{−1}(i) > suc^{n}(⟨0, 1, 2, 3...⟩/F) \end{matrix}

k is not even and k ≮ 2n + 1 because otherwise direct calculations show s ∈ C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc^{H}}^{A}(a). (These calculations are similar to the proof of claim 2.3.1) So k = 2n + 1. Analogously, s ∈ C_{0}^{A}C_{2}^{A}S_{[1,2]}^{A}(a) − C_{0}^{A}C_{2}^{A}t_{3}^{4}^{A}t_{1}^{3}^{A}S_{suc^{H}}^{A}(a) implies l = 2n + 1. This means l = k, other words s ∈ D_{1,2}^{A}, which is a right hand side of e′_{2}.

To show A ⊧ e′_{3}[a] assume s ∈ (a ∧ D_{3,4}^{A}), so it is enough to prove s ∈ C_{0}^{A}C_{1}^{A}C_{2}^{A}(a ∧ D_{3,4}^{A} − C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc^{H}}^{A}(a)). Suppose that s_{h((suc^{M′′})^{n}(⟨0,1,2,3,...⟩/F)} = 0 and s_{h((suc^{M′′})^{n+1}(⟨0,1,2,3,...⟩/F)} = 1. Such an n ∈ ω exists because s ∈ a. Let s′ ∈ ^{ω}ω be the following sequence.

s′_{i} = \{ \begin{matrix}4n+2 & if i = 0, \\ 0 & if i = 1, \\ 2n+1 & if i = 2, \\ 0 & if h^{−1}(3) ≤ h^{−1}(i) ≤ suc^{n}(⟨0, 1, 2, 3...⟩/F) \\ 1 & if h^{−1}(i) > suc^{n}(⟨0, 1, 2, 3...⟩/F) \end{matrix}

Observe s and s′ differs at most in the 0th, 1th and the 2nd coordinate. Using this, direct calculations would lead to conclude s′ ∈ a∧D_{3,4}^{A}−C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc^{H}}^{A}(a). Thus s ∈ C_{0}^{A}C_{1}^{A}C_{2}^{A}(a ∧ D_{3,4}^{A} − C_{0}^{A}C_{1}^{A}t_{3}^{4}^{A}t_{2}^{3}^{A}S_{suc^{H}}^{A}(a)). This completes the proof.

Now the proof of Theorem 3.1 is as follows. Suppose P EA_{ω}^{+} ⊧ e_{CM}. Then e′_{CM} is provable in P EA_{ω}^{+} (by proposition 3.1.2), RP EA_{ω} is a subclass of P EA_{ω}^{+}, and e′_{CM} is not valid in RP EA_{ω} (by proposition 3.1.3). This contradiction completes the proof.

Finally, Theorems 1.7 and 1.7^{∗} hold, because by Theorem 3.1 P EA_{ω}^{+} |̸= e_{CM} but by Theorem 2.9 RP EA_{ω} ⊧ e_{CM}.

4 Complexity of the equational theories.

As we mentioned in the introduction, in [5] 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 is that the language of P A_{ω} consists of continuum many operation symbols. Actually, in [10] we proved the following. There is a strictly finite reduct L_{G} of the language of P A_{ω}, such that the following set of equations is not recursively enumerable: {e ∈ L_{G} : (P A_{ω} axioms) ⊢ e}. Moreover, the indices of the substitutions and cylindrifications occurring in L_{G} are recursive functions and sets, respectively.

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

To prove this, we will recursively reduce the second order universal theory of standard arithmetic to Eq(RP EA_{ω}). Recall that N is the standard model of arithmetic.

Theorem 4.1 Eq(RP EA_{ω}) is Π_{1}^{1} hard, which means that 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 σ

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

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

Remark. By a Π_{1}^{1} formula of arithmetic we mean a second order formula in which every second order variable is bounded universally (in prenex form). 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 really means, that Eq(RP EA_{ω}) is more complex than any Π_{1}^{1} set, so it is Π_{1}^{1} hard.

Proof. The proof based on a systematic translation of the Π_{1}^{1} formulas of arithmetic into polyadic equations. First we introduce some notation. Throughout t, y, z denote the following terms.

t(a) is s_{pred}s_{pred}s_{pred}c_{0}c_{1}c_{2}(a). y(a) is s_{pred}s_{pred}(−c_{0}c_{1}(a)) ∧ s_{pred}s_{pred}s_{pred}(c_{0}c_{1}(s_{[3/4]}(a))). z(a) is c_{ω−{0,1}}(s_{[0,1]}s_{suc}(y(a)) ∧ s_{[0/1]}s_{[1/2]}(y(a))).

Proposition 4.1.1 If A ∈ RP EA_{ω} with base U and a ∈ A then the preceding terms describe the following sets:

t^{A}(a) = {h ∈ ^{ω}U : (∃v_{0}v_{1}v_{2})(⟨v_{0}v_{1}v_{2}⟩^{⌢}h ∈ a)}.

y^{A}(a) = {⟨u⟩^{⌢}h ∈ ^{ω}U : h ∈ t^{A}(a), u ∉ (a)_{h}, u ∈ (a)_{h_{0}h}}.

z^{A}(a) = {⟨u, v⟩^{⌢}h ∈ ^{ω}U : (∃h′ ∈ ^{ω}U)(u^{⌢}h′ ∈ y^{A}(a), v^{⌢}h′_{0}h′ ∈ y^{A}(a)}.

Proof. The proof is a simple computation.

Throughout e_{8} − e_{12} denote the following equations:

e_{8} = c_{ω}(z) = 1. e_{9} = c_{ω−{0,1}}(z) = z. e_{10} = s_{[0/3]}(c_{1}(z) − c_{1}s_{[0,1]}(z)) ∧ (c_{1}(z) − c_{1}s_{[0,1]}(z)) ≤ d_{0,3}. e_{11} = y − d_{1,2} ≤ c_{1}(z) − c_{1}s_{[0,1]}(z). e_{12} = y ∧ d_{1,2} ≤ s_{suc}c_{0}(y).

Proposition 4.1.2 If A ∈ RP EA_{ω} with a nonempty base U and a, b ∈ A then the preceding equations mean the following:

A ⊧ e_{8}[a] iff a is not empty. A ⊧ e_{10}[a] iff the following set contains at most one element:

{u ∈ U : (∃h ∈ ^{ω}U)(u^{⌢}h ∈ a)} − {u ∈ U : (∃v ∈ U, h ∈ ^{ω}U)(v^{⌢}u^{⌢}h ∈ a)}. A ⊧ e_{11}[a, b] iff

⟨v, h⟩ ∈ a − D_{1,2}^{A} ⇒ v ∈ {u ∈ U : (∃h ∈ ^{ω}U)(u^{⌢}h ∈ b)} − {u ∈ U : (∃v ∈ U, h ∈ ωU)(v^{⌢}u^{⌢}h ∈ b)}. A ⊧ e_{12}[a] iff ⟨v, h⟩ ∈ a ∧ D_{1,2}^{A} ⇒ ⟨v, h_{1}, h_{2}, ...⟩ ∈ a.

Proof. Direct computation.

The requirement that a given element b of A is an injective function on its first two coordinates such that range(b) ⊆ dom(b), is also expressible by an equation. Let e_{13} be such an equation, so

e_{13} = c_{ω−2}(b) = 1 & s_{[1,2]}(b) ∧ s_{[1,3]}(b) ≤ d_{2,3} &s_{[0,2]}(b) ∧ s_{[0,3]}(b) ≤ d_{2,3} & s_{[0,1]}(b) ≤ c_{1}(b).

If for some a ∈ A, A ⊧ e_{9}[z(a)], then we may assume that z(a) is a binary relation.

Proposition 4.1.3 If A ∈ RP EA_{ω} with a nonempty base U and a ∈ A such that A ⊧ e_{1}&e_{2}&e_{3}[a] and A ⊧ e_{8}&...&e_{13}[a, t^{A}(a), y^{A}(a), z^{A}(a)] then ⟨ω, suc⟩ ≅ ⟨dom(z^{A}(a)), z^{A}(a)⟩.

Proof. We will define an isomorphism ˆ : ω → dom(z^{A}(a)).

By proposition 4.1.2 and e_{8}, e_{10} there is an uniqe u ∈ U such that u ∈ dom(z^{A}(a)) − range(z^{A}(a)). Let 0ˆ = u. Now suppose nˆ is defined for some n ∈ ω. Let (n+1)ˆ = v such that (∃h ∈ ^{ω}U)(⟨nˆ , v⟩^{⌢}h ∈ z^{A}(a)). Such a v is exists and uniqe because of e_{13}[z^{A}(a)].

The function ˆ is injective because of e_{13}[z^{A}(a)]. We have to show that surjectivity is also true. Choose an element u ∈ dom(z^{A}(a)). By e_{13}[z^{A}(a)] there is an uniqe v ∈ U such that (∃h ∈ ^{ω}U)(⟨u, v⟩^{⌢}h ∈ z^{A}(a)). By proposition 4.1.1 and the definition of z(a) this means (∃h′ ∈ ^{ω}U)(u^{⌢}h′ ∈ y^{A}(a)), v^{⌢}h′_{0}h′ ∈ y^{A}(a). By the definition of y(a), h′ ∈ t^{A}(a). This implies (a)_{h′} ≠ 0. By e_{1}&...&e_{3}[a], h′ is not a constant sequence. (This is proved in the first paragraph of the proof of theorem 2.4.) So (∃n ∈ ω)(h′_{0} = ... = h′_{n} ≠ h′_{n+1}).

If n = 0 then u^{⌢}h′ ∈ y^{A}(a) − D_{1,2}^{A} so by e_{11}[y^{A}(a), z^{A}(a)] and proposition 4.1.2, u ∈ dom(z^{A}(a)) − range(z^{A}(a)) which is uniqe, so u = 0ˆ .

If n > 0 then u^{⌢}h′ ∈ y^{A}(a) ∧ D_{1,2}^{A} thus by e_{12}[y^{A}(a), z^{A}(a)] and proposition 4.1.2, u^{⌢}⟨h′_{1}h′_{2}...⟩ ∈ C_{0}^{A}y^{A}(a). That is, (∃u_{1} ∈ U)(u_{1}^{⌢}⟨h′_{1}h′_{2}...⟩ ∈ y^{A}(a). Observe ⟨u_{1}, u⟩^{⌢}⟨h′_{1}h′_{2}...⟩ ∈ z^{A}(a) (by the definition of z(a)). Repeating the previous argument n times, we have u_{1}, u_{2}, ..., u_{n} ∈ U such that (∀ 2 ≤ k ≤ n)(⟨u_{k}, u_{k−1}⟩^{⌢}⟨h′_{k}h′_{k+1}...⟩ ∈ z^{A}(a) and u_{k}^{⌢}⟨h′_{k}h′_{k+1}...⟩ ∈ y^{A}(a). Observe u_{n}^{⌢}⟨h′_{n}h′_{n+1}...⟩ ∈ y^{A}(a) − D_{1,2}^{A}. Using the previous case, this implies u = nˆ .

It is easy to see that ˆ preserves the successor function (according to z^{A}(a)).

Now we systematically translate the Π_{1}^{1} formulas of arithmetic into polyadic equations. We will do this in several steps. If φ is a Π_{1}^{1} formula of arithmetic, then l_{φ} denotes the number of different individuum variables occurring in φ. First we translate the terms, then the first order formulas then the Π_{1}^{1} formulas. The idea is the following. We will define an RP EA_{ω} term Un^{l_{φ}}(z) which simulates all interpretations over ω. That is, the first l_{φ} coordinates of Un^{l_{φ}}(z) can be identified by ω.

After this we can postulate the meaning of a term, first order formula, Π_{1}^{1} formula of arithmetic, as usual.

Translation of the terms.

Definition 4.2 Let l ∈ ω. Un^{l}(z) denotes the following term: Un^{l}(z) = s_{suc}c_{1}(z) ∧ s_{suc}^{2}c_{1}(z) ∧ ... ∧ s_{suc}^{l}c_{1}(z).

To translate addition and multiplication we need a definition for them in the polyadic environment. In ⟨ω; 0, suc, +, ·⟩ addition and multiplication is definable form suc as follows.

(∀n ∈ ω)(n + 0 = n). (∀n, m ∈ ω)(n + suc(m) = suc(n + m)).

(∀n ∈ ω)(n · 0 = 0). (∀n, m ∈ ω)(n · suc(m) = (n · m) + n).

Using induction it is easily seen that the previous formulas define addition and multiplication. We will express these formulas in the language of RP EA_{ω}.

Definition 4.3 Throughout e_{14} − e_{18} denote the following equations: (here Plus, Mul and z are variables in the equational language of RP EA_{ω}).

e_{14} = c_{ω−3}(P lus) = P lus, c_{ω−3}(Mul) = Mul, P lus ≤ c_{1}(z)∧s_{suc}c_{1}(z)∧s_{suc}^{2}c_{1}(z). e′_{14} = Mul ≤ c_{1}(z) ∧ s_{suc}c_{1}(z) ∧ s_{suc}^{2}c_{1}(z), c_{1}c_{2}(P lus) = c_{1}(z), s_{[0,1]}c_{1}c_{2}(P lus) = c_{1}(z), c_{1}c_{2}(Mul) = c_{1}(z), s_{[0,1]}c_{1}c_{2}(Mul) = c_{1}(z). e_{15} = s_{[0,1]}c_{1}(z) − c_{0}(z) ∧ P lus ≤ d_{0,2}. e_{16} = s_{[0,3]}(z) ∧ P lus ∧ s_{[1,3]}s_{[2,4]}(P lus) ≤ s_{[0,4]}s_{[1,2]}(z). e_{17} = s_{[0,1]}c_{1}(z) − c_{0}(z) ∧ Mul ≤ s_{[0,2]}c_{1}(z) − s_{[1,2]}c_{0}(z). e_{18} = s_{[0,3]}(z) ∧ Mul ∧ s_{[1,3]}s_{[2,4]}(Mul) ≤ s_{[1,4]}(P lus).

Proposition 4.3.1 If A ∈ RP EA_{ω} with base U and a, P lus, Mul ∈ A such that A ⊧ e_{1}&e_{2}&e_{3}[a] and A ⊧ e_{8}&...&e_{18}[a, t^{A}(a), y^{A}(a), z^{A}(a), P lus, Mul] then The following hold:

P lus = {⟨u, v, w⟩^{⌢}h ∈ ^{ω}U : u, v, w ∈ dom(z^{A}(a)) and (∃n_{1}, n_{2} ∈ ω)(n_{1}ˆ = u, n_{2}ˆ = v, (n_{1} + n_{2})ˆ = w)}.

Mul = {⟨u, v, w⟩^{⌢}h ∈ ^{ω}U : u, v, w ∈ dom(z^{A}(a)) and (∃n_{1}, n_{2} ∈ ω)(n_{1}ˆ = u, n_{2}ˆ = v, (n_{1} · n_{2})ˆ = w)}.

Proof. By e_{14} the first 2 coordinates of P lus ∈ A consists of all (the images of the) natural numbers, (and hence Plus is not empty) so there is an h ∈ P lus. Suppose h = ⟨u_{0}ˆ , u_{1}ˆ , u_{2}ˆ , u_{3}, u_{4}...⟩ so the first 3 elements of h are the images of the natural numbers u_{0}, u_{1}, u_{2}, respectively. If u_{1}ˆ ∈ dom(z(a)) − range(z(a)) then u_{1} = 0 and h is an element of the left hand side of e_{15}, thus h ∈ D_{0,2}^{A} hence u_{0}ˆ = u_{2}ˆ . This means (∀n ∈ ω)(n + 0 = n) is satisfied.

Now suppose h is in the left hand side of e_{16}. This means (∃v_{3}, v_{4} ∈ ω)(v_{3}ˆ = u_{3}, v_{4}ˆ = u_{4} and u_{1} = v_{3} + 1, u_{0} + u_{1} = u_{2}, u_{0} + v_{3} = v_{4}). Using the truth of e_{16}, v_{4}+1 = u_{2} also hold in this case, which means (∀n, m ∈ ω)(n+suc(m) = suc(n+m)) is satisfied.

So P lus satisfies the definition of addition, thus the first statement is true.

The proof of the statement about Mul is similar.

Now we can define the translation function T r on the terms of arithmetic. Before reading carefully Definition 4.4, probably useful to read proposition 4.4.1.

Definition 4.4 Let t be a term of arithmetic, which contains at most l distinct variables. Then T r(t), the translation of t is an RP EA_{ω} term, computable by the following recursive rules.

T r(0) = Un^{l} ∧ c_{1}(z) − c_{1}s_{[0,1]}(z). T r(v_{i}) = t_{0}^{i}(Un^{l}). T r(suc(t)) = s_{pred}c_{0}(z ∧ s_{[0,1]}s_{suc}(T r(t)). T r(t_{1} + t_{2}) = s_{pred}s_{pred}c_{0}c_{1}(P lus ∧ s_{[0,2]}s_{suc}s_{suc}(T r(t_{1})) ∧ s_{[1,2]}s_{suc}s_{suc}(T r(t_{2}))). T r(t_{1} · t_{2}) = s_{pred}s_{pred}c_{0}c_{1}(Mul ∧ s_{[0,2]}s_{suc}s_{suc}(T r(t_{1})) ∧ s_{[1,2]}s_{suc}s_{suc}(T r(t_{2}))).

Here z, P lus, Mul are variables in the equational language of RP EA_{ω}.

Proposition 4.4.1 If a, Un, P lus, Mul ∈ A such that

A ⊧ e_{1}&...&e_{18}[a, t(a), y(a), z(a), Un, P lus, Mul]

then for every term t of arithmetic which contains at most l distinct variable, hold the following:

T r(t) = {⟨u_{0}, ...u_{l}⟩^{⌢}h ∈ ^{ω}U : (∃n_{0}, ...n_{l} ∈ ω)(n_{0}ˆ = u_{0}, ..., n_{l}ˆ = u_{l}, and n_{0} = (t^{ω}[n_{1}, ...n_{l}])ˆ )}.

Proof. Obvious.

Translation of the first order formulas.

Definition 4.5 Let φ be a first order formula of arithmetic. Then T r(φ), the translation of φ is an RP EA_{ω} term, computable by the following recursive rules.

T r(t_{1} = t_{2}) = c_{0}(T r(t_{1}) ∧ T r(t_{2})). T r(φ_{1}&φ_{2}) = T r(φ_{1}) ∧ T r(φ_{2}). T r(¬φ) = c_{0}(Un^{l_{φ}}) − T r(φ). T r(∃v_{i}φ) = c_{i+1}(T r(φ) ∧ c_{0}(Un^{l_{φ}})).

Proposition 4.5.1

(i) If a, Un, P lus, Mul ∈ A such that

A ⊧ e_{1}&...&e_{18}[a, t(a), y(a), z(a), Un, P lus, Mul]

then for every first order formula φ of arithmetic, the following hold:

T r(φ) = {⟨u_{0}, ...u_{l_{φ}}⟩^{⌢}h ∈ ^{ω}U : (∃n_{1}, ...n_{l_{φ}} ∈ ω)(n_{1}ˆ = u_{1}, ..., n_{l_{φ}}ˆ = u_{l_{φ}}, and ⟨ω; 0, suc, +, ·⟩ ⊧ φ[n_{1}, ...n_{l_{φ}}]}.

(ii) ⟨ω; 0, suc, +, ·⟩ ⊧ φ iff RP EA_{ω} ⊧ (e_{1}&...&e_{18}) ⇒ Un^{l_{φ}} = T r(φ).

Proof. Obvious.

Translation of the Π_{1}^{1} formulas.

We can use such a second order language, which contains relation variables, all of them having rank 1. This is enough, because in the the arithmetic we can encode the pairs of natural numbers by one number, using a first order formula. Similarly, we may assume that our second order language does not contain function variables, because functions can be identified by their graphs, which is a binary relation, so encodable by an unary one. However, when convenient, we will write function variables, but one can see this as only short forms of some second order formulas.

For every relational variable X_{i} we associate a new variable x_{i}, which is in the equational language of RP EA_{ω}. Of course, all the relational variables have arity 1, see the remarks in the beginning of this section.

Definition 4.6 Let φ be a first order formula of arithmetic, which contains a relation variable X_{i}. Then T r(φ), the translation of φ is an RP EA_{ω} term, computable by the following recursive rules.

T r(X_{i}(t)) = x_{i} ∧ T r(t). The other rules are similar to the preceding case.

Definition 4.7 Throughout, e_{19}, e_{20} denote the following equations:

e_{19} = c_{ω−1}(x_{i}) = x_{i}. e_{20} = x_{i} ≤ c_{1}(z).

Proposition 4.7.1 If a, Un, P lus, Mul, b_{1}, ...b_{k} ∈ A such that

A ⊧ e_{1}&...&e_{20}[a, t(a), y(a), z(a), Un, P lus, Mul, b_{1}, ...b_{k}]

then for any X_{1}, ..., X_{k} relation variables and for every first order formula φ of arithmetic containing X_{1}, ..., X_{k}, hold the following:

⟨ω; 0, suc, +, ·⟩ ⊧ (∀X_{1}, ..., X_{k})φ iff RP EA_{ω} ⊧ e_{1}&...&e_{20} ⇒ Un^{l_{(∀X_{1},...,X_{k})(φ)}} = T r( (∀X_{1}, ...X_{k})φ ).

Note that, we may assume (∀X_{1}, ...X_{k})φ is an arbitrary Π_{1}^{1} formula of arithmetic.

Proof. Obvious.

Now we can finish the proof of Theorem 4.1 as follows. Observe that in e_{1}, e_{2}, e_{3} and in e_{8}...e_{20} are exactly the following operation symbols can occur:

the Booleans, c_{i}, d_{i,j}, i, j ∈ ω, s_{suc}, s_{pred}, s_{[0,1]}, s_{[0,2]}, s_{[0,3]}, s_{[0,4]}, s_{[1,2]}, s_{[1,3]}, s_{[1,4]}, s_{[2,4]}, s_{[0/3]}, c_{ω}, c_{ω−1}, c_{ω−2}, c_{ω−3}.

Let L_{1} be this reduct of RP EA_{ω}.

So the remaining part is finding a strictly finite reduct L of the language of RP EA_{ω} in which all the preceding operations are term definable.

Definition 4.8 Let f, g, h be the following ω → ω functions:

∀x ∈ ω, f(x) = 2 · x

.

∀x ∈ ω, g(x) = \{ \begin{matrix}x − 2 & if x > 1 and x is even \\ 1 & if x = 0 \\ x + 2 & if x is odd \end{matrix}

∀x ∈ ω, h(x) = \{ \begin{matrix}k & if x = 2k \\ k & if x = 2k + 1 \end{matrix}

Note that g is a bijection.

Definition 4.9 Let L be the following strictly finite reduct of the language of RP EA_{ω}: The booleans, c_{0}, d_{0,1}, s_{f}, s_{g}, s_{g^{−1}}, s_{h}, s_{suc}, s_{pred}, s_{[0,1]}, s_{[0,2]}, s_{[0,3]}, s_{[0,4]}, s_{[1,2]}, s_{[1,3]}, s_{[1,4]}, s_{[2,4]}, s_{[0/3]}, c_{ω−3}.

Proposition 4.9.1 For every i, j ∈ ω the following operations are term definable in L: c_{i+1}, d_{i,j}, c_{ω}, c_{,ω−1}, c_{ω−2}.

Proof. It is easy to see that the following definitions are work:

c_{i+1}(x) = s_{h}s_{g}^{i+1}c_{0}s_{g^{−1}}^{i+1}s_{f}(x). d_{0,j+1} = (s_{[0,1]}s_{suc})^{j}(d_{0,1}). d_{i+1,j+1} = s_{suc}(d_{i,j}). c_{ω}(x) = c_{0}c_{1}c_{2}c_{ω−3}(x). c_{ω−1}(x) = c_{1}c_{2}c_{ω−3}(x). c_{ω−2}(x) = c_{2}c_{ω−3}(x).

This completes the proof of Theorem 4.1.

As we mentioned in the introduction, if Eq(RP EA_{ω}) were finitely axiomatizable by some kind of schemas, then the equational consequences of these schemas written in the above defined language L would form a Π_{1}^{1} hard set (by Theorem 4.1). Usually, finite (schema) axiomatizability of some theory implies recursively enumerability of this theory. However, in [10] there is an other strictly finite reduct of the language of P A_{ω} such that the equational consequences of the P A_{ω} axioms written in this language, form a not recursively enumerable set. Moreover, the indices of the substitutions and cylindrifications occurring in this reduct, are recursive functions and sets, respectively.

The intuitive meaning of these results is that Eq(RP EA_{ω}) is not computable. This is not a precise mathematical statement, because the cardinality of this set is continuum, so too big to handle by a computer. But suppose one generalizes the concept of computability in a meaningful way to continuum big sets. The only thing we assume about the new, generalized concept of computability is the following. The intersection of two computable set is computable, and the old, countable noncomputable sets are not computable in the new sense. Now Eq(RP EA_{ω}) is not computable in the new, generalized sense, because its intersection with a decidable (in the old sense) set L, forms a Π_{1}^{1} hard set, as Theorem 4.1 states. Summing up, the set Eq(RP EA_{ω}) is really not computable.

Let us turn briefly to trying to give upper bounds for complexity. What we do below are only the first steps in exploring this direction.

Definition 4.10 If Σ is a set of Halmos schemas then

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

We will single out certain kinds of reducts L′ of the language of RP EA_{ω} such that the axiomatic approximations of RP EA_{ω} have the following property. Roughly speaking, if 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 will be “of relatively low complexity”. More formally: if Σ is a finite set of Halmos schemas valid in RP EA_{ω} then Ded(Σ) ∩ L′ i.e. the equational consequences of Σ written in the language L′ form a Σ_{1}^{1} enumerable set. That is, there exists an algorithm, which uses an oracle deciding the Σ_{1}^{1} theory of standard arithmetic, and enumerates Ded(Σ) ∩ L′.

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

Definition 4.11 If L is a reduct of the language of RP EA_{ω} such that

– L contains at most countably many operation symbol, and

– in L only finitely many operation symbol occur which is not a CA_{ω} operation symbol, and

– whenever c_{Γ} or s_{τ} is an operation symbol in L then Γ, τ are first order definable over ⟨ω; 0, suc⟩, respectively,

then we say that L is a simple language.

The language L defined in 4.9 is not simple because of s_{f}, s_{g}, s_{h} but L_{1} is simple. (L_{1} is defined after proposition 4.7.1.)

Let A = ⟨ω; 0, suc⟩. Note that the Σ_{1}^{1} theory of A is as hard as the Σ_{1}^{1} theory of standard arithmetic, because addition and multiplication are definable by a Σ_{1}^{1} formula.

Definition 4.12 Let L be a simple language, Σ be a set of Halmos schemas, and e be an equation written in L and derivable from (the ω dimensional instances of the elements of) Σ. Then w(e) is a witness sentence of e iff the following hold.

– w(e) is a Σ_{1}^{1} formula of A, and

– w(e) = (∃R_{1}, ..., R_{k})(∃f_{1}, ..., f_{l})(φ_{1}&...&φ_{n}&ψ_{1}&...&ψ_{m}) such that

– φ_{1}, ..., φ_{n} are the left hand side of some Halmos schemas occurring in Σ, and – ψ_{1}, ..., ψ_{m} are the definitions of the indices of the operation symbols of L, that is, if c_{Γ_{p}} is the p − th operation symbol in L then ψ_{p} = (∀x)(R_{p}(x) ⇔ the definition of Γ_{p}) (similarly for substitutions), and

– e is provable from Σ_{0} where Σ_{0} = {f : f is an equation in L such that f is an ω dimensional instance of some ⟨φ_{m}, g⟩ with respect to ⟨ω, Γ_{1}, ..., Γ_{p_{1}}, τ_{1}, ..., τ_{p_{2}}⟩. (p_{1} + p_{2} = m.)

Obviously, if all conditions hold, then there exists a witness sentence for e.

Note that if Σ ⊢ e and w(e) is a witness sentence of e then A = ⟨ω; 0, suc⟩ ⊧ w(e).

Theorem 4.13 Let L′ be a simple language. Let Σ be any finite (or recursively enumerable) set of Halmos schemas. Then Ded(Σ) ∩ L′ is recursively enumerable over the Σ_{1}^{1} theory of A.

Proof. We will construct an algorithm (see alg_{3} below), which enumerates Ded(Σ)∩ L′. Let alg_{0} be an algorithm (oracle) which enumerates the Σ_{1}^{1} theory of A. As we mentioned, the complexity of Σ_{1}^{1} theory of A is the same as the complexity of the Σ_{1}^{1} theory of standard arithmtic. For a given valid Σ_{1}^{1} sentence σ we will systematically enumerate the equations having witness sentence σ.

Let alg_{1} be the following algorithm. alg_{1} maps the Σ_{1}^{1} formulas σ of A to the finite subsets of Σ such that if σ = (∃X_{1}...X_{k})(φ_{1}&...&φ_{n}) where φ_{1}, ...φ_{n} are first order formulas containing the definitions of the indices of operation symbols of L′ then alg_{1}(σ) = {h ∈ Σ : (∃1 ≤ m ≤ n)(∃e_{φ_{m}} ∈ L_{P T})(h = ⟨φ_{m}, e_{φ_{m}}⟩)}. If σ has different form, then alg_{1}(σ) = 0 (the empty set).

Let alg_{2} be an algorithm, which enumerates the consequences of a recursively enumerable set of equations written in L_{P T}, using logic of equations as inference system.

Let alg_{3} be the following algorithm. Combining alg_{0}, alg_{1} first alg_{3} enumerates the (finite) sets of Halmos schemas H produced by alg_{1} on the output of alg_{0}. Secondly alg_{3} between two such steps, using alg_{2}, enumerates the consequences of the set {e ∈ L_{P T} : (∃φ)(⟨φ, e⟩ ∈ H}. More precisely, alg_{3} enumerates all pairs of natural numbers, and if ⟨i, j⟩ are computed, then alg_{2} runs j steps on the i − th output of alg_{0}, alg_{1}. Now the derived equation is in L_{P T}, so finally, of course, alg_{3} substitute every relation and function variables with the corresponding set or function (using the current output of alg_{0} and the definitions of the indices of the operation symbols of L′) so the result equation is written in L′. After this, alg_{3} take the next pair. we claim that alg_{3} do the job.

Proposition 4.13.1 alg_{3} is sound, that is, if e is listed by alg_{3}, then e ∈ Ded(Σ) ∩ L′.

Proof. Assume e is the i − th output of alg_{3}. By the definition of alg_{3} e ∈ L′. Suppose e was obtained from e′ ∈ L_{P T} by substitutions, and the i − th output of alg_{0} is φ. (This is a Σ_{1}^{1} sentence of A.) There exist a proof p′ of e′ such that p′ uses the second components of the i − th output of alg_{1} as hypotheses. By the definition of alg_{0}, alg_{1} this proof is translatable into an RP EA_{ω} proof for e (using the same substitutions).

Proposition 4.13.2 alg_{3} is complete, that is, if e ∈ Ded(Σ) ∩ L′ then e is listed by alg_{3}.

Proof. Assume e ∈ Ded(Σ) ∩ L′. Let w(e) be a witness sentence for e. This is an element of the Σ_{1}^{1} theory of A, so alg_{0} will enumerate w(e). Then, by the definition of witness sentence, e is provable from the corresponding output of alg_{1} so alg_{3} really enumerates e.

This completes the proof of theorem 4.5.

5 Related Results

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

Case of algebras without equality

By the theorem of Daigneault and Monk every P A_{ω} is representable, so 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 recursively 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 following set of equations is not recursively enumerable: {e ∈ L_{G} : (Axioms of P A_{ω}) ⊢ e}. Moreover, the indices of the substitutions and cylindrifications are recursive functions and sets, respectively.

For the proof see [10].

Definition 5.2 Throughout L_{suc,pred} denote the following language. L_{suc,pred} 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 following operations are term definable: c_{i}, s_{[i,j]}, i, j ∈ ω. The following theorem is due to I. Sain and V. Gyuris, (see [8]) which is a possible solution of (some variant of) the finitization problem.

Theorem 5.3 Let L_{suc,pred,ω} = L_{suc,pred} ∪ {c_{ω}}. Then the reduct of RP A_{ω} to L_{suc,pred,ω} generates a variety, which 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 a representation theorem, but the axiom system is recursive, so Eq(RP A_{ω}) ∩ L_{suc,pred,ω} = Ded(Σ_{suc,pred,ω}) ∩ L_{suc,pred,ω} is recursively enumerable.

Case of algebras with equality

The following theorem is also in [8].

Theorem 5.4 Let L_{suc,pred,D} = L_{suc,pred}∪{d_{0,1}, i, j ∈ ω}. Note that in this language all the D_{i,j}’s are term definable, i, j ∈ ω. Then the reduct of RP EA_{ω} to L_{suc,pred,D} generates a variety, which 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 preceding remarks hold for this case, 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.

Finally about the complexity of the first order theory of RP EA_{ω}. One can continue the proof of Theorem 4.1 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 Th(RP EA_{ω}) ∩ L does not form an analytical set (so 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_{ω}.

Methodological conclusions

Comparing the negative and positive results above, we found the following. There are two paradigms. In the first paradigm (called polyadic algebraic 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 mirroring in the equational theories that we are studied, and possibly this is the reason of our negative results.

The other paradigm (called cylindric algebraic oriented) is the opposite. In this case the indices of operation symbols have no essentially structure. There are no operations and relations defined between the names of the operation symbols. We observed, that all the positive results follow the cylindric paradigm.

These paradigms not are rigid things, for example the results about quasi polyadic algebras in [9] follow the cylindric paradigm (and the results are positive).

The main methodological conclusion is the following. Suppose one wants to apply polyadic algebras to the 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 [4] 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 2, North-Holland, Amsterdam (1985).

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

[6] I. Németi, Algebraization of Quantifier Logics, an introductory overview. Studia Logica vol. 50, No 3/4. p485-569. (A strongly updated and expanded version is available from the author.)

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

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

[9] 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, p 539-571.

[10] G. Sági, Non-computability of the consequences of the axioms of the ω dimensional polyadic algebras, Math. Inst. Budapest, Preprint (1995).

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