Alonzo Church

How to use this course

Alonzo Church spent almost his entire career at two universities and left a mark on three subjects. In mathematical logic he proved, in 1936, that first-order logic is undecidable, and gave with his students the first precise definition of an effectively calculable function. In computer science his λ-calculus became the core of functional programming, of the theory of programming languages and of modern proof assistants. In philosophy he developed an intensional logic of meaning and kept it going for half a century. He also founded, with others, the Journal of Symbolic Logic and edited its reviews for 43 years, and he supervised 31 doctoral students, among them Alan Turing.

Each technical lesson opens with a paragraph for the general reader, then gives precise statements, proof sketches and exercises with folded solutions. We write λ-terms in modern notation, \(\lambda x.\,M\), where Church wrote \(\lambda x[M]\). Lessons 04 to 07 follow the work of 1932–1936; Lesson 08 the type theory of 1940; Lessons 09 and 10 his later work in probability, automata and philosophical logic.

Timeline

Washington, Ridgefield, Princeton, 1903–1927

Alonzo Church was born in Washington, D.C., on 14 June 1903. His father, Samuel Robbins Church, was a judge of the Municipal Court of the District of Columbia. The family had academic roots: Church’s great-grandfather, also named Alonzo Church, had been professor of mathematics and astronomy and later president of the University of Georgia, and his grandfather Alonzo Webster Church was Librarian of the United States Senate for twenty years.

As a boy Church was blinded in one eye by an air-gun accident. His father’s eyesight also failed, forcing him to give up his position, and the family moved to Virginia. With help from an uncle, Alonzo went to the Ridgefield School for Boys in Connecticut, where he helped edit the school magazine, and graduated in 1920.

Princeton

He entered Princeton in 1920 and stayed, apart from three years, for almost half a century. As an undergraduate he won the Class of 1861 Prize, was elected to Phi Beta Kappa and in 1924 published his first paper, on Lorentz transformations. He graduated A.B. in 1924 and went straight into graduate work under Oswald Veblen, the geometer who was building Princeton into a mathematical centre. While still a graduate student he married Mary Julia Kuczinski; they had three children.

His doctoral thesis, Alternatives to Zermelo’s Assumption (1927), studied what happens to set theory if the axiom of choice is replaced by alternatives, in the spirit of the non-Euclidean geometries that arise from replacing the parallel postulate. It marked the direction of his work: foundations, treated with complete formal precision.

A new foundation for logic, 1927–1935

After the PhD Church held a National Research Fellowship for two years: 1927–28 at Harvard, and 1928–29 at Göttingen and Amsterdam, the homes of David Hilbert’s formalism and L. E. J. Brouwer’s intuitionism. Hilbert’s programme was at its height, and the Entscheidungsproblem, the problem of finding a procedure to decide validity in first-order logic, had just been posed sharply by Hilbert and Wilhelm Ackermann in their 1928 textbook. In 1929 Church returned to Princeton as an assistant professor of mathematics.

The postulates of 1932–33

Church’s plan was a new foundation for logic that avoided both Bertrand Russell’s theory of types and the free variables of ordinary logic. In “A set of postulates for the foundation of logic”, published in two parts in the Annals of Mathematics in 1932 and 1933, every notion was built from functions, written with an abstraction operator \(\lambda\). Logical constants such as implication and the universal quantifier were functions too. To escape the paradoxes he restricted the law of excluded middle.

Two graduate students, Stephen Kleene and J. Barkley Rosser, worked on the system with him and received their doctorates in 1934. They developed the arithmetic of the pure function part. Kleene showed that a surprisingly wide class of number-theoretic functions could be defined in it, including the predecessor function, which Church had doubted was definable at all.

In 1935 Kleene and Rosser proved that the whole system was inconsistent: a version of the Richard paradox could be derived. Church abandoned the logic. He kept the part concerned only with functions and their application, which was consistent. This was the λ-calculus. In the same years Kurt Gödel lectured at Princeton (1934) on the incompleteness theorems and on recursive functions. When Church suggested that λ-definability captured exactly the effectively calculable functions, Gödel was unconvinced. The resolution of that disagreement is the subject of Lesson 06.

