The aim of this paper is to present a definition of a formal reasoning system called object-oriented logic (OOL), and to show its utility by its application on some examples. The essential feature of OOL is that general rules are represented by the same type of network-like structures as are individual facts with some small additional information. Except for that information, the OOL rules look exactly like the facts that can be derived from them. The question of validity in the OOL framework is formally irrelevant because the OOL system has no axioms, and any conclusion deemed invalid can be blamed on the premises. Since there is no obvious mapping of OOL rules into an established logical system, any comparison to other systems is difficult, although comparison is discussed.
   The paper contains no mathematical results regarding the proposed OOL system since the author considers it more important to refine the OOL definitions within various applications. However, an interesting example presents a natural mapping of Prolog into OOL, suggesting that OOL can represent arithmetic and recursive functions. An experimental implementation and some programming techniques included in an extended version of the present paper can be seen at the address: http://www.math.spbu.ru/∼tseytin/ARTICLE.ps.gz.

Mathematical thought, in the sense of mathematical reasoning, is contrasted with ordinary thought. The author suggests that neither is derived from, nor attempts to model, the other. He sees mathematical thought not as completely objective, but as depending on reproducibility. He claims that ordinary thought is richer in its diversity of subtle distinctions which mathematics treats as equivalent, but that the application of mathematical methods to other sciences serves as an index for a certain level of maturity of that science, though without the presence of a suitable base in the science, introduction of mathematical apparatus reduces to science-like but useless exercises.
   It seems that the author is attacking some unspecified and (to the reviewer) unknown philosophical position or trend in nonmathematical disciplines. A good deal may be lost in the translation of what is a very succinct article.

The English original of this article has been reviewed [Algorithms in modern mathematics and computer science (Urgench, 1979), 390–396, Springer, Berlin, 1981; MR0657627].

The author describes his conversion from viewing mathematical knowledge as consisting of statements about mathematical structures to viewing it as knowledge of algorithmic procedures, as a result of his experiences with theoretical and applied computer science.

The authors consider two versions of propositional calculus, Σ1 and Σ2. The former is defined by ten axiom schemes and three rules of inference; the latter by ten axioms (particular instances of the above schemes) and the same three rules of inference plus the rule of substitution. Li(ϕ) denotes the length of the shortest deduction of a (provable) formula ϕ in Σi, and Sˇi,j(n)=maxLi(ϕ)≤nLj(ϕ) ("Sˇ'' is for "Shannon''). Theorem 1: Sˇ1,2(n)≤2n+22. Theorem 2: 2n/2/4≤Sˇ2,1(n)≤3⋅2n/2/√2 for n>0.
   These results were announced in an earlier paper by the authors [Akad. Nauk Armjan. SSR Dokl. 55 (1972), 10–12; MR0360189].

The authors introduce a notion of a generating scheme as a generalization of the notion of a regular expression, namely, the operations of set-theoretic intersection and complement are accepted and concatenations actions of these operations are controlled by a directed multigraph. First the author establishes bounds for the minimal number of states of a finite automaton accepted by the set represented by a generating scheme in terms of the complexity of the generating scheme [the first author, Dokl. Akad. Nauk SSSR 213 (1973), 26–29].
   For a class of special generating schemes an upper bound of the type 22n was stated by him [op. cit.]. In the present paper this upper bound is reduced to ψ(n), where ψ(n) is the number of monotone n-ary Boolean functions.
   {For the entire collection see MR0345791.}

From the author's introduction: "One of the things we need in order to use theorem-proving techniques in actual programming (and not only in illustrations) is a language that would enable a programmer to state his reasoning about the program in a convenient form that easily matches his way of thinking. In this paper an approach to creating such a language is suggested and some features of it are discussed. Thus the main attention is given to making statements about programs rather than to proving them.''
   {For the entire collection see MR0411218.}

This paper begins with the observation that the state of programming language technology has changed primarily by dint of a natural desire to make programming languages more convenient for human users. The author correctly observes that in this process features of natural languages have cropped up in programming language design. The point of this discursive article is to argue that even when the borrowing of natural language features is not an immediate goal in programming language design, "deeper features of natural languages are reproduced in the programming language...''.
   There is a major confusion over what constitutes a language feature (in paragraph 2, for example, a grammar is listed as a feature). In the author's subsequent discussion of ALGOL 60 and ALGOL 68 as vehicles for demonstrating the ineffable appearance of natural language features, there are a number of ill-founded or incorrect analogies drawn to natural linguistic phenomena. The superficiality of the treatment of linguistic phenomena is evident in the following quote which appears towards the end of the paper: "Similarly, when we assign a meaning... to a value or a word, we do not expect that the affect of this assignment will be valid until the next assignment to the same symbol is made; it is expected to be valid neither forever or within a specified portion of text...''. Referential opacity is a counterexample.
   The author closes with the hope that the deliberate imitation of some "deep features'' of natural languages will show a way to create ever more powerful programming languages.
   {For the entire collection see MR0434692.}

