UDC 517.1+502.16

MATHEMATICS

A. G. DRAGALIN

TRANSFINITE COMPLETIONS OF CONSTRUCTIVE ARITHMETIC CALCULUS

(Presented by Academician P. S. Novikov, 21 IV 1969)

The well-known Gödel incompleteness theorem (see, for example, (¹), pp. 188 and 278) asserts that an axiomatic theory with a recursively enumerable set of axioms and containing constructive arithmetic calculus (in other terminology, intuitionistic arithmetic calculus, (¹), p. 94) is necessarily incomplete. Therefore, in order to obtain axiomatic theories that are complete with respect to some notion of truth and are extensions of constructive arithmetic calculus, one must consider the so-called semiformal theories, in which the notion of derivation is no longer a decidable notion.

By the calculus \(Z\) we shall mean the ordinary constructive arithmetic calculus (the intuitionistic system, (¹), p. 94), supplemented by terms for all primitive-recursive functions and by the corresponding primitive-recursive schemes as axioms. By a formula we shall everywhere mean a formula in the syntax of the calculus \(Z\). Every calculus considered in this note is specified by a recursively enumerable set \(A\) of closed formulas, called the axioms of the calculus. A formula \(\Phi\) is derivable in \(A\) if \(\Phi\) is derivable from a finite list of axioms of \(A\) according to the rules of constructive predicate calculus. A calculus \(A\) is an extension of a calculus \(B\) if every axiom of \(B\) is derivable in \(A\). In particular, classical arithmetic calculus \(Z^0\) is an extension of \(Z\), obtained by adding to the set of axioms \(Z\) all closed formulas of the form \(\forall x_1 \ldots x_k(\Phi \vee \neg \Phi)\).

We consider two methods of completing a calculus \(A\):

1. For every calculus \(B\) one may consider the calculus \(B^*\), obtained by adding to \(B\), as axioms, all closed formulas of the form (in the notation of (²), p. 274):

\[ (\forall x)\operatorname{Pr}_{\alpha}(\overline{\Phi}(\overline{x})) \to (\forall x)\Phi(x). \]

Each such axiom says that if, for every natural \(n\), the closed formula \(\Phi(\overline{n})\) is derivable in \(B\), then the formula \(\forall x\Phi(x)\) is also true. This method of extending \(B\) is Definition 2.16 (iii) of (²). To obtain a completion of \(A\), one should, roughly speaking, starting from \(A\), repeat this method of extension a transfinite number of times over all constructive ordinals. More precisely, as was shown by Feferman ((²), Theorems 3.3 and 3.8), for a given calculus \(A\) there can be constructed a primitive-recursive function \(F\) which transforms every constructive ordinal number \(d\), \(d \in O\) (\(d\) is a constructive ordinal in Kleene’s system \(S_3\) (³)), into the number of a recursively enumerable set of closed formulas \(A_d\). Here:

\[ \text{(a)}\quad A_1 = A; \]

\[ \text{(b)}\quad A_{2^d} = A_d^*; \]

\[ \text{(c)}\quad A_{3\cdot 5^l} = \bigcup_{b <_O 3\cdot 5^l} A_b. \]

Moreover, the function \(F\) can be constructed verifiably (\((^{2})\), Theorem 3.8), i.e., in such a way that the formalized analogues of the equalities (a)—(c) are derivable in \(Z\). Such a function \(F\) we shall call a transfinite progression based on \(A\), and the calculi \(A_d\) we shall call the members of \(F\). We shall call a formula \(\Phi\) derivable in the progression \(F\) if there exists a member \(A_d\) of the progression \(F\) such that \(\Phi\) is derivable in the calculus \(A_d\).

1. The second method of completing \(A\) consists, roughly speaking, in extending the number of rules of inference of \(A\) by adding to \(A\) a certain non-elementary rule of inference—the constructive Carnap rule (the restricted \(\omega\)-rule in the terminology of \((^{4})\)). The precise formulations are as follows.

Let \(A\) be a calculus. We introduce inductively the notion of an \(A\chi\)-derivation of a formula \(\Phi\):

a) if \(p\) is a derivation of \(\Phi\) in the calculus \(A\), then \([0,\Phi,p]\) is an \(A\chi\)-derivation of \(\Phi\);

b) if \(p_1,\ldots,p_n\) are \(A\chi\)-derivations of the formulas \(\Phi_1,\ldots,\Phi_n\), respectively, and \(p\) is a derivation of \(\Phi\) in the calculus \(A\) from the formulas \(\Phi_1,\ldots,\Phi_n\) with fixed variables (\((^{1})\), p. 89), then \([1,\Phi,p,p_1,\ldots,p_n]\) is an \(A\chi\)-derivation of \(\Phi\);

c) if \(e\) is a natural number such that for every \(n\) the partial recursive function \(\{e\}\) is defined at \(n\) and yields an \(A\chi\)-derivation of the closed formula \(\Phi(\bar n)\), then \([2,\forall x\Phi(x),e]\) is an \(A\chi\)-derivation of the formula \(\Phi\).

In this definition it is assumed, of course, that formulas and tuples of natural numbers are encoded by natural numbers in some standard way, so that \(A\chi\)-derivations may also be regarded as natural numbers of a special kind. The definition just given, like the definition of constructive ordinals, is a transfinite inductive definition \((^{3})\) and, from the constructive point of view, is not reducible to an explicit definition.

We shall say that a formula \(\Phi\) is derivable in the theory \(A\chi\) if an \(A\chi\)-derivation of the formula \(\Phi\) can be constructed.

The following theorem asserts that the two methods of completion are equivalent.

Theorem 1. Let \(A\) be a calculus and let \(F\) be a transfinite progression based on \(A\). Then primitive recursive functions \(G_0\) and \(G_1\) can be constructed such that:

