丘奇Alonzo Church

丘奇的父母是Mildred Hannah Letterman Parker和皮埃尔·萨米埃尔 Robbins Church。他的父亲是一名法官。他在普林斯顿大学学习，1924年获得第一个学位，即文学学士，三年后获得博士学位。他的博士工作由奥斯瓦尔德·维布伦指导，他于1927年获得博士学位，学位论文题为Alternatives to Zermelo's Assumption。在他还在攻读博士学位期间，他于1926年在普林斯顿与Mary Julia Kuczinski结婚。他们有三个孩子：小丘奇、Mary Ann和Mildred。

丘奇作为国家研究员度过了两年，一年在哈佛大学，然后在哥廷根和阿姆斯特丹各一年。他回到美国，于1929年成为普林斯顿大学数学助理教授。Enderton在[4]中写道：-

20世纪30年代的普林斯顿是逻辑学的激动人心之地。有丘奇和他的学生Rosser和克林。有冯·诺伊曼。艾伦·图灵，一直在思考有效可计算性概念，于1936年作为访问研究生来到这里，并留下来在丘奇指导下完成博士学位。而库尔特·弗雷德里希·哥德尔在1933年和1935年访问了高等研究院爱德华·斯图迪，之后永久迁往那里。

他于1939年晋升为副教授，1947年晋升为教授，担任此职位直到1961年成为数学与哲学教授。1967年，他从普林斯顿退休，前往加州大学洛杉矶分校担任肯特哲学讲席教授和数学教授。他继续在洛杉矶教学和研究，直到1990年再次退休，距他第一次退休已有二十三年！1992年，他从洛杉矶搬到俄亥俄州的希尔达·菲比·哈德森，在那里度过了生命的最后三年。

他的工作在数理逻辑、递归论和理论计算机科学中具有重大重要性。早期贡献包括论文On irredundant sets of postulates（1925年）、On the form of differential equations of a system of paths（1926年）和Alternatives to Zermelo's assumption（1927年）。他在1930年代创建了λ-演算，如今这是计算机科学家不可或缺的工具。文章[10]分为三部分，在最后一部分中Manzano：-

……试图表明丘奇的伟大发现是λ-演算，而他其余的贡献主要是受此启发的事后思考，因为他的大部分贡献以及他的一些学生的贡献都源自这一初始成就。

1941年，他出版了77页的著作The Calculi of Lambda-Conversion，作为普林斯顿大学出版社《数学研究年刊》的一卷。它实际上是丘奇1936年在普林斯顿关于λ-演算讲座的重写和润色版本。

丘奇最著名的可能是“丘奇定理”和“丘奇论题”，两者都于1936年首次印刷发表。丘奇定理表明一阶逻辑的不可判定性，发表在Journal of Symbolic Logic第一期上的A note on the Entscheidungsproblem中。当然，这与基于真值表的命题演算形成对比，后者有判定程序。丘奇定理扩展了1931年对库尔特·弗雷德里希·哥德尔给出的不完备性证明。

丘奇论题出现在American Journal of Mathematics 58（1936），345-363上发表的An unsolvable problem in elementary 数论中。在论文中，他定义了有效可计算性的概念，并将其与递归函数的概念等同起来。他在On the concept of a random sequence（1940）中使用了这些概念，试图给出“随机序列”的逻辑上令人满意的定义。Folina [6]支持通常接受的观点，即丘奇论题可能是真的，但无法严格证明。Sieg在[11]中考察了丘奇在可计算性和不可判定性方面工作的背景，该背景基于他在1934-1937年间与保罗·贝尔奈斯的通信。

丘奇是1936年Journal of Symbolic Logic的创始人之一，并从一开始直到1979年担任评论栏目的编辑。事实上，他在该期刊第4卷发表了一篇论文A bibliography of symbolic logic，并将评论栏目视为这项工作的延续和扩展。他写道，其目的是提供：-

……提供一份完整、适当索引的符号逻辑领域所有出版物的列表……无论在哪里、以何种语言发表……[给出]批判性、分析性的评论。

文章5强调了丘奇通过这项编辑工作，在界定符号逻辑学科边界方面的指导作用，并证明了他不懈的勤勉与尽责以及他高标准的编辑要求。全面覆盖的目标在1936年曾显得相当可行，但随着岁月流逝变得不那么可行，到1975年，符号逻辑出版物的迅速扩张迫使丘奇放弃这一方面，开始只提供选择性覆盖。我们上文提到，丘奇于1967年从普林斯顿退休，前往加州大学洛杉矶分校。也许这里正是我们应当提及他为何在普林斯顿服务38年后离开的原因。Enderton写道：-

