Reports of the Academy of Sciences of the USSR
1967. Vol. 175, No. 5

UDC 517.1+502.16

MATHEMATICS

A. G. DRAGALIN

CONSTRUCTIVE TRANSFINITE SYSTEMS AND THE CONSTRUCTION OF AN ALGORITHM BY TRANSFINITE RECURSION

(Presented by Academician P. S. Novikov on 21 XI 1966)

It is known that initial segments of countable transfinite numbers can be treated constructively as words of a special kind with an order relation defined on them. Under such an interpretation, for rather broad systems of transfinite numbers it is possible to justify constructively also the principle of transfinite induction (see, for example, \((^1)\)). There arises the general problem of transferring to constructive mathematics some part of the theory of countable transfinite numbers. Besides transfinite induction, in constructive proofs it is important to be able also to construct algorithms by transfinite recursion, similarly to the construction of algorithms by arithmetical recursion. Such recursions arise, for example, in attempts to transfer to constructive mathematics results on the consistency of various formal axiomatic systems, when these results are obtained by means of transfinite induction, and also in the study of so-called semiformal systems with the rule of infinite induction

\[ \frac{A(0),\ A(1),\ldots,\ A(u),\ldots}{\forall x A(x)} \]

(such results, see, for example, \((^2)\)).

The possibility of constructing an algorithm by transfinite recursion for a broad class of transfinite systems is provided by the theorem stated below. Further, the constructive acceptability of certain constructive transfinite systems is discussed.

1. A constructive transfinite system is given by a triple of objects: \(B, O, <\), where \(O\) is a set of words in the alphabet \(B\), and \(<\) is a partial relation on words from the set \(O\)*. Moreover the following conditions must be satisfied 1), 2) (below \(\alpha, \beta, \gamma, \eta\) are variables for words from the set \(O\); we shall call these words ordinals of the system):

1) \(\alpha < \beta \& \beta < \gamma \supset \alpha < \gamma\).

2) If \(A(x)\) is a property of ordinals, then for it the following assertion is valid, expressing the principle of transfinite induction:

\[ \forall \alpha(\forall \eta(\eta < \alpha \supset A(\eta)) \supset A(\alpha)) \supset \forall \alpha A(\alpha). \]

Let \((B, O, <)\) be a constructive transfinite system. Then the following assertions hold:

Lemma 1. \(\neg(\alpha < \alpha)\).

Proof by transfinite induction on \(\alpha\).

Lemma 2. \(\alpha < \beta \supset \neg \beta < \alpha\).

Consequence of Lemma 1 and property 1).

Lemma 3. Let \(\mathfrak A\) be a normal algorithm over the alphabet \(B \, 0|\), applicable to every natural number** and such that for every natu-

* We use the terms and notation introduced in \((^{6-8})\). In particular, the terms set, relation and, further, property are treated constructively (see \((^8)\)).

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

of the natural number \(n\), \(\mathfrak A\lfloor n\rfloor\) is the result of applying \(\mathfrak A\) to \(n\), is an ordinal of the system. Suppose, moreover,

\[ \text{a)}\quad \forall n\bigl(\neg\,\mathfrak A\lfloor n+1\rfloor \,\bar\circ\, \mathfrak A\lfloor n\rfloor \supset \mathfrak A\lfloor n+1\rfloor < \mathfrak A\lfloor n\rfloor\bigr), \]

\[ \text{b)}\quad \forall n\bigl(\mathfrak A\lfloor n+1\rfloor \,\bar\circ\, \mathfrak A\lfloor n\rfloor \supset \forall m(m\ge n \supset \mathfrak A\lfloor m\rfloor \,\bar\circ\, \mathfrak A\lfloor n\rfloor)\bigr). \]

Then there exists \(n_0\) such that

\[ \forall n(n\ge n_0 \supset \mathfrak A\lfloor n\rfloor \,\bar\circ\, \mathfrak A\lfloor n_0\rfloor). \]

Proof by transfinite induction on \(\mathfrak A\lfloor 0\rfloor\).

Lemma 4. Let \(A(x)\) be a property of ordinals; then

\[ \neg\neg\bigl((\exists \alpha(A(\alpha)\,\&\,\forall\eta(\eta<\alpha \supset \neg V(\eta))))\vee \forall\alpha\,\neg V(\alpha)\bigr). \]

