Diff — Alonzo Church

{{infobox

| title = Alonzo Church

| image = church-blackboard.svg

| caption = The Church blackboard — he lectured writing with one hand, erasing with the other (our illustration)

| born = 14 June 1903, Washington, D.C.

| died = 11 August 1995, Hudson, Ohio (aged 92)

| education = Princeton — AB 1924, PhD 1927 (under Oswald Veblen)

| institutions = Princeton 1929–1967 · UCLA 1967–1990

| known_for = [[Lambda calculus]] · [[Church-Turing thesis]] · Church's theorem · Church–Rosser · founding the JSL

| students = Turing · Kleene · Rosser · Henkin · Davis · Rogers · Rabin · Scott · Smullyan · Andrews

}}

**Alonzo Church** (14 June 1903 – 11 August 1995) was the Princeton logician who gave computing its first precise definition — and then proved, with it, that mathematics itself has limits no machine can cross. He invented the **[[lambda calculus]]**, answered Hilbert's Entscheidungsproblem before [[Alan Turing|Turing]]'s machines were ink, founded the *Journal of Symbolic Logic*, and supervised a generation of doctoral students that reads like a hall of fame of computing. He did all of it at a blackboard, one hand writing, the other erasing, in a voice so steady his students measured the centuries by it.

```alb The advisor's advisor

Turing got a PhD under Church. So did **Kleene, Rosser, Henkin, Davis, Rogers, Rabin, Scott, Smullyan, and Andrews.** Between them: two Turing Awards, the solution of Hilbert's Tenth Problem, the fixpoint theorems, the textbooks, and the recursive-function theory on which all of computability stands. There may be no greater advising record in the history of the field.

```

Church was born in Washington, D.C., in 1903 — named for his great-grandfather, a professor of mathematics and astronomy who had become president of the University of Georgia. His father was a municipal court judge, and something of the law's precision seems to have lodged in the son: colleagues would spend a lifetime remarking on a mind that moved slowly, exactly, and never twice over the same ground.

He entered **Princeton** in 1920, took his degree in mathematics in 1924, and stayed for a doctorate under **Oswald Veblen** — the geometer who was then building Princeton into a mathematical power. The 1927 dissertation concerned the foundations of set theory; the real education was Princeton itself, which was assembling — in Veblen, von Neumann shortly after, and the Institute for Advanced Study to come — the capital of twentieth-century mathematics.

A fellowship took him to Harvard, then to Europe in 1928–29: **Göttingen**, still the Rome of mathematics under Hilbert, and **Amsterdam**, where L.E.J. Brouwer's intuitionism was challenging logic's foundations. Church came home to a Princeton assistant professorship in 1929 — a chair he would hold for thirty-eight years.

In 1925 he had married **Mary Julia Kuczinski**; they raised three children and stayed married for the rest of his life — a domestic fact that mattered, because Church's working habits were monastic and Mary Julia ran everything else.

Church's ambition in the early 1930s was the largest one logic offered: a complete formal foundation for all of mathematics, built not on sets but on **functions**. His "set of postulates" papers (1932–33) erected a grand system whose atoms were unnamed functions written in a new notation — **λx.M**, "the function that takes x and yields M."

In 1935 the grand system collapsed: his own graduate students, **Stephen Kleene** and **J. Barkley Rosser**, showed it inconsistent — the Kleene–Rosser paradox. Lesser ambitions would have died with the postulates. Church's did not, because carved out of the wreckage was a perfect surviving fragment: the pure calculus of λ-terms, free of the logic that had been bolted onto it. What remained was not a foundation for mathematics.

It was a foundation for *computation* — though nobody yet had that word for it. The full story of the calculus itself is told on [[Lambda calculus|its own page]].

A single Princeton year produced three of the century's foundational results:

- **April 1936** — *"An Unsolvable Problem of Elementary Number Theory."* Church defined **"effectively calculable"** as *λ-definable*, exhibited a problem no such function could solve, and thereby proved **Hilbert's Entscheidungsproblem unsolvable**: there is no mechanical procedure that decides every mathematical question. It was the first great impossibility theorem of the computer age — **Church's theorem** — and it appeared months before Turing's machines.

- **1936** — with Rosser, *"Some Properties of Conversion"* — the **Church–Rosser theorem**: the λ-calculus is *confluent*. However you reduce a term, every path rejoins; computation under his rules is deterministic in outcome even when free in order. Every functional language still breathes through this theorem.

- **1936** — Church founded the **Journal of Symbolic Logic**, the field's first journal, and edited it himself for over forty years — building, almost single-handedly, the institutional home formal logic had never had.

```fact The thesis that can't be proved

Church proposed that *effectively calculable* — the informal idea of "computable by some definite procedure" — **is** λ-definability. Turing's equivalent machines, Gödel's recursive functions: three different roads, one boundary. You cannot prove an identification between an intuition and a formalism — which is why it stays a **thesis**. Eighty-nine years of computing have yet to find a single counterexample.

```

```chart One boundary, three doors

process a "λ-definable\nChurch"

process b "computable\nTuring"

process c "recursive\nGödel–Kleene"

terminal t "effective\ncalculability"

a -> t

b -> t

c -> t

```

Church's teaching was legend, and legend of a specific kind. He lectured in a flat, careful monotone, filling the blackboard in dense, immaculate script — **writing with one hand while erasing with the other** — so that by the end of the hour the board held exactly one hour of completed logic and nothing else. Students described the experience variously as soporific and sublime; several took the same course twice to catch what the monotone concealed.

What the board produced was better measured in people than in theorems:

```chart Church's students

process c  "Church"

process n  "PhD students\n1934–65"

process a  "Kleene · Rosser"

process b  "Turing · Henkin"

process d  "Davis · Rogers"

process e  "Rabin · Scott"

process f  "Smullyan\nAndrews"

c -> n

n -> a

n -> b

n -> d

n -> e

n -> f

```

- **Stephen Kleene** (1934) — founded recursion theory as a discipline; regular expressions and the `*` of every regex engine are his.

- **J. Barkley Rosser** (1934) — co-author of the paradox and of Church–Rosser; the Rosser trick repaired Gödel's own proof.

- **[[Alan Turing]]** (1938) — sailed to Princeton after proving his machines equivalent to Church's λ; wrote his doctorate on ordinal logics under the man whose formalism his own had just vindicated. Temperamental opposites — Turing rough and improvising, Church formal to the cufflink — they gave each other the century's deepest idea in duplicate.

- **Leon Henkin** (1947) — the completeness proofs; the Henkin construction logic students still learn.

- **Martin Davis** (1950) — a third of the solution to **Hilbert's Tenth Problem**; *Computability and Unsolvability* taught the subject to generations.

- **Hartley Rogers** (1952) — wrote *the* recursion-theory textbook.

- **Michael Rabin** (1957) and **Dana Scott** (1958) — nondeterministic automata; joint Turing Award, 1976.

- **Raymond Smullyan** (1959) — logician, magician, and the most beloved puzzle-writer the field ever produced.

- **Peter Andrews** (1965) — carried Church's typed logic into the Q0 system and its provers.

During the war years Church did what Princeton mathematicians did — classified and applied work for the war effort — and then returned to logic, to the JSL desk, and to a second major creation: in **1940** he had published the **simply typed λ-calculus**, his untyped system fitted with a type discipline. It could no longer express the self-eating Ω — a limitation that turned out to be a foundation. Typed λ-calculi are the grammar of nearly every modern type system, and of the proof assistants that now verify mathematics itself.

In **1956** came *Introduction to Mathematical Logic, Volume I* — five hundred pages of the most careful logic textbook ever written, with footnotes of legendary density and a bibliography maintained like a state archive. *Volume II* was announced, awaited, anticipated — and never written, becoming a running half-century joke in a field that adored its author enough to wait for him.