The authors consider two systems of propositional calculi. The first is Σ1, which has ten axiom-schemas and modus ponens and the rule of syllogism as the rules of proof. Σ2 is obtained from Σ1 by changing the schemas into axioms (by substituting propositional variables for metavariables), and adding the substitution rule. If W is the proof of the formula F, let L(W) be the length of W and Li(F)=min{L(W):W is a proof of F in Σi}, i=1,2. One can define the following two functions (called relative Shannon functions): Shi,jn=max{Lj(F):Li(F)≤n} for i≠j, i, j=1,2. The following inequalities hold: (i) Sh1,2(n)≤2n+22, (ii) 2n/2−2≤Sh2,1(n)≤3⋅2(n−1)/2. The authors outline proofs of (i) and the left inequality of (ii).

Table of Contents: N. K. Kosovskiĭ, Some questions in the constructive theory of normed Boolean algebras [Trudy Mat. Inst. Steklov 113 (1970), 3–38; MR0288792] (pp. 1–41); B. A. Kušner, Some mass problems connected with the integration of constructive functions [ibid. 113 (1970), 39–72; MR0289729] (pp. 42–83); A. O. Slisenko, Some questions on the approximation of maximal regulators of continuity [ibid. 113 (1970), 73–78; MR0302826] (pp. 84–90); R. I. Freĭdzon, A characterization of the complexity of recursive predicates [ibid. 113 (1970), 79–101; MR0289311] (pp. 91–117); G. S. Ceĭtin, On upper bounds of recursively enumerable sets of constructive real numbers [ibid. 113 (1970), 102–172; MR0321710] (pp. 119–194); V. A. Šurygin, Constructive sets with equality and their mappings [ibid. 113 (1970), 173–259; MR0290964] (pp. 195–287).

This volume contains translations from the Russian of the following articles: G. E. Minc, On predicate and operator variants of the formation of theories of constructive mathematics [MR0194333] (pp. 1–68); V. P. Orevkov, On constructive mappings of a disk into itself [MR0205844] (pp. 69–100); V. P. Orevkov, Certain questions of the theory of polynomials with constructive real coefficients [MR0202597] (pp. 101–133); A. O. Slisenko, On certain algorithmic problems connected with arithmetic operations over duplexes [MR0202598] (pp. 135–183); A. O. Slisenko, Example of a nondiscontinuous but not continuous constructive operator in a metric space [MR0195730] (pp. 184–194); A. O. Slisenko, On constructive non-separable spaces [MR0195731] (pp. 195–199); G. S. Ceĭtin, Three theorems on constructive functions [MR0205843] (pp. 201–209); A. L. Verner, Polyhedral angles with one-to-one spherical representation [MR0199767] (pp. 211–242); I. F. Donin, On deformations of holomorphic vector bundles over the Riemann sphere [MR0208624] (pp. 234–251); A. V. Černavskiĭ, Finite-to-one open mappings of manifolds [MR0172256] (pp. 253–267); A. V. Černavskiĭ, Addendum to the paper "Finite-to-one open mappings of manifolds'' [MR0220254] (pp. 269–270); Ju. Ju. Trohimčuk, Continuous mappings of domains in euclidean space [MR0161313] (pp. 271–291); B. M. Šaĭn, Restrictive bisemigroups [MR0174647] (pp. 293–307); B. M. Šaĭn, Restrictive bisemigroups of mappings [MR0210804] (pp. 308–316).

This volume contains translations from the Russian of the following articles:
   Table of Contents: G. S. Ceĭtin, A method of presenting the theory of algorithms and enumerable sets [MR0205842] (pp. 1–39); N. N. Vorobʹev, A constructive calculus of statements with strong negation [MR0191817] (pp. 40–82); A. V. Idelʹson, Calculi of constructive logic with subordinate variables [MR0195687] (pp. 83–227); I. D. Zaslavskiĭ and G. S. Ceĭtin, Concerning a generalized principle of constructive selection [MR0200156] (pp. 228–232); N. A. Šanin, Concerning the constructive interpretation of auxiliary formulas. I [MR0218236] (pp. 233–275).

This volume contains translations from the Russian of the following articles:
   Table of Contents: A. A. Markov, On constructive mathematics [MR0153564] (pp. 1–9); G. S. Ceĭtin, Mean value theorems in constructive analysis [MR0152427] (pp. 11–40); I. D. Zaslavskiĭ and G. S. Ceĭtin, On singular coverings and properties of constructive functions connected with them [MR0152428] (pp. 41–89); S. Ju. Maslov, Certain properties of E. L. Post's apparatus of canonical calculi [MR0204284] (pp. 91–161); I. D. Zaslavskiĭ, Graph schemes with memory [MR0205763] (pp. 163–288).

