STEPHEN COLE KLEENE
January 5, 1909–January 25, 1994
BY SAUNDERS MAC LANE
STEVE KLEENE, A YANKEE from Maine, became a pioneer mathematical logician. His clear, precise ideas developed the modern study of computable functions and of automata. He was also a devoted mountaineer.
Kleene was born in 1909 in Hartford, Connecticut, but his real home was his paternal grandfather's farm in Union, Maine. In 1930 Kleene graduated summa cum laude from Amherst College. He had become fascinated with mathematics, and he went to Princeton University for graduate study in that subject.
At Princeton, the mathematician Oswald Veblen had understood that the development of logic required careful analysis by mathematicians. His student Alonzo Church joined the Princeton faculty and initiated the mathematical and logical study of those functions that are computable.” For this purpose Church devised his so-called lambda calculus, which provided the names for all functions. For example, the notation λ x • (x2 + 1) with the Greek letter lambda names the function that sends each number x to its square plus 1, and likewise with other functions. Church developed this calculus as a new formal foundation for all of mathematics. Kleene and his fellow student Barkley Rosser
studied it with care, and presently found that it led to a contradiction.
Precision was clearly needed. Kleene's subsequent research provided this, as for example, in his influential and authoritative 1952 book Introduction to Metamathematics, which was translated into Russian, Chinese, Romanian, and Spanish. One feature of this book is the clear formulation of Gödel's theorem.
In 1932 Kurt Gödel in Vienna had proved his famous incompleteness theorem: In any specific and adequate formal system of logic containing all of number theory there are true statements that cannot be proved in the system. This result applied both to the Whitehead-Russell system of Principia Mathematica” and to Church's revised ?-calculus. Gödel's proof made essential use of functions defined by recursion. An example of this is the definition of multiplication from addition by the recursion
m • 1 = m, m • (n + 1) = m • n + m.
In effect, this defines m(n + 1) in terms of m times n. Gödel's theorem became at once the focus of attention in logic. In 1934 Gödel came to Princeton and lectured on his results. A central question arose. Which functions are really computable? Church proposed that they are exactly the functions definable in the λ-calculus (called lambda definable); Kleene in his thesis (1934) carefully examined this proposal. Rosser showed the equivalence to the combinatory calculus of Haskell Curry. Turing (and independently Emil Post) proposed a definition of computable, as by a (Turing) machine. And Kleene examined the more general recursive functions used by Gödel. Church advanced the speculative thesis that the effectively computable functions (of numbers) could be identified with the λ-definable func-
tions. Presently various experts proved that, for such functions of numbers,
λ-definable = recursive = Turing machine computable.
With this established, Church's thesis so describing computable functions was generally accepted.
Much of Kleene's subsequent work was devoted to the systematic study of this class of recursive (computable) functions, as well represented in his magnificent 1952 book Introduction to Metamathematics and his treatment of the partial recursive functions—those defined recursively, but only for some numbers, hence partial.
In 1934 Kleene went from Princeton to the University of Wisconsin as instructor of mathematics. He became an assistant professor there in 1937. In 1941-42 he moved to become associate professor at his alma mater Amherst College. In 1942 he married Nancy Elliott and in the same year he enlisted in the U.S. Navy Reserve as a lieutenant, rising to lieutenant commander by the time of his discharge in 1946. At that time he returned to the University of Wisconsin as associate professor (full professor in 1948). He and his wife Nancy had four children (Paul, Kenneth, Bruce, and Nancy).
At Wisconsin, Kleene continued his research, proving his famous normal form” theorem for general recursive functions. In 1940 he considered also arithmetic predicates (of numbers) and showed that they could be arranged in a systematic hierarchy, now called the arithmetic hierarchy. Later, in 1955, he introduced a more extensive hyper arithmetic hierarchy. Similar orderings and hierarchies have been extensively examined. For instance, Emil Post, a professor of mathematics at the City College of New York, in 1948 defined a notion of degree of insolvability” for predicates
or functions, the lowest degree in this hierarchy being that of general recursive predicates (and unsolvable” problems were much examined). The 1954 joint paper of Kleene and Post about these degrees has been a major influence, for example, in emphasizing the following 1944 Post problem: Can there be two recursively enumerable sets with incomparable degrees? This fascinating problem was solved simultaneously yes” in 1956 by Muchnik1 (U.S.S.R.) and by R. M. Friedberg.2
Kleene at some point inherited his grandfather's farm in Maine. He did not work the farm, but he kept it up and kept it as a base for climbing Mount Katahdin. He was fascinated by mountains. In 1949 he and I, about to attend a meeting at Dartmouth of the American Mathematical Society, got together on a project to climb all the peaks in the Presidential range, and we were joined by a third climber, a vacationing bellhop. Then, as we three stood finally on top of the last peak (Mount Madison), a thunderstorm struck. Kleene bounded down from the peak shouting, Get down; it's lightning.” I stepped down a bit, searched for our third companion only to find him flat on the ground, unconscious. Steve (quicker by way of his height) went down to the Madison Pass hut for help. When we got the injured man there we found that the lightning had singed his scalp and left a blister on his foot opposite a hobnail. We ferried him to a hospital, and I (complete with a burned-out seat of the pants) notified his employer at the elegant Eastern Slopes Inn. He later recovered. Steve and I continued to climb assorted mountains and Steve kept on rock climbing.
In 1951 Kleene spent the summer at the RAND Institute, where he studied the famous paper of W. S. McCulloch and Walter Pitts on neural networks. 3 Kleene combined those ideas with notes of von Neumann on automata to produce a RAND report that has been very influential in the study
of automata. The lambda calculus meanwhile has been extensively used in computer science (e.g., the high-level programming language LISP).
In the 1920s the great Dutch mathematician L. E. J. Brouwer introduced intuitionism with its insistence that mathematics throughout should be treated by logical means that are constructive.” Kleene early realized that this could be connected with the fact that his recursive functions are the constructive ones (constructed by a recursion). He first formulated this connection in a 1945 paper, and in 1950 he spent a period as a Guggenheim fellow in Amsterdam consulting with Dutch intuitionists. His resulting concept of realizability” for intuitionism was systematically developed in a book written with his student Richard E. Vesley. The basic idea is that a constructive proof is one that can be realized” by an appropriate computation of a number.
Professor Michael Dummett, an authority on intuitionism, has pointed out to me that chapter one of this book provides the first systematic exposition of the foundations of intuitionist analysis set out as an axiomatic system treating Brouwer's fan theorem, the bar theorem, and the continuity principle (called Brouwer's principle). In these respects, this was far superior to the earlier well-known axiomatization by Heyting.”
At the University of Wisconsin, Kleene directed more than thirteen Ph.D. dissertations in various aspects of logic. His students included John W. Addison, Jr. (now at the University of California, Berkeley), Clifford Spector (deceased), Yiannis N. Moschovakis (University of California, Los Angeles), and Joan Rand Moschovakis (Oriental College). At Wisconsin Kleene built up an effective faculty engaged in research in mathematical logic. He brought his Princeton friend J. Barkley Rosser from Cornell University to Wisconsin to direct the Army Mathematics Research Center there.
He continued to care for the family farm in Maine. I had the chance to visit him there and to admire the venerable farmhouse and nearby private lake.
Kleene was elected to membership in the National Academy of Sciences in 1969. In 1964 he became the Cyrus C. MacDuffee professor of mathematics and computer sciences and served as dean of the College of Letters and Science in 1969-74. (This was a comeback; when Kleene left Wisconsin for Amherst in 1941, the dean of the college had declined to promote him, but he had assured Kleene that he would return.)
His wife Nancy died in 1970. Kleene married Jeanne Steinmetz in 1988; she survives him. In 1990 he was awarded the National Medal of Science. (I was privileged to attend the ceremony.) The award recognized his decisive contribution to mathematical logic: To precision, to the clear definition of the notion of constructable and recursive functions, and to the application of these notions to intuitionism, in computer science, and in logic generally.
1. Translated in American Mathematical Society, Translation 2nd Ser. 29(1963):157-215.
2. Proc. Natl. Acad. Sci. U. S. A. 43(1957):236-38.
3. Bull. Math. Biophys. 5(1949):115-33.
Proof by cases in formal logic. Ann. Math., Ser. 2, 35:529-44.
A theory of positive integers in formal logic (Ph.D. thesis). Am. J. Math., Ser. 2, 57:153-73. 219-44.
With J. B. Rosser. The inconsistency of certain formal logics. Ann. Math.36:630-36.
General recursive functions of natural numbers. Math. Ann.112:727-42.
?-definability and recursiveness. Duke Math. J.2:340-53.
With A. Church. Formal definitions in the theory of ordinal numbers. Fundam. Math.28:11-21.
Recursive predicates and quantifiers. Trans. Am. Math. Soc.53:41-73.
On the interpretation of intuitionistic number theory. J. Symb. Logic10:109-24.
Introduction to Metamathematics. Amsterdam: North-Holland.
With E. L. Post. The upper semi-lattice of degrees of recursive unsolvability. Ann. Math., Ser. 2, 59:379-407.
Hierarchies of number-theoretic predicates. Bull. Am. Math. Soc.61:193-213.
Representation events in nerve nets and finite automata. InAutomata Studies (Annals of Mathematics Studies no. 34), eds. C. E. Shannon and J. McCarthy, pp. 3-41. Princeton: Princeton University Press.
Recursive functionals and quantifiers of finite types I. Trans. Am. Math. Soc.91:1-52.
Quantification of number-theoretic functions. Compos. Math.14:23-40.
Turing-machine computable functionals of finite types II. Proc. Lond. Math. Soc.12:245-58.
Lambda-definable functionals of finite types. Fundam. Math.50:281-303.
Recursive functionals and quantifiers of finite types II. Trans. Am. Math. Soc.108:106-42.
With R. E. Vesley. The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions. Amsterdam: North-Holland.
Mathematical Logic. New York: Wiley & Sons.
Formalized recursive functionals and formalized realizability. Mem. Am. Math. Soc.89.
Brief mathematical autobiography. InScienziati e Technologi Contemporanei,vol. 2,pp 109-11. Milan: Arnoldo Mondadori Editore.
The work of Kurt Gödel. J. Symb. Logic41:761-78.
Recursive functionals and quantifiers of finite types revisited I. Generalized recursion theory II. InProceedings of the 1977 Oslo Symposium, eds. J. E. Fenstad, R. O. Gandy, and G. E. Sacks, pp. 185-222. Amsterdam: North-Holland.
The work of Kurt Gödel (addendum). J. Symb. Logic43:613.
The role of logical investigations in mathematics since 1930. In A Century of Mathematics in America, part 1, pp. 85-92. Providence, R. I.: American Mathematical Society.