```quote

"The question whether a given expression is λ-definable is, in a sense, the question whether it can be computed — and the answer to that question is the subject of the thesis that bears his name."

```

Colleagues preserved the small facts because the large ones seemed impossible in a person so ordinary:

- **The files.** Church kept an indexed card file of *everything* — correspondence, references, reviews — and could produce any letter on demand. The JSL's bibliography was, for decades, essentially his private system.

- **The lectures at eight in the morning**, monotone, perfect, unforgettable-in-hindsight.

- **The ice cream.** He was a large, unhurried man with a devotion to ice cream that his obituaries felt honor-bound to record; students remembered the cones — plural.

- **The pulp science fiction.** The most rigorous mind in logic kept a large collection of SF magazines and read them with the same completeness he brought to Frege.

- **The monotone that concealed the kindness** — former students, writing his memorials, kept reaching for the same discovery: behind the formalism was a shy, gentle, unfailingly generous man who answered every serious letter seriously.

Princeton retired him in **1967** — mandatory retirement, sixty-four years old, still writing. **UCLA** hired him that year into a joint chair of mathematics and philosophy, and he taught there for **twenty-three more years**, running a logic seminar past his eightieth birthday and retiring a second time only in 1990.

His late work returned to the problem of meaning itself — the intensional logic of *sense and denotation*, a decades-long project refining Frege's semantics into a formal calculus — and to **Church's problem** (1957): whether a desired input–output behavior can automatically be *synthesized* into a circuit. Büchi and Landweber solved it in 1969; its descendants are the program-synthesis tools of today. Even his open problems had grandchildren.

Elected to the **National Academy of Sciences** in 1978; honored across mathematics and philosophy; the steady, late-arriving recognition that the man who defined computability had also built its institutions. He left UCLA in 1990, moved to Ohio to be near his son, and died in Hudson on **11 August 1995**, at ninety-two — six months after his paper's sixty-year-old subject had become, via the Web, the busiest concept on Earth.

```fact What his students' students built

From Church's advisees came recursion theory, the first computability textbooks, automata theory's Turing Awards, Hilbert's Tenth's solution, and Q0 — and through the typed λ-calculus, ML, Haskell, Coq, Agda, and the type systems inside Rust and TypeScript. Your `map` function is five handshakes from his blackboard.

```

- The **[[lambda calculus]]** — the field's other great formalism, and the skeleton under every functional language.

- The **[[Church-Turing thesis]]** — the load-bearing axiom of computing: "computable" *means* λ-definable / Turing-computable.

- **Church's theorem** and **Church–Rosser** — impossibility and confluence, the twin pillars.

- The **JSL** — forty-three years of his editorship; the journal that gave logic a home.

- The **students** — ten doctorates that became a century of the field.

- And, in every editor, every language, every `lambda` and `=>` — the notation itself, chosen, he said, because it was easy and distinctive.

- [Learn it interactively — the step-by-step lambda calculus guide](/math/lambda-calculus)

- [[Lambda calculus]] · [[Church-Turing thesis]] · [[Church encoding]] · [[Y combinator]]

- [[Alan Turing]] · [[Konrad Zuse]] · [[LISP]]

- [[History of Programming]] · [[FORTRAN]] · [[ALGOL]] · [[Plankalkül]]

- [[History of Mathematics]]

- [[History of Science]]

1. Church, Alonzo. "An Unsolvable Problem of Elementary Number Theory." *American Journal of Mathematics* 58(2), 1936 — the lambda-definability paper.

2. Church, Alonzo. *The Calculi of Lambda-Conversion* (Princeton UP, 1941).

3. Barendregt, Henk. *The Lambda Calculus: Its Syntax and Semantics* (North-Holland, 1984).

4. Hodges, Andrew. *Alan Turing: The Enigma* (Simon & Schuster, 1983) — for the Princeton context.

[[Category:People]]

[[Category:Mathematics]]

[[Category:Theory]]

[[Category:History]]