1936

In 1935 Church announced, and in 1936 published, a definite claim: a function of positive integers is effectively calculable if and only if it is λ-definable, or equivalently, by work of Kleene, general recursive in the sense of Jacques Herbrand and Gödel. With this definition he could, for the first time, prove that some problems have no algorithmic solution. His paper “An unsolvable problem of elementary number theory” appeared in the American Journal of Mathematics in 1936. Within weeks he applied it to Hilbert’s problem: “A note on the Entscheidungsproblem”, in the first volume of the new Journal of Symbolic Logic, proved that no such decision procedure exists. With Rosser he proved the confluence theorem that now carries both names.

In Cambridge, Alan Turing reached the same negative answer independently, with his machines. Max Newman wrote to Church that Turing’s work was independent and different in method, and recommended him. Turing proved that his computable functions were exactly the λ-definable ones and arrived in September 1936. He wrote his thesis under Church on ordinal logics and received the PhD in 1938. Church, reviewing Turing’s paper in the Journal of Symbolic Logic in 1937, coined the term “Turing machine” and wrote that Turing’s analysis made the identification of computability with effectiveness evident immediately.

1936 was also the year the Association for Symbolic Logic was founded and its journal launched. Church was one of the principal founders and the journal’s first editor. Through its reviews section, which he ran until 1979, he set a standard of rigour for the whole field.

The λ-calculus

For the general reader. The λ-calculus is a language with only three kinds of expression: variables, functions and applications of functions to arguments. There are no numbers, no truth values and no loops. Church and Kleene showed that numbers, arithmetic, logic and recursion can all be coded in it. It is the smallest programming language, and every functional language, from Lisp to Haskell, is built on it.

Syntax

Church’s own system, the λI-calculus, required \(x\) to occur free in \(M\) in every \(\lambda x.\,M\). The unrestricted version above, called the λK-calculus, is the one used today.

Church numerals

A natural number \(n\) is represented by the operation “apply a function \(n\) times”:

Successor, addition and multiplication are then

Booleans are coded as selectors, \(\mathsf T=\lambda x.\,\lambda y.\,x\) and \(\mathsf F=\lambda x.\,\lambda y.\,y\), so that “if \(B\) then \(M\) else \(N\)” is simply \(B\,M\,N\). Pairs are \(\langle M,N\rangle=\lambda z.\,z\,M\,N\), with projections obtained by applying to \(\mathsf T\) and \(\mathsf F\). These codings are now called Church encodings.

Confluence and fixed points

For the general reader. A λ-term can usually be simplified in several places, in any order. Could different orders give different answers? Church and Rosser proved in 1936 that they cannot: if a term has a final answer, it is unique. The proof guarantees that the calculus is consistent as a theory of computation. Meanwhile the same calculus allows a term to be applied to itself, which yields fixed-point combinators: the means by which recursion, and the paradoxes that sank Church’s logic, both arise.

Proof sketch

One-step reduction does not have the diamond property: in \((\lambda x.\,x\,x)\,(I\,a)\), contracting the inner redex first and then the outer gives \(a\,a\) in two steps, while contracting the outer first duplicates the inner redex and needs three. The standard proof, due to William Tait and Per Martin-Löf, uses parallel reduction \(\Rightarrow\): \(x\Rightarrow x\); if \(M\Rightarrow M'\) then \(\lambda x.M\Rightarrow\lambda x.M'\); if \(M\Rightarrow M'\) and \(N\Rightarrow N'\) then \(MN\Rightarrow M'N'\) and \((\lambda x.M)N\Rightarrow M'[x:=N']\).

1. \(\to_\beta\ \subseteq\ \Rightarrow\ \subseteq\ \twoheadrightarrow_\beta\), so \(\Rightarrow\) and \(\to_\beta\) have the same reflexive transitive closure.
2. Define \(M^*\) by contracting all redexes of \(M\) at once: \(x^*=x\), \((\lambda x.M)^*=\lambda x.M^*\), \(((\lambda x.M)N)^*=M^*[x:=N^*]\), and \((MN)^*=M^*N^*\) otherwise. By induction on \(M\), using a substitution lemma, \(M\Rightarrow N\) implies \(N\Rightarrow M^*\).
3. So \(\Rightarrow\) has the diamond property, and a diamond property passes to the transitive closure by tiling. ∎

