UDC 517.11

MATHEMATICS

I. L. BONDI

ON THE DECIDABILITY OR UNDECIDABILITY OF CERTAIN FORMAL-LOGICAL CALCULI

(Presented by Academician P. S. Novikov on 11 IV 1966)

In 1936 Church proved the undecidability of the predicate calculus \((^1)\). P. S. Novikov posed the question of the decidability or undecidability of formal-logical calculi obtained from the predicate calculus by deleting various sets of axioms and rules of inference.

Let \(S(\supset,\forall)\) denote the calculus with postulates for the symbols \(\supset\) and \(\forall\):

\[ \begin{aligned} &1)\quad A\supset(B\supset A);\\ &2)\quad (A\supset(B\supset C))\supset((A\supset B)\supset(A\supset C));\\ &3)\quad \frac{A,\ A\supset B}{B};\\ &4)\quad \forall x A(x)\supset A(t),\ \text{where } t \text{ does not occur bound in } \forall x A(x);\\ &5)\quad \frac{A\supset B(x)}{A\supset \forall x B(x)},\ \text{where } A \text{ does not contain } x . \end{aligned} \]

It is not hard to show that the calculus \(S(\supset,\forall)\) is undecidable.

To each formula \(E\) of the predicate calculus we assign a formula \(E'\) in the following way: \(E'\equiv \overline{E}\) for elementary formulas \(E\),

\[ (A\supset B)'\equiv A'\supset B',\quad (A\&B)'\equiv A'\supset \overline{B'},\quad (A\vee B)'\equiv \overline{A'}\supset B',\quad (\overline A)'\equiv \overline{A'}, \]

\[ (\exists xA(x))'\equiv \overline{\forall xA'(x)},\quad (\forall xA(x))'\equiv \forall xA'(x). \]

If \(S'\) is a calculus with transformation rules and postulates for the symbols \(\supset\), \(-\), and \(\forall\), then for the provability of \(E\) in the predicate calculus it is necessary and sufficient that the corresponding formula \(E'\) be provable in \(S'\). Thus the calculus \(S'\) is undecidable.

Next, to each formula \(E\) of the calculus \(S'\) we assign a formula \(E^0\) in the following way: \(E^0\equiv \overline E\) for elementary formulas \(E\),

\[ (A\supset B)^0\equiv \overline{A^0}\supset B^0,\quad (\overline A)^0\equiv \overline{A^0},\quad (\forall xA(x))^0\equiv \overline{\forall xA^0(x)}. \]

If \(S^0\) is a calculus with transformation rules for the symbols \(\supset\), \(-\), and \(\forall\), with postulates for the symbols \(\supset\), \(\forall\), and with the axiom

\[ (A\supset B)\supset((A\supset \overline B)\supset \overline A), \]

then for the provability of the formula \(E\) in the calculus \(S'\) it is necessary and sufficient that the corresponding formula \(E^0\) be provable in \(S^0\). Consequently, the calculus \(S^0\) is undecidable.

Let \(S^*\) be the calculus obtained from the calculus \(S^0\) by adding 1) the symbol \(L\) to the alphabet; 2) the clause “\(L\) is a formula” to the basic clauses of the definition of a formula; 3) the axioms \(\overline L\) and \(\overline A\supset(A\supset L)\). To each formula \(E\) of the calculus \(S^*\) we assign a formula \(E^*\), replacing all occurrences of the symbol \(L\) in \(E\) by the formula \(\mathcal A\supset \mathcal A\), where \(\mathcal A\) is some propositional letter. It can be shown that from the provability of a formula \(E\) in \(S^*\) there follows the provability of the corresponding formula \(E^*\) in \(S^0\). Therefore the formulas of the calculus \(S^0\) are provable in \(S^0\) if and only if they are provable in \(S^*\), and consequently the calculus \(S^*\) is undecidable.

Next, to each formula \(E\) of the calculus \(S^*\) we assign a formula \(E^+\) in the following way: \(E^+\equiv E\) for elementary formulas \(E\),

\[ (A\supset B)^+\equiv A^+\supset B^+,\quad (\overline A)^+\equiv A^+\supset L,\quad (\forall xA(x))^+\equiv \forall xA^+(x). \]

If \(S^+\) is the calculus obtained from the calculus \(S^*\) by deleting the axioms \(\overline L\), \(\overline A\supset(A\supset L)\), and

\[ (A\supset B)\supset((A\supset \overline B)\supset \overline A), \]

then for the provability of the formula \(E\) in \(S^*\) it is necessary and sufficient that the corresponding formula

\(E^+\) was provable in \(S^+\). Thus, the calculus \(S^+\) is undecidable, and consequently the calculus \(S(\supset,\ \forall)\), which differs from \(S^+\) only in the rules for formation of formulas, is also undecidable.

If by \(S(\supset,\ \exists)\) we denote the calculus with postulates for the symbols \(\supset\) and \(\exists\), then \(S(\supset,\ \exists)\) is also undecidable. Moreover, every calculus obtained from the calculus \(S(\supset,\ \forall)\) (or \(S(\supset,\ \exists)\)) by adding an arbitrary set from among the remaining postulates of the predicate calculus is undecidable.

However, if from the predicate calculus one deletes, one at a time, a single postulate for the symbol \(\supset\), then each of the three calculi obtained in this way is decidable. Moreover, if from the predicate calculus one deletes, one at a time, two postulates: one for the symbol \(\forall\), the other for the symbol \(\exists\), then again each of the four calculi obtained in this way turns out to be decidable.

Orsk State Pedagogical Institute
named after T. G. Shevchenko

Received
1 IV 1966

REFERENCES

1. S. Kleene, Introduction to Metamathematics, IL, 1957.