MATHEMATICS

Academician A. I. MAL’TSEV

ON THE ELEMENTARY THEORIES OF LOCALLY FREE UNIVERSAL ALGEBRAS

A set \(A\) together with some sequence \(\varphi_i(x_1,\ldots,x_{r_i})\) \((i=1,\ldots,s)\) of operations defined on it is called an algebra of type \(\langle r_1,\ldots,r_s\rangle\). This type will henceforth be regarded as arbitrary, but fixed. The symbols \(\varphi_1,\ldots,\varphi_s\) will denote the fundamental operations of an arbitrary algebra of the given type. Object symbols \(x,y,\ldots\) will be called terms of length 1. If \(a_1,\ldots,a_{r_i}\) are terms of lengths \(n_1,\ldots,n_{r_i}\), then the expression \(\varphi_i(a_1,\ldots,a_{r_i})\) is called a term of length \(n_1+\cdots+n_{r_i}+1\). Let \(a(a_1,\ldots,a_n)\) be a term composed of elements \(a_1,\ldots,a_n\) of the algebra \(A\) and of the functional symbols \(\varphi_1,\ldots,\varphi_s\). Performing on \(a_1,\ldots,a_n\) the operations indicated in the notation of the term, we obtain an element \(a\in A\), called the value of the term \(a\). The elements \(a_1,\ldots,a_n\) are mutually free in \(A\) if the values of arbitrary terms \(a,b\) in \(a_1,\ldots,a_n\) are equal only when the terms \(a,b\) themselves are (graphically) equal. An algebra \(A\) is called free if it has a mutually free system of generators. An algebra \(A\) is locally free if each of its subalgebras generated by a finite system of elements is free. A free algebra is also locally free, since every subalgebra of a free algebra is free \((^4)\).

The class of locally free algebras is completely characterized by the axioms

\[ \varphi_i(x_1,\ldots,x_{r_i})\ne \varphi_j(y_1,\ldots,y_{r_j}) \qquad (i\ne j;\ i,j=1,\ldots,s); \tag{1} \]

\[ \varphi_i(x_1,\ldots,x_{r_i})=\varphi_i(y_1,\ldots,y_{r_i})\to x_1=y_1\ \&\ \cdots\ \&\ x_{r_i}=y_{r_i}\quad (i=1,\ldots,s). \tag{2} \]

By formulas we shall henceforth mean formulas of the narrow predicate calculus (NPC), composed from equalities of the form \(f(x_1,\ldots,x_n)=g(x_1,\ldots,x_n)\), where \(f,g\) are terms, by means of the logical operations \(\neg,\ \&,\ \vee,\ \forall,\ \exists\).

The purpose of the present note is to indicate an algorithm which, for each formula \(\mathfrak F(x_1,\ldots,x_n)\), constructs a formula \(\mathfrak F^*\) of a simpler form, equivalent to \(\mathfrak F\) on every locally free algebra.

As a consequence it will follow that the set of closed formulas true on locally free algebras is algorithmically decidable.

An algebra with one binary operation is called a groupoid. In the works of Post \((^2)\) and Yas’kovskii \((^3)\) it was shown that the question of the realizability of any formula of NPC reduces to the question of the realizability of a suitable formula in the class of all free groupoids with an additional unary predicate, and thus the class of NPC formulas true on all free groupoids with a unary predicate is algorithmically undecidable. From the general result of the present note it follows that the class of formulas true on a free groupoid (without an additional predicate) is decidable.

We introduce the following permanent notation:

\[ N_i(x)\leftrightarrow (y_1\ldots y_{r_i})(x\ne \varphi_i(y_1,\ldots,y_{r_i})) \qquad (i=1,\ldots,s); \]

\[ N_{\mathfrak p}(x)\leftrightarrow N_{i_1}(x)\&\ldots\&N_{i_k}(x) \qquad (\mathfrak p=\langle i_1,\ldots,i_k<;\ i_1<\ldots<i_k); \]

