UDC 517.11

MATHEMATICS

Yu. Sh. GUREVICH

ON THE DECISION PROBLEM

FOR THE PURE NARROW PREDICATE CALCULUS

(Presented by Academician A. I. Mal’cev on 26 V 1965)

1. In (¹) a summary is given of results on the reduction of the decision problem for satisfiability for the pure narrow predicate calculus. It is indicated there that, if one excludes classes of formulas of the form

\[ \mathfrak{G}^{a}\mathfrak{G}^{b}\mathfrak{G}^{n}M(F_1,\ldots,F_c), \]

containing not only unary predicates, where \(a,b,c\) are bounded in the given class and \(b>0\), then for any of the remaining classes of prenex formulas without free variables and with a fixed set of predicates the problem is solved.

Theorem. Let \(\sigma\) contain one binary and \((9+k)\) unary predicates, where \(2^k \ge m^*\) and \(m^*\) is the number of states of a universal Turing machine. The sets of refutable and finitely satisfiable \(\sigma\)-formulas of the form \(\forall \exists \forall \& \mathfrak{G}^n\) are recursively inseparable.

The present paper is devoted to the proof of this theorem.

1. By a Turing machine we shall here mean the variant of such machines described in (²). \(M^*\) will further denote a universal Turing machine. Let \(X_1\) (respectively \(X_2\)) be the set of those \(n\) such that \(M^*\) halts from the tape (respectively cycles), if in the initial situation

\[ \overset{n+1}{\overbrace{11\ldots100\ldots}} \]

\(M^*\) scans the leftmost cell. \(X_1\) and \(X_2\) are recursively inseparable.

