JOVANA
Library Glossary Getting Started Three Levels Fields How it works Mission
Join the mission
Back to the library
Mathematics 1936

An Unsolvable Problem of Elementary Number Theory

Alonzo Church

Some yes-or-no questions no procedure can ever answer.

Choose your version
In depth · the introduction

Some questions sound perfectly clear — yes or no? — yet Church proved that no recipe, no machine, no procedure could ever answer them.

The big idea

Before you can ask “can every problem be solved by following a recipe?”, you have to pin down what a recipe even is. Church built the smallest possible language for recipes — the λ-calculus, with just one move: take a function, hand it an input, and substitute. He then proposed that anything we'd intuitively call “computable” is exactly what this little language can express. That bold equation is now called Church's Thesis.

With computing finally made precise, he could ask a sharper question — and got a startling answer. He found a problem stated in plain mathematical terms whose answer is always either yes or no, yet for which no procedure whatsoever can give the right answer in every case. Not “we haven't found one yet,” but “one cannot exist.” That was something genuinely new: a problem proven to be beyond all method.

How it came about

In the 1920s the great mathematician David Hilbert set an agenda: put all of mathematics on a footing so secure that, in principle, a mechanical procedure could decide whether any statement was true. It was a confident dream of a tidy, fully knowable mathematics. Then the 1930s took it apart. In 1931 Kurt Gödel showed no consistent system could prove all truths about arithmetic. A few years later, working at Princeton, Alonzo Church aimed at the rest of Hilbert's dream — the “decision problem.”

To attack it, Church and his students Stephen Kleene and J. Barkley Rosser had spent years developing the λ-calculus. Kleene proved it computed exactly the same functions as a rival definition (the “recursive” functions), and that agreement gave Church the confidence to declare what computability is. Months later, an unknown young Englishman named Alan Turing arrived at the same wall from a completely different direction — imagining a simple machine reading a tape — and the two answers turned out to be the same. Their combined verdict is the Church–Turing thesis.

Why it mattered

This is where computer science gets its foundations — decades before the first electronic computer. By saying precisely what “to compute” means, Church made it possible to prove, rigorously, what computers can and can't do. And the very first thing proven was a limit: there are well-posed questions no program will ever settle. Every time a tool says it cannot, in general, tell whether your program will crash or loop forever, it is bumping into the boundary Church drew in 1936.

A way to picture it

Think of a recipe: a finite list of unambiguous steps a patient cook can follow with no cleverness, always reaching the same dish. Church's claim is that “computable” means exactly “has such a recipe.” Now imagine a question like: “Will following this recipe ever actually finish?” For some recipes you can see the answer; but Church proved there is no master recipe that, fed any recipe at all, always tells you correctly whether it finishes. The checker would have to outwit every recipe, including cleverly self-referential ones — and no recipe can do that.

An interactive λ-calculus reducer: pick a small term and press a button to take one computation step at a time, replacing a function applied to an input by the result. Most terms shrink to a tidy final form (the successor of 1 becomes 2; 1 plus 2 becomes 3); one term, called Ω, turns back into itself at every step and never finishes — a tiny program with no stopping point.

Where it sits

Church's paper is one corner of a remarkable trio. Gödel (already in the Library) showed truth outruns proof; Church showed that solvability has hard limits; and Alan Turing, in the same year, recast the same boundary with his imagined machine — the blueprint of every computer since. Read together, these three results from the 1930s map the outer edges of what reasoning and machinery can do. Everything from Shannon's information theory to today's software lives inside the space they fenced off.

The original document
Original source text

Introduction — the question

Alonzo Church · An Unsolvable Problem of Elementary Number Theory · Amer. J. Math. 58 (1936): 345–363
There is a class of problems of elementary number theory which can be stated in the form that it is required to find an effectively calculable function f of n positive integers, such that f(x₁, x₂, …, xₙ) = 2 is a necessary and sufficient condition for the truth of a certain proposition of elementary number theory involving x₁, x₂, …, xₙ as free variables.
The purpose of the present paper is to propose a definition of effective calculability which is thought to correspond satisfactorily to the somewhat vague intuitive notion in terms of which problems of this class are often stated, and to show, by means of an example, that not every problem of this class is solvable.

The definition (Church's Thesis)

§7 · The definition of effective calculability (p. 356)
We now define the notion, already discussed, of an effectively calculable function of positive integers by identifying it with the notion of a recursive function of positive integers (or of a lambda-definable function of positive integers).
This definition is thought to be justified by the considerations which follow, so far as positive justification can ever be obtained for the selection of a formal definition to correspond to an intuitive notion.

Two definitions, one notion

On the equivalence of λ-definability and (general) recursiveness
The fact, established by the present author and S. C. Kleene, that every λ-definable function of positive integers is recursive, and conversely, is here taken as fundamental.
Thus it is shown that no more general definition of effective calculability than that proposed above can be obtained by either of two methods which naturally suggest themselves (1) by defining a function to be effectively calculable if there exists an algorithm for the calculation of its values (2) by defining a function F (of one positive integer) to be effectively calculable if, for every positive integer m, there exists a positive integer n such that F(m) = n is a provable theorem.

The unsolvable problem

The negative result — a recursively unsolvable problem
It is shown that there is no recursive function of two formulas A and B, whose value is 2 or 1 according as A conv B or not. That is, the property of two well-formed formulas, that they are convertible into each other, is not recursive.
Likewise it is shown that there is no recursive function of a formula whose value tells whether or not the formula has a normal form. A problem which, like these, cannot be solved by any recursive — hence by Church's definition, any effectively calculable — function is said to be unsolvable.
[ … ]
In a companion note, the author applies the same method to Hilbert's Entscheidungsproblem, concluding that the general case of that decision problem for first-order logic is likewise unsolvable.
Alonzo Church · Princeton, New Jersey · received April 15, 1935; presented to the American Mathematical Society, April 19, 1935