If \(M=_\beta N\), the chain of reductions and expansions joining them is straightened by repeated use of the theorem. If \(N_1,N_2\) are normal forms of \(M\), their common reduct must equal both. In particular \(\mathsf T\ne_\beta\mathsf F\) and \(\overline m\ne_\beta\overline n\) for \(m\ne n\): the equational theory is consistent.

Fixed points

The combinator \(\mathsf Y\) is usually credited to Haskell Curry; Turing published \(\Theta\) in 1937. With a fixed point, any recursive definition \(g=F\,g\) has a solution \(g=\mathsf Y F\). Inside a logic, the same construction applied to negation produces a sentence equal to its own negation, which is how paradoxes entered Church’s 1932 system.

Normal forms and strategies

The term \(\Omega=(\lambda x.\,x\,x)(\lambda x.\,x\,x)\) reduces only to itself and has no normal form. The term \((\lambda x.\,y)\,\Omega\) has normal form \(y\), but reducing inside \(\Omega\) first loops forever. The standardization theorem of Curry and Robert Feys says that always contracting the leftmost outermost redex (normal-order reduction) reaches the normal form whenever one exists.

Church’s thesis and an unsolvable problem

For the general reader. To prove that no algorithm solves a problem, one first needs to say exactly what an algorithm is. Church proposed that the functions computable by any mechanical method are exactly those definable in his λ-calculus, which turned out to be exactly the recursive functions of Herbrand and Gödel, and exactly those computable by Turing’s machines. With this definition in hand, he exhibited a precise question about λ-terms that no algorithm can answer.

The equivalences

Kleene proved (i)⇔(ii) in “λ-definability and recursiveness” (1936); Turing proved (i)⇔(iii) in 1937. The proof of (ii)⇒(i) codes the initial functions, composition, primitive recursion (as in Exercise 4.3) and minimization (by a fixed-point search, as in Exercise 5.2). The proof of (i)⇒(ii) Gödel-numbers terms and observes that one-step reduction is primitive recursive, so that the value is found by searching for a reduction sequence ending in a numeral.

The thesis relates an informal notion to a formal one, so it is not a theorem. Church’s arguments were the equivalence of independent definitions and the fact that every known calculable function fell under them. Gödel accepted the thesis only after reading Turing’s analysis of what a human computer does. The combined claim is now called the Church–Turing thesis.

Self-reference in the calculus

Fix a computable Gödel numbering of terms, and write \(\ulcorner M\urcorner\) for the Church numeral of the code of \(M\).

Proof. There are terms \(\mathsf{App}\) and \(\mathsf{Num}\) with \(\mathsf{App}\,\ulcorner M\urcorner\,\ulcorner N\urcorner=_\beta\ulcorner MN\urcorner\) and \(\mathsf{Num}\,\ulcorner M\urcorner=_\beta\ulcorner\ulcorner M\urcorner\urcorner\), since both operations on codes are recursive. Let \(W=\lambda x.\,F\,(\mathsf{App}\,x\,(\mathsf{Num}\,x))\) and \(X=W\,\ulcorner W\urcorner\). Then \(X=_\beta F\,(\mathsf{App}\,\ulcorner W\urcorner\,\ulcorner\ulcorner W\urcorner\urcorner)=_\beta F\,\ulcorner W\,\ulcorner W\urcorner\urcorner=F\,\ulcorner X\urcorner\). ∎

Proof (in the form given by Dana Scott and Curry). Suppose \(D\) is a term with \(D\,\ulcorner M\urcorner=_\beta\mathsf T\) if \(M\) has a normal form and \(\mathsf F\) otherwise. Let \(F=\lambda n.\,D\,n\,\Omega\,\overline0\) and take \(X\) with \(F\,\ulcorner X\urcorner=_\beta X\). If \(X\) has a normal form, \(D\,\ulcorner X\urcorner=\mathsf T\) and \(X=_\beta\Omega\), which has none, contradicting Church–Rosser. If not, \(X=_\beta\overline0\), which is normal. ∎ Church’s own 1936 paper reached the same conclusion through Gödel numbering and a diagonal argument on recursive functions. Since equality of terms is a question about integers once terms are coded, he described it as an unsolvable problem of elementary number theory.

