10 S. Mazurkiewicz: Wir haben demnach folgenden Hilfssatz bewiesen: Hilfssat». Sei M„-■> Xm-m{l) 8„ -> Xam-m(2, a). L ->Xarm-m{3,a,r). 1„ ->«„(()„), 20->fl8(l„), etc. The formulas ()„, 1„, 2„, ... are taken to represent the finite ordinals. Here we are using the subscript o to distinguish notations used in connection with the present theory from like notations used in other connections. When the context precludes ambiguity, we may omit this subscript o, writing for instance «+2 instead of w+02„ (of. §4 below). We adopt the following rules for the assignment of formulas to represent particular ordinals of the first and second number classes: i. If a represents the ordinal a, and 6 conv a, then b also represents a. ii. ()„ represents the ordinal zero. iii. if a represents the ordinal a, .then B„{a) represents the successor of a. A. Church and S. G. Kleene: Formal definitions 15 iv. If b is the limit of an increasing sequence (series) of ordinals, b &!, &2,of order type w, and if »" is a formula such that the formulas r(0o), r(l0), r(20),... represent the ordinals b0, &„ 68, respectively, then L{Oa,r) represents 6. Since one of the formulas assigned by these rules to represent the least ordinal —>L(0„, I). We shall call an ordinal of the first or second number class formally definable, or ^-definable, if there is, under Rules i—iv, at least one formula assigned to represent it. From the possibility under iv of using different sequences for any particular b (or of using different J''s for any particular sequence) it follows that every formally definable ordinal of the second number class has an infinite number of non-interconvertible formulas assigned to represent it. We shall say that a sequence of ordinals of order type a> is formally defined as a function of ordinals by r if, for every formula a which represents a finite ordinal a, r(a) represents the (l+a)th ordinal of the sequence. It is clear that the question what ordinals of the second number class are formally definable is tied up with the question what sequences of ordinals are formally definable as functions of ordinals, in such a way that neither question can be regarded as prior to the other. From Theorem 2 below and the enumerability of the set of all well-formed formulas, it follows (by a non-constructive argument) that the set of all formally definable ordinals is enumerable, and hence that there is a least ordinal f in the second number class whicli is not formally definable. It is then readily proved that no ordinal in the second class greater than % is formally definable. It is to be emphasized, however, that the definition of £ which has just been given is not constructive, in any usual sense of that term, and that no means is known, to the authors of obtaining constructively an ordinal of the second number class which is not formally definable. In particular, it will be shown below that, if a and b are formally definable ordinals out of the first and second number classes, then the sum of a and b, the product of a and b, and the result of raising a to the power b are formally definable, and hence all ordinals less than e0 are formally definable Moreover, if a is formally definable, then f„ is formally definable, and hence it foUows that all ordinals less than the least solution of ex=x are formally definable. Similar theorems can be estabbshed in which various generalizations of the f-numbers4) appear. Thus the boundary of ordinals in the second number class known to be formally definable is continually pushed upwards, and no constructively obtainable bmit to this process is seen. We prove the two following theorems by transfinite induction. Theorem 1, Every formula which represents an ordinal number under Rules i—iv has a normal form. Any formula which represents the ordinal zero must be convertible into 0o and hence has the normal form 0„. Suppose that every formula which represents an ordinal less than b has a normal form. If b is the successor of an ordinal a, any formula which represents 6 must be convertible into S0(a), where a represents a, and hence must have the normal form lm-m{2, A), where A is the normal form of a. If b is the limit of an increasing sequence of ordinals of order type a», any formula which represents b must be convertible into £(0o, r), where tbere is some increasing sequence of ordinals of order type a> which has b as its bmit and which is formally defined as a function of ordinals by >'; moreover r must have a normal form It, because otherwise r(Q0) would lack a normal form6), and hence L(0o, r) must have the normal form 2m-m(3, 0„, It). Theorem 2. If, under Rules i—iv, a formula b represents an ordinal b, then b cannot represent an ordinal distinct from b. The theorem is true if b is zero, because b then has im-w(l) as a normal form, and formulas whicb represent ordinals distinct from zero have a normal form of one of tbe forms, Am-m(2, A), or Am-m(3, 0o, H), and hence cannot have Am-m(l) as a normal form6). We proceed by induction with respect to b. 4) Cf. 0. Veblen, Continuous increasing functions of finite and transfinite ordinals, Trans. Amer. Math. Soc, vol. 9, 1908, pp. 280—-292. AH the particular ordinals defined by Veblen in this paper are formally definable in our present sense, including the ordinals E(l), E(2), and even the first (second, and so on) solutions of the equation f(li,...,ltc)=a, page 292. B) Church and Rosser, Thm. 2 Cor. 6) Church and Rosser, Thm. I Cor. 2. 16 A. Church and S. C. Kloene: ■cm H b is the successor of an ordinal a, then h is not the limit, of any increasing sequence of ordinals and is not, the successor of any ordinal other than a, and consequently ft must have a normal form lm-m(2,A where A represents a, Therefore") every normal form of b must be of the form Xn-n{%,A'\ whore ^conv2 and J'convJL (being the same formulas except for possible alphabetical differences of bound symbols). Therefore ft can represent only a successor of an ordinal represented by A. By hypothesis of induction, A cannot represent an ordinal distinct from a. Therefore ft cannot represent an ordinal distinct from b. If 6 is the limit of an increasing sequence of ordinals of order type a, then b is not the successor of any ordinal, and consequently ft must have a normal form Am-m(3, 0„, It), where .it formally defines as a function of ordinals an increasing sequence of ordinals of order type co which has b as its limit. Therefore«) every normal form of 6 must be of the form Xn-n{3, 0,lt'), where # cony 3, Oeonv 0„, R' conv B. Therefore ft can represent only a limit of an increasing sequence of ordinals which is formally defined as a, function of ordinals by B. But it follows from the hypothesis of induction that It can define only one increasing sequence of ordinals of order type w. Therefore ft can represent only b. 3. We shall call a function a junction in the first and ftecond number classes it the range of the independent variable (or of each independent variable) consists of the first and second number classes and the range of the dependent variable is contained in the first and second number classes. We shah say that a function /, of n variables, in the first and second number classes, is formally defined by a formula / if, for every set of n formulas xt, x-2, xn which represent ordinals respectively, in the first and second number classes, /(ccj, x2,xa) is a formula which represents the ordinal f{$\, *2,m„). We shall call a function / in the first and second number classes formally definable, or X-definable, if there is at least one formula / by which it is formally defined. We remark that if a formula/is to define (formally) a function, of n variables, in the first and second number classes, not, only must f{Xi,X2, ...,xn) represent an ordinal in the first and second number classes for every set of n formulas X\,x.l}x„ which represent ordinals in the first and. second number classes, but also, if U\, ill, //« Formal definitions 17 are formulas which represent ordinals equal respectively to the ordinals represented by xh xi} x„, then f{yh y2, yn) must represent an ordinal equal to the ordinal represented by f(x,, x2, xn). It is clear that any function in the first and second number classes which is formally definable must be in a certain sense constructive, because given a formal definition of the function, the process of reduction to normal form provides an algorithm for calculating the values of the function (provided that we consider an ordinal to have been calculated if a formula in normal form which represents it has been obtained). Therefore certain functions which are not constructive in this sense are clearly not formally definable; in particular, the function /, such that f{x, y) is equal to the ordinal zero or the ordinal one according to whether the ordinals x and y are equal or distinct, is not formally definable 7). It is conjectured, however, that every constructive function in the first and second number classes is formally definable. This conjecture is vague because of the lack of a satisfactory definition of the notion of a constructive function of ordinals, but it is supported by analogy with the case of functions of positive integers, where it is possible to give a plausible definition of eonstructivity and to prove the equivalence of eonstructivity and -l-definabihty8). 4. We proceed now to the proof of a theorem which is useful in many particular cases where it is required to obtain a formal definition of some given function in the first and second number classes. Theorem 3. If A, G- and H are given formulas having no free symbols, it is possible to find a set of eight formulas (where the subscripts i, j, Tc take the values 1 and 2) satisfying the following conditions: A/*(0o) conv A fnik(80(a)) conv G(a) ftjx{L(a, r)) conv H(a, r) A/a(0„) ocmvA{fm) fnk(8o{a)) conv G(ftii, a) fm(L{a, r)) conv M{fm, a, r). ') The full proof of this assertion makes use of the results of Church, An umolvable problem of elementary number tlieory. B) See Church, An unsohable problem of elementary number theory, and S. C. Kleene, ^-definability and reeursivenep^arthoommg (abstract in Bull. Amer. Math. Soc, Vol. 41, 1933, No. 7). /jj i y> Kumliummta MaUiomntioac. T. XXVIII. ■ 18 A. Church and S. 0. Kleene: Iran This theorem is to be understood, to mean, not merely that the formulas /»,* "exist", but that means are at hand by which they can be effectively obtained in any given ease. In order to construct the formulas fm we proceed as follows. We let, d^Afb-bd, /), ]->f(«, t>). Likewise we may obtain a formula f such that f(0„) convl, f{80(a)) conv f(a), and f(X(a, *•)) convf(a, f(*'(0o))). Then, by transfinite induction, if a represents an ordinal, f(a)convI. Hence a constancy function, K„, of ordinals may be defined by letting, K0^Xxy-f(y,x). If b represents an ordinal, K„{a, b) conv a. Likewise we may obtain a formula f such "that f(0o)convif„(0„), f(30(a)) convAx-f (a,cc)-\-0x, and f(L(a,v))conyXx-L(a,Xm-f(r(m),oi!)). Then, if a and b represent ordinals a and 6 respectively, f(a, b) represents the product of a and 6 (with a as multiplier and b as multiplicand). Hence we let, [«]x0[6]->f(ff, b) The expression [a]x„[ft] may be abbreviated as [>][*>], when no ambiguity arises thereby. Similarly, we may obtain a formula f such that f (0„)convJ£„(lo), f(So[a))oomrZx-xx0f(a,x), and f{L{a,r))aQmXx-L{a,lm-f(r{m),«i)). Formal definitions 19 Then, if a and b represent ordinals a and b, f(a, b) represents the result of raising b to the power a. Hence we. let, exp0-^>toy-f(y, x) and in any case where no confusion with exponentiation of positive integers, or other forms of exponentiation, is produced, we abbreviate exp0(6, a) as« [6]W. A predecessor function of ordinals is formally defined by a formula Pa chosen to satisfy the relations 9) Po(0o) conv O0, P0{80{a)) conv a, and P0(L(a, r)) conv£(a, r). Let % be so chosen that g(0o) conv O0, ff(S0(a)) conv $(a)> and 5(£(a, **)) convK0(l0, L(a,r)).. Then, if a represents an ordinal a, ifi convertible into O0 or 10 according as a is finite or infinite. Choose 5? so that S?(0o) conv O0, R(30(a)) conviT0(l0, a), and j?|L(a, r)) conv K0{20, L{a, »•)). Then formally defines the fcm3(n, exp0 (w), O0)), e(fl0(a))conv.L(Oo,Xn-3(n,exp„(L(a, I). Moreover, using Theorem 3, we may find a formula o such that o(0o) conv L(00,1), o(8a[a)) conv L(l0+Oa, I), and o(L(a,r)) convi(a, An-L(r[n),I)), and so obtain a set of ordinals co„ defined formally by g>ft->. o(a). It can be proved, by a non-constructive argument, that all the ordinals aa are contained within the second number class, nevertheless there is an analogy between these ordinals cj„ and the first ordinals of the successive number classes, in which the notion of /l-defmability corresponds, in general, to the notion of existence. In particular, Q, the first ordinal of the third number class, can be described as the least ordinal of the second kind which is not the limit of an increasing sequence of ordinals of order type a. Correspondingly, a1 is the least ordinal of the second kind which is not the bruit of a 2-definable increasing sequence of ordinals of order type w. In fact, if we are willing to take the position that an ordinal less than w1 is not constructively calculated unless a formula representing it is constructively calculated, then we may regard an infinite sequence of ordinals (of order type a) as constructive if some function / such that f(n) is the Godel representation of a formula representing the nfh ordinal of the sequence is effectively calculable in the sense of Church, An unsolvable problem of elementary number theory, and hence conclude, by use of 3 and of Kleene, X-definability and recursiveness, (25), that g)x is not the limit of any constructive increasing sequence of ordinals of order type w.