\[ E_{\mathfrak p}^{m}\leftrightarrow(\exists y_1\ldots y_m)(N_{\mathfrak p}(y_1)\&\ldots\&N_{\mathfrak p}(y_m)\& \bigwedge_{i\ne j} y_i\ne y_j) \qquad (m=2,3,\ldots); \]

\[ E_{\mathfrak p}^{1}\leftrightarrow(\exists y)N_{\mathfrak p}(y);\qquad D_{\mathfrak p}^{m}\leftrightarrow \neg E_{\mathfrak p}^{m} \qquad (m=1,2,\ldots). \]

Here \(\bigwedge\), \(\bigvee\) are the symbols, respectively, of conjunction and disjunction.

Theorem. There exists an algorithm which, for every formula
\(\mathfrak A(x_1,\ldots,x_n)\) with free individual variables \(x_1,\ldots,x_n\),
constructs a formula \(\mathfrak A^*(x_1,\ldots,x_n)\), equivalent to \(\mathfrak A\) on every locally free algebra and which is a conjunction of disjunctions of formulas of the form
\(N_i(z)\), \(D_{\mathfrak p}^{m}\), \(E_{\mathfrak p}^{m}\) and formulas of the form

\[ (\exists y_1\ldots y_m)(x_1=f_1\&\ldots\&x_p=f_p\& \bigwedge x_{\alpha_i}\ne g_i\&\bigwedge y_{\beta_j}\ne h_j\& \bigwedge N_{\gamma_k}(y_{\delta_k})), \tag{3} \]

where \(f_l,g_i,h_j\) are terms in
\(x_{p+1},\ldots,x_n,\ y_1,\ldots,y_m;\)
\(\alpha_i=p+1,\ldots,n\), \(\beta,\delta=1,\ldots,m\).

If the formula \(\mathfrak A\) contains no free individual variables, then, according to the theorem, it is equivalent to a conjunction of disjunctions of formulas \(D_{\mathfrak p}^{m}\), \(E_{\mathfrak p}^{m}\), asserting the existence or nonexistence in the algebra of a given number of elements of fixed type \(N_{\mathfrak p}\). The number of types of elements is \(2^s-1\), and if for each type \(N_{\mathfrak p}\) it is known how many distinct elements of this type there are in the algebra, then it is easy to compute also the value of the standard formula \(\mathfrak A^*\).

Calling a standard class a class of algebras characterized by one of the axioms \(D_{\mathfrak p}^{m}\) or \(E_{\mathfrak p}^{m}\), we arrive at the conclusion that every axiomatizable class of locally free algebras is an intersection of finite unions of standard classes.

We shall now describe the algorithm for reducing a formula \(\mathfrak A\) to the normal form \(\mathfrak A^*\), whose existence is asserted by the theorem.

Let us agree to call an \(\exists\)-formula a formula constructed from expressions of the form \(f=g\), \(f\ne g\), \(N_i(z)\), where \(f,g\) are terms, only by means of the symbols \(\&,\vee,\exists\), i.e., without the symbols \(\neg\) and \(\forall\).

Algorithm for reducing \(\exists\)-formulas. Let a prenex form for \(\mathfrak A\) be \((\exists y_1\ldots y_m)\mathfrak A_0\), where \(\mathfrak A_0\) is the quantifier-free part \((^1)\). Reducing \(\mathfrak A_0\) to disjunctive form and distributing the quantifiers \(\exists\), we reduce the matter to transforming a formula \((\exists y_1\ldots y_m)\mathfrak A_1\), where \(\mathfrak A_1\) is a conjunction of terms of the form \(D_{\mathfrak p}^{i}\), \(E_{\mathfrak p}^{i}\), \(N_i(x)\), \(N_i(y)\), \(f=g\), \(f\ne g\). All terms not depending on \(y_1,\ldots,y_m\) may be taken out and thereafter not considered. By virtue of (1), (2), terms of the form
\(\varphi_i(a_1,\ldots,a_{r_i})=\varphi_j(b_1,\ldots,b_{r_j})\) for \(i\ne j\) are false, and terms
\(\varphi_i(a_1,\ldots,a_{r_i})=\varphi_i(b_1,\ldots,b_{r_i})\) may be replaced by the equivalent expression
\(a_1=b_1\&\ldots\&a_{r_i}=b_{r_i}\).
If in \(\mathfrak A_1\) there is a term of the form \(x=f\), then \(x\) cannot occur in \(f\), since otherwise this term will have the value false. Leaving such a term unchanged, in all the other terms in which \(x\) occurs we replace \(x\) by \(f\). Repeating several times transformations of the indicated types, after a finite number of steps we arrive at a formula of the required form.