Soient f et g deux fonctions réelles constructives définies respectivement sur les segments [x1,x2], [y1,y2]. Soient α1=min(f(x1),f(x2)), α2=max(f(x1),f(x2)), β1=min(g(y1),g(y2)) et β2=max(g(y1),g(y2)). On démontre que si les intervalles (α1,α2), (β1,B2) ont des points communs alors on peut construire x dans [x1,x2] et y dans [y1,y2] tels que f(x)=g(y).

The objective of syntactic analysis, according to the author, is to determine for each word in a sentence which of its homonyms is appropriate for that sentence and whether the word is subordinate to any other word in the sentence (and, if so, to which). As a mathematical model for syntactic analysis suitable for computer implementation, the concept of admissible syntactic analysis, defined by a system of logical conditions on the homonyms and on the disposition of the words in the sentence, is introduced. In the present instance the conditions consist of the general projectivity conditions (in the sense of Fitialov) and special connectivity properties. An algorithm written in ALGOL 68 for reducing the analysis of a sentence to that of shorter strings is presented.

Der Autor beschreibt eine neue Methode zur Beurteilung der Rechenzeit eines Markovschen Algorithmus und beweist einen grundlegenden Satz über Zeitabschätzungen bei Markovschen Algorithmen. Wendet man einen Markovschen Algorithmus A auf ein beliebiges Wort PQ aus seinem Definitionsbereich an, so hängt jedes Endwort (und jedes Anfangswort) eines jeden Wortes der Abarbeitungsfolge in bestimmter Weise von P bzw. Q ab. Der Autor betrachtet Wahrscheinlichkeitsfelder auf endlichen Wortmengen und führt auf dieser Grundlage ein Maß für jene Abhängigkeit ein. Er nennt es Informationsmenge über P (bzw. über Q), die im betrachteten Endwort (bzw. Anfangswort) enthalten ist. Das genaue Studium dieser Informationsmengen ist grundlegend für den Beweis des folgenden, äußerst interessanten und sehr tiefliegenden allgemeinen Zusammenhanges (tA bedeutet die Abarbeitungszeit von A, |P| bedeutet die Länge des Wortes P; P~, Q~, K~ und L~ sind zufällige Wörter über einem Wahrscheinlichkeitsfeld auf einer endlichen Wortmenge): Ist die Wahrscheinlichkeit des Ereignisses "A(P~Q~)=K~L~∧tA(P~Q~)+|P~Q~|≤t0'' nicht kleiner als p0, so muß t0 größer als eine bestimmte, von p0, P~, Q~, L~, K~ abhängige Zahl sein. (Eine genauere Formulierung dieses Satzes würde zu umfangreiche definitorische Vorbereitungen erfordern.) Als Anwendung ergibt sich die folgende Übertragung eines von Barsdin für Turingmaschinen bewiesenen Sachverhalts auf den Fall Markovscher Algorithmen: Jeder Markovsche Algorithmus, der die Wortinversion realisiert, arbeitet mindestens mit quadratischer Zeit.

Der Autor beweist das folgende interessante Resultat, über das er bereits 1956 auf der 3. Sowjetischen Mathematikertagung berichtet hat. Es sei M ein Markovscher Algorithmus. Durch einführung von Hilfsbuchstaben (operatives Alphabet) kann ein zu M äquivalenter Markovascher Algorithmus N konstruiert werden, der folgende Eigenschaften hat: (1) Ist M auf das Wort p anwendbar, so enthält jedes Wort der Abarbeitungsfolge, die bei Anwendung von N auf p entsteht, mit Ausnahme des ersten und (evtl.) letzten Wortes genau einen Hilfsbuchstaben, und jeder Substitutionsschritt besteht darin, daß eine gewisse Umgebung dieses Hilfsbuchstaben verändert wird. (2) Bezeichnen tN(p) und tM(p) die Rechenzeiten der Algorithmen N und M bei Anwendung auf p und |p| die Länge des Wortes p, so gibt es Konstanten c1,c2,c3 mit tN(p)≤c1tM(p)+c2|p|+c3. Ferner gilt: Zu jedem ε>0 existiert ein zu M äquivalenter Markovscher Algorithmus N mit der Eigenschaft (1), für den die Zeitabschätzung tN(p)≤ε(tM(p)+|p|)+2 richtig ist.

Eine berechenbare Folge φ rationaler Zahlen heißt Pseudofundamentalfolge, wenn gilt Zwei berechenbare Folgen φ und ψ heißen äquivalent, wenn gilt ∀m¬¬∃n∀l(l>n→|φ(l)−ψ(l)|<2−m). Unter Benützung des Satzes von Friedberg und Mučnik, der die Existenz unvergleichbarer nichtrekursiver rekursiv aufzählbarer Turinggrade sichert, wird bewiesen, daß es Pseudofundamentalfolgen gibt, die im angegebenen Sinne zu keiner monotonen berechenbaren Folge äquivalent sind. Für diesen Sachverhalt wird ein zweiter Beweis angegeben, der den Satz von Friedberg und Mučnik nicht benützt.

