UDC 517.12

MATHEMATICS

N. V. BELYAKIN

ON THE COMPLETENESS OF ARITHMETIC

(Presented by Academician A. I. Mal’tsev on 26 X 1966)

In this note one axiomatic system of first-order arithmetic is considered. It is equivalent to ordinary classical arithmetic with the so-called rule of constructive infinite induction and therefore is not a formal system. The peculiarity of the proposed system consists in the fact that it does not explicitly contain the traditional logical rules, such as modus ponens, etc. The concept of derivability adopted in it essentially coincides with the concept of regularity, which was introduced in (¹).

As it turns out, in terms of regular formulas it is convenient to carry out a proof of the completeness of arithmetic. In this system every true formula has a derivation of height \(< \omega^2\). We note that the completeness fact (for the traditional variant of arithmetic) was earlier established by A. V. Kuznetsov (²).

For definiteness we shall adopt the formal arithmetical language described in (³). However, it will be convenient for us to deal at once with formulas reduced to a special form. Namely, we shall assume that they contain no implication sign, and that negation may apply only to elementary subformulas. Using the well-known parallelism between quantifiers and the connectives \(\&,\ \vee\), we shall say that all formulas are built from elementary formulas and their negations by means of the operations of addition \((\vee,\ \exists)\) and multiplication \((\&,\ \forall)\).

Let the formula \(\mathfrak A\) be a sum, i.e. have the form \(\mathfrak A_1 \vee \mathfrak A_2\) or \((\exists x)\mathfrak A_1(x)\). Then the subformulas \(\mathfrak A_1,\ \mathfrak A_2\) (respectively \(\mathfrak A_1(k),\ k=0,1,\ldots\)) are naturally called its terms. It is possible that some of the terms will in turn be sums; then we shall also regard their terms as terms of the formula \(\mathfrak A\) itself, etc. Ultimately we arrive at such terms which are no longer sums and which we shall call simple terms of the formula \(\mathfrak A\). We further agree that if a formula is not a sum, then it itself will be its only simple term. Similarly, considering the operations \(\&,\ \forall\), we define simple factors. It is clear that the sequence of simple terms (factors) for an arbitrary formula may be either finite or countable; in the latter case it can be enumerated with the aid of a suitable algorithm.

We now pass to the description of the deductive apparatus of our system. True elementary formulas, and also the negations of false elementary formulas, will be called trivially true.* By definition, a formula is considered an axiom if it contains a trivially true simple term. Obviously, the set of axioms is algorithmically enumerable.

The proposed system has only one rule of inference, which looks as follows. Let \(\mathfrak A\) be some formula and \(\mathfrak B\) any one of its simple terms. Form all possible formulas of the form \(\mathfrak C_{\mathfrak B}^{\,i} \vee \mathfrak A\), where \(\mathfrak C_{\mathfrak B}^{\,i}\) are the simple factors of the formula \(\mathfrak B\). From the totality of all such

* What is meant are elementary formulas containing no variables.

formulas, as from premises, \(\mathfrak A\) is derivable. In other words, a finite or infinite figure

\[ \frac{\ldots,\ \mathfrak C_{\mathfrak B}^{\,i}\vee \mathfrak A,\ \ldots}{\mathfrak A}, \]

by definition, is what is usually called an application of an inference rule. In this figure, above the line all the premises are assumed to have been written out, i.e. \(\mathfrak C_{\mathfrak B}^{\,i}\) ranges over the totality of all simple multipliers of the formula \(\mathfrak B\). We shall say that the passage from the conclusion \(\mathfrak A\) to the premises is effected by splitting the summand \(\mathfrak B\). It is clear that if all premises are true, then the conclusion is also true, and conversely (truth is understood in the usual classical sense). The number of premises in a given application may be either any finite number or countable, depending on \(\mathfrak A\) and \(\mathfrak B\). It is possible that there will be only one premise—when an elementary formula or its negation is subjected to splitting. In any case, the set of all premises can be effectively enumerated.