Algorithm for reducing the negation of an \(\exists\)-formula. Since an \(\exists\)-formula is reducible to a conjunction of disjunctions of standard formulas of the form (3) and \(E_{\mathfrak p}^{m}\), \(D_{\mathfrak p}^{m}\), in order to reduce the negation of an \(\exists\)-formula it is enough to be able to reduce the negations of these standard parts. But

\[ \neg E_p^m \leftrightarrow D_p^m \quad \text{and} \quad \neg D_p^m \leftrightarrow E_p^m, \]
and \(\neg N_i(x)\) has the form (3). Therefore it is necessary to be able to transform only the negation of formula (3), i.e., the formula

\[ (y_1,\ldots,y_m)\left(\bigwedge x_l=f_l \to \bigvee x_{\alpha_i}=g_i \vee \bigvee y_{\beta_j}=h_j \vee \bigvee \neg N_{i_k}(y_{\delta_k})\right). \]

This formula can be rewritten in the form

\[ (y_{t+1}\ldots y_m)\left(\bigwedge x_l=f_l \to (y_1\ldots y_t)\,\mathfrak{B}\right), \tag{4} \]

where \(y_1,\ldots,y_t\) are all those \(y\)'s that do not occur in the terms \(f_1,\ldots,f_p\). For given \(x_1,\ldots,x_p\), the system of equations \(x_1=f_1,\ldots,x_p=f_p\) with respect to \(y_{t+1},\ldots,y_m\) can have at most one solution. Therefore formula (4) is equivalent to the formula

\[ (y_{t+1}\ldots y_m)\left(\bigvee x_l\ne f_l\right)\vee (\exists y_{t+1}\ldots y_m)\left(\bigwedge x_l=f_l \,\&\, (y_1\ldots y_t)\,\mathfrak{B}\right). \tag{5} \]

We have to transform into \(\exists\)-formulas the first member of the disjunction (5) and the expression \((y_1\ldots y_t)\mathfrak{B}\).

We shall illustrate the reduction of a formula of the form
\[ (y_1\ldots y_\lambda)\bigl(x\ne f(x_1,\ldots,x_\mu,y_1,\ldots,y_\lambda)\bigr) \]
by the example \((y)(x\ne x_1y\cdot y)\), assuming that a groupoid is being considered.

Since for a given \(x\) in a locally free groupoid the equation
\[ x=uv\cdot w \]
has at most one solution for \(u,v,w\), the indicated formula is equivalent to the formula

\[ (\exists uv)(x=x_1u\cdot v \,\&\, u\ne v)\vee (\exists uv)(x=uv \,\&\, (w)(u\ne x_1w)), \]

where

\[ (w)(u\ne x_1w)\leftrightarrow (\exists yz)(u=yz \,\&\, y\ne x_1)\vee N(u). \]

Suppose that for the formula
\[ (y_1\ldots y_\lambda)(x_1\ne f_1\vee \cdots \vee x_q\ne f_q) \]
an equivalent \(\exists\)-form has already been found. The longer formula
\[ (y_1\ldots y_\lambda)(x_1\ne f_1\vee \cdots \vee x_{q+1}\ne f_{q+1}) \]
is, for the reasons indicated above, equivalent to the formula

