Adapted from a paper I wrote for a computability and logic class. The original is here.
Underneath almost everything we say about computers and algorithms sits a single claim, the Church–Turing Thesis, which nearly everyone who invokes it treats as settled. Yet it cannot be a theorem, as it does not admit of proof. A deeper question emerges: what, exactly then, entitles us to believe it?
The convergence
In the 1930s, several mathematicians set out to make precise an informal idea: what is it for something to be computable, that is, calculable by a finite, mechanical, step-by-step procedure? This was before computers existed, so the target was a human activity—the rote calculation a clerk could carry out with pencil and a fixed set of rules, requiring no ingenuity. Philosophers call it effective calculability.
Three figures approached it from unrelated directions. Alan Turing imagined an idealized machine reading and writing symbols on a tape. Alonzo Church built an abstract symbolic system, the lambda calculus. And Kurt Gödel, with Stephen Kleene, defined a class of "recursive functions" in pure arithmetic. Three frameworks with nothing obvious in common, and yet they proved extensionally equivalent. Each picks out exactly the same class of functions, invariant under any change of machine, notation, or physical implementation. This is what the Church–Turing Thesis records.
The stability is striking, especially beside its sibling result. Gödel's 1931 incompleteness theorems showed that mathematical truth cannot be captured by any single system of rules: for any consistent set of axioms strong enough for arithmetic, there are truths it cannot prove. One may always add axioms, but one never finishes. Provability, in this sense, is relative; it depends on the system. Computability is not. So I asked: why should one notion be absolute when the other is relative?
Why it cannot be a theorem
A theorem proves something within mathematics—one formal statement following from others. The Church–Turing Thesis instead asserts an identity between two different kinds of thing: effective calculability, an informal, pre-theoretic concept about what a person can do by following rules, and a rigorous mathematical object—the Turing machine, the lambda calculus, what have you. To prove an equivalence between the two is not a hard problem but a category error: proof relates formal statements to formal statements, and the informal concept is, necessarily, not yet formal—it is precisely what we are trying to capture.
Horizontal and vertical
The tempting answer is to appeal to the convergence itself. At first blush, one could think that if three independent formalizations agree, surely they have captured the concept.
Consider five witnesses to a crime, interviewed separately, who describe it identically. Their agreement is reassuring—unless all five watched from the same obstructed angle, in which case they agree with one another and yet miss the same thing. Their consistency tells us nothing about what none of them could see.
So with the formalisms. Their agreement is horizontal: it certifies coherence among the candidate definitions. But the question we care about is vertical: is any of them faithful to the original concept? Horizontal agreement cannot answer a vertical question—namely, that a uniform formalization is perfectly consistent with a uniform omission. Invariance is thus necessary for having captured effective calculability, but cannot be sufficient. Gödel made essentially this point, that a satisfying analysis would require a notion of computability that is genuinely absolute, and I cite him here as evidence, not authority.
The grounding problem
We therefore need something different in kind. No relation among the formalisms speaks to their fidelity to the concept; what is needed is a grip on the informal idea that is not itself wholly supplied by the formalism whose adequacy is in question. I call this independent epistemic access, and the demand for it the grounding problem. Without such access, any claim that the formal system has tracked the informal notion is either circular or unfalsifiable.
This radicalizes a difficulty Rudolf Carnap had identified: that replacing an informal concept (the explicandum) with a formal one (the explicatum) requires the two to be genuinely similar. The grounding problem presses the further question of how that similarity could ever be verified. My answer is that it cannot, unless we reach the concept from somewhere other than the formalism—and since that cannot be done from within any formalism, the warrant for the thesis must be extra-mathematical.
What Turing did
Church had tried to settle the matter by stipulation: λ-definability simply is what we mean by effective calculability. But this does not answer the question; it restates it, supplying one more candidate definition and leaving the vertical question intact.
Turing, in 1936, did the opposite. Rather than propose another symbolic language, he turned to the calculating agent and asked what, of necessity, constrains any process we would recognize as a calculation. He isolated a few invariants on the human computer: for instance, a finite alphabet of distinguishable symbols; attention confined at any moment to a bounded portion of the work; finitely many internal states of mind; and steps determined by, and altering, only the local configuration and the current state. These are features not of a notation but of the embodied activity the notation is about—and interrogating the explicandum directly, rather than supplying another explicatum, is precisely what furnishes the independent epistemic access the grounding problem demands.
The witness who mattered
That this is the right diagnosis is corroborated by the one reader whose assent mattered most. Gödel was conspicuously unmoved by the convergence of formalisms; that they agreed settled nothing for him, as one would expect if convergence is merely horizontal. Turing's analysis was another matter. In 1946 he singled out computability as the first absolute epistemological notion, and in a 1964 postscript credited Turing with a precise definition of the general concept of a formal system.
Where this leaves us
So why is computability absolute while provability relative? Because we have no access to proof überhaupt except through some formal system—there is no phenomenology of "being a proof" to point to from outside. Turing supplied exactly such access for computation, grounding it in what a calculating agent can do, and that is what sets the two notions apart.
The point generalizes beyond the Church-Turing Thesis. The grounding problem confronts any explication: where independent access to the concept can be found, that concept can become absolute; where it cannot, relativity remains. The line between the absolute and the relative is drawn not by our formalisms, but by whether we can find a standpoint outside them.