Church-Turing Thesis
Origin. Church (1936), Turing (1936), Kleene. Identifies the informal notion of effective calculability with a formal model of computation. A thesis, not a theorem: it links intuition to mathematics.
Models. Any function computable by an algorithm is computable by a Turing machine (equivalently λ-definable, general recursive). The convergence of many independently designed models is the central evidence.
Formalism.
Statement: Effectively calculable = Turing computable = partial recursive = λ-definable. The informal class equals the formal class.
Equivalent models: Turing machines. λ-calculus. General recursive functions. Register/counter machines. Post canonical systems. Cellular automata. All define the same function class.
Evidence: Every proposed model of effective computation coincides. Robust under variation (tapes, symbols, nondeterminism → same class). No counterexample in ninety years.
Physical Church-Turing thesis: Any physically realizable computation is Turing computable. Stronger, empirical claim about nature.
Extended (feasibility) thesis: Efficiently computable = polynomial time (P). Challenged by randomized and quantum models.
Turing completeness: A system that can simulate a universal Turing machine. Sufficient for full computational power.
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| λ | U+03BB | Lambda | λ-definability |
| μ | U+03BC | Mu / Minimization | Unbounded search; the one partial operator |
| = | U+003D | Equality | Coextensiveness of the function classes |
| TM | — | Turing machine | Standard model |
| CT | — | Church-Turing | The thesis |
| CT₀ | — | Church's thesis, internalized | Formal schema: every total function has an index |
| P | — | Polynomial time | Feasibility class of the extended thesis |
| BQP | — | Bounded-error quantum polynomial time | Challenger to the extended thesis |
Metatheory. The thesis has no proof and can have none, because one of the two classes it equates is informal; what is theorem is the equivalence of the formal models. Church (1936) and Kleene (1936) established that λ-definability and Herbrand–Gödel general recursiveness are coextensive, and Turing (1936), in an appendix to "On Computable Numbers," showed his machines compute exactly the λ-definable functions. Kleene's normal form theorem sharpens the picture: a single application of μ suffices, so one unbounded search accounts for all partiality. Gödel rejected Church's argument from the λ-calculus and accepted the identification only after Turing's analysis of a human calculator working under finiteness and locality constraints, which he took to make the notion of formal system absolute. Gandy (1980) turned a restricted version into a theorem: any discrete deterministic mechanism satisfying his principles on the form, boundedness and local causation of its states computes only Turing-computable functions. The thesis is refutable in principle — an accepted effective procedure for a non-computable function would end it — and none has appeared in ninety years.
Applies to. Foundations of computation. Undecidability proofs. Complexity theory (extended form). Philosophy of mind and computation.
Limitations. The thesis is not a theorem and cannot occur as a step in a derivation; every undecidability proof that says "this procedure is clearly effective" leans on it informally, and discharging that lean means exhibiting the machine. It bounds no resources: in the basic form it is compatible with any total computable running time, so it settles nothing about feasibility, and the extended version equating feasible with P is contested by randomized and quantum models without being refuted, since P = BPP and P = BQP are both open. The physical version is not a claim about logic: whether Malament–Hogarth spacetimes are realizable is a question in general relativity, and were they realizable the physical thesis would fail while the mathematical one stood. Relativized to an oracle the thesis holds again, so "effectively calculable" is absolute only in the absence of oracles. Internalized as the schema CT₀ it becomes a proposition with a truth value — consistent with Heyting arithmetic, inconsistent with classical logic — but that schema is not the thesis.
© 2026 Lingenic LLC