The author studies bounded recursively enumerable sets M of rational numbers that do not have constructive least upper bounds (Specker's example) and for which there is a lowering algorithm that assigns to each upper bound of the set a smaller upper bound (Zaslavskiĭ's example). Conditions are found for the existence of a least upper bound for M and for the existence of a lowering algorithm. Among other things, it is shown that there is a bounded r.e. set M that has no constructive least upper bound and for which there exists no lowering algorithm. An essential pre-requisite for the reader is a knowledge of the terminology and results of the author's earlier paper [same Trudy 72 (1964), 69–98; MR0205842; for a translation see MR0321636 above].

Cover-to-cover translation of Volume 8 of Zap. Naučn. Sem. Leningrad. Otdel. Mat. Inst. Steklov. (LOMI).
   Table of Contents: G. V. Davydov, Some remarks on proof search in the predicate calculus [MR0277355] (pp. 1–6); O. Demuth, The Lebesgue integral and the concept of function measurability in constructive analysis [MR0240256] (pp. 7–10); O. Demuth, The relation between the Riemann integrability and Lebesgue integrability of constructive functions [MR0239018] (pp. 11–12); A. G. Dragalin, The computability of primitive recursive terms of finite type and primitive recursive realizability [MR0274280] (pp. 13–18); A. G. Dragalin, Word operator algorithms [MR0242675] (pp. 19–21); M. M. Kipnis, The constructive classification of arithmetic predicated and the semantic bases of arithmetic [MR0276088] (pp. 22–27); N. K. Kosovskiĭ, A system of operators simplifying the theory of combination of K-algorithms [MR0272629] (pp. 28–35); N. K. Kosovskiĭ, The construction of basic operators of the theory of combination of K-algorithms from operators of simple types [MR0272630] (pp. 36–42); B. A. Kushner [B. A. Kušner], Some examples of quasi-dense but not dense sets of duplexes [MR0302426] (pp. 43–46); B. A. Kushner [B. A. Kušner], Remarks on the domain of definition of constructive functions [MR0290967] (pp. 47–48); B. A. Kushner [B. A. Kušner] and G. S. Tseitin [G. S. Ceĭtin], Some properties of F-numbers [MR0238697] (pp. 49–55); V. A. Lifshits [V. A. Lifšic], Constructive analytic functions of one real variable [MR0281612] (pp. 56–60); Yu. V. Matiyasevich [Ju. V. Matijasevič], The connection between Hilbert's tenth problem and systems of equations between words and lengths [MR0246772] (pp. 61–67); Yu. V. Matiyasevich [Ju. V. Matijasevič], Two reductions of Hilbert's tenth problem [MR0246773] (pp. 68–74); Yu. V. Matiyasevich [Ju. V. Matijasevič], Arithmetic representations of powers [MR0238698] (pp. 75–78); G. E. Mints [G. E. Minc], Cut-free calculi of the S5 type (pp. 79–82); G. E. Mints [G. E. Minc], Implicative complexity of axiomatic systems [MR0277354] (pp. 83–85); G. E. Mints [G. E. Minc], Disjunctive interpretation of the LJ calculus [MR0280336] (pp. 86–89); G. E. Mints [G. E. Minc], Admissible and derived rules [MR0278900] (pp. 90–91); G. E. Mints [G. E. Minc], The independence of the postulates of natural calculi [MR0277357] (pp. 92–94); V. P. Orevkov, Glivenko classes of sequents [MR0270892] (pp. 95–97); V. P. Orevkov, Two undecidable classes of formulas in classical predicate calculus [MR0270893] (pp. 98–102); R. A. Plyushkevichus [R. A. Pljuškjavičjus], Kanger's variant of predicate calculus with symbols for functions that are not everywhere defined [MR0292642] (pp. 103–109); R. I. Freĭdzon, A definition of recursive-predicate complexity which does not depend on the standardization of the concept of algorithm [MR0272623] (pp. 110–114); G. S. Tseitin [G. S. Ceĭtin], On the complexity of derivation in propositional calculus [MR0280378] (pp. 115–125); G. S. Tseitin [G. S. Ceĭtin], The disjunctive rank of formulas in constructive arithmetic [MR0277385] (pp. 126–132); V. A. Shurygin [V. A. Šurygin], Complete constructive sets with equality and some of their properties [MR0252227] (pp. 133–135); Errata for Seminars in Mathematics, Vol. 4: Studies in constructive mathematics and mathematical logic, Part I [see MR0241253] (p. 136).
   {The translation of Part I has been reviewed [MR0241253].}

The first author proved [same Izv. 2 (1967), no. 2, 69–82; MR0216953] that in constructive mathematics for a plane curve x=K1(t), y=K2(t) to be rectifiable, it is necessary that K1 and K2 be of bounded variation, but that this condition is not sufficient. Here it is proved that it is sufficient that every linear combination uK1+vK2 is of bounded variation. In this case the length of the curve between a and b is given by 12∫π0h(φ)dφ, where h(φ) is the total variation of K1cosφ+K2sinφ between a and b. This formula is also remarkable from the classical point of view.