First one proves the assertion

\[ \forall\beta\,\neg\neg\bigl((\exists\alpha(A(\alpha)\,\&\,\alpha<\beta\,\&\,\forall\eta(\eta<\alpha \supset \neg A(\eta))))\vee \]

\[ \forall\alpha(\alpha<\beta \supset \neg A(\alpha))\bigr) \]

by transfinite induction on \(\beta\). Then from it we obtain the desired assertion, using the true assertion

\[ \neg\neg\bigl((\exists\alpha A(\alpha))\vee \forall\alpha\,\neg A(\alpha)\bigr). \]

2. Let, as before, \((B,O,<)\) be a constructive transfinite system. Fix an alphabet \(\mathcal Э\) containing the alphabet \(Б0|\), but not containing the letters \(шщ\square\). By algorithms in this section we mean normal algorithms in the alphabet \(\mathcal Эшщ\square\). By \(\mathfrak A\lfloor P\rfloor\), where \(\mathfrak A\) is an algorithm and \(P\) is in the alphabet \(\mathcal Эшщ\square\), we shall denote the result of applying \(\mathfrak A\) to the word \(P\), if such a result exists.

The expression \(!\mathfrak A\lfloor P\rfloor\) means that \(P\) is in the alphabet \(\mathcal Э\square\), \(\mathfrak A\) is applicable to \(P\), and the result \(\mathfrak A\lfloor P\rfloor\) is a word in the alphabet \(\mathcal Э\). By \(\mathfrak E\mathfrak A\mathfrak Z\) we shall denote the standard notation of the algorithm \(\mathfrak A\) as a word in the alphabet \(0|\) (see \((^6)\)).

Theorem. Let \(A(P,\alpha,R)\) and \(B(\alpha,R)\) be ternary and binary relations. Here \(P\) is a variable for words in the alphabet \(\mathcal Э\); \(R\) is a variable for words in the alphabet \(\mathcal Э\square\), and \(\alpha\) is a variable for ordinals. Suppose the algorithm \(\mathfrak B\) has the following property:

For every algorithm \(\mathfrak A\) and ordinal \(\beta\), if

\[ \forall\eta\forall R(\eta<\beta\,\&\,B(\eta,R)\supset !\mathfrak A\lfloor\eta\square R\rfloor\,\&\,A(\mathfrak A\lfloor\eta\square R\rfloor,\eta,R)), \]

then for every \(R\) such that \(B(\beta,R)\), we have

\[ !\mathfrak B\lfloor\mathfrak E\mathfrak A\mathfrak Z\square\beta\square R\rfloor,\qquad A(\mathfrak B\lfloor\mathfrak E\mathfrak A\mathfrak Z\square\beta\square R\rfloor,\beta,R). \]

Then an algorithm \(\mathfrak C\) can be constructed such that

\[ \forall\alpha\forall R\bigl(B(\alpha,R)\supset !\mathfrak C\lfloor\alpha,R\rfloor\,\&\,A(\mathfrak C\lfloor\alpha\square R\rfloor,\alpha,R)\bigr). \]

The algorithm \(\mathfrak C\) in this theorem, given \(\alpha\) and \(R\), outputs the corresponding \(P\) such that \(A(P,\alpha,R)\). The algorithm \(\mathfrak C\) is constructed with the help of the algorithm \(\mathfrak B\). The latter algorithm, in order to obtain the corresponding \(P\), in addition to \(\alpha\) and \(R\), also needs a special algorithm \(\mathfrak A\), which outputs \(P\) for all \(\eta<\alpha\). The theorem states that, having \(\mathfrak B\), one can also obtain the more powerful algorithm \(\mathfrak C\). \(R\) in the theorem plays the role of a parameter of the algorithms.

To prove the theorem, using the algorithmic variant of Kleene’s recursion theorem (see \((^{10})\), p. 314), we construct an algorithm \(\mathfrak C\) such that,

that the conditional equality holds

\[ \mathfrak C_{\llcorner a \square R\lrcorner}\simeq \mathfrak B_{\llcorner \mathfrak E\mathfrak Z \square a \square R\lrcorner}^{*}. \]

