UDC 517.11

MATHEMATICS

A. G. DRAGALIN

ON THE JUSTIFICATION OF A. A. MARKOV’S PRINCIPLE OF CONSTRUCTIVE SELECTION

(Presented by Academician P. S. Novikov on 4 III 1967)

1. The principle of constructive selection was proposed by A. A. Markov in 1954 \((^1)\) as a method of meaningful logical reasoning that does not go beyond the constructive trend in mathematics. The principle consists in the following (A. A. Markov \((^2)\)):

“Suppose that for a property \(\mathfrak{P}\) there is an algorithm which determines, for every natural number \(n\), whether \(n\) has the property \(\mathfrak{P}\). If the proposition that no number has the property \(\mathfrak{P}\) is refuted, then there is a natural number with the property \(\mathfrak{P}\).”

Here by an algorithm is meant one of the precisifications of the intuitive concept of algorithm, for example, a normal algorithm, a partial recursive function, etc. In the present work we shall use the apparatus of normal algorithms \((^3)\).

The principle of constructive selection has found broad application in constructive mathematical logic and constructive analysis (see, for example, \((^{4-7})\)); however, its admissibility also gives rise to serious objections. It is therefore natural to seek cases in which the application of the principle can be justified by other methods, to show its eliminability. The first result of this kind (appearing long before the formulation of the principle itself) is the theorem of P. S. Novikov \((^8)\).

Let \(Z\) denote the classical logico-arithmetical calculus and \(Z'\) the corresponding constructive calculus, described in Kleene’s monograph \((^9)\). A property \(\mathfrak{P}\) of natural numbers will be called recursive if a normal algorithm \(\mathfrak{A}\) over the alphabet \(0|\) can be constructed, applicable to every natural number and such that \(\mathfrak{A}\lfloor n\rfloor \equiv 0\) if and only if \(n\) has the property \(\mathfrak{P}\). Let \(A(x)\) be a formula of \(Z\) with the single parameter \(x\), and let \(\mathfrak{P}\) be a property of natural numbers. We shall say that \(A(x)\) defines* \(\mathfrak{P}\) in \(Z\) (in \(Z'\)) \((^{10})\) if, for every natural \(n\), whenever \(n\) has the property \(\mathfrak{P}\), then \(\vdash A(\bar n)\) in \(Z\) (in \(Z'\)), and whenever \(n\) does not have the property \(\mathfrak{P}\), then \(\vdash \neg A(\bar n)\) in \(Z\) (in \(Z'\)). Here \(\bar n\) is an expression of the form \(0''\ldots'\) with \(n\) primes. Obviously, if \(A(x)\) defines \(\mathfrak{P}\) in \(Z'\), then \(A(x)\) defines \(\mathfrak{P}\) also in \(Z\).

P. S. Novikov’s theorem asserts that if \(A(x)\) defines some recursive property in \(Z'\) and \(\vdash \neg \forall x A(x)\) in \(Z\), then there is a natural \(n\) such that in \(Z'\), \(\vdash A(\bar n)\). The proof given in \((^8)\), however, is not constructive and essentially uses the existence of certain objects whose constructive character is open to objection.

The aim of the present note is a constructive proof of an algorithmic variant of P. S. Novikov’s theorem.