他退休后，普林斯顿不愿继续为从事《符号逻辑杂志》评论工作的小型员工提供办公场所。

丘奇于1956年撰写了经典著作Introduction to Mathematical Logic。这是丘奇十二年前于1944年出版的Introduction to mathematical logic的修订版，且篇幅大为扩充。正如他在导言中所说，这第一版是：-

……[1943年在普林斯顿]为数学专业研究生开设的数理逻辑入门课程的前半部分。

哈斯凯尔·加里在评论1944年那部著作时写道：-

它是以作者作品普遍具有的那种一丝不苟的精确性写成的。……主题或多或少是经典的，即命题代数与一阶函数演算，另加一章概述高阶函数演算的某些特征，但不加证明。对于专家而言，这本小册子的主要兴趣在于它便于获取某些标准定理的细致表述与证明，例如演绎定理、归约为真值表、函数演算的替换规则、库尔特·弗雷德里希·哥德尔的完备性定理等。

Manzano 在10中写道，该书的1956年版：-

……界定了数理逻辑的主题内容、所采用的方法以及所讨论的基本论题。

该书以一篇导论开篇，讨论名称、变量、常量和函数，并进而引出逻辑主义方法、语形学和语义学。第一章和第二章涉及命题演算，讨论重言式与判定问题、对偶性、一致性与完全性，以及公理和推理规则的独立性。一阶函数演算在第三章和第四章中研究，而第五章主要讨论二阶函数演算。

丘奇 感兴趣的另一领域是公理集合论。他于1940年出版了A formulation of the simple theory of types，其中他试图给出一个与阿尔弗雷德·诺思·怀特海以及伯特兰·罗素的Principia Mathematica相关的系统，旨在避免朴素集合论的悖论。丘奇将其类型论形式建立在他的λ-演算之上。丘奇在这一领域的其他工作包括1971年出版的Set theory with a universal set，其中考察了ZF型公理集合论的一个变体，以及1976年出版的Comparison of Russell's resolution of the semantical antinomies with that of Tarski。丘奇的另一项研究兴趣是内涵语义学，这在[3]中有详细讨论。这里发展的思想与戈特洛布·弗雷格的思想相似，区分一个词项的扩展与一个词项的内涵或意义。丘奇在其职业生涯后期约40年间考虑这一主题，始于他1951年的论文A formulation of the logic of sense and denotation。

尽管丘奇 的大部分贡献都指向数理逻辑，他确实也写了几篇其他主题的数学论文。例如，他于1965年出版了Remarks on the elementary theory of differential equations as area of research，1966年出版了A generalization of Laplace's transformation。第一篇考察常微分方程和偏微分方程初等理论中的思想与结果，丘奇觉得这可能会鼓励对该主题的进一步研究。该论文包括对拉普拉斯变换的一个推广的讨论，他将其推广到非线性偏微分方程。对皮埃尔·西蒙·拉普拉斯变换的这一推广是第二篇论文的研究主题，同样使用该方法来获得二阶偏微分方程的解。

丘奇 有31名博士生，包括Foster、艾伦·图灵、克林、约翰·克米尼、Boone和雷蒙·梅里儿·思木里安。他因其贡献获得许多荣誉，包括1978年当选国家科学院（美国）。他还当选为英国科学院和美国艺术与科学院院士。凯斯西储大学（1969年）、普林斯顿大学（1985年）和纽约州立大学布法罗分校（1990年）授予他荣誉学位。

Alonzo Church's parents were Mildred Hannah Letterman Parker and Samuel Robbins Church. His father was a judge. He was a student at Princeton receiving his first degree, an A.B., in 1924, then his doctorate three years later. His doctoral work was supervised by Veblen, and he was awarded his doctorate in 1927 for his dissertation entitled Alternatives to Zermelo's Assumption. While he was still working for his doctorate he married Mary Julia Kuczinski at Princeton in 1926. They had three children, Alonzo Jr, Mary Ann and Mildred.

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 [4]:-

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 [10] 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 [6] 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 [11].

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 [5] 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 [10] 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 [3]. 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.