a) if \(p\) is an \(A\chi\)-derivation of \(\Phi\), then \(d=G_0(p)\) is a constructive ordinal and \(\Phi\) is derivable in \(A_d\);

b) if \(d\) is a constructive ordinal such that the formula \(\Phi\) is derivable in the member \(A_d\) of the progression, then \(G_1(\Phi,d)\) is an \(A\chi\)-derivation of the formula \(\Phi\).

This theorem is a generalization of Feferman’s Theorems 5.10 and 5.11 \((^{2})\) to the case of constructive logic. The proof of Theorem 1 proceeds in general analogously to the proof of the theorems just mentioned \((^{2})\); however, the key Theorem 4.9 \((^{2})\) is proved only in a weakened form, namely (in the notation of \((^{2})\)): binary primitive recursive functions can be constructed

\[ h_1=H_1(b,\Phi),\qquad h=H(b,\Phi),\qquad q_1=Q_1(b,\Phi) \]

such that for every \(b\in O\), \(\vdash_{A_1}\Phi\) we have:

I. \(h,h_1\in O,\ b<_0 h,\ h_1=h+_0 1_0\)

II. \(\operatorname{Pr} f_{A_1}[\operatorname{Pr}(\bar h_1,\operatorname{Pr}(\bar h;\Phi));q_1]\).

At the cost of a certain complication of the reasoning, this form of 4.9 makes it possible to establish Theorem 5.2 \((^{2})\) and to complete the proof.

For each formula \(\Phi\) we define its neutral variant \(\Phi'\): this is the formula obtained from \(\Phi\) by inserting a double negation \(\neg\neg\) before and after each logical connective of \(\Phi\). A closed formula \(\Phi\) is, by definition, classically true if its neutral variant \(\Phi'\) is realizable in Kleene’s sense (\((^{1})\), p. 442).

Theorem 2. A primitive recursive function \(R(x)\) can be constructed such that, for every classically true formula \(\Phi\), \(R(\Phi)\) cannot be a \(Z\chi\)-derivation of the formula \(\Phi\).

This is the constructive variant of the theorem of Kuznetsov and Shoenfield \((^5,\,^4)\). From the constructive point of view, the words “cannot fail to be” in the formulation of the theorem cannot be replaced by “is.” To prove the theorem one should consider the sequential variant \(Z^{0}\chi\), without cut and without structural rules of inference, but with two kinds of Carnap rule, corresponding to the introduction of \(\forall\) into the succedent and the introduction of \(\exists\) into the antecedent (for the corresponding predicate calculus see, for example, \((^6)\)). The function \(R\) is defined with the aid of Kleene’s recursion theorem \((^1,\) p. 314) and carries out a systematic search for a \(Z^{0}\chi\)-derivation of \(\Phi\) “from the bottom up.” If the formula \(\Phi\) is classically true, this search “cannot fail to terminate.” Analysis of the proof shows that the height of the derivation obtained in this way (for the definition of height see \((^4)\) or \((^2),\) p. 303) is always \(< \omega^3\), contrary to Shoenfield’s hypothesis that the required height is at least \(\omega^\omega\) \((^4)\).

We shall call a formula \(\Phi\) normal if it contains no logical connectives, \(\exists\), or \(\vee\). A formula beginning with some number of quantifiers, followed by a normal formula, will be called normally prefixed.

Theorem 3. A primitive recursive function \(R_1\) can be constructed such that, if \(\Phi\) is a normally prefixed formula and \(e\) is its realization, then \(R_1(e,\Phi)\) cannot fail to be a \(Z\chi\)-derivation of \(\Phi\).

Remark. A prefixed closed formula \(\Phi\) can be constructed such that neither \(\Phi\) nor \(\neg\Phi\) is derivable in \(Z\chi\).

Denote by \(Z^{+}\) the calculus \(Z\) supplemented by two axiom schemata:

1) the closure of all formulas of the form

\[ \neg\neg \exists x\Phi(x)\to \exists x\Phi(x), \]

where \(\Phi(x)\) contains no quantifiers (the formalized Markov principle);

2) the closure of all formulas of the form

\[ \forall x(\neg\Phi(x)\to \exists y\psi(x,y))\to \exists z\forall x(\neg\Phi(x)\to \exists y(T_1(z,x,y)\ \&\ \psi(x,U(y)))) \]

(the formalized Church thesis); for the definitions of \(T_1\) and \(U\), see \((^1)\).

Theorem 4. A primitive recursive function \(R_2\) can be constructed such that, if \(\Phi\) is a closed formula and \(e\) is its realization, then \(R_2(e,\Phi)\) cannot fail to be a \(Z^{+}\chi\)-derivation of \(\Phi\).

From Theorems 1 and 4 it follows that a transfinite progression \(F\) can be constructed, based on \(Z^{+}\) and complete with respect to realizability. This is a positive answer to the problem posed by Kurata in \((^7)\).

The author expresses his deep gratitude to Corresponding Member of the Academy of Sciences of the USSR A. A. Markov for his attention to the work.

Moscow State University
named after M. V. Lomonosov

Received
3 IV 1969.

REFERENCES

\(^1\) S. K. Kleene, Introduction to Metamathematics, IL, 1957.
\(^2\) S. Feferman, J. Symb. Logik, 27, No. 3, 259 (1962).
\(^3\) S. C. Kleene, ibid., 3, 150 (1938).
\(^4\) J. R. Shoenfield, Bull. Akad. Polon., 7, 405 (1959).
\(^5\) A. V. Kuznetsov, UMN, 12, 4(76), 218 (1957).
\(^6\) V. A. Matushis, DAN, 148, No. 4, 768 (1963).
\(^7\) R. Kurata, J. Math. Soc. Japan, 17, 140 (1965).