Theorem 1. Let \(\mathfrak{A}\) be a normal algorithm over the alphabet \(0|\), applicable to every natural number. Let \(A(x)\) define in \(Z'\) the property—

* By natural numbers we mean words in the alphabet \(0|\) of the form \(0, 0|, 0||, \ldots\), etc. (see \((^7)\)).

\[ \mathfrak{A}\left[\frac{x}{n}\right]\doteq 0 \]
and let \(\vdash \exists x A(x)\) in \(Z\). Then there is a natural number \(n\) such that
\[ \mathfrak{A}\left[\frac{\bar n}{n}\right]\doteq 0 . \]

Corollary 1. If \(A(x)\) defines in \(Z'\) some recursive property and \(\vdash \exists x A(x)\) in \(Z\), then there is a natural number \(n\) such that \(\vdash A(\bar n)\) in \(Z'\).

This is precisely the theorem cited above from \((^8)\).

Corollary 2. If \(A(x)\) defines in \(Z'\) some recursive property and \(\vdash \neg\neg \exists x A(x)\) in \(Z'\), then also \(\vdash \exists x A(x)\) in \(Z'\).

This corollary may be regarded as a certain justification of the principle of constructive selection, in the sense that if \(A(x)\) is recursive and \(\neg\neg \exists x A(x)\) is provable in \(Z'\), then in \(Z'\) one can also find a derivation of \(\exists x A(x)\), and this circumstance is established constructively and without the aid of the principle of constructive selection.

1. We shall use the terminology and results of the paper \((^{12})\). By ordinals we here mean the constructive transfinite numbers of the system \(M_0\). For the application of the theorem on the construction of an algorithm by transfinite recursion, we fix in this note the alphabet \(\mathfrak{E}\):

\[ 0 |' ( ) [ ] \{ \} \vee \& \supset \forall \mathfrak{A} \neg + \cdot \times . \]

Further, by algorithms we mean normal algorithms in the alphabet \(\mathfrak{E}\) or \(\square\). The formal system \(Ze\) described below is a constructive refinement of a certain modification of an arithmetic system with the rule of infinite induction (see \((^{11})\)).

The concept of a term (of the system \(Ze\)) is introduced inductively. 1. \(0\) is a term of \(Ze\). 2. Every variable* is a term of \(Ze\). 3–5. If \(s\) and \(t\) are terms of \(Ze\), then \((s)+(t)\), \((s)\cdot(t)\), \((s)'\) are terms of \(Ze\). 6. If \(\mathfrak{A}\) is an algorithm applicable to every natural number and transforming it into a natural number, and \(t\) is a term of \(Ze\), then \((\mathfrak{A}\mathfrak{E}(t))\) is a term of \(Ze\).

Formulas are defined in the usual way and have the form \((s)=(t)\), \((A)\supset(B)\), \((A)\&(B)\), \(\forall x(A)\), etc. (see \((^9)\)).

The formulas of the system \(Ze\) are those formulas which contain no free variables and no occurrences of the letters \(\supset \& \forall\). The concept of a sequent is introduced inductively. 1. The empty word is a sequent. 2. If \(\Gamma\) is a sequent and \(A\) is a formula of the system \(Ze\), then \(\Gamma A\) is a sequent. Classically, the sequent \(A_1A_2\ldots A_k\) is interpreted as the disjunction
\[ A_1 \vee A_2 \vee \cdots \vee A_k \vee 0=1 . \]
In particular, the empty sequent represents the “standard falsehood” \(0=1\). The system \(Ze\) is organized so that sequents are derived in it.

For each term of \(Ze\) without free variables there is naturally determined a natural number—its value. In this case the value of a term of the form \((\mathfrak{E}\mathfrak{A}(t))\) is the result of applying the algorithm \(\mathfrak{A}\) to the value of the term \(t\). A formula of the form \((s)=(t)\) without free variables will be called true or false according as the values of the left- and right-hand sides of this formula are equal or not. Each axiom of the system \(Ze\) has one of two forms: a) \((s)=(t)\), a true formula without free variables, or b) \(\neg((s)=(t))\), where \((s)=(t)\) is a false formula without free variables.

The concept of a tuple is introduced inductively. 1. A natural number is a tuple. 2. If \(a\) is a tuple and \(n\) is a natural number, then \(an\) is a tuple. Thus, a tuple is an ordered nonempty list of natural numbers.

We shall say that an algorithm \(P\) is a derivation of the system \(Ze\) if \(P\) is applicable to every tuple and transforms it into the empty word or into a word of the form \(\Pi(kam)\), where \(\Pi\) is a sequent, \(k m\) are natural numbers and \(a\) is an ordinal. In addition, the following conditions are satisfied:

* Here by variables we mean words of the form \((\times)\), \((\times\times)\), \((\times\times\times)\), …, etc. in the alphabet \(( )\times\).

a) \(\neg P\lfloor 0\rfloor \bar{\circ}\Lambda\), and for every natural \(k\), \(P\lfloor k+1\rfloor \bar{\circ}\Lambda\).

b) If \(P\lfloor a\rfloor \bar{\circ}\Lambda\), then for every \(k\), \(P\lfloor ak\rfloor \bar{\circ}\Lambda\).

c) If \(P\lfloor a\rfloor \bar{\circ}\Pi(k\alpha m)\), then at least one of the following conditions 1)—6) holds:

1) \(\Pi\) is an axiom of the system \(Ze\), \(m=0\), and for every natural \(l\)

\[ P\lfloor al\rfloor \bar{\circ}\Lambda . \]

