ordinal logic any means of associating effectively and uniformly a logic (in the sense of a formal axiomatic system) Sa with each constructive ordinal notation a. This notion and term for it was introduced by Alan Turing in his paper ‘Systems of Logic Based on Ordinals’ (1939). Turing’s aim was to try to overcome the incompleteness of formal systems discovered by Gödel in 1931, by means of the transfinitely iterated, successive adjunction of unprovable but correct principles. For example, according to Gödel’s second incompleteness theorem, for each effectively presented formal system S containing a modicum of elementary number theory, if S is consistent then S does not prove the purely universal arithmetical proposition Cons expressing the consistency of S (via the Gödelnumbering of symbolic expressions), even though Cons is correct. However, it may be that the result S’ of adjoining Cons to S is inconsistent. This will not happen if every purely existential statement provable in S is correct; call this condition (E-C). Then if S satisfies (E-C), so also does S; % S ! Cons; now S; is still incomplete by Gödel’s theorem, though it is more complete than S. Clearly the passage from S to S; can be iterated any finite number of times, beginning with any S0 satisfying (E-C), to form S1 % S;0, S2 % S;1, etc. But this procedure can also be extended into the transfinite, by taking Sw to be the union of the systems Sn for n % 0,1, 2 . . . and then Sw!1 % S;w, Sw!2 % S;w!1, etc.; condition (E- C) is preserved throughout. To see how far this and other effective extension procedures of any effectively presented system S to another S; can be iterated into the transfinite, one needs the notion of the set O of constructive ordinal notations, due to Alonzo Church and Stephen C. Kleene in 1936. O is a set of natural numbers, and each a in O denotes an ordinal a, written as KaK. There is in O a notation for 0, and with each a in O is associated a notation sc(a) in O with Ksc(a)K % KaK ! 1; finally, if f is a number of an effective function {f} such that for each n, {f}(n) % an is in O and KanK < Kan!1K, then we have a notation ø(f) in O with Kø(f)K % limnKanK.
For quite general effective extension procedures of S to S; and for any given S0, one can associate with each a in O a formal system Sa satisfying Ssc(a) % S;a and Sø(f) % the union of the S{f}(n) for n % 0,1, 2. . . . However, as there might be many notations for each constructive ordinal, this ordinal logic need not be invariant, in the sense that one need not have: if KaK % KbK then Sa and Sb have the same consequences. Turing proved that an ordinal logic cannot be both complete for true purely universal statements and invariant. Using an extension procedure by certain proof-theoretic reflection principles, he constructed an ordinal logic that is complete for true purely universal statements, hence not invariant. (The history of this and later work on ordinal logics is traced by the undersigned in ‘Turing in the Land of O(z),’ in The Universal Turing Machine: A Half Century Survey, edited by Rolf Herken [1988].)
See also GÖDEL’S INCOMPLETENESS THEO- REMS , REFLECTION PRINCIPLE. S.Fe.