Church’s theorem

For the general reader. Hilbert hoped for a mechanical test that would decide, for any statement of logic, whether it follows from given axioms. Church proved in 1936 that no such test exists; Turing found a different proof weeks later. Logic can be searched for proofs, and every valid statement will eventually be found, but there is no procedure that also recognizes the statements that are not valid.

Proof sketch

Let \(\mathsf Q\) be Raphael Robinson’s arithmetic (1950): seven axioms about \(0\), successor, addition and multiplication, without induction. Its key property is that every recursive function is representable in \(\mathsf Q\): for recursive \(\varphi\) there is a formula \(\psi(x,y)\) with \(\mathsf Q\vdash\forall y\,(\psi(\overline n,y)\leftrightarrow y=\overline{\varphi(n)})\).

1. \(\mathsf Q\) is undecidable. If \(\{\ulcorner\sigma\urcorner:\mathsf Q\vdash\sigma\}\) were recursive, a diagonal argument as in Lesson 06 (or in Gödel’s theorem) produces a sentence \(\sigma\) with \(\mathsf Q\vdash\sigma\leftrightarrow\neg\mathrm{Thm}(\ulcorner\sigma\urcorner)\), where \(\mathrm{Thm}\) represents the decidable theoremhood; either answer yields a contradiction, since \(\mathsf Q\) is consistent (it has the standard model).
2. Reduction to logic. Let \(\bigwedge\mathsf Q\) be the conjunction of the seven axioms. Then \(\mathsf Q\vdash\sigma\) iff \(\bigwedge\mathsf Q\to\sigma\) is valid. A decision procedure for validity would decide \(\mathsf Q\). ∎

Church’s 1936 note derived the result from his unsolvable problem, using Gödel’s representation of recursive functions in a formal system of arithmetic. The finite system \(\mathsf Q\) came later and makes the reduction to pure logic transparent. Turing’s proof instead encoded the behaviour of a machine directly in a first-order sentence (see the Turing course, Lesson 05).

What remains decidable

Validity is semi-decidable: by the completeness theorem the valid sentences are exactly the theorems, which can be listed. Some fragments are fully decidable. Leopold Löwenheim showed in 1915 that monadic first-order logic, with only one-place predicates, is decidable, and the prefix classes of sentences whose validity is decidable were classified over the following decades.

The simple theory of types

For the general reader. The untyped λ-calculus lets a function be applied to itself, which gives it its full computational power and also its paradoxes. In 1940 Church tamed it by giving every term a type, as in Russell’s theory of types, so that a function on numbers can only be applied to numbers. The result is a clean higher-order logic. Its descendants are the type systems of modern programming languages and the logic of proof assistants such as HOL and Isabelle.

Church’s logic adds constants: \(\neg:o\to o\), \(\wedge:o\to o\to o\), and for each type \(\alpha\) a universal quantifier \(\Pi_\alpha:(\alpha\to o)\to o\), so that \(\forall x^\alpha.\,\varphi\) is \(\Pi_\alpha(\lambda x^\alpha.\varphi)\), and a description or choice operator \(\iota_\alpha:(\alpha\to o)\to\alpha\). Sets of individuals are terms of type \(\iota\to o\). Axioms include extensionality and, for arithmetic, an axiom of infinity. All of mathematics formalized in Principia Mathematica can be carried out in this system.

Proof idea (weak normalization). Define the degree of a redex \((\lambda x^\alpha.M)N\) as the length of its type \(\alpha\to\beta\). Contracting a redex of maximal degree that contains no other redex of that degree creates only redexes of smaller degree. A multiset induction on degrees then terminates. Turing wrote down an argument of this kind in an unpublished note, which Robin Gandy published in 1980. Strong normalization was proved later by Tait’s method of computability predicates.