The notions of a derivable formula and of a derivation tree are defined in the usual way \((^4)\), so that we shall not repeat the corresponding definitions. One must only bear in mind that the derivation tree, generally speaking, will be infinite. Taking this into account, we shall require, by definition, that every derivation in our system be an algorithmically generated tree. Such a restriction corresponds to the constructivity condition that is usually imposed on the rule of infinite induction \((^2,^4)\). Let us note that without this condition derivability would differ little from classical truth, and the problem of completeness (for first-order arithmetic) would at once become trivial.

We now give some heuristic arguments by virtue of which the given system turns out to be complete. Let \(\mathfrak A\) be a closed true formula; then some of its simple summands must also be true. Denote by \(\rho(\mathfrak A)\) the minimum of the logical depths of the true summands of \(\mathfrak A\). This quantity may serve as a natural measure of the complexity of true formulas, since it agrees well with the notion of derivability in our system. Indeed, axioms are, in this sense, the simplest true formulas—for them \(\rho(\mathfrak A)=0^*\). Further, in any application of the inference rule all simple summands of the conclusion will also be simple summands of every premise. Therefore the premises, in any case, are no more complex than the conclusion. However, they may also turn out to be simpler than the conclusion. This will occur when the conclusion in the given application has complexity \(\rho>0\), and the summand being split has precisely depth \(\rho\).

Using only the circumstance just noted, one can prove the following lemma.

Lemma. Let \(\mathfrak A_0,\mathfrak A_1,\ldots\) be a sequence of true formulas in which \(\mathfrak A_{j+1}\) is obtained as one of the premises by splitting some summand of \(\mathfrak A_j\). Suppose that any simple summand of any formula \(\mathfrak A_i\) in the process of constructing this sequence is eventually split. Then all the \(\mathfrak A_i\), beginning with some point, are axioms.

Indeed, \(\rho(\mathfrak A_{j+1})\leqslant \rho(\mathfrak A_j)\), and if \(\rho(\mathfrak A_j)>0\), then there is an \(k>j\) such that \(\rho(\mathfrak A_k)<\rho(\mathfrak A_j)\). The latter is true because all simple summands of \(\mathfrak A_j\) will be split in the further construction of the sequence. In particular, at some step a true summand of depth \(\rho(\mathfrak A_j)\) will be subjected to splitting. Thus the complexity of the formulas \(\mathfrak A_i\) gradually decreases until it reaches zero, which was required to be proved.

Let us now take an arbitrary true formula \(\mathfrak A\) and split in it some (simple) summand. In each premise obtained we again split one of the summands, and so on. It is assumed that we are guided—

* To the negation of an elementary formula we assign depth zero.

we use some algorithm which, in each already obtained formula, singles out a term for further splitting. As a result, a certain algorithmically generated tree arises. The procedure described can be organized so that, for each chain of this tree, the condition of the lemma will be satisfied. It remains only to cut off all chains at the appropriate places, and we obtain a proof tree for the formula \(\mathfrak A\). Let us note that for the last operation there is also a corresponding algorithm.

Thus, all true formulas are derivable. For a more precise formulation of the result of this note, we introduce one more concept.

Definition. A proof tree has rank zero if its height is finite. A proof tree has rank \(n+1\) if there exists an \(l\) such that all subtrees beginning at height \(l\) have rank \(\leq n\).

If the heights of trees are estimated in the usual way by means of transfinite numbers, then a tree of rank \(n\) has height \(< \omega \cdot (n+1)\).

Theorem. A true formula of depth \(n\) has a proof of rank \(n\).

Institute of Mathematics
Siberian Branch of the Academy of Sciences of the USSR

Received
20 IX 1966

REFERENCES

1. P. S. Novikov, Matem. sborn., 12(54), 231 (1943).
2. A. V. Kuznetsov, UMN, 12, 4, 218 (1957).
3. S. K. Kleene, Introduction to Metamathematics, IL, 1957.
4. K. Schütte, Beweistheorie, 1961.