Non-computability of the consequences of the axioms of the ω dimensional polyadic algebras

Gábor Sági^{∗}

December 6, 1996

Abstract

In [2] Daigneault and Monk proved that the class of (ω dimensional) representable polyadic algebras (RP A_{ω} for short) is axiomatizable by finitely many equation-schemas. However, this result does not imply that the equational theory of RP A_{ω} would be recursively enumerable; one simple reason is that the language of RP A_{ω} consists of continuum many operation symbols. Here we prove the following. Roughly, for any reasonable generalization of computability to continuum large languages, Eq(RP A_{ω}) remains non-recursively enumerable, or non-enumerable in the generalized sense too. This will be seen to be an “intuitive” consequence of the following more formal statement. There is a strictly finite reduct L_{G} of the language of RP 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.

1 Introduction

In [2] Daigneault and Monk proved that the class of (ω dimensional) representable polyadic algebras (RP A_{ω} for short) is axiomatizable by finitely many equationschemas. (The class RP A_{ω} is concrete in the following sense. Every RP A_{ω} is a set algebra, and the operations are definable in a set theoretic way. There is an other class: the class of polyadic algebras (with dimension ω). This class is defined by (finitely many schemas of) equations, so the class of polyadic algebras (P A_{ω} for short) is an abstract class (which contain the representables). The above mentioned theorem states, that every P A_{ω} is representable (as a concrete set-algebra), in other words, the class RP A_{ω} is axiomatizable by finitely many schemas of equations, thus RP A_{ω} = P A_{ω}, under isomorphism. For details see [2], [4].) However, the result of Daigneault and Monk does not imply that the equational theory of P A_{ω} would be recursively enumerable; one simple reason is that the language of P A_{ω} consists of continuum many operation symbols. Here we prove the following. Roughly, for any reasonable generalization of computability to continuum large languages, Eq(P A_{ω}) remains non-recursively enumerable, or non-enumerable in the generalized sense too. This will be seen to be an “intuitive” consequence of the following more formal statement. 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:

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

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

2 Construction of L_{G}.

Definition 2.1 Ax_{P A} denotes the set of usual defining equations of (ω dimensional) polyadic algebras. (For details, see [4], p.225.)

The construction presented below will be an example for a finite reduct L_{G} such that the following set of equations is not recursively enumerable:

{e ∈ L_{G} : Ax_{P A} ⊢ e}.

The intuitive meaning of this result is that the set of equational consequences of Ax_{P A} 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 non-computable sets are not computable in the new sense. Now {e ∈ L_{G} : Ax_{P A} ⊢ e} is not computable in the new, generalized sense, because its intersection with a decidable (in the “old” sense) set L_{G}, forms a non-recursively enumerable set, as we will prove. Summing up, the set {e ∈ L_{G} : Ax_{P A} ⊢ e} is really not computable.

Construction 2.2

• Let f(i, j, k) be the following function.