Normalization rules out \(\Omega\) and \(\mathsf Y\), so typed terms cannot express general recursion. On Church numerals of type \((\alpha\to\alpha)\to\alpha\to\alpha\), Helmut Schwichtenberg showed in 1976 that the definable functions are exactly the extended polynomials, built from constants, addition, multiplication and a case distinction on zero. Higher-order logic regains arithmetic through its axioms, not through computation.

Completeness and Curry–Howard

By Gödel’s incompleteness theorem, Church’s type theory with its intended semantics, where type \(\alpha\to\beta\) ranges over all functions, has no complete proof system. In 1950 Church’s student Leon Henkin proved completeness with respect to general models, in which function types may range over smaller sets of functions. Read differently, the typing rules are the rules of natural deduction for implication: a type is a proposition and a closed term of that type is a proof. This correspondence, observed by Curry and made explicit by William Howard in 1969, links Church’s calculus to constructive logic and underlies proof assistants such as Coq and Lean.

Random sequences and circuit synthesis

For the general reader. Twice Church brought computability to bear on other fields. In 1940 he used it to repair a definition of randomness: a sequence of coin tosses is random if no computable betting rule can pick out a biased subsequence. In 1957 he asked whether a machine can automatically build a circuit that meets a specification written in logic, for every possible future input. The question founded the theory of reactive synthesis, now used to construct controllers that are correct by design.

Randomness

Richard von Mises had defined a random sequence, a collective, as one in which the limiting frequency of 1s exists and is unchanged in every subsequence chosen by an admissible place-selection rule: a rule that decides whether to select the \(n\)-th term using only the earlier terms. If every rule is admissible, no sequence qualifies. Abraham Wald showed in 1937 that collectives exist for any countable family of rules.

There are countably many recursive rules, and for each, the strong law of large numbers shows that the selected subsequence has frequency \(\tfrac12\) almost surely; a countable intersection of measure-one sets has measure one. Jean Ville showed in 1939 that von Mises–Wald collectives can still violate other laws of probability: for any countable family of rules there is a collective whose initial frequencies of 1s are always at least \(\tfrac12\). The definition that answered this, Per Martin-Löf’s of 1966, uses effective statistical tests and coincides with the algorithmic randomness of Andrey Kolmogorov, Gregory Chaitin and Leonid Levin.

Synthesis

At the 1957 Summer Institute for Symbolic Logic at Cornell, Church posed the following problem. Given a specification \(\Phi\) in a logic of infinite sequences, relating an input stream \(x_0x_1\dots\) to an output stream \(y_0y_1\dots\), decide whether there is a finite-state circuit that produces \(y_t\) from \(x_0,\dots,x_t\) so that \(\Phi\) holds for every input, and if so, construct it.

The proof views synthesis as an infinite game between the environment, choosing inputs, and the circuit, choosing outputs, with a winning condition given by an automaton; such games are determined, and the winner has a finite-memory strategy. Michael Rabin, Church’s student, gave another solution using automata on infinite trees.

Sense, denotation and knowability

For the general reader. “The morning star” and “the evening star” name the same planet, yet someone can believe that the morning star is bright without believing the evening star is. Gottlob Frege explained this by distinguishing what an expression refers to from the way it presents it. Church spent more than forty years building a formal logic for Frege’s distinction. In the course of his philosophical refereeing he also found a short argument with a startling conclusion about knowledge.

The logic of sense and denotation

In Church’s papers of 1946, 1951 and later, every type of his type theory acquires a hierarchy of concept types: for each type \(\alpha\) there is a type \(\alpha_1\) of senses of expressions of type \(\alpha\), a type \(\alpha_2\) of senses of those, and so on. A relation \(\Delta\) connects a concept to what it is a concept of. Belief and other attitudes take senses, not denotations, as arguments, so that substituting co-referring names inside a belief report need not preserve truth. John Myhill found in 1958 that one formulation was inconsistent, and Church revised the system several times; the last paper appeared in 1993, when he was 90.

Two arguments