The required property of \(\mathfrak C\) is established by transfinite induction on \(\alpha\).

1. An example of a constructive transfinite system may be a finite list of words in some alphabet with a recognizable partial order relation on it. The set of natural numbers with the usual order relation also constitutes a constructive transfinite system. Let us describe the system \(M_0\) of constructive transfinite numbers \(<\varepsilon_\omega\).

We shall call a valency a pair of natural numbers \((m,n)\). Among valencies we define the lexicographic order:

\[ (a,b)<(c,d)\equiv a<c\vee(a=c\ \&\ b<d). \]

In addition, put \((a,b)\ll(c,d)\equiv a<c\).

Definition 1. a) The only ordinal figures of valency \((0,0)\) are, by definition, the natural numbers.

b) Ordinal figures of valency \((k+1,m)\) are words of the form
\((\theta_1[k\triangle \gamma_1]\ldots\theta_n[k\triangle \gamma_n]\theta)\), where
1) \(\theta_1,\ldots,\theta_n,\theta\) are ordinal figures of valencies \(\ll(k+1,m)\);
2) \(\gamma_1,\ldots,\gamma_n\) are figures with valencies \(<(k+1,m)\);
3) \(\neg\,\theta_i \doteq 0,\ \gamma_i \doteq 0\ (i=1,\ldots,n)\);
4) if \(m\ne0\), then \(\gamma_1\) has valency \((k+1,m-1)\).

This completes the definition of an ordinal figure. Thus there are no ordinal figures of valencies of the form \((0,m+1)\).

Among ordinal figures introduce the relation \(A<B\) by induction on \(\max(\operatorname{val} A,\operatorname{val} B)\).

Definition 2. a) If \(A\) and \(B\) are natural numbers, then the relation \(A<B\) coincides with the usual ordering of the natural numbers.

b) Every ordinal figure of valency \(<(k+1,m)\) is, by definition, less than an ordinal figure of valency \((k+1,m)\).

c) Let
\[ A\doteq(\theta_1[k\triangle \alpha_1]\ldots \theta_n[k\triangle \alpha_n]\theta) \]
and
\[ B\doteq(\eta_1[k\triangle \beta_1]\ldots \eta_p[k\triangle \beta_p]\eta) \]
be of one and the same valency \((k+1,m)\). Denote by \(T(i)\) the assertion
\[ \forall j\,(j\leq i\supset \theta_j\doteq\eta_j\ \&\ \alpha_j\doteq\beta_j). \]
Then \(A<B\) if and only if at least one of the following conditions is satisfied:

1) \(n<p\ \&\ T(n)\).

2) \(n=p\ \&\ T(p)\ \&\ \theta<\eta\).

* If \(X\doteq \xi\mathfrak A3\), then put \(\langle X\rangle=\mathfrak A\); but if \(X\) is not a standard notation of an algorithm, then as \(\langle X\rangle\) we take the normal algorithm with scheme \(\{\to\).

To construct \(\mathfrak C\), first, with the aid of a universal algorithm, we construct an algorithm \(\mathfrak L\) such that

\[ \mathfrak L_{\llcorner S\square X\lrcorner}\simeq \langle S\rangle_{\llcorner S\square X\lrcorner}; \]

here \(S\) is in the alphabet \(01\), and \(X\) is in the alphabet \(\mathfrak E\square\).

Next we construct an algorithm \(\mathfrak F\) such that

\[ \langle \mathfrak F_{\llcorner S\lrcorner}\rangle_{\llcorner X\lrcorner}\simeq \mathfrak L_{\llcorner S\square X\lrcorner} \]

(in the terminology of article (9), for this it is enough to construct \(\mathfrak F\) so that the equality
\[ \mathfrak F_{\llcorner S\lrcorner}\doteq \xi\mathfrak L_{S\square}^{3} \]
holds).

Next we construct an algorithm \(\mathfrak P\) such that

\[ \mathfrak P_{\llcorner S\square X\lrcorner}\simeq \mathfrak B_{\llcorner \mathfrak F_{\llcorner S\lrcorner}\square X\lrcorner}. \]

Let \(T\doteq \xi\mathfrak P3\). Then put
\(\mathfrak C=\langle \mathfrak F_{\llcorner T\lrcorner}\rangle\). We have

\[ \begin{aligned} \mathfrak C_{\llcorner a\square R\lrcorner} &\simeq \langle \mathfrak F_{\llcorner T\lrcorner}\rangle_{\llcorner a\square R\lrcorner} \simeq\\ \mathfrak L_{\llcorner T\square a\square R\lrcorner} &\simeq \langle T\rangle_{\llcorner T\square a\square R\lrcorner} \simeq\\ \mathfrak P_{\llcorner T\square a\square R\lrcorner} &\simeq \mathfrak B_{\llcorner \mathfrak F_{\llcorner T\lrcorner}\square a\square R\lrcorner} \simeq\\ &\mathfrak B_{\llcorner \xi\mathfrak C3 \square a\square R\lrcorner}. \end{aligned} \]

3) $\exists i(1 \leq i \leq \min(n,p)\ \&\ T(i-1)\ \&\ \alpha_i=\beta_i\ \&\ \theta_i<\eta_i)$.