This article contains corrections to the following articles: G. V. Davydov, same Zap. 8 (1968), 8–20 [MR0277355]; A. G. Dragalin, ibid. 8 (1968), 46–52 [MR0242675]; N. K. Kosovskiĭ, ibid. 8 (1968), 66–79 [MR0272629]; N. K. Kosovskiĭ, ibid. 8 (1968), 80–94 [MR0272630]; V. A. Lifsič, ibid. 8 (1968), 121–131 [MR0281612]; R. A. Pljuškevičius [R. A. Pljuškjavičjus], ibid. 8 (1968), 221–224 [MR0292642]; R. I. Freĭdzon, ibid. 8 (1968), 225–233 [MR0272623]; G. S. Ceĭtin, ibid. 8 (1968), 234–259 [MR0280378].

This article contains corrections to the following articles: O. Demuth, same Zap. 4 (1967), 30–43 [MR0253899]; N. K. Kosovskiĭ, ibid. 4 (1967), 44–57 [MR0239975]; V. A. Lifšic, ibid. 4 (1967), 58–64 [MR0237293]; V. A. Lifšic, ibid. 4 (1967), 69–77 [MR0237314]; S. Ju. Maslov, ibid. 4 (1967), 96–111 [MR0245428]; R. A. Pljuškevičius [R. A. Pljuškjavičjus], ibid. 4 (1967), 174–188 [MR0237295]; M. G. Rogava, ibid. 4 (1967), 189–200 [MR0239939]; R. I. Freĭdzon, ibid. 4 (1967), 209–218 [MR0238703]; A. G. Dragalin, ibid. 8 (1968), 32–45 [MR0274280]; G. S. Ceĭtin, ibid. 8 (1968), 234–259 [MR0280378].

The author deals with the question of minimal complexity of a deduction of the given formula in classical propositional calculus and proves that for different versions of propositional calculus these estimates may vary essentially. He considers the version of classical propositional calculus A based on the resolution principle [see J. A. Robinson, J. Assoc. Comput. Mach. 12 (1965), 23–41; MR0170494].
   The parameters characterizing the complexity of a deduction in calculus A are introduced, and the interconnection between these parameters is defined. Further, the author gives a way of establishing the connection between these parameters and characteristics of deductions in propositional calculus in a sequential form.
   In the final part of the article he considers estimates for systems of disjunctions, which are compared with connected non-oriented graphs, and gives estimates for concrete graphs.

In the work under review a negative answer is given to the following question of M. M. Kipnis [same Zap. 8 (1968), 53–65; MR0276088]: Is the alphabet C={∀,&,∨,⊃,¬} a semantical basis for arithmetic, i.e., can we find for any arithmetical predicate an arithmetical predicate equivalent to it whose logical symbols belong to C? Moreover, it is proved that disjunctions with a large number of members are "irreplaceable'' in a certain sense.
   The disjunctive rank of a formula of constructive logical-arithmetical calculus is defined by recursion on the logical length in the following way: δ(A)=1 if A is an elementary formula δ(¬A)=1; δ(A∨B)=δ(A)+δ(B); δ(A & B)=max(δ(A),δ(B)); δ(A⊃B)=δ(B); δ(∀xA)=δ(A); δ(∃xA)=∞. Theorem: For every r (1≤r≤∞) one can construct a formula of disjunctive rank r that is not equivalent to any formula of lower disjunctive rank.
   The desired formulas are: for r=∞, the formula ∃y¬U(x,x)=y, and, for r<∞, the formula where U is the universal function for one-place partial-recursive functions. Finally the author points out a new class of formulas, which are realizable but not deducible, in intuitionistic formal systems.

The authors prove the following results about the constructive real numbers called F-numbers and FR-numbers by N. A. Šanin [Trudy Mat. Inst. Steklov. 67 (1962), 15–294; MR0156786]. Theorem 1 (Ceĭtin): If A is an algorithm mapping each F-number into an FR-number, then one can construct an F-number which is a fixed point of A. Theorem 2 (Kušner): There is no algorithm transforming the transcription of each fundamental sequence of F-numbers into an F-number to which the sequence converges. Theorem 3 (Kušner): One can construct an algorithm transforming every word of the form {}^{\ulhook}_{\tsize\lhook}\lambda{}^{\urhook}_{\tsize\rhook}
\square{}^{\ulhook}_{\tsize\lhook}\delta{}^{\urhook}_{\tsize\rhook}, where λ is a sequence of F-numbers and δ is a regulator of convergence of λ, into an F-number to which λ converges.