∀i, j, k ∈ ω, f(i, j, k) = \{ \begin{matrix}l + 1 & if the i-th Register Machine program on the input \\ & j terminates at most k step, and the result is l. \\ 0 & otherwise. \end{matrix}

• Let σ_{3} be a function, which codes the triples of natural numbers, that is, the domain of σ_{3} is ω × ω × ω and σ_{3} is bijective, and σ_{3}, σ_{3}^{−1} are recursive. It is well known that such a σ_{3} is exist.

• Let g = f ∘ σ_{3}^{−1}.

• Let h be a recursive function which enumerates the σ_{3} codes of those triples, in which the first coordinate equal to zero, and the other two is arbitrary.

• Let s = σ_{3}([1, 0, 0] + σ_{3}^{−1}). So s first computes the tripe encoded by its input, then increments the first component, then computes the σ_{3} code of the new triple.

• Let null be the constant zero function (on ω).

• Finally, let G = {g, h, s, null}.

Let L_{G} be such a finite reduct of the language of Polyadic Algebras, which consists of the following basic operations: s_{g}, s_{h}, s_{s}, s_{null}. Note that the elements of G are recursive functions.

Above we defined a reduct L_{G} of polyadic algebras. Now we attempt to demonstrate, that the set of equational consequences of Ax_{P A} written in the language L_{G} form a non-recursively enumerable set. Throughout, i is a natural number.

Claim 2.1 g ∘ \underbrace{s ∘ ⋯ ∘ s}_{i} ∘h = null iff the i-th Register Machine program computes

the empty function (the domain of the empty function is the empty set).

Proof. g ∘ \underbrace{s ∘ ⋯ ∘ s}_{i} ∘h = null iff

(∀n ∈ ω)(g ∘ \underbrace{s ∘ ⋯ ∘ s}_{i} ∘h (n) = 0) iff

(∀j, k ∈ ω)(g ∘ \underbrace{s ∘ ⋯ ∘ s}_{i} ∘σ_{3} (0, j, k) = 0) iff

(∀j, k ∈ ω)(g ∘ σ_{3} (i, j, k) = 0) iff (∀j, k ∈ ω)(f(i, j, k) = 0) iff The i − th Register Machine program computes the empty function.

Claim 2.2 Ax_{P A} ⊢ s_{g} \underbrace{s_{s} ⋯ s_{s}}_{i} s_{h}(x) = s_{null}(x) iff the i-th Register Machine program

computes the empty function.

Proof. ⇐ If the i-th Register Machine program computes the empty function, then by the pre-

vious claim g ∘ \underbrace{s ∘ ⋯ ∘ s}_{i} ∘h = null and then s_{g} \underbrace{s_{s} ⋯ s_{s}}_{i} s_{h}(x) = s_{g∘\underbrace{s ∘ ⋯ ∘ s}_{i} ∘h}(x) =

s_{null}(x) ⇒ If the i-th Register Machine program terminates, say, on the input j, then by the previous claim g ∘ \underbrace{s ∘ ⋯ ∘ s}_{i} ∘h and null are not equal.

Let A = ⟨P(^{ω}ω), the Booleans, C_{γ}, S_{τ}⟩_{γ⊆ω,τ∈^{ω}ω}, (so A ∈ P A_{ω})

and let b = \{g∘\underbrace{s ∘ ⋯ ∘ s}_{i} ∘h\} ∈ A. Now one can easily see that id_{ω} ∈ S_{g}^{A} \underbrace{S_{s}^{A} ⋯ S_{s}^{A}}_{i} S_{h}^{A}(b),

but id_{ω} is not in S_{null}^{A}(b), and hence s_{g} \underbrace{s_{s} ⋯ s_{s}}_{i} s_{h}(x) = s_{null}(x) is not valid in A, so

(by soundness of logic of equations) this equation is not derivable from Ax_{P A}.

Now we want to recursively reduce the set of indices of the empty function to the set of equations derivable from Ax_{P A} and written in L_{G}.

Theorem 2.3 The consequences of Ax_{P A} (written in the language L_{G}) are not recursively enumerable.

Proof. Assume the opposite. That is, there exists an algorithm which enumerates the consequences of Ax_{P A} (written in the language L_{G}). But then exists an other algorithm, which enumerates the following set I.

I = \{i ∈ ω : Ax_{P A} ⊢ s_{g} \underbrace{s_{s} ⋯ s_{s}}_{i} s_{h}(x) = s_{null}(x)\}.

By the previous claim i ∈ I iff the i-th. Register Machine program computes the empty function. But it is well known that this set (and hence I) is not recursively enumerable. This contradiction completes the proof.

3 Related Results

Here we summarize some results about the complexity of the equational theory of some reduct of polyadic (equality) algebras.

Definition 3.1 RP EA_{ω} denotes the class of ω dimensional representable polyadic equality algebras. If K is a class of algebras, then Eq(K) denotes the equational theory of K. If Σ is a set of equations then Ded(Σ) denotes the set of all equational consequences of Σ.

3.1 Case of algebras without equality

By the theorem of Daigneault and Monk Eq(P A_{ω}) = Ded(Ax_{P A}), so the “complexity” of the equational theory of P A_{ω} is the same as the “complexity” of the set of all equational consequences of Ax_{P A}.

Definition 3.2 Throughout L_{suc,pred} denotes 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 ∈ ω. Here suc, pred, [0, 1], [i/j] are the following functions on ω:

(∀n ∈ ω)suc(n) = n + 1,

pred(n) = \{ \begin{matrix}n-1 & if n ≠ 0, \\ 0 & otherwise. \end{matrix}

[0, 1](n) = \{ \begin{matrix}n & if n ≠ 0, n ≠ 1, \\ 1 & if n = 0, \\ 0 & if n = 1. \end{matrix}

[i/j](n) = \{ \begin{matrix}n & if n ≠ i, \\ j & if n = i. \end{matrix}

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 [7]) which is a possible solution of (some variant of) the finitization problem.

Theorem 3.3 Let L_{suc,pred,ω} = L_{suc,pred}∪{c_{ω}}. Then the reduct of P 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.

This theorem is a representation theorem, but the axiom system is recursive, so Eq(P A_{ω}) ∩ L_{suc,pred,ω} = Ded(Σ_{suc,pred,ω}) is recursively enumerable.

3.2 Case of algebras with equality

It is well known that RP EA_{ω} is not closed under taking ultraproducts, and hence this class is not axiomatizable. Particularly, Eq(RP EA_{ω}) is not equal with the set of all equational consequences of P EA_{ω} axiom schemas. (see [4]). The equational theory of RP EA_{ω} is very complex, in [5] we proved, that this theory is not axiomatizable by schemas similar to the usual defining schemas of P EA_{ω}. The following theorem is proved in [7].

Theorem 3.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, 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.

All the preceding remarks hold for this case, too. The following theorem is due to R. McKenzie.

Theorem 3.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.

The equational theory of RP EA_{ω} is extremely high, as the following theorem claims.

Theorem 3.6 Eq(RP EA_{ω}) is Π_{1}^{1} hard ^{1}, in the sense 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 σ the arithmetical validity of σ is equivalent with RP EA_{ω} ⊧ T r(σ). (For the second order logical and recursion theoretic notions used here we refer to [6].)

For the proof see [5]. The message of this result is non-computability of Eq(RP EA_{ω}) similarly to the remark below definition 2.1.

Finally about the complexity of the first order theory of RP EA_{ω}. In [5] we proved that Th(RP EA_{ω}) ∩ L_{∗} is 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_{ω}.

1Π_{1}^{1} hardness is a very strong form of non-computability, e.g. it implies non-enumerability by any kind of algorithm, but Π_{1}^{1} hardness is a much stronger negative property than this cf. Odifreddi [6] for the definition of Π_{1}^{1} sets.

References

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

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

[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] I. Németi, G. Sági, On the Equational Theory of Representable Polyadic Algebras, Manuscript (1996).

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

[7] I. Sain, V. Gyuris, Finite Schematizable Algebraic Logic, Bulletin of IGPL, to appear (1996). e-mail: sagi@circle.math-inst.hu