UDC 517.11

MATHEMATICS

L. L. TSINMAN

ON SOME ALGORITHMS IN A FORMAL ARITHMETICAL SYSTEM

(Presented by Academician P. S. Novikov on 17 IV 1969)

In this paper we shall consider arithmetic in the form of a formal calculus \(S\), in whose signature there are two predicate symbols \(=\) and \(<\), one individual symbol \(0\), the functional symbol \({}'\), and an infinite set of functional symbols for representing all primitive-recursive functions. The logical postulates of the formal calculus under consideration are the postulates of the classical predicate calculus. The nonlogical postulates of our system are, as usual, axioms characterizing the indicated symbols of the signature, including all defining equalities for primitive-recursive functions, and one rule of inference—the rule of complete mathematical induction\(^*\):

\[ \frac{A(0),\ A(x)\supset A(x')}{A(x)}. \tag{1} \]

Let us note that the axioms defining the order predicate may be chosen in various ways. In doing so, if the inference rule (1) is removed from the list of postulates, then the order axioms, generally speaking, may be supplemented by new independent order axioms. However, one can indicate a system of order axioms which, together with the axiom scheme of equality \(x=y\supset (A(x)\supset A(y))\) and without rule (1), is complete in the class of formulas containing only the following nonlogical symbols: \(=,<,0,{}'\). This system of axioms is considered in \((^1)\). Together with the indicated axiom scheme of equality, it consists of the following axioms:

\[ x=y\supset (A(x)\supset A(y)), \]

\[ x<y\supset (y<z\supset x<z), \]

\[ x<x', \]

\[ x<y\supset \overline{y<x'}, \]

\[ \overline{x<0}, \]

\[ \overline{x=0}\supset \exists y\,(y'=x). \]

For our purpose it is convenient to assume that precisely this system of axioms is present among the nonlogical postulates of the formal calculus \(S\).

We shall be interested in the question of which formulas of our arithmetic can be derived without rule (1), or with the use of this rule only at the very end of the derivation.

For this purpose let us define a sequence of classes of arithmetical formulas \(K_0, K_1, K_2,\ldots\).

\(K_0\) is the class of all formulas derivable in the formal system \(S\) without rule (1).

Suppose we have already defined the class of formulas \(K_n\) for some integer nonnegative \(n\). We now define the class of formulas \(K_{n+1}\) in the following way—

\(^*\) It is known that it is immaterial in what form mathematical induction is represented in the formal calculus: in the form of the written rule, or in the form of the axiom scheme

\[ A(0)\ \&\ \forall x\,(A(x)\supset A(x'))\supset A(x). \]

with the following rule: 1) every formula of the class \(K_n\) belongs to the class \(K_{n+1}\); 2) if, for some formula \(A(x)\), the formulas \(A(0)\) and \(A(x) \supset A(x')\) belong to the class \(K_n\), then the formula \(A(x)\) belongs to the class \(K_{n+1}\); 3) the class \(K_{n+1}\) contains no other formulas.

Thus, for every nonnegative integer \(n\), a class of formulas \(K_n\) is defined. Let us also form the class

\[ K=\bigcup_{n=1}^{\infty} K_n . \]

It is clear that the class \(K_n\) consists of precisely those formulas for which, in the system \(S\), one can construct a derivation in which applications of the logical rules of inference precede all applications of rule (1), and the number of applications of this rule does not exceed \(n\). Let us note that if two formulas are equivalent in the predicate calculus and one of them belongs to the class \(K_n\), then the other formula also belongs to the same class.

The following facts hold.

I. For every \(n\) one can specify a formula belonging to the class \(K_{n+1}\), but not belonging to the class \(K_n\).

II. One can specify a formula derivable in the system \(S\), but not belonging to the class \(K\).

III. For every \(n\) one can specify an algorithm that tests, for quantifier-free formulas of the system \(S\), whether they belong to the class \(K_n\).

IV. There exists an algorithm that tests, for quantifier-free formulas of the system \(S\), whether they belong to the class \(K\).

Commentary. As G. Gentzen showed \((^2)\), for every derivable arithmetical formula one can construct a derivation in which rule (1) is used only once. In our notation this means that if the class of formulas \(K_1\) is augmented by all possible formulas derivable in the predicate calculus from formulas of this class, then we obtain the whole class of formulas derivable in arithmetic. On the other hand, it follows from the results formulated above that not for every formula derivable in arithmetic can one construct a derivation using rule (1) any number of times, but only at the end of the derivation.

Results I–IV remain valid if, in constructing arithmetic, instead of rule (1), one introduces into the system, for each natural number \(l\), the rule of simultaneous induction on \(l\) variables:

\[ \frac{ \begin{gathered} A(0,0,\ldots,0);\ A(x_1,x_2,\ldots,x_l)\supset A(x'_1,x_2,\ldots,x_l),\ldots \\ \ldots,\ A(x_1,x_2,\ldots,x_l)\supset A(x_1,x_2,\ldots,x'_l) \end{gathered} }{ A(x_1,x_2,\ldots,x_l) } \tag{2} \]

In this case, it is natural to assign to the class \(K_{n+1}\) all those formulas which can be obtained by one application of one of the rules (2) to formulas belonging to the class \(K_n\).

The formulated results are a generalization of a result of P. S. Novikov, who in paper \((^3)\) proved the existence of an algorithm that tests, for quantifier-free formulas of arithmetic, whether they are derivable without induction or not (in our notation, this is an algorithm testing, for quantifier-free formulas, membership in the class \(K_0\)). In the same paper P. S. Novikov indicated that for the class of arithmetical formulas containing at least one existential quantifier in prenex form, such an algorithm can no longer exist.

In proving results I–IV, the method of regular formulas developed by P. S. Novikov in paper \((^4)\), and the constructions built by him in paper \((^3)\), are used.

Received
26 III 1969

REFERENCES

1. D. Hilbert, P. Bernays, Grundlagen der Mathematik, 1, 1934, p. 263.
2. G. Gentzen, Arch. math. Logik und Grundlagenforsch., 2, No. 1–2, 27 (1954).
3. P. S. Novikov, DAN, 64, No. 4, 457 (1949).
4. P. S. Novikov, DAN, 64, No. 3, 293 (1949).