1. In (²), for each Turing machine \(M\) there is constructed a formula \(\alpha_M(x,x',y)\), containing binary predicates \(S,K\), and \(H\) and a certain number of unary ones, such that \(M\), scanning at the zero moment the zero cell of the empty tape, eventually halts from the tape (respectively cycles) if and only if \(\forall xy\,\alpha_M(x,x+1,y)\cdot Z0\) is unsatisfiable (respectively satisfiable by periodic predicates) in the domain of natural numbers. Here \(Zy\) is interpreted as: \(y\) is zero, and \(Syx\) as: at moment \(y\) the cell numbered \(x\) is nonempty. In \(\alpha_{M^*}\) we replace \((Zy \supset \neg Syx')\) by \((Zy \supset (Syx' \supset Syx))\). We obtain the formula \(\alpha(x,x',y)\).

Lemma 1. \(n \in \overline{X}_1\) (respectively \(n \in X_2\)) if and only if
\(\forall xy\,\alpha(x,x+1,y)\cdot Z0\cdot S0n\cdot \neg S0(n+1)\) is satisfiable (respectively satisfiable by periodic predicates) in the domain of natural numbers.

1. Let \(\beta(x,x',y)\) be the conjunction of the following five formulas:

4.1. \(\neg Ax\cdot \neg Ay\cdot Cxy \supset Dx'y\).

4.2. \(Dyx \supset \neg Ax'\cdot Cyx'\).

4.3. \(Ay\cdot Cyx \supset Ax'\).

4.4. \(Ax\cdot Bx\cdot Zy \supset Syx\cdot \neg Syx'\).

4.5. \(Bx \supset Bx'\).

Let

\[ \begin{aligned} \varphi_n = {}& \forall x\,\mathfrak{G}x'\,\forall y\bigl(\alpha(x,x',y)\cdot\beta(x,x',y)\bigr)\ \& \\ & {}\&\,\mathfrak{G}x_0x_1\ldots x_n \bigl[Ax_0\cdot \bigwedge_{i>0}\neg Ax_i\cdot \bigwedge_{i<n}Cx_i x_{i+1}\cdot \\ & \qquad\qquad\qquad\qquad \cdot\bigwedge_{1+i\ne j}\neg Cx_i x_j\cdot Zx_n\cdot Bx_n\bigr]. \end{aligned} \]

Lemma 2. \(\varphi = [\forall x y \alpha(x, x+1, y).\, Z0.\, Son.\, \neg So(n+1)]\) is satisfiable (respectively, finitely satisfiable by periodic predicates) in the domain of natural numbers if and only if \(\varphi_n\) is satisfiable (respectively, finitely satisfiable).

Let us show how a model for \(\varphi_n\) is constructed if there exists a suitable model \(\mathfrak M\) for \(\varphi\). Let
\[ |\mathfrak M_i|=\{(i,k)\mid k=0,1,\ldots\} \]
and let \((i,k)\leftrightarrow k\) be an isomorphism of \(\mathfrak M_i\) and \(\mathfrak M\), \(i=0,\ldots,n\).

For \(i\ne j\) we put
\[ \neg S(i,k)(j,l),\quad \neg K(i,k)(j,l),\quad \neg H(i,k)(j,l). \]
Further, we put:
\[ \begin{aligned} A(i,k)&\quad \text{is equivalent to } i=k,\\ B(i,k)&\quad \text{is equivalent to } i=n,\\ C(i,k)(j,l)&\quad \text{is equivalent to } j=i+1 \text{ and } k=l\le i,\\ D(i,k)(j,l)&\quad \text{is equivalent to } j=i+1 \text{ and } k=l+1\le i. \end{aligned} \]

The pairs \((i,k)\), with the relations defined, form a model for \(\varphi_n\). If, conversely, there is a model \(\mathfrak M\) for \(\varphi_n\), then, without loss of generality, we may assume that \(|\mathfrak M|\) consists of pairs \((i,k)\), where \(i=0,\ldots,n\) and \(k=0,1,\ldots\). The element \((i,0)\) plays the role of \(x_i\) from \(\varphi_n\). By induction on \(i\), \(A(i,i)\) is proved. From \(A(n,n)\) and \(B(n,0)\), by means of 4.5 and 4.4, one derives \(S(n,0)(n,n)\) and \(\neg S(n,0)(n,n+1)\). The elements \((n,k)\), \(k=0,1,\ldots\), with the corresponding relations form a suitable model for \(\varphi\).

1. Let \(\mathfrak M\) be a model for \(\varphi_n\). Replace each element \(a\) of \(\mathfrak M\) by eleven new elements \(a^0,\ldots,a^{10}\). Let \(h\) be any unary predicate from \(\varphi_n\); if \(ha\) held (respectively, \(\neg ha\)), put \(ha^i\) (respectively, \(\neg ha^i\)), \(i=0,\ldots,10\). We now define on the set
   \[ \{a^i\mid a\in\mathfrak M,\ i=0,\ldots,10\} \]
   a new predicate \(Fxy\) (or simply \(xy\)):

\[ \text{5.1. }\quad Cab\to \bigwedge_i (a^i b^0 . b^i a^2). b^i a^{10}. \]

\[ \text{5.2. }\quad Dab\to \bigwedge_i (a^i b^1 . b^i a^3). \]

5.3; 5.4; 5.5—analogously to 5.1 and 5.2, but for \(S\), \(K\), and \(H\), respectively.

5.6. \(a^i b^j\) holds only in the case when this follows from 5.1—5.5.

As a result we obtain a model for the formula \(\psi_n\) defined below.

1. Let \(\gamma(x,x',y)\) be the conjunction of the following formulas:

\[ \text{6.1. }\quad \bigvee_{i=0}^{10} f^i x\ .\ \bigwedge_{i\ne j}\neg(f^i x . f^j x). \]

\[ \text{6.2. }\quad \bigwedge_{i<10}(f^i x\sim f^{i+1}x'). \]

\[ \text{6.3. }\quad \bigwedge_{h,\ i<10} f^i x \supset (hx\sim hx') \]
(here \(h\) ranges over the unary predicates from \(\varphi_n\)).

\[ \text{6.4. }\quad \bigwedge_{i<10}\,[\,f^i x . (f^0 y\vee f^2 y)\supset (xy\sim x'y)\,]\ .\ [\,f^{10}y . f^0x\supset (yx\sim x'y)\,]. \]

6.5—6.8. Formulas concerning \(D,S,K\), and \(H\), respectively, just as 6.4 concerns \(C\).

\[ \text{6.9. }\quad f^{10}x . f^1y . \neg Ax . \neg Ay . yx\subset x'y. \]

6.10 and thereafter—formulas concerning 4.2, \(\ldots\), 4.5 and the conjuncts from \(\alpha(x,x',y)\), just as 6.9 concerns 4.1.

Let
\[ \psi_n=\forall x\exists x'\forall y\ \gamma(x,x',y)\ \& \]
\[ \&\exists x_0x_1\ldots x_n\,[\,\bigwedge_i f^0x_i . Ax_0 . \bigwedge_{i>0}\neg Ax_i . \]
\[ \cdot \bigwedge_{i<n}x_ix_{i+1} . \bigwedge_{1+i\ne j}\neg x_ix_j . Zx_n . Bx_n\,]. \]

Lemma 3. \(\varphi_n\) is satisfiable (respectively, finitely satisfiable) if and only if \(\psi_n\) is satisfiable (respectively, finitely satisfiable).

1. \(\psi_n\) contains one binary predicate and \(m^* + 17\) unary ones. The individual groups of unary predicates here satisfy a property similar to 6, 1, which makes it possible to reduce the necessary number of unary predicates to \(9 + k\), where \(2^k \geq m^*\).

Thus, the assertion of the theorem follows from Lemmas 1, 2, and 3.

I express my gratitude to Academician A. I. Mal'tsev for posing the problem.

Ural State University
named after A. M. Gorky

Received
21 V 1965

REFERENCES

1. V. F. Kostyrko, Algebra and Logic, 3, no. 5–6, 45 (1964).
2. J. R. Buchi, Math. Ann., 148, 201 (1962).