Published online by Cambridge University Press: 12 March 2014
Consider a system of formal notations for ordinal numbers in the first and second number classes, with the following properties. Given a notation for an ordinal, it can be decided effectively whether the ordinal is zero, or the successor of an ordinal, or the limit of an increasing sequence of ordinals. In the second case, a notation for the preceding ordinal can be determined effectively. In the third case, notations for the ordinals of an increasing sequence of type ω with the given ordinal as limit can be determined effectively.
Are there systems of this sort which extend farthest into the second number class? When the conditions for the systems have been made precise, the question will be answered in the affirmative. There is an ordinal ω1 in the second number class such that there are systems of notations of the sort described which extend to all ordinals less than ω1, but none in which ω1 itself is assigned a notation.
1. An effective or constructive operation on the objects of an enumerable class is one for which a fixed set of instructions can be chosen such that, for each of the infinitely many objects (or n-tuples of objects), the operation can be completed by a finite process in accordance with the instructions. This notion is made exact by specifying the nature of the process and set of instructions. It appears possible to do so without loss of generality.
1 A closely related result, and a discussion of the significance of these questions of notation, are given in Church, Alonzo, The constructive second number class, Bulletin of the American Mathematical Society, vol. 44 (1938), pp. 224–232CrossRefGoogle Scholar. The ordinal ω1 is the least ordinal not represented by formulas in the λ-notation, Church, Alonzo and Kleene, S. C., Formal definitions in the theory of ordinal numbers, Fundamenta mathematicae, vol. 28 (1936), pp. 11–21, Rules i–ivGoogle Scholar.
2 Gödel, Kurt, On undecidable propositions of formal mathematical systems, mimeographed lecture notes, Princeton 1934, pp. 26–27Google Scholar; Kleene, S. C., General recursive functions of natural numbers, Mathematische Annalen, vol. 112 (1936), pp. 727–742CrossRefGoogle Scholar.
This notion of effectiveness appears, on the following evidence, to be general. A variety of particular effective functions and classes of effective functions (selected with the intention of exhausting known types) have been found to be recursive. Two other notions, with the same heuristic property, have been proved equivalent to the present one, viz., Church-Kleene λ-definability and Turing computability. Turing's formulation comprises the functions computable by machines. See Kleene, S. C., λ-definability and recursiveness, Duke mathematical journal, vol. 2 (1936), pp. 340–353CrossRefGoogle Scholar, and Turing, A. M., On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, vol. 42 (1936–1937), pp. 230–265Google Scholar, and Computability and λ-definability, this Journal, vol. 2 (1937), pp. 163–163Google Scholar. Functions determined by algorithms and by the derivation in symbolic logics of equations giving their values (provided the individual steps have an effectiveness property which may be expressed in terms of recursiveness) are recursive. See Church, Alonzo, An unsolvable problem of elementary number theory, American journal of mathematics, vol. 58 (1936), pp. 345–363CrossRefGoogle Scholar, where it was first proposed to identify effectiveness with recursiveness. Church's remarks should be generalized in one particular, as will appear in Footnote 3.
3 This condition is more general than potential recursiveness (An unsolvable problem of elementary number theory, p. 352). For there are functions f(x 1, …, xn) not equal throughout their range of definition to any recursive function, e.g., üyT 1(x, x, y), where ü is defined below, it being noted that the number f in General recursive functions of natural numbers, proof of Theorem XIV, belongs to the range of definition of üyT 1(x, x, y). The condition is more general than partial recursiveness, since a partial recursive function has a range of definition of a special form, (Ey)Tn(e, x 1, …, xn, y).
4 For details, see General recursive functions of natural numbers. Dr. Barkley Rosser has called my attention to an error in No. 17, p. 733, which is corrected by reading
5 There is also a partial recursive function ry (r)R(, y) of which, for each fixed , takes as value a y such that R(, y) is true, provided such a y exists (whether or not R(, y) is defined for all the preceding values of y), and is undefined otherwise. For let r be a number defining recursively the function corresponding to R(, y), and set ry(r)R(, y) ≃ 1 Gl üw(Tn(r, , 1 Gl w, 2 Gl w) & S(r, 2 Gl w) = 0).
6 Loc. cit. Proof of some remarks which follow may be based on λ-definability and recursiveness.
7 At this point, the analogy between the two systems is improved by writing {z}(x 1, …, xn) or z(x 1, …, xn) as an abbreviation for Φn(z, x 1, …, xn). Then ϕ(x 1, …, xn) is expressible as e(x 1, …, xn), where e is a number defining ϕ recursively. The use of the numbers e rather than the functions ϕ conforms to the finitary standpoint. For only the numbers e (or the systems of equations E) are given directly, and there is no effective decision in general whether two e's (or two E's) define the same function.
8 The constructive second number class. Stated by Church for the system of formulas in the λ-notation.
9 The writer does not know whether any one univalent r-system contains notations for all the ordinals < ω1, as is the case for multivalent r-systems. It is possible to describe non-constructively an r-subsystem of S 2 simply ordered by the relation <∘, which assigns a number to each ordinal < ω2, and which does not admit of extension to ω2 preserving the simple ordering.