The constructive direction in mathematics (CDM) (as this school of thought calls itself), to which the authors have copiously contributed, has developed a variant of analysis that differs not only from classical analysis but also from other constructive attempts at doing analysis—above all in the stringency of its demands for rigor. {The full story of this school is told in Volumes 42, 52, 67, and 72 of Trudy Mat. Inst. Steklov. with a most formidable apparatus of esoteric conventions and notations.}
   The present survey succinctly, but very readably, summarizes the characteristic assumptions, procedures, and results of CDM in a way that the layman can understand and appreciate. In fact, the emphasis on the essentials, and the precise reference to the locus classicus of each major result should make the paper valuable to the specialist, too.
   "... in general these differences between classic and constructive analysis usually appear in problems remote from concrete computation. The nearer we come to concrete computational problems the less are the differences.... In some cases the difference... warns us that the classic theorem suggests an incorrect formulation of the computational problem, i.e., an algorithm with the properties suggested by the classic formulation proves to be impossible.... On the other hand, because of unrestricted use of potential realizability this approach is inadequate for problems of computation within given time and given memory capacity. This is of course a subject of special theories and perhaps also of some kind of `hyper-constructive' analysis still to be created.''
   {This article is also available in American Mathematical Society Translations, Ser. 2, Vol. 70, pp. 16–25, Amer. Math. Soc., Providence, R.I., 1968 [see MR0225620].}

Let E be a linearly ordered set. The paper defines a D-tree to be a tree whose nodes are elements of E. A D-tree is projective if the set of nodes of the tree is a segment of E. Let S be a collection of subsets of E with the two properties (1) S contains E and all single elements of E, (2) if two sets in S intersect, then one is contained in the other. A P-tree is a tree whose nodes are elements of S with E as the root and single element subsets as pendant nodes. Node X is a direct descendant of Y if X⊂Y and if for no Z in S is X⊂Z⊂Y. A P-tree is continuous if each X∈S is an interval in E.
   Asymptotic formulas are obtained for the number of trees with n nodes. For arbitrary D-trees and p-trees the formulas are nn−1 and a constant times (kn)n/n, k≈0.95, respectively. For projective D-trees and continuous P-trees, the formulas have the asymptotic form of a constant times Rn/n3/2, where R equals 6.75 for D-trees and approximately 5.83 for P-trees. Width, depth and degree of nesting are defined. (Depth as used in the paper is not the length of the longest path.) Applying restrictions on width, depth or degree of nesting results in formulas of the form a constant times naRm7, where m is the value of the restricted quantity and a and Rm>1 are constants.

The paper belongs to constructive mathematics in the sense of Markov. (1) Definition of a constructive function of a real variable, which is defined at 0, but in no neighbourhood of 0. Such a function was first defined by Mučnik (unpublished); here a simpler example is given by a construction analogous to one used by R. M. Friedberg [C. R. Acad. Sci. Paris 247 (1958), 852–854; MR0099919]. (2) Every constructive function of a real variable is the limit of a constructive sequence of polygonal functions with rational vertices. (3) Let f and g be constructive functions of a real variable whose domains have a common point and such that f(x)<g(x) for every x where both are defined. There is a pseudo-polygonal function φ such that f(x)<φ(x)<g(x) for every x where f and g are defined. (A function is called pseudo-polygonal if it is the union of a sequence of compatible polygonal functions, each defined on an interval.)

Recursively enumerable sets are defined in such a way that the resulting theory is, according to the author, more convenient for various theoretical applications (for example, for the verification in constructive analysis that certain processes can be carried out by normal algorithms). Given a basic finite alphabet A, define O to be {Λ}, where Λ is the empty word, and define, for any letter ξ, the relation Rξ to be the set of all pairs of words in A of the form (P,Pξ). The recursively enumerable relations are those relations obtainable from O and the Rξ by (i) finite unions and intersections, (ii) permutations of two components, (iii) projections, (iv) geometric products (i.e., from (X1,⋯,Xm)∈A and (Y1,⋯,Yn)∈B, derive (X1,⋯,Xm,Y1,⋯,Yn)∈A×B), and (v) transitive closure * (i.e., given a relation A on 2m-tuples of words, take the closure A∗ of A under the rule which, from (X1,⋯,Xm,Y1,⋯,Ym)∈A∗ and (Y1,⋯,Ym,Z1,⋯,Zm)∈A, yields (X1,⋯,Xm,Z1,⋯,Zm)∈A∗). All notions are interpreted in a constructive way. Computable operators on sets are also introduced and briefly studied.

Given, a logico-mathematical language L and a basic set A in this language, in the sense of N. A. Šanin [same Trudy 52 (1958), 226–311; MR0101189]. Extend L to L′ by adding restricted individual variables ranging over the set of words in A. The set A is said to be compatible with the principle of constructive selection (briefly, compatible) if every formula of L′ of the form where α is one of the new variables, is constructively true. A set B is called infinite if there is no finite sequence containing all elements of B. It is proved that every infinite compatible set is recursively enumerable, and hence that every non-recursively enumerable set is not compaible. But it is also shown that it is not true (in the constructive sense) that every compatible set is recursively enumerable.