2) \(P\lfloor a0\rfloor \bar{\circ}\Delta(k'\alpha'm')\), \(k\geq k'\), \(\alpha\geq\alpha'\), \(m=m'+1\), and the figure \(\dfrac{\Delta}{\Pi}\) has one of the following forms:

\[ \frac{(A)\vee(B)\Gamma}{AB\Gamma}; \qquad \frac{AB\Gamma}{(A)\vee(B)\Gamma}; \qquad \frac{\Gamma AB\Phi}{\Gamma BA\Phi}; \qquad \frac{A\Gamma}{A\Gamma}; \qquad \frac{\Gamma}{A\Gamma}, \]

where \(A,B\) are formulas of the system \(Ze\) and \(\Gamma,\Delta,\Phi\) are sets. In addition, for every \(l\), \(P\lfloor a(l+1)\rfloor \bar{\circ}\Lambda\).

3) \(P\lfloor a0\rfloor \bar{\circ}\Delta(k'\alpha'm')\), \(k\geq k'\), \(\alpha>\alpha'\), \(m=0\), and the figure \(\dfrac{\Delta}{\Pi}\) has one of the following forms:

\[ \frac{A\Gamma}{\neg\neg A\Gamma} \qquad \frac{A(t)\Gamma}{\exists xA(x)\Gamma}. \]

In addition, for every natural \(l\), \(P\lfloor a(l+1)\rfloor \bar{\circ}\Lambda\).

4) \(P\lfloor a0\rfloor \bar{\circ}\Delta(k'\alpha'm')\) and \(P\lfloor a1\rfloor \bar{\circ}\Phi(k''\alpha''m'')\), \(k\geq k'\), \(k\geq k''\), \(\alpha>\alpha'\), \(\alpha>\alpha''\), \(m=0\), and the figure \(\dfrac{\Delta;\Phi}{\Pi}\) has the form

\[ \frac{\neg A\Gamma;\ \neg B\Gamma}{\neg(A\vee B)\Gamma}. \]

In addition, for every \(l\), \(P\lfloor a(l+2)\rfloor \bar{\circ}\Lambda\).

5) \(P\lfloor a0\rfloor \bar{\circ}\Delta(k'\alpha'm')\) and \(P\lfloor a1\rfloor \bar{\circ}\Phi(k''\alpha''m'')\), and the figure \(\dfrac{\Delta;\Phi}{\Pi}\) has the form

\[ \frac{\Gamma A;\ \neg A\Sigma}{\Gamma\Sigma}, \]

where \(k\geq k'\), \(k\geq k''\), \(k\) is greater than the number of occurrences of the letters \(\exists,\neg,\vee\) in \(A\), \(\alpha>\alpha'\), \(\alpha>\alpha''\), \(m=0\).

In addition, for every \(l\), \(P\lfloor a(l+2)\rfloor \bar{\circ}\Lambda\).

6) \(\Pi\) has the form \(\neg \exists xA(x)\Sigma\), and for every natural \(i\), \(P\lfloor ai\rfloor\) has the form \(\neg A(i)\Sigma(k_i\alpha_i m_i)\), where \(m=0\) and for every \(i\), \(k\geq k_i\), \(\alpha>\alpha_i\).

With this, the definition of a derivation of the system \(Ze\) is completed. If \(P\) is a derivation in \(Ze\) and \(P\lfloor 0\rfloor \bar{\circ}\Pi(k\alpha m)\), then \(P\) shall be called a derivation of the set \(\Pi\), \(\alpha\) the height of the derivation \(P\), \(k\) the order of \(P\), and \(m\) the structural height of \(P\). A set \(\Pi\) is derivable in \(Ze\) if there is a derivation \(P\) of this set in the system \(Ze\). In case 2) of the definition we shall say that \(P\lfloor a\rfloor\) was obtained by means of a structural rule of inference; in cases 3) and 4), by means of a logical rule of inference; in case 5), by means of a cut; and in case 6), by the rule of infinite induction.

A derivation of the system \(Ze\) without cuts is defined in the same way as a derivation of \(Ze\), with the sole difference that item 5) is absent from the definition.

Lemma 1. An algorithm \(\mathfrak A\) can be constructed satisfying the following condition: whatever the natural number \(k\), the set \(\Pi\), and its derivation \(D\) in \(Ze\) of height less than \(\varepsilon_k\), \(\mathfrak A\lfloor D\rfloor\) is a derivation in \(Ze\) without cuts of the set \(\Pi\), and the height of \(\mathfrak A\lfloor D\rfloor\) is less than \(\varepsilon_k\).

The proof of this lemma is a constructive refinement of the proof of the corresponding theorem of Schütte \((^{11})\). The algorithms whose necessity arises in such a refinement are constructed with the aid of transfinite recursion on the height of the derivations being processed \((^{12})\).

Let \(A\) be a formula of \(Z\). Then by \(A^0\) we denote the formula obtained by eliminating, in the usual way, the logical connectives \(\& \supset \vee\) with the aid of the connectives \(\vee\neg\exists\).

Lemma 2. An algorithm \(\mathfrak A\) can be constructed satisfying the following condition: whatever the formula \(A\) without free variables and its derivation

$D$ in $Z$, $\mathfrak A\!\lfloor D\rfloor$ has a derivation $A^0$ in $Z\varepsilon$, and the height of $\mathfrak A\!\lfloor D\rfloor$ is less than $2\omega$.

