UDC 517.11

MATHEMATICS

L. L. TSINMAN

ON THE AXIOM OF COMPLETE INDUCTION

(Presented by Academician P. S. Novikov on 10 V 1966)

This article gives answers to some questions posed to the author by P. S. Novikov.

1. Let \(S\) be Kleene’s formal arithmetic system \(((^1), § 49)\), supplemented by primitive-recursive definitions.

From Gentzen’s result \((^2)\) it follows that for every formula provable in \(S\) one can construct another proof containing no more than one application of the induction axiom:

\[ \mathfrak{A}(0)\ \&\ \forall x\,(\mathfrak{A}(x)\to \mathfrak{A}(x'))\to \mathfrak{A}(y). \]

On the other hand, it is known \(((^1), § 79)\) that if in the system \(S\) the induction scheme is restricted by the requirement that \(\mathfrak{A}(x)\) contain no quantifiers or that (which in fact amounts to the same thing) the variable \(x\) in \(\mathfrak{A}(x)\) not occur free in the scope of any quantifier, then one obtains a new system (denote it by \(S^{(0)}\)), the consistency of which can be shown by elementary means; and this means that induction cannot be completely eliminated from proofs in \(S\), nor can it be retained with the indicated restrictions.

Question: can one nevertheless, in \(S\), restrict oneself to an induction scheme with “not very complicated” \(\mathfrak{A}(x)\)?

Let \(S^{(l)}\) be the formal system obtained from \(S\) as a result of the following restriction imposed on the induction scheme: the induction formula \(\mathfrak{A}(x)\) may contain no more than \(l\) quantifiers.

Theorem 1. For every natural number \(*\) \(l\) one can indicate a formula \(\mathfrak{B}\), provable in \(S\), but not provable in \(S^{(l)}\).

The proof of the theorem uses the method of regular classes proposed by P. S. Novikov \((^3)\). Namely, the validity of this theorem follows from the fact that for each natural number \(l\) one can construct in \(S^{(l)}\) a regularity class \(K^{(l)}\) with the following properties:

(a) every formula provable in \(S^{(l)}\) is contained in \(K^{(l)}\);

(b) one can indicate a formula \(\mathfrak{B}^{(l)}\), provable in \(S\), but not belonging to \(K^{(l)}\).

Remark 1. In fact the regularity classes \(K^{(l)}\) are constructed so that they possess a stronger property than (a). Namely, each class \(K^{(l)}\) contains exactly those formulas of the system \(S\) which either are (substantively) true and contain no more than \(l\) quantifiers, or can be obtained from these formulas by means of the rules of inference of the predicate calculus. And this, in turn, means that the union of all the classes \(K^{(l)}\) contains all formulas of \(S\) that are true under the interpretation (and only these formulas).

Remark 2. Theorem 1 is also valid for Kleene’s arithmetic system.

To show this, it suffices to verify that in the process of eliminating primitive-recursive definitions \(((^1), § 74)\) from formulas of \(S\) not belonging to \(K^{(l)}\), one obtains formulas that likewise do not belong to \(K^{(l)}\).

Remark 3. Theorem 1 is proved by classical means.

\[ \text{—} \]

\(*\) We shall also regard the number 0 as a natural number.

Apparently, it can also be proved constructively. But this theorem cannot be proved by elementary means, in view of Gödel’s second theorem.

1. In proving arithmetical theorems the following situation sometimes arises: certain assertions \(A(n)\) and \(B(n)\), taken separately, do not in any way yield to proof by the method of complete induction, whereas the stronger assertion \(A(n)\&B(n)\) is proved by this method without difficulty. Pólya \((^4)\) calls such a situation the “inventor’s paradox.”

A question arises: do such “paradoxical” assertions really exist?

Of course, this question can be posed in a more precise form, and an answer to it can be sought, only for arithmetic specified in the form of a system with an exactly defined concept of proof, for example for arithmetic specified as a formal system (of type \(S\)) or a “semiformal” system (one may regard as such arithmetic with a distinguished class of regularity in place of the class of provable formulas).

Denote by \(\widetilde K^{(l)}\) the class of formulas provable in the system \(S^{(l)}\). It was indicated above that \(\widetilde K^{(l)}\).

Theorem 2. For any natural numbers \(l\) and \(m\) \((m>1)\) one can specify formulas \(\mathfrak B^{(l)}_1(n),\ldots,\mathfrak B^{(l)}_m(n)\) of the system \(S^{(l)}\) such that the following conditions are fulfilled:

\[ \text{(1) the formula } \mathfrak B^{(l)}_1(0)\&\ldots\&\mathfrak B^{(l)}_m(0) \text{ belongs to } \widetilde K^{(l)}\bigl(K^{(l)}\bigr); \]

\[ \text{(2) the formula } \mathfrak B^{(l)}_1(n)\&\ldots\&\mathfrak B^{(l)}_m(n) \to \mathfrak B^{(l)}_1(n')\&\ldots\&\mathfrak B^{(l)}_m(n') \text{ belongs to } \widetilde K^{(l)}\bigl(K^{(l)}\bigr); \]

\[ \text{(3) but for every } i\ (i=1,2\ldots m) \text{ the formula } \mathfrak B^{(l)}_i(n)\to \mathfrak B^{(l)}_i(n') \text{ does not belong to } \widetilde K^{(l)}\bigl(K^l\bigr). \]

Conditions (1) and (2) mean that the formula \(\mathfrak B^{(l)}_1(n)\&\ldots\&\mathfrak B^{(l)}_m(n)\) can be obtained directly (i.e. by a single application at the last step) by induction from formulas provable (regular) in \(S^{(l)}\). At the same time, from condition (3) it follows that not one of the formulas \(\mathfrak B^{(l)}_i(n)\) \((i=1,2,\ldots m)\) can be obtained in a similar way.

Remark 4. Theorem 2 actually contains two separate assertions: for the classes \(\widetilde K^{(l)}\) and for the classes \(K^{(l)}\). Neither of these assertions is a consequence of the other.

1. Let \(\mathfrak B(x,y)\) be an arbitrary formula of the system \(S\), containing freely only the variables \(x\) and \(y\), and let \(B(x,y)\) be the predicate which it expresses under interpretation. Define the function \(\varepsilon_y B(x,y)\) as follows:

\[ \varepsilon_y B(x,y)= \begin{cases} \text{the least } y \text{ such that } B(x,y), & \text{if } (Ey)B(x,y);\\ 0, & \text{otherwise.} \end{cases} \]

Adjoin to the system \(S\) a new functional symbol (an \(\varepsilon\)-term), expressing this function, and the corresponding axiom (the \(\varepsilon\)-axiom).

The system obtained as a result of adding to \(S\bigl(S^{(l)}\bigr)\) all \(\varepsilon\)-terms and \(\varepsilon\)-axioms at once will be denoted by \(S_\varepsilon\bigl(S_\varepsilon^{(l)}\bigr)\).

It is known \(((^1), \S 74)\) that the new functional symbols and axioms introduced in this way are eliminable from \(S_\varepsilon\) into \(S\).

In the elimination, the induction axiom is also used.

Question: Is the induction axiom needed in full form in this process of elimination?

Theorem 3. For no natural number \(l\) are the \(\varepsilon\)-terms and \(\varepsilon\)-axioms eliminable from \(S_\varepsilon^{(l)}\) into \(S^{(l)}\).

Moscow State
Pedagogical Institute named after V. I. Lenin

Received
18 V 1966

CITED LITERATURE

1. C. K. Kleene, Introduction to Metamathematics, Moscow, 1957.
2. G. Gentzen, Arch. math. Logik u. Grundlagenforsch., 2, 1–3 (1954).
3. P. S. Novikov, DAN, 64, No. 4 (1949).
4. G. Pólya, How to Solve It, Moscow, 1959.