Church’s translation argument (1950) objected to analyses of belief sentences as statements about sentences: “Seneca said that man is a rational animal” and its translation into German say the same thing, but a statement about English words does not survive translation. His version of the slingshot argued, in Frege’s spirit, that if co-referring terms can be substituted and logically equivalent sentences have the same reference, then all true sentences have the same reference, so sentences should be taken to denote truth values.

The knowability paradox

In 1945 Church refereed a paper by Frederic Fitch and pointed out an argument that Fitch published in 1963. Now called Fitch’s paradox, or the Church–Fitch paradox, it shows that if every truth is knowable, then every truth is known.

Proof. First, \(K(p\wedge\neg Kp)\) is impossible: by (i) it gives \(Kp\) and \(K\neg Kp\), and by (ii) the latter gives \(\neg Kp\), a contradiction. So \(\neg\Diamond K(p\wedge\neg Kp)\). Applying the knowability principle to the sentence \(p\wedge\neg Kp\) gives \(\neg(p\wedge\neg Kp)\), that is, \(p\to Kp\). ∎

The Princeton school, 1936–1967

Church became associate professor in 1939 and professor of mathematics in 1947; from 1961 he was professor of mathematics and philosophy. For three decades Princeton was a world centre of mathematical logic, and Church was its organizer. He supervised 31 doctoral dissertations. Among his students were Stephen Kleene and Barkley Rosser (1934), Alan Turing (1938), Leon Henkin (1947), John Kemeny (1949), Martin Davis (1950), William Boone (1952), Hartley Rogers (1952), Michael Rabin (1957), Dana Scott (1958), Raymond Smullyan (1959), Simon Kochen (1959) and Peter Andrews (1964). Rabin and Scott shared the 1976 Turing Award; Davis contributed to the negative solution of Hilbert’s tenth problem; Boone proved the word problem for groups unsolvable; Kemeny co-created the BASIC programming language.

His books set standards. The Calculi of Lambda-Conversion (1941) was for decades the reference on the λ-calculus. Introduction to Mathematical Logic, issued in a first version in 1944 and in a revised, enlarged Volume I in 1956, treated propositional and first-order logic with a rigour and historical scholarship that few textbooks have matched; its notes and exercises are a history of the subject in miniature. A planned second volume never appeared.

The editor

From 1936 to 1979 Church edited the reviews section of the Journal of Symbolic Logic, and he compiled its bibliography of symbolic logic from Leibniz onwards. He wrote many reviews himself and edited others line by line. Colleagues described him as exceedingly polite and careful, a worker of unflagging industry and high editorial standards, whose blackboard writing was immaculate. He read science fiction and was known to write to magazine editors pointing out scientific errors. He gave an invited address at the International Congress of Mathematicians in Stockholm in 1962.

UCLA, death and legacy, 1967–1995

In 1967, at the age of 64, Church left Princeton for the University of California, Los Angeles, as professor of philosophy and mathematics. He joined a strong group of logicians and philosophers and continued to teach and supervise students until he retired in 1990, at 87. His work in these years was mainly on intensional logic and on the theory of types. He was elected to the American Academy of Arts and Sciences in 1967 and to the National Academy of Sciences in 1978, and he became a corresponding fellow of the British Academy. He received honorary doctorates from Case Western Reserve University (1969), Princeton (1985) and the State University of New York at Buffalo (1990).

His wife Mary Julia died in 1976. In 1992 he moved to Hudson, Ohio. He died there on 11 August 1995, aged 92, and was buried in Princeton Cemetery.

Legacy

• Computability: Church’s thesis, with Turing’s analysis, is the foundation of the theory of computation; Church’s theorem gave the first undecidable problem in logic.
• Programming languages: John McCarthy’s Lisp (1958) borrowed the λ notation; Peter Landin used the λ-calculus to give meaning to Algol 60; Dana Scott and Christopher Strachey built denotational semantics on models of it; ML, Haskell and the lambdas of mainstream languages descend from it.
• Logic and proof: Church’s simple type theory is the logic of the HOL family of proof assistants; typed λ-calculi underlie Coq, Lean and Agda through Curry–Howard.
• Automata and verification: Church’s synthesis problem is the origin of reactive synthesis and of the game-theoretic approach to verification.
• Honours: the Alonzo Church Award, established in 2015 and given jointly by ACM SIGLOG, the EATCS, the EACSL and the Kurt Gödel Society, recognizes outstanding contributions to logic and computation.