From Lemmas 1 and 2 it is not difficult to obtain a constructive proof of the consistency of $Z$, using the obvious fact that the empty set is not derivable without cuts in $Z\varepsilon$.

Lemma 3. An algorithm $\Phi$ can be constructed satisfying the condition: whatever the general recursive function $\mathfrak A$ and the formula $A(x)$ defining in $Z$ the property $\mathfrak A\!\lfloor x\rfloor \simeq 0$, $\Phi\!\lfloor \mathfrak A\mathfrak Z \square A(x)\square x\rfloor$ is a derivation of the set $\neg\exists x A^0(x)\, \exists x(\varepsilon\mathfrak Z(x)=0)$ in $Z\varepsilon$, and the height of $\Phi\!\lfloor \varepsilon\mathfrak Z \square \bar A(x)\rfloor$ is less than $\varepsilon_2$ (in the notation of article (12)).

We shall denote by $0^n$ the word in the alphabet $0$ of length $n$ $(n \ge 0)$.

Lemma 4. An algorithm can be constructed which transforms every derivation $P$ in $Z\varepsilon$ into a natural number $n$ such that $P\!\lfloor 0^n\rfloor \simeq \Pi(kat)$, where $\Pi$ is an axiom of $Z\varepsilon$, and moreover for every natural $l$, $P\!\lfloor 0^n l\rfloor \simeq \Lambda$.

The required algorithm is constructed by means of transfinite recursion on the height of the given derivation $P$.

We now prove Theorem 1. Let $\mathfrak A$ and $A(x)$ be as in the condition of the theorem. Construct an algorithm $\mathfrak A'$ such that, for every natural $n$, $\mathfrak A'\!\lfloor n\rfloor \simeq 0$ if and only if $\mathfrak A\!\lfloor n\rfloor \simeq 0$, while if $\neg\,\mathfrak A\!\lfloor n\rfloor \simeq 0$, then $\mathfrak A\!\lfloor n\rfloor \simeq 0|$. Obviously, $A(x)$ defines in $Z$ also the property $\mathfrak A'\!\lfloor x\rfloor \simeq 0$. With the aid of Lemma 3 construct a derivation of the set $\neg\exists x A^0(x)\, \exists x(\varepsilon\mathfrak Z(x)=0)$ in $Z\varepsilon$. Since $\vdash \exists x A(x)$ in $Z$, by Lemma 2 one can construct a derivation of $\exists x A^0(x)$ in $Z\varepsilon$. Applying the cut rule (p. 5) to the definition of a derivation in $Z\varepsilon$, we obtain a derivation of $\exists x(\varepsilon\mathfrak Z(x)=0)$ in $Z\varepsilon$. Finally, with the aid of Lemma 1 one can obtain a derivation of $\exists x({}^{\varepsilon}\mathfrak Z(x)=0)$ without cuts as well. Consider this last derivation $P$. By Lemma 4, a natural number $l$ can be constructed such that $P\!\lfloor 0^l\rfloor$ has the form $\Pi(kat)$, where $\Pi$ is an axiom of the system $Z\varepsilon$. From the definition of derivation without cuts one can see that in the present case $\Pi$ has the form $(\varepsilon\mathfrak Z(\bar n)=0)$. And since this formula is an axiom of $Z\varepsilon$, $\mathfrak A\!\lfloor n\rfloor \simeq 0$. Thus, the constructed $\bar n$ is to be taken as the desired one.

In the outlined proof only ordinals less than the second Cantor $\varepsilon$-number are used ($\varepsilon_2$ in the notation of (12)).*

In conclusion the author expresses his deep gratitude to his scientific adviser A. A. Markov for his attention to the work.

Moscow State University
named after M. V. Lomonosov

Received
16 II 1967

REFERENCES

1. A. A. Markov, UMN, 9, 236 (1954).
2. A. A. Markov, Tr. Mat. inst. im. V. A. Steklova AN SSSR, 67, 8 (1962).
3. A. A. Markov, ibid., 42 (1954).
4. G. S. Tseitin, ibid., 67, 295 (1962).
5. I. D. Zaslavskii, ibid., 67, 458 (1962).
6. V. P. Orevkov, ibid., 72, 437 (1964).
7. N. A. Shanin, ibid., 52, 226 (1958).
8. P. S. Novikov, Matem. sborn., 12 (54), 231 (1943).
9. C. K. Kleene, Introduction to Metamathematics, IL, 1957.
10. R. Montague, Essays on Found., Jerusalem, 1961, p. 91.
11. K. Schütte, Math. Ann., 122, 369 (1951).
12. A. G. Dragalin, DAN, 175, No. 5 (1967).

* Precisely this set of transfinite numbers is used by A. S. Esenin-Volpin in Appendix VII to the Russian translation of (9).