Die vorliegende Arbeit geht aus von der Tatsache, daß in der konstruktiven Analysis von A. A. Markov [dieselben Trudy 52 (1958), 315–348; MR0098676], Šanin [ibid. 67 (1962), 15–294] und Zaslavskiĭ [ibid. 67 (1962), 385–457; MR0153555] der Überdeckungssatz von Borel nicht gilt, d.h. man kann zu jedem konstruktiven Intervall eine konstruktive Überdeckungsfolge von Intervallen angeben, so daß keine endliche Teilmenge dieser Folge das gegebene Intervall überdeckt. Es wird zunächst gezeigt, daß man sogar eine Überdeckungsfolge finden kann, bei der die Summe der Längen einer beliebigen endlichen Teilmenge von Intervallen kleiner als eine beliebig vorgegebene positive Zahl ist. Überdeckungen dieser Art werden singulär genannt. Mit ihrer Hilfe werden eine Reihe von Beispielen für konstruktive Funktionen mit interessanten Eigenschaften konstruiert. So wird unter anderem folgendes bewiesen: (1) Es können zwei auf einem Intervall monotone konstruktive Funktionen realisiert werden, deren Differenz keine Funktion beschränkter Variation (im Sinne der konstruktiven Analysis) ist (ein ähnliches Resultat wurde von Lacombe [C. R. Acad. Sci. Paris 244 (1957), 838–840; ibid. 244 (1957), 996–997; MR0088456] formuliert, wobei jedoch ein anderer Begriff von konstruktiver Funktion verwendet wurde). (2) Man kann eine konstruktive Funktion mit beschränkten Variationssummen angeben, die nicht gleichmäßig stegit ist. (3) Es läßt sich eine gleichmäßig stetige konstruktive Funktion mit beschränkten Variationssummen realisieren, die sich (im Sinne der konstruktiven Mathematik) nicht als Differenz zweier monotoner Funktionen darstellen läßt. (4) Es läßt sich eine konstruktive Funktion realisieren, die auf keinem Intervall gleichmäßig stetig ist. (Es sei hier bemerkt, daß die gleichmäßig stetigen konstruktiven Funktionen der vorliegenden Theorie im wesentlichen mit den konstruktiven Funktionen von Goodstein [Proc. London Math. Soc. (2) 52 (1950), 81–106; MR0040250] äquivalent sind.) (5) Es läßt sich eine konstruktive Funktion angeben, die bezüglich keines Integrals, das gewisse Axiome erfüllt, integrierbar ist (insbesondere ist diese Funktion nicht Riemann-integrierbar und hat keine Stammfunktion).

The author considers constructive versions of the following five theorems of classical real analysis: (1) every sequence of nested intervals contains a point; (2) a continuous function which takes values of both signs in an interval has a zero there; (3) a continuous function takes in an interval every value between its values at the end points; (4) Rolle's theorem; (5) the first mean-value theorem. For the notion of constructive real number used see the preceding review [MR0152426]; it is important to remember that it is a computably convergent sequence of rationals together with its modulus of convergence. He shows that all of these are false in the sense that there is no algorithm for constructing a point satisfying the conditions from the given data (i.e., in (1) from the sequence of intervals, in (2) the function and the end points of the interval, in (3) the given value (i.e., constructive version false even with a suitable fixed function and end points), in (4) the given function, (5) the end points of the segment). However, none of them can be refuted by counter-examples for they are true in the sense that a point (constructive real number) satisfying the conditions does exist in each case; indeed, in each case a computably convergent sequence of rationals corresponding to the point can be constructed, but not the corresponding modulus of convergence. Full proofs of these and many subsidiary results are given.

