UDC 517.11

MATHEMATICS

Yu. Sh. GUREVICH

THE DECISION PROBLEM

FOR THE NARROW PREDICATE CALCULUS

(Presented by Academician A. I. Mal’cev on 1 XI 1965)

Let \(\Phi\) be a class of formulas. We shall say that \(\Phi\) is decidable if the problems of recognizing satisfiability and finite satisfiability of formulas of the class \(\Phi\) are algorithmically decidable. We shall say that \(\Phi\) is a reduction class if there exists an algorithm which, to every formula \(\alpha\) of the narrow predicate calculus with equality, assigns such a formula \(\beta \in \Phi\) that \(\alpha\) and \(\beta\) are simultaneously satisfiable or unsatisfiable and simultaneously satisfiable or unsatisfiable on finite models.

In \((^1)\) a summary is given of results on the decision problem. The corollaries formulated below follow from these results and from the theorem of the present article. Here \(F\) everywhere is the symbol of a binary predicate, and \(M\) denotes a quantifier-free formula.

Theorem. The class of formulas of the NPC without equality of the form

\[ \forall x \exists u \forall y \exists z_1 \ldots z_n M(F; x,u,y,z_1,\ldots,z_n) \tag{1} \]

is a reduction class.

Let \(\Pi\) be some set of words in the alphabet \(\{\forall,\exists\}\), and let \(\sigma\) be a collection of predicate symbols. By \(\Phi(\Pi,\sigma)\) we denote the class of all formulas of the NPC without equality of the form

\[ Q_1x_1 \ldots Q_nx_n M(\sigma; x_1,\ldots,x_n), \]

where \(Q_1 \ldots Q_n \in \Pi\). By \(\Phi^*(\Pi,\sigma)\) we denote the corresponding class of formulas of the NPC with equality.

Corollary 1. Either \(\Phi(\Pi,\sigma)\) is decidable, or it is a reduction class. The same also applies to \(\Phi^*(\Pi,\sigma)\).

Corollary 2. \(\Phi(\Pi,\sigma)\) is decidable if and only if \(\Phi^*(\Pi,\sigma)\) is decidable.

Corollary 3. Let

\[ \Pi_1=\{\exists^m\forall^n \mid m,n=0,1,\ldots\}, \qquad \Pi_2=\{\exists^m\forall^2\exists^n \mid m,n=0,1,\ldots\}. \]

\(\Phi(\Pi,\sigma)\) is decidable if and only if at least one of the following three possibilities holds:

a) \(\sigma\) contains only symbols of unary predicates;
b) \(\Pi \subseteq \Pi_1 \cup \Pi_2\);
c) \(\sigma\) and \(\Pi \setminus (\Pi_1 \cup \Pi_2)\) are finite.

Corollary 4. If \(\Phi^*(\Pi,\sigma)\) is decidable, then, with the exception of a finite number of formulas, satisfiability for formulas of \(\Phi^*(\Pi,\sigma)\) coincides with satisfiability on finite models.

Remark. The indicated corollaries for the case of infinite \(\sigma\) are given in the works of a group of American mathematicians headed by Wang Hao.

We outline the proof of the theorem. Let \(i=\varepsilon(i)+2\delta(i)\) be the binary notation, \(i=0,1,2,3\), and let

\[ \varphi=\forall x \exists u \forall y \exists z_1 \ldots z_n (A_0.A_1,\ldots A_l.M) \]

be a formula of the form (1). Instead of \(Fab\) we shall write simply \(ab\).

\[ A_0=(\neg xx.yy \supset \neg uu.(xu\sim xy).(ux\sim yx)).z_1z_1. \]

Put \(f_0^i x \sim \neg xx.(-1)^{\varepsilon(i)}xu.(-1)^{\delta(i)}Ux\). In view of \(A_0\), \(f_0^i u\) may be regarded as an abbreviation for \(\neg uu.(-1)^{\varepsilon(i)}uz_1.(-1)^{\delta(i)}z_1u\).

\[ A_1=\bigl[\neg xx.\neg f_0^3x.f_0^3y \supset \neg uu.\neg f_0^3u. \bigwedge_{i=0}^{2}(f_0^i u\sim (-1)^{\varepsilon(i)}xy.(-1)^{\delta(i)}yx)\bigr].f_0^3z_2. \]

Put, for \(i=0,1,2\), \(f_1^i x \sim \neg xx.\neg f_0^3x.f_0^i u\). Then \(f_1^i u\), in view of \(A_1\), may be regarded as an abbreviation for \(\neg uu.\neg f_0^3u.(-1)^{\varepsilon(i)}uz_2.(-1)^{\delta(i)}z_2u\), and so on, so that in \(M\) we can use an already larger number of unary predicates. Then the theorem from \({}^{2}\) is applied.

The author expresses his gratitude to Academician A. I. Mal’cev for posing the problem.

Krasnoyarsk State
Pedagogical Institute

Received
28 X 1965

CITED LITERATURE

\({}^{1}\) V. F. Kostyrko, Algebra and Logic, 3, 5–6, 45 (1964). \({}^{2}\) Yu. Sh. Gurevich, DAN, 166, No. 5 (1966).