Church spent two years as a National Research Fellow, one year at Harvard University then a year at Göttingen and Amsterdam. He returned to the United States becoming Assistant Professor of Mathematics at Princeton in 1929. Enderton writes in :-
Princeton in the 1930's was an exciting place for logic. There was Church together with his students Rosser and Kleene. There was John von Neumann. Alan Turing, who had been thinking about the notion of effective calculability, came as a visiting graduate student in 1936 and stayed to complete his Ph.D. under Church. And Kurt Gödel visited the Institute for Advanced Study in 1933 and 1935, before moving there permanently.He was promoted to Associate Professor in 1939 and to Professor in 1947, a post he held until 1961 when he became Professor of Mathematics and Philosophy. In 1967 he retired from Princeton and went to the University of California at Los Angeles as Kent Professor of Philosophy and Professor of Mathematics. He continued teaching and undertaking research at Los Angeles until 1990 when he retired again, twenty-three years after he first retired! In 1992 he moved from Los Angeles to Hudson, Ohio, where he lived out his final three years.
His work is of major importance in mathematical logic, recursion theory, and in theoretical computer science. Early contributions included the papers On irredundant sets of postulates (1925), On the form of differential equations of a system of paths (1926), and Alternatives to Zermelo's assumption (1927). He created the λ-calculus in the 1930's which today is an invaluable tool for computer scientists. The article  is in three parts and in the last of these Manzano:-
... attempt[s] to show that Church's great discovery was lambda calculus and that his remaining contributions were mainly inspired afterthoughts in the sense that most of his contributions, as well as some of his pupils', derive from that initial achievement.In 1941 he published the 77 page book The Calculi of Lambda-Conversion as a volume of the Princeton University Press Annals of Mathematics Studies. It is effectively a rewritten and polished version of lectures Church gave in Princeton in 1936 on the λ-calculus.
Church is probably best remembered for 'Church's Theorem' and 'Church's Thesis' both of which first appeared in print in 1936. Church's Theorem, showing the undecidability of first order logic, appeared in A note on the Entscheidungsproblem published in the first issue of the Journal of Symbolic Logic. This, of course, is in contrast with the propositional calculus which has a decision procedure based on truth tables. Church's Theorem extends the incompleteness proof given of Gödel in 1931.
Church's Thesis appears in An unsolvable problem in elementary number theory published in the American Journal of Mathematics 58 (1936), 345-363. In the paper he defines the notion of effective calculability and identifies it with the notion of a recursive function. He used these notions in On the concept of a random sequence (1940) where he attempted to give a logically satisfactory definition of "random sequence". Folina  argues for the usually accepted view that Church's Thesis is probably true but not capable of rigorous proof. The background to Church's work on computability and undecidability, based on his correspondence with Bernays during the years 1934-1937, is examined by Sieg in .
Church was a founder of the Journal of Symbolic Logic in 1936 and was an editor of the reviews section from its beginning until 1979. In fact he published a paper A bibliography of symbolic logic in volume 4 of the Journal and he saw the reviews section as a continuation and expansion of this work. Its aim, he wrote, was to provide:-
...to provide a complete, suitably indexed, listing of all publications ... in symbolic logic, wherever and in whatever language published ... [giving] critical, analytical commentary.The article  highlights Church's guiding role in defining the boundaries of the discipline of symbolic logic through this editorial work and testifies to his unflagging industry and conscientiousness and his high editorial standards. The aim of comprehensive coverage, which in 1936 had seemed quite practical, became less so as the years went by and by 1975 the rapid expansion in symbolic logic publications forced Church to give up this aspect and begin to provide only selective coverage. We mentioned above that Church retired from Princeton in 1967 and went to the University of California at Los Angeles. Perhaps this is the place where we should mention why he left Princeton after 38 years of service there. Enderton writes:-
Upon his retirement, Princeton was unwilling to continue accommodating the small staff working on the reviews for the Journal of Symbolic Logic.Church wrote the classic book Introduction to Mathematical Logic in 1956. This was a revised and very much enlarged edition of Introduction to mathematical logic which Church published twelve years earlier in 1944. This first edition was, as he states in the Introduction:-
... the first half of an introductory course in mathematical logic given to graduate students in mathematics [at Princeton in 1943].Haskell Curry in a review of the 1944 work writes:-
It is written with the meticulous precision which characterizes the author's work generally. ... The subject matter is more or less classical, namely, the propositional algebra and the functional calculus of first order, to which is added a chapter summarizing without proofs certain features of functional calculi of higher order. For the expert the chief interest in the tract is that it makes readily accessible careful detailed formulation and proofs of certain standard theorems, for example, the deduction theorem, the reduction to truth tables, the substitution rule for the functional calculus, Gödel's completeness theorem, etc.Manzano writes in  that the 1956 edition of the book:-
... defined the subject matter of mathematical logic, the approach to be taken and the basic topics addressed.The book begins with an Introduction which discusses names, variables, constants and functions, and leads on to the logistic method, syntax and semantics. Chapters I and II are concerned with the propositional calculus, discussing tautologies and the decision problem, duality, consistency and completeness, and independence of the axioms and rules of inference. The first order functional calculus is studied in Chapters III and IV, while Chapter V deals mainly with second order functional calculi.
Another area of interest to Church was axiomatic set theory. He published A formulation of the simple theory of types in 1940 in which he attempted to give a system related to that of Whitehead and Russell's Principia Mathematica which was designed to avoid the paradoxes of naive set theory. Church bases his form of the theory of types on his λ-calculus. Other work by Church in this area includes Set theory with a universal set published in 1971 which examines a variant of ZF-type axiomatic set theory and Comparison of Russell's resolution of the semantical antinomies with that of Tarski published in 1976. Another of Church's research interests was intensional semantics which is considered in detail in . The idea developed here was similar to that of Frege, distinguishing between the extension of a term and the intension, or sense, of a term. Church considered this topic for about 40 years during the latter part of his career, beginning with his paper A formulation of the logic of sense and denotation in 1951.
Although most of Church's contributions are directed towards mathematical logic, he did write a few mathematical papers of other topics. For example he published Remarks on the elementary theory of differential equations as area of research in 1965 and A generalization of Laplace's transformation in 1966. The first examines ideas and results in the elementary theory of ordinary and partial differential equations which Church feels may encourage further investigation of the topic. The paper includes a discussion of a generalization the Laplace transform which he extends to non-linear partial differential equations. This generalization of the Laplace transform is the topic of study of the second paper, again using the method to obtain solutions of second-order partial differential equations.
Church had 31 doctoral students including Foster, Turing, Kleene, Kemeny, Boone, and Smullyan. He received many honours for his contributions including election to the National Academy of Sciences (United States) in 1978. He was also elected to the British Academy, and the American Academy of Arts and Sciences. Case Western Reserve (1969), Princeton (1985) and the State University of New York at Buffalo (1990) awarded him honorary degrees.
Article by: J J O'Connor and E F Robertson
Click on this link to see a list of the Glossary entries for this page