This paper consists of extremely detailed proofs of theorems whose proofs were very briefly indicated in the author's earlier paper [Dokl. Akad. Nauk SSSR 128 (1959), 49–52; MR0115910]. There they were stated in the language of partial recursive functions, but here the treatment uses Markov algorithms throughout. The basic theorem is on the constructive uniform continuity of constructive mappings between constructive metric spaces and is applied to Theorems 1 and 2 on the relation between effective operations on general recursive functions and partial recursive functionals, and to Theorems 3 and 4 on the continuity and approximability by polygons of constructive functions of computable real numbers. Theorem 2 implies the result proved independently by Kreisel, Lacombe and Shoenfield [C. R. Acad. Sci. Paris 245 (1957), 399–402; MR0088457] that every effective operation which sends general recursive functions (GRF) into GRF coincides on the set of GRF with some partial recursive functional; the basic theorem is essentially a generalisation of Theorem 2. Theorem 3 strengthens the theorem of Markov [Trudy Mat. Inst. Steklov. 52 (1958), 315–348, § 5.5.1; MR0098676].
   The computable real numbers are here introduced as (computable) duplexes: an algorithm B of type (N→N) (i.e., sending words which stand for natural numbers into words of the same form) is called a modulus of convergence for an operator A of type (N→R) (R= rational numbers) if |A(n2)−A(n3)|<2−n1 for all n1,n2,n3 such that n2,n3≥B(n1); a duplex is either a rational number or a word of the form H◊H1, where H is a word for an algorithm A of type (N→R) and H1 a word for an algorithm B of type (N→N) which is a modulus of convergence for A. A constructive metric space is a set A of words on an alphabet A (not containing the sign □) and an algorithm ρ such that (1) for any pair of elements P,Q of A the algorithm ρ is applicable to the word P□Q and ρ(P□Q) is a duplex; (2) for all P of A ρ(P□P)=0; (3) for all P,Q,R of A ρ(P□Q)≤ρ(P□R)+ρ(Q□R). Two elements P,Q of A are called equivalent if their distance ρ(P□Q)=0. A sphere of A is a word of the form P□n where P∈A; a point Q of A is said to belong to this sphere if ρ(Q□P)<2−n. A constructive sequence of elements of A is an algorithm ϕ sending every natural number into an element of A; it is called regularly convergent if for all m,n with m≤n, ρ(ϕ(m)□ϕ(n))<2−m. A is called complete if there exists an algorithm γ such that, for every regularly convergent sequence ϕ of A and for all m,γ sends the word for ϕ into an element of A within distance 2−m of ϕ(m). A is called separable if there is a constructive sequence β of elements of A and an algorithm α which sends each sphere S of A into a natural number α(S) such that β(α(S))∈S. An algorithmic operator from a constructive metric space A to another B is an algorithm Ψ such that (1) for all P in A if Ψ(P) is defined and ∈B; (2) for all P,Q of A if P,Q are equivalent in A and Ψ(P) is defined, Ψ(Q) is defined and equivalent to Ψ(P) in B.
   Basic theorem: Let Ψ be an algorithmic operator from a complete separable constructive metric space A to a constructive metric space B. Then one can construct algorithms σ and τ such that (1) for all m,n if σ(m□n) is defined, it is a sphere of A; (2) if τ(m□n) is defined and ∈B; (3) for all m,n and P∈A, if σ(m□n) is defined, P∈σ(m□n) and Ψ(P) is defined, then τ(m□n) is defined and is within distance 2−m of Ψ(P), (4) for all P∈A and all m if Ψ(P) is defined there exists n such that σ(m□n) is defined and P∈σ(m□n). (In other words, there is for each m a recursively enumerable set of spheres which cover the domain of definition of Ψ each of which is mapped into a sphere of radius 2−m.)
   Theorem 1: For every effective operation Ψ sending GRF1 (general recursive one-place functions) into natural numbers there exists a partial recursive functional F such that if {k} is GR and Ψ(k)=m, then F({k})=m. Theorem 2: For every effective operation Ψ sending GRF1 into PRF there exists a partial recursive functional F such that if {k} is GR and {ψ(k)}(m)=n, then F({k})(m)=n. The author remarks that Muchnik has pointed out to him {and Friedberg [C. R. Acad. Sci. Paris 247 (1958), 852–854; MR0099919] has published a counter-example} that these can not be strengthened to have "if and only if'' in the conclusions, which answers negatively a question of Myhill and the reviewer [Z. Math. Logik Grundlagen Math. 1 (1955), 310–317; MR0077475]. Theorems 1, 2 have also been given by Kreisel, Lacombe and Shoenfield [Constructivity in Math. (Proc. Colloq. Amsterdam, 1957), pp. 290–297, North-Holland, Amsterdam, 1959; MR0108443; Summer Institute for Symbolic Logic (Cornell Univ., Ithaca, N.Y., 1957), Summaries, pp. 364–365, Inst. for Defense Analyses, Princeton, N.J., 1960]. In comparing the two versions note that although Ceĭtin does not insist that Ψ be defined for all k such that {k} is a GRF1, his definition of effective functional (operator) ensures that ψ(k)≃ψ(l) ({ψ(k)}(m)≃{ψ(l)}(m)) for all k,l such that {k}, {l} are equal GRF1, and the proofs of KLS go through under these conditions. Theorem 3: For each constructive function Ψ (arguments and values constructive real numbers, i.e., duplexes) there exists an algorithm ω such that, for arbitrary x,m, if Ψ(x) is defined, then ω(x□m) is defined and is a natural number such that for all y if |y−x|≤2−ω(x□m) and Ψ(y) is defined, then |Ψ(y)−Ψ(x)|≤2−m. Theorem 4: If Ψ is a constructive function and Ψ(x) is defined for at least one x, then for arbitrary m one can construct a pseudopolygonal function Ψ∗ (a sort of constructive limit of polygonal functions) such that for all x if Ψ(x) is defined, then Ψ∗(x) is defined and |Ψ(x)−Ψ∗(x)|<2−m.