Connections

People linked to Alonzo Church across this collection. A name without a link has no page here yet. See Alonzo Church in the network of all 337 lives →

Teachers and advisors

• Oswald Veblen 1927

Students

• Alan Turing 1938
• Stephen Cole Kleene 1934
• Dana Scott 1958
• George Alfred Barnard 1936
• Hartley Rogers Jr. 1952
• J. Barkley Rosser 1934
• John George Kemeny 1949
• Leon Henkin 1947
• Martin Davis 1950
• Michael O. Rabin 1957
• Nicholas Rescher 1951
• Peter Andrews 1964
• Raymond Smullyan 1959
• Simon Kochen 1959
• William Boone 1952

Influenced by

• Bertrand Russell
• David Hilbert
• Gottlob Frege
• L. E. J. Brouwer 1928-1929
• Richard von Mises

Influenced

• John McCarthy

Colleagues and collaborators

• Kurt Gödel 1934-1967
• Frederic Fitch
• Haskell Curry

Also mentioned in this life

• Andrey Kolmogorov
• Gottfried Wilhelm Leibniz
• Hendrik Antoon Lorentz
• Peter Guthrie Tait

Fields

• mathematical logic 10 lives
• philosophy of language 3 lives

Sources and further reading

Biography

1. J. J. O’Connor and E. F. Robertson, Alonzo Church, MacTutor History of Mathematics.
2. Alonzo Church, Wikipedia.
3. Princeton Alumni Weekly, Alonzo Church ’24 *27 (memorial).
4. H. B. Enderton, Alonzo Church: life and work, introduction to T. Burge and H. B. Enderton (eds.), The Collected Works of Alonzo Church, MIT Press, 2019.
5. H. B. Enderton, In memoriam: Alonzo Church, 1903–1995, Bulletin of Symbolic Logic 1 (1995).
6. Open Logic Project, Alonzo Church (short biography).
7. S. C. Kleene, Origins of recursive function theory, Annals of the History of Computing 3 (1981) 52–67.

Mathematics and philosophy

1. A. Church, A set of postulates for the foundation of logic, Ann. of Math. 33 (1932) 346–366; second paper, 34 (1933) 839–864.
2. S. C. Kleene and J. B. Rosser, The inconsistency of certain formal logics, Ann. of Math. 36 (1935) 630–636.
3. A. Church, An unsolvable problem of elementary number theory, Amer. J. Math. 58 (1936) 345–363.
4. A. Church, A note on the Entscheidungsproblem, J. Symbolic Logic 1 (1936) 40–41; correction, 101–102.
5. A. Church and J. B. Rosser, Some properties of conversion, Trans. Amer. Math. Soc. 39 (1936) 472–482.
6. S. C. Kleene, λ-definability and recursiveness, Duke Math. J. 2 (1936) 340–353.
7. A. Church, On the concept of a random sequence, Bull. Amer. Math. Soc. 46 (1940) 130–135.
8. A. Church, A formulation of the simple theory of types, J. Symbolic Logic 5 (1940) 56–68.
9. A. Church, The Calculi of Lambda-Conversion, Annals of Mathematics Studies 6, Princeton, 1941.
10. A. Church, Introduction to Mathematical Logic, Vol. I, Princeton, 1956.
11. J. R. Büchi and L. H. Landweber, Solving sequential conditions by finite-state strategies, Trans. Amer. Math. Soc. 138 (1969) 295–311.
12. H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland, revised ed. 1984.
13. F. Cardone and J. R. Hindley, History of lambda-calculus and combinatory logic, in Handbook of the History of Logic 5, 2009.
14. H. B. Enderton and others, Alonzo Church, Stanford Encyclopedia of Philosophy.
15. The Church–Turing thesis, Stanford Encyclopedia of Philosophy.