4) $\exists i(1 \leq i \leq \min(n,p)\ \&\ T(i-1)\ \&\ \alpha_i<\beta_i)$.

Definition 3. Ordinal figures of a special kind shall be called ordinals. Namely:

a) A natural number is an ordinal.

b) The ordinal figure $(\theta_1[k \triangle \alpha_1]\ldots \theta_n[k \triangle \alpha_n]\theta)$ shall be called an ordinal if $\alpha_1>\alpha_2>\cdots>\alpha_n$ and $\alpha_1,\ldots,\alpha_n,\theta_1,\ldots,\theta$ are ordinals.

This completes the definition of the system $M_0$. It can be verified that the ordinals form a decidable subset of the set of all words in the alphabet $(\ )[\,]0|\triangle$, and that the relation $<$ between ordinals of the system $M_0$ is a decidable relation. Moreover, by induction on the max of the valencies of $\alpha$ and $\beta$ one establishes the trichotomy of the relation: $\alpha<\beta \vee \alpha \simeq \beta \vee \beta<\alpha$.

For ordinals one can naturally introduce constructive operations of addition, multiplication, and exponentiation, possessing the usual properties. In this case it turns out that

$$ \theta_1[k \triangle \alpha_1]\ldots \theta_n[k \triangle \alpha_n]\theta)\simeq \theta_1\cdot \varepsilon_k^{\alpha_1}+\ldots+\theta_n\cdot \varepsilon_k^{\alpha_n}+\theta^*, $$

where $\varepsilon_k \simeq (1[k \triangle 1]0)$.

The principle of transfinite induction in the system $M_0$ is justified by generalizing, for $M_0$, Hilbert and Bernays’ proof of the principle of transfinite induction up to transfinite numbers less than the first $\varepsilon$-number greater than $\omega$ (see (1), pp. 361–366). An important role in the proof is played by the definition of certain predicates by means of ordinary arithmetical induction.

The system $M_0$ can be considerably extended while preserving its most important properties. Powerful transfinite systems with a decidable relation $<$, whose constructive character, however, is considerably more problematic, are described in works (4, 5).

1. The presence of the principle of transfinite induction makes it possible to define predicates by transfinite induction.

In conclusion, the author expresses profound gratitude to A. A. Markov for his attention to the work.

Moscow State University
named after M. V. Lomonosov

Received
20 X 1966

REFERENCES

1 D. Hilbert, P. Bernays, Grundlagen der Mathematik, 2, Berlin, 1939.
2 F. Schütte, Beweistheorie, Berlin, 1960.
3 K. Schütte, Math. Zs., 1, H. 2, 160 (1954).
4 K. Schütte, Math. Ann., 127, H. 1, 15 (1954).
5 W. Ackermann, Math. Zs., 53, 403 (1951).
6 A. A. Markov, Tr. Matem. inst. im. V. A. Steklova AN SSSR, 42 (1954).
7 A. A. Markov, ibid., 67, 8 (1962).
8 N. A. Shanin, ibid., 52, 226 (1958).
9 G. S. Tseitin, ibid., 67, 295 (1962).
10 S. K. Kleene, Introduction to Metamathematics, IL, 1957.

* Here the $\varepsilon$-numbers are numbered beginning with $\omega$, i.e. $\varepsilon_0=\omega$.