\[ (y_1\ldots y_\lambda)(x_1\ne f_1\vee \cdots \vee x_q\ne f_q) \vee (\exists y_1\ldots y_\sigma)(x_1=f_1 \,\&\, \cdots \,\&\, x_q=f_q \,\&\, (y_{\sigma+1}\ldots y_\lambda)(x_{q+1}\ne f_{q+1})), \]

where \(y_{\sigma+1},\ldots,y_\lambda\) are all those bound variables which do not occur explicitly in \(f_1,\ldots,f_q\). The reduction of both subformulas beginning with universal quantifiers was indicated above.

Now consider in (5) the subformula \((y_1\ldots y_t)\mathfrak{B}\). Its reduction is based on the following lemma.

Lemma. Let \(T_1,\ldots,T_t\) be fixed sets of elements of a locally free algebra. If each of these sets contains more than \(u+v\) elements, then the expression

\[ (\forall y_1\in T_1)\ldots(\forall y_t\in T_t) (x_{\alpha_1}=g_1\vee \cdots \vee x_{\alpha_u}=g_u \vee y_{\beta_1}=h_1\vee \cdots \vee y_{\beta_v}=h_v) \tag{6} \]

is false for any \(x_1,\ldots,x_n,y_{t+1},\ldots,y_m\), provided that, for every \(i\), the term \(g_i\) is distinct from \(x_{\alpha_i}\) and the term \(h_i\) is distinct from \(y_{\beta_i}\). If the latter condition is not satisfied, then expression (6) is identically true.

Indeed, each of the equations \(x_{\alpha_i}=g_i\) has, for those \(y\)'s which actually occur in it, at most one solution. Removing these solutions from the corresponding sets \(T_1,\ldots,T_t\), we obtain sets \(T'_1,\ldots,T'_t\), each containing not fewer than \(v\) elements; moreover, for ...

\(y_1\in T'_1,\ldots,y_t\in T'_t\), all the equalities \(x_{\alpha_1}=g_1,\ldots,x_{\alpha_u}=g_u\) will be false. Now fix \(y_{\beta_1}\) in \(T'_{\beta_1}\) and, instead of (6), consider the formula

\[ (\forall y_1\in T'_1)\cdots(\forall y_t\in T'_t) (y_{\beta_1}=h_1\vee\cdots\vee y_{\beta_v}=h_v) \quad (\forall y_{\beta_1}\ \text{is omitted}), \]

to which we apply the same arguments, and so on.

A locally free algebra is infinite. Therefore, if in \(\mathfrak{B}\) there are no terms \(\neg N_\gamma(y_s)\), then it follows from the lemma that the formula \((y_1\ldots y_t)\mathfrak{B}\) will be either identically false or identically true.

Suppose that in \(\mathfrak{B}\) there are terms \(\neg N_\gamma(y_s)\). If not all \(y\)’s occur in these terms, then, transforming \((y_1\ldots y_t)\mathfrak{B}\) to the form

\[ (y_1\ldots y_w) \left(\bigvee \neg N_{\gamma_k}(y_{\delta_k})\vee (y_{w+1}\ldots y_t)\left(\bigvee x_{\alpha_i}=g_i\vee\bigvee y_{\beta_j}=h_j\right)\right), \tag{7} \]

we conclude, on the basis of the lemma, that the expression
\[ (y_{w+1}\ldots y_t)\left(\bigvee x_{\alpha_i}=g_i\vee\bigvee y_{\beta_j}=h_j\right) \]
is either identically true or identically false. In the second case (7) will be equivalent to a disjunction of the form
\[ D^1_{\mathfrak{p}_1}\vee\cdots\vee D^1_{\mathfrak{p}_v}, \]
and in the first case (7) is identically true.

It remains to consider formula (7) under the condition that \(w=t\), i.e., that each of \(y_1,\ldots,y_t\) occurs in a suitable term \(\neg N_\gamma(y_s)\). Combining the terms referring to one and the same \(y_i\), we transform (7) to the form

\[ (y_1\ldots y_t)\left(N_{\mathfrak{p}_1}(y_1)\ \&\ \cdots\ \&\ N_{\mathfrak{p}_t}(y_t) \to \bigvee x_{\alpha_i}=g_i\vee\bigvee y_{\beta_j}=h_j\right). \tag{8} \]

Let \(M_i\) be the totality of all \(N_{\mathfrak{p}_i}\)-elements of the algebra. Rewriting (8) in the form

\[ (\forall y_1\in M_1)\cdots(\forall y_t\in M_t) (x_{\alpha_1}=g_1\vee\cdots\vee x_{\alpha_u}=g_u\vee y_{\beta_1}=h_1\vee\cdots \]
\[ \cdots\vee y_{\beta_v}=h_v), \tag{9} \]

we conclude, on the basis of the lemma, that (9) is identically false if each set \(M_i\) contains more than \(u+v\) elements. Consequently, formula (8) is equivalent to the expression

\[ (D^{z+1}_{\mathfrak{p}_1}\ \&\ \mathfrak{F})\vee\cdots\vee (D^{z+1}_{\mathfrak{p}_t}\ \&\ \mathfrak{F}) \quad (z=u+v), \]

where \(\mathfrak{F}\) denotes formula (8) itself. But

\[ D^{z+1}_{\mathfrak{p}}\leftrightarrow D^1_{\mathfrak{p}}\vee(D^2_{\mathfrak{p}}\ \&\ E^1_{\mathfrak{p}})\vee\cdots\vee (D^{z+1}_{\mathfrak{p}}\ \&\ E^z_{\mathfrak{p}}), \]

therefore formula (8) is equivalent to a disjunction of formulas \(D^1_{\mathfrak{p}}\) and
\[ D^{\sigma+1}_{\mathfrak{p}}\ \&\ E^\sigma_{\mathfrak{p}}\ \&\ \mathfrak{F} \quad (\sigma=1,\ldots,z). \]
But

\[ D^{\sigma+1}_{\mathfrak{p}_1}\ \&\ E^\sigma_{\mathfrak{p}_1}\ \&\ \mathfrak{F}D \leftrightarrow \]

\[ \leftrightarrow D^{\sigma+1}_{\mathfrak{p}_1}\ \&\ (\exists w_1\ldots w_\sigma) \left(N_{\mathfrak{p}_1}(w_1)\ \&\ \cdots\ \&\ N_{\mathfrak{p}_1}(w_\sigma)\ \&\ \bigwedge w_i\ne w_j\ \&\ \bigwedge \mathfrak{G}(u_i)\right), \]

where we have put

\[ \mathfrak{G}(u_i)\leftrightarrow (y_2\ldots y_t)\left(N_{\mathfrak{p}_2}(y_2)\ \&\ \cdots\ \&\ N_{\mathfrak{p}_t}(y_t) \to \mathfrak{H}(u_i,y_2,\ldots,y_m,x_1,\ldots,x_n)\right), \]

\[ \mathfrak{H}(y_1,\ldots,y_m,x_1,\ldots,x_n) \leftrightarrow \bigvee x_{\alpha_i}=g_i\vee\bigvee y_{\beta_j}=h_j. \]

Thus the matter has been reduced to bringing formulas \(\mathfrak{G}(u_i)\) of the form (8), containing a smaller number of universal quantifiers, into the desired form.

Received
9 III 1961

CITED LITERATURE

1. P. S. Novikov, Elements of Mathematical Logic, Moscow, 1959.
2. J. Peris, Fund. Math., 30, 257 (1938).
3. S. Jaśkowski, Fund. Math., 43, No. 1, 36 (1956).
4. A. I. Mal’tsev, UMN, 16, No. 3 (1961).