Reading companion to Alonzo Church, 1936
Where computation stops: Church’s unsolvable problem
TLDR
- A decision procedure must halt with the right answer for every permitted input.
- Church identified effective calculability with two independently motivated but equivalent formalisms.
- Lambda syntax can be numbered, enumerated and supplied to lambda-defined functions as data.
- A supposed normal-form decider enables a diagonal formula missing from an allegedly complete list.
- The result limits uniform mechanical procedures, not proof, ingenuity or every altered model of computation.
The inspector that must inspect itself
Imagine a code-review service with an unusually strong promise. Submit any program and it will always stop. Its answer is either “this program settles to a finished result” or “this program never does”. It accepts toy functions, compilers, other reviewers and, crucially, its own source code.
For a while the service looks plausible. It spots a loop whose counter never changes. It certifies a function that returns immediately. It even recognises many complicated recursive programs. Those successes do not test the promise. The dangerous word is any.
Now construct a program that reads the inspector’s verdict about the program listed on the same row. When the inspector predicts an ordinary numerical answer, the new program returns the next number. When the inspector predicts no answer, it returns a fixed number instead. The constructed program has a result. Yet on its own row that result is forced to differ from the result attached to that row. A complete list has missed something it was required to contain.
This is the pressure inside Alonzo Church’s 1936 paper, An Unsolvable Problem of Elementary Number Theory.1 Church’s actual argument is not the modern halting-problem proof, and it should not be retold as one. His target is whether an arbitrary lambda formula has a normal form, followed by whether two formulas are convertible. His machinery is lambda conversion, recursive functions, Gödel numbering and an enumeration that turns against itself. The shape of the reasoning became foundational because it tells us how to challenge a universal automation claim: make the proposed method precise, admit its own descriptions as inputs, and test the diagonal.
What kind of problem can be unsolvable?
Church begins with a family of familiar mathematical requests. Given an instance, find an effectively calculable function that returns one designated number when a proposition is true and another when it is false. The examples range from questions in elementary number theory to the search for complete invariants in topology. Every finite instance has a truth value. The question is whether one uniform method can deliver the correct value across the whole class.
That last distinction is easy to blur. A problem can have many solved instances without having a general decision procedure. A proof for one equation, a clever classification of one manifold or a terminating trace for one program does not supply an algorithm for all equations, manifolds or programs. Church is not announcing that a particular calculation is too large. He is asking whether a total method exists.
A decider is a total, uniform map. For every input in its stated domain, it must halt and return the correct yes-or-no value. Running for a billion years is practically useless but still a computability question of time. Failing to return on one legal input means the procedure is not a decider at all.
Why “effective” needed a mathematical home
In ordinary speech, an effective method is a recipe a person could follow without invention: finitely stated, mechanically applicable and guaranteed to finish for each input. That description guides intuition but it cannot bear a proof until its terms are formal. “Mechanical”, “step” and “method” all conceal choices. A loose definition lets a critic rescue a failed procedure by adding one more clever move.
Church therefore proposes an identification. A function of positive integers is effectively calculable when it is recursive in the Herbrand–Gödel sense, or equivalently lambda-definable. The paper proves the two classes extensionally equal through Theorems XVI and XVII. This equality matters because the formalisms arrive from different directions. Lambda calculus treats function formation and application as primitive. General recursion builds functions from numerical equations and sanctioned operations. Their convergence is evidence that the boundary is not a quirk of one notation.
It is evidence, not a proof that an informal idea equals a formal class. Church says as much. His proposal is justified as far as positive justification can be obtained when selecting a formal definition for an intuitive notion. That modest sentence is the hinge of the paper. The undecidability theorem is mathematical once the class has been fixed. The claim that this class captures every ordinary mechanical calculation is a thesis supported by convergence, analysis and continued failure to find a counterexample.
Church’s paper carries two logically different burdens. Sections 2–6 develop exact formalisms and prove equivalence results. Section 7 argues that either form can stand for effective calculability. Section 8 then proves an impossibility inside that adopted class. Calling the entire paper “a proof that no algorithm exists” hides the bridge between intuition and theorem.
Church tests two tempting ways to enlarge the class
Section 7 does more than announce a definition. Church considers two routes that might appear broader than recursion. The first defines a function as calculable when an algorithm exists for its values. Imagine a calculation on input n as a finite sequence of written expressions. The initial expression can be obtained from n; each later expression can be obtained from the earlier history; termination is recognisable; the final expression yields the value.
Gödel numbering can compress each finite history into one integer. Numerical functions can then describe the next expression and the terminal value. If those next-step functions count as effectively calculable, and “effectively calculable” is read as recursive, the whole algorithm computes a recursive function. Church is candid about the interpretive turn: refusing this or a similar reading makes it difficult to give “algorithm” an exact meaning at all. The passage is an adequacy argument, not a derivation of formality from an untouched everyday word.
The second route starts from proof. Call a numerical function calculable within a symbolic logic when an expression represents it and the equation giving each output is provable exactly when the corresponding numerical claim is true. For a logic to perform ordinary formal work, its axioms and rules must be effectively listable and each rule application effectively checkable. Under the recursive interpretation of those conditions, the theorems are recursively enumerable. Church then argues that every function calculable within such a logic is recursive.
These two tests close obvious escape routes. Replacing “recursive” with “there is an algorithm” does not widen the class once the algorithm’s steps are made executable. Replacing it with “the value is formally provable” does not widen the class when the proof system itself has effective rules. Neither test establishes a metaphysical limit on all possible reasoning. Both force a proposed general method to disclose the operations by which another agent could carry it out.
The contractor with a private flash of insight
A contractor promises to classify every submitted formula. For each formula examined so far, she eventually produces a correct answer. On difficult cases she cannot state the next step in advance; she waits for a new mathematical idea. Has she supplied an effective decision method?
No, not in Church’s sense. The output history may be impressive, and each particular answer may have a proof. The promise still lacks a uniform operation that another agent can execute from the input alone. This is not a criticism of insight. It marks which achievement the theorem addresses. A potentially endless succession of new methods is different from one method that decides the whole domain.
What Church had not yet proved
Nothing in the opening pages licenses the claim that a human mind is a computer, that physical reality permits no stronger process or that mathematical creativity has a ceiling. Nor does the paper show that every interesting question is undecidable. Its first commitment is narrower: if we mean a uniform effective procedure, lambda-definability and recursiveness are proposed as exact accounts. The rest of the argument earns a negative result under that commitment.
This discipline is worth preserving in modern debates. When someone advertises an automated verifier, autonomous scientist or universal reasoning engine, ask for the domain, the output contract and the permitted operations. “Works on the benchmark” is evidence about sampled performance. “Decides the property” is a quantified mathematical claim. They belong to different ledgers.
A calculus made from binding, application and conversion
Church needs a formalism spare enough to analyse and expressive enough to represent numerical functions. Lambda calculus supplies three pieces. A variable such as x is a formula. If F and X are formulas, then applying the first to the second gives a formula. If M contains a free occurrence of x, abstraction binds it: λx.M.
A modern reader will recognise function definition and function call, but Church’s system is not a programming language specification. Its objects are formulas and its central relation is conversion. Renaming a bound variable, substituting an argument into a function body and removing an extensional wrapper such as λx.F x when x is not free in F can preserve the formula’s role. Church calls the relevant operations changes of bound variable, contraction and expansion. Current notation usually separates alpha conversion, beta reduction and eta conversion.
The identity formula
Take the abstraction λx.x. It returns whatever occupies the bound position. Applying it to y creates a beta redex, a reducible expression:
The move is local and checkable. Substitute the argument for the bound occurrences of x in the body. A long calculation is a sequence of such licensed transformations.
Binding makes substitution a real operation
Substitution is not blind text replacement. In λy.x, the x is free and the y is bound. If we substitute the free variable y for x without care, the surrounding binder captures it. The result would falsely turn a reference from outside into a locally bound occurrence.
Capture-avoiding substitution first renames the binder to a fresh variable. The abstraction λy.x can be alpha-renamed to λz.x; only then may the free x be replaced by y. The answer is λz.y, not λy.y. Church’s definitions track free and bound occurrences precisely because later arithmetic on syntax must preserve these distinctions.
The change from y to fresh z changes no binding relation. It prevents the substituted variable from being captured. Any implementation of the article’s reduction bench must do the same.
A normal form is a destination, not a time limit
A formula is in normal form when it contains no beta redex. If a formula can be converted to such a formula, it has a normal form. Church proves that normal forms do not reduce further and, when one exists, it is unique apart from harmless renaming of bound variables. He also proves a normalisation result: a suitable continued reduction reaches that form. The conclusion is structural. It does not say every formula has a destination.
The smallest counterexample is the self-application loop conventionally called omega. Let Δ = λx.x x. Applying Δ to itself recreates the original expression in one beta step.
No amount of patience turns this particular reduction into a normal form. Yet observing a repeated state is a special luxury. Other non-normalising formulas can expand or wander without revisiting an identical surface string. A fixed step cap is therefore a testing policy, not a proof of divergence.
The evaluator example below uses the modern untyped calculus, which permits a binder even when its variable is absent from the body. Church’s 1936 grammar required the bound variable to occur free before abstraction. The harmless modern extension makes evaluation order unusually visible, but the example is not a quoted step in his proof.
Swipe horizontally to inspect the full reduction field.
The impatient evaluator
Consider (λx.a) Ω. The function ignores its argument. An outermost-first evaluator contracts the function call and returns a. An eager evaluator insists on reducing the argument first and remains inside omega forever. Has the formula got a normal form?
Yes. One bad journey does not erase an existing destination. This intervention separates three questions: whether a normal form exists, whether a chosen strategy will find it, and how long a particular run has lasted. Church’s theorem concerns the first across all well-formed formulas.
Church numerals turn functions into arithmetic
To connect formula conversion with number-theoretic calculation, Church represents positive integers by iteration. In the paper’s one-based list, the formula for one applies a function once to an argument; two applies it twice; three applies it three times. In the more common zero-based presentation, 0 = λf.λx.x, 1 = λf.λx.f x and 2 = λf.λx.f(f x).
A numerical function is lambda-definable when one formula maps the numeral for each input to the numeral for its output. Addition, multiplication, tests and bounded constructions can be assembled from abstractions and applications. Reduction is therefore doing more than simplifying symbols. It performs arithmetic in a representation that can also describe the functions performing the arithmetic.
Apply the Church numeral two to the successor-like operation s and seed z:
The star means several beta steps. If s adds one and z denotes zero, the result denotes two. The same formal medium holds data, procedure and application.
Optional depth: Church’s three early normal-form theorems
Theorem I says a formula already in normal form admits no reduction. Theorem II supplies uniqueness, apart from bound-variable renaming, and convergence of a continued suitable reduction when a normal form exists. Theorem III says every well-formed part of a formula with a normal form also has a normal form. The third result is later used to infer that Church’s diagonal formula itself normalises from the normalisation of one of its applications.
When syntax becomes arithmetic, the system can meet its own descriptions
A diagonal argument needs an index. We must be able to list formulas, refer to the formula in position n, apply it to the numeral for n, and keep every operation inside the formal class under examination. Church obtains that leverage by assigning each symbol a number and each finite symbol sequence a unique Gödel representation.
The encoding uses the prime numbers in order. If a formula has token codes t₁, t₂, …, tₖ, its representation is the product 2^t₁ 3^t₂ … pₖ^tₖ. Unique prime factorisation makes the map reversible. A natural number may be inconveniently large, but its factorisation preserves the ordered token sequence without ambiguity.
Encoding λa[a]
Church assigns code 1 to lambda, 11 to an opening square bracket, 13 to a closing one, and successive primes beginning at 17 to variables. The five tokens λ, a, [, a, ] therefore carry codes 1, 17, 11, 17, 13.
Decoding reads the exponent on the first prime as the first token code, the exponent on the second prime as the second code, and so on. This is an exact representation, not a hash. Distinct formulas receive distinct integers.
Swipe horizontally to inspect the complete encoding.
The tedious middle is the load-bearing middle
Once formulas have numbers, Church must show that the operations used later are recursive. Is a number the representation of a well-formed formula? Which occurrences are free? What is the result of substituting one formula into another? What appears at the nth position in an enumeration of a formula’s conversions? Does a code denote a principal normal form? Theorems VI through XV build this infrastructure.
Readers often hurry from the encoding to the diagonal. That shortcut makes the final contradiction look like verbal magic. The intervening theorems certify that each piece of the construction is an allowed computation. Self-reference alone proves nothing. The contradiction matters because the index, application operation, normal-form test and enumeration are all assumed or shown to remain inside one closed formal class.
Church proves that well-formed formulas are recursively enumerable, that having a principal normal form is a recursive property of a formula already presented in that form, and that the wider set of formulas which have some normal form is recursively enumerable. The last set can be listed by searching conversion histories. This does not yet give a decision procedure.
Two calculability roads arrive at the same functions
Theorem XVI says every recursive function of positive integers is lambda-definable. Theorem XVII says every lambda-definable numerical function is recursive. Together they identify the extensions of the two formalisms. Church credits the equivalence principally to Stephen Kleene, with contributions from himself and J. Barkley Rosser. Kleene’s own 1936 paper develops the relation directly.2
Equivalence does not mean the descriptions look alike. A recursive definition presents equations governing numerical values. A lambda term presents a conversion object whose applications reduce to numerals. One begins with arithmetical clauses, the other with binding and application. Their agreement is valuable precisely because they make different primitive choices.
What if the roads had not met?
Suppose lambda-definability excluded a numerical method everyone could plainly execute, while general recursion included it. An undecidability proof inside lambda calculus would remain a theorem about lambda formulas. Its claim to mark the boundary of all effective calculation would be weaker.
Now reverse the intervention: let both formalisms coincide, and add Turing’s analysis of a person working by discrete, locally determined steps on a finite visible portion of a tape.3 The models begin from distinct intuitions yet settle on the same functions. No single coincidence proves exhaustiveness, but each independent convergence raises the cost of proposing a counterexample.
Enumeration is not decision
A set is recursively enumerable when a mechanical process can list its members, eventually reaching each one. A set is recursive when a mechanical process can answer membership correctly for any candidate and always halt. The gap appears when absence has no finite witness.
Formulas that have a normal form can be enumerated. Dovetail all possible finite conversion sequences; whenever one reaches a principal normal form, emit the starting formula. Every normalising formula will eventually appear. If a submitted formula does not appear today, however, we learn nothing. It may appear after another million search rounds, or never. Silence is not a negative verdict.
Run three reduction searches in parallel. Formula A reaches a normal form after 5 steps; formula B after 4,000; formula C has not done so after 10 million. The search has certified A and B. It has not classified C. Calling C non-normalising would import a time budget that Church’s property does not contain.
Optional depth: why principal normal form appears
Bound-variable names can vary while binding structure remains the same. Church uses a principal normal form to remove that naming ambiguity in effective comparisons. The construction renames bound variables into a prescribed natural order and prevents one variable from appearing both free and bound. This gives the later arithmetic predicates a canonical target.
The diagonal formula that a complete list cannot contain
Church now assumes the device he intends to rule out. Let H(m) return 2 when m encodes a formula with a normal form, and 1 otherwise. Suppose H is recursive. The assumed test closes the one-sided gap: for any formula we can learn whether the search for a normal form will eventually succeed.
By Theorem XV, list all well-formed formulas that have a normal form as A₁, A₂, A₃, …. This is meant to be exhaustive, not a sample. Church then constructs a numerical function E that inspects the nth listed formula on input n and chooses a different numeral.
If Aₙ(n) converts to numeral m, set E(n)=m+1. If it does not convert to a numeral, set E(n)=1. Either way, E(n) is a numeral and differs from the diagonal value associated with Aₙ.
The assumed normal-form inspector makes the branch effective. First ask whether Aₙ(n) has a normal form. If it does, enumerate conversions until its principal normal form appears and check whether that form is a numeral. Every operation required to index, apply, inspect and increment has already been shown recursive. Therefore E would be effectively calculable under the assumption.
The equivalence theorem now bites. Every recursive numerical function is lambda-definable, so some formula e represents E. Church establishes that e has a normal form. The exhaustive list must therefore contain it. Suppose it appears at row k, so e is convertible to Aₖ. Evaluating both on k says they agree. The definition of E(k) says they differ. No row can be the row for e.
Swipe horizontally to inspect the diagonal table.
In Figure 6, row 1 returns 2 on input 1, so the new function returns 3. Row 2 yields a non-numeral on input 2, so the new function returns 1. Rows 3, 4 and 5 return 8, 4 and 6 on their own indices, so the new outputs are 9, 5 and 7. The new row differs from A₁ somewhere, from A₂ somewhere, and so on. For the infinite proof, “somewhere” is always the row’s own index.
The perfect normal-form inspector
Place the inspector’s implementation in the same language it inspects. Enumerate every formula it certifies as normalising. Use its answers to write the diagonal function, and compile that function back into a formula. Where can the compiled formula appear?
It must appear because it has a normal form. It cannot appear at row 1 because it differs from row 1 on input 1; it cannot appear at row 2 because it differs there on input 2; the same exclusion applies to every row. The contradiction is not that the inspector gives a visibly wrong answer on an ordinary test case. Its existence would make an exhaustive catalogue construct its own omission.
Why the contradiction needs every earlier link
Remove unique numbering and there is no reliable index. Remove effective enumeration and the list cannot be used by the proposed method. Remove closure under application and Aₙ(n) may leave the system. Remove the equivalence between recursiveness and lambda-definability and the new numerical function need not return as a formula. Remove totality from the hypothetical inspector and the branch constructing E can stall.
The proof is therefore better understood as a dependency structure than as the slogan “self-reference causes paradox”. Many self-referential systems are consistent. Church’s contradiction arises from a particular package: an exhaustive effective list, a total membership oracle, representation of syntax as data, diagonal evaluation and closure strong enough to internalise the constructed function.
Swipe horizontally to follow all five currents.
Theorem XVIII and its sharper corollary
The contradiction discharges the assumption. There is no recursive function that returns 2 or 1 according as an arbitrary well-formed formula has a normal form or not. Church’s Corollary 1 then shows that formulas without normal forms are not recursively enumerable. If both the normalising and non-normalising sets could be enumerated, run the two enumerators in parallel. Every submitted formula lies in exactly one set, so one list would eventually emit it, yielding a decider forbidden by Theorem XVIII.
The asymmetry matters. Positive instances have finite witnesses: a conversion reaching normal form. Negative instances do not admit a complete mechanical catalogue. This is more exact than saying “some programs run forever”. It identifies a one-sided evidential structure that recurs throughout computability and formal verification.
The two archivists
One archivist lists every formula for which a normal form has been found. A second claims to list every formula that lacks one. Give both the same candidate and alternate one step of work between them. If both catalogues are complete, exactly one archivist must eventually produce the candidate.
That race would decide normalisation. Church’s theorem says the second complete archive cannot be effectively maintained. The first archivist’s silence is permanent evidence only when another effective process can certify the complement.
From normalisation to conversion
Church’s Lemma establishes an effective equivalence between two proposed decision problems. Given formulas A and B, one can construct a formula C that has a normal form exactly when A and B are convertible. In the other direction, from a formula C one can construct a formula convertible to the numeral one exactly when C has a normal form.
Theorem XIX follows immediately: no recursive function decides conversion for every pair of formulas. Church then transfers the result to the Entscheidungsproblem for sufficiently expressive, omega-consistent systems of symbolic logic meeting his effective conditions. In particular, if the system of Principia Mathematica is omega-consistent, its decision problem is unsolvable. The qualification is part of the theorem and should stay attached to it.
Church proves undecidability of normal-form existence and conversion in his formal setting, then derives an unsolvability result for qualifying logical systems. He does not formulate Turing’s later machine-halting problem. The modern results are intimately related, but historical accuracy requires keeping the targets distinct.
The boundary Church drew, and the claims it does not settle
Church’s formal theorem is secure. The philosophical thesis connecting effective calculability to the recursive functions remains a proposed identification. That distinction has not made the thesis fragile. It has made the evidence for it cumulative. Within months, Alan Turing described a different model based on a human calculator reading, writing and moving over a bounded visible portion of an unbounded tape. He showed that his computable functions match Church’s lambda-definable ones, with the detailed equivalence completed in his 1937 paper.4
Turing’s analysis supplies something Church’s extensional convergence could not provide by itself: a decomposition of mechanical work into elementary acts. Emil Post independently offered a spare instruction-worker model and treated the identification with recursiveness as a working hypothesis in need of continuing confirmation.5 Different routes kept returning to the same extension. The familiar label “Church–Turing thesis” records that convergence, though the two men’s original justifications were not interchangeable.
A theorem, a thesis and an empirical speculation
Three layers should remain separate. First, mathematical theorems relate fixed formal systems: recursive functions equal lambda-definable functions; normalisation and conversion are undecidable. Second, the Church–Turing thesis identifies ordinary effective procedure with that formal extension. Third, stronger claims concern physical reality, human cognition or consciousness. Does every physically realisable process fall within Turing computability? Is every human cognitive capacity mechanically simulable? Could consciousness require a noncomputable process?8
Church’s paper does not answer the third layer. It provides vocabulary and constraints for posing those questions cleanly. An argument from undecidability to “consciousness is noncomputable” needs an additional premise connecting conscious performance to the solution of a specified undecidable function. An argument in the opposite direction, from computational success to “consciousness is computation”, also needs premises about what consciousness is. Neither conclusion arrives free with Theorem XVIII.
Kalmár’s objection changes the meaning of “method”
László Kalmár pressed a serious objection in 1959.6 Perhaps every individual value of a nonrecursive function can be found by some finite mathematical argument, even though no single recursive procedure generates all the values. Mathematics develops; new proofs and rules may be accepted. Why insist that effective calculability must be captured once and for all by a uniform algorithm?
Máté Szabó’s reconstruction shows both the force and the limit of the argument.7 Kalmár allows the method to vary with the input and to draw on open-ended human mathematical development. On that interpretation, the thesis looks too restrictive. Yiannis Moschovakis’s response is that this is not the usual notion of a mechanical procedure. A different argument for each input does not give one executable operation from arbitrary input to output.
The disagreement is productive because it identifies the disputed uniformity condition. If “effectively calculable” means what a fixed agent can execute from stated instructions, Kalmár has changed the subject. If it means what mathematical culture may eventually establish case by case, Church’s thesis does not capture the enlarged notion. The right response is not to declare one side foolish. It is to name which notion a claim uses.
The cabinet of future methods
Imagine a cabinet with one drawer for every positive integer. Drawer n contains a proof settling the nth case, but there is no uniform way to locate or verify the right proof from n. Over centuries, mathematicians happen to open every drawer. Has the cabinet defined a computable function?
As an extensional story, every value is present. As a procedure, the cabinet is empty: it supplies no rule for producing the relevant proof from a submitted index. Kalmár’s challenge asks whether human mathematical possibility should be judged extensionally or procedurally. Church’s thesis answers the procedural question.
An oracle moves the boundary; it does not erase it
Suppose we add a black box that answers the normal-form question correctly. Ordinary machines equipped with that oracle can solve problems ordinary machines cannot. This does not refute Church’s theorem, because the oracle’s answer is a new primitive outside the recursive operations the theorem quantifies over. The enlarged model has its own relative undecidable problems: one can diagonalise against machines that may query that oracle and ask for a stronger oracle.
The same discipline applies to proposals involving analogue physics, quantum devices or exotic spacetime. A faster implementation of recursive functions changes complexity, not computability. A genuine hypercomputer must realise an operation outside the Church–Turing class and must make its answer accessible with reliable finite evidence. The mathematical implication may be clear while the physical premise remains open.
An oracle-assisted solver is not a counterexample unless the oracle itself is shown to be an effective procedure under the original meaning. Naming the unavailable answer as a primitive relocates the unexplained work.
What this changes in engineering and assurance
Most deployed systems do not need to decide an unrestricted semantic property of every possible program. They work over bounded languages, typed workflows, finite state spaces, resource limits or proof-carrying inputs. Undecidability is therefore a design signal, not a reason to abandon verification. Restrict the domain until the property becomes decidable, accept one-sided certification, require a human escalation path, or state a resource-bounded guarantee.
A static analyser may certify memory safety for a disciplined subset and return “unknown” elsewhere. A termination checker may accept structurally recursive definitions and reject programs outside its proof rules without claiming they diverge. A model monitor may classify observed traces statistically, which is a measurement claim rather than a semantic decision procedure. These are honest contracts.
Three places where the boundary earns its keep
Procurement. A supplier says its platform “proves every agent plan safe before execution”. Ask whether safety is a syntactic policy over a finite action grammar, a semantic property of arbitrary code or a statistical risk score. The first may be decidable, the second may contain undecidable cases, and the third is not a proof. The same slide can make all three look alike unless the output contract is written down.
Architecture. A workflow language gains expressiveness by adding unbounded loops, dynamic tool discovery and code generation. Those additions may also destroy the finite-state assumptions that made exhaustive checking possible. Computability is not the only concern, but it is a reason to treat language design as part of the control system. Sometimes the right feature is a smaller grammar with a visible escape hatch to supervised execution.
Incident review. After a system times out, teams often label the case “non-terminating”. A timeout establishes that the run exceeded a budget under one strategy and environment. It does not establish semantic divergence. The distinction changes remediation. A slow terminating workflow may need cost controls or a better reduction order; an exact repeated state may reveal a cycle; an undecidable general property may require abstention and scope restriction. The evidence should determine which claim enters the incident record.
Unusable claim: “The agent verifies that every generated workflow will terminate correctly.”
Defensible contract: “For workflows in grammar G, with finite loop bounds and tools satisfying declared postconditions, the checker either emits a machine-verifiable termination certificate or abstains. Execution outside G is blocked.”
The second statement exposes the domain, assumptions, positive evidence and failure behaviour. It may be less dramatic. It can be tested.
| Claim type | Obligation | Honest negative output | Typical use |
|---|---|---|---|
| Sampled predictor | Estimate performance on a defined distribution | Low confidence or error rate | Risk scoring, anomaly detection |
| Recogniser | Eventually certify every positive instance | Silence is inconclusive | Proof search, witness discovery |
| Bounded checker | Decide within a restricted grammar or resource envelope | Out of scope or abstain | Typed workflows, model checking |
| Total decider | Halt correctly on every input in the full stated domain | Correct “no” | Finite domains, decidable theories |
Before accepting a universal automation claim, write its quantifier and domain in one sentence. Then ask whether the system promises a sampled prediction, a positive recogniser, a bounded checker or a total decider. If its documentation slides between those four, the assurance case is not ready.
Watch a reduction strategy make its commitments
A trace can prove that a term reaches normal form. A finite trace that has not finished usually proves much less. The bench below parses a small untyped lambda-calculus syntax, performs capture-avoiding substitution and lets the reader compare normal-order with applicative-order reduction.
Use a backslash or lambda sign for abstraction, followed by a variable and full stop. Application associates to the left. The implementation is deliberately small enough to inspect. It is a demonstration of the mechanism, not a decider for every lambda formula.
Choose a term, then reduce it
Ready. No claim has been made.
Current term
(λx.x) y
Steps taken 0
(λx.x) y
Inspect the demonstration algorithm
The parser and reducer are included in the document’s final script. They have no network dependency. Fully parenthesised printing favours unambiguous traces over compact notation.
Carry the proof as four moves, not a slogan
The phrase “there are undecidable problems” is too blunt to reconstruct Church’s argument. A useful memory keeps the obligation chain: number the syntax, assume a total inspector, diagonalise across the certified catalogue, then separate the theorem from the thesis.
1 · Definition check
What three obligations make a procedure a decider?
Correctness, halting on every permitted input and one uniform rule over the stated domain.
2 · Mechanism check
Why does Gödel numbering matter to the diagonal?
It makes formulas indexable data so recursive operations can select, apply and inspect the formula on row n.
3 · Evidence check
Why does enumerating all normalising formulas not decide normalisation?
Arrival is a finite positive witness; non-arrival at any finite time cannot distinguish late arrival from absence.
4 · Boundary check
Does Theorem XVIII prove that consciousness is noncomputable?
No. That conclusion needs an independent premise tying consciousness to the exact computation of a specified nonrecursive function.
Close the page and say the proof without using “halting problem”. Your answer should contain these nouns: normal form, Gödel representation, recursive enumeration, diagonal function, missing row. If one is absent, the slogan has displaced a mechanism.
The decision this changes
When a team proposes a universal analyser, reasoner or verification layer, the first decision is no longer “which model should we buy?” It is “what kind of claim are we making?” Write the input domain, the permitted procedure, the output contract and the behaviour on unsupported cases. Then decide whether the requirement is total decision, one-sided recognition, bounded checking or statistical prediction.
If the full property is undecidable, redesign the contract. Constrain the language. Require certificates. Bound the state space. Permit abstention. Separate the tool that finds evidence from the authority that accepts consequences. Those moves do not evade Church’s result; they use it to locate a tractable and auditable problem.
Church’s proof earns a disciplined scepticism. A universal automation promise is not defeated because the system has failed on a hard example, and it is not established because the system has passed many examples. The decisive question is whether the promised map can exist over the stated domain. Before measuring performance, inspect the quantifier.
Glossary
- Alpha conversion
- Renaming a bound variable without changing binding structure.
- Beta reduction
- Applying an abstraction by capture-avoiding substitution of its argument into the body.
- Church’s thesis
- The identification of effectively calculable numerical functions with recursive, equivalently lambda-definable, functions.
- Convertible
- Related through Church’s permitted conversion operations; written here as two formulas belonging to the same conversion relation.
- Decider
- A uniform procedure that halts with the correct yes-or-no answer on every input in its domain.
- Diagonalisation
- A construction that differs from the item on row n at coordinate n, preventing membership in an alleged exhaustive list.
- Effectively calculable
- An intuitive notion of calculation by definite mechanical procedure, identified by Church with a formal function class.
- Gödel representation
- An injective arithmetic encoding of formal syntax, allowing formulas and operations on them to be handled numerically.
- Lambda-definable
- Representable by a lambda formula whose applications to input numerals convert to the corresponding output numerals.
- Normal form
- A well-formed lambda formula containing no beta redex; a formula has a normal form if it can be converted to one.
- Recursive
- Belonging to the Herbrand–Gödel class of numerical functions used by Church and proved extensionally equal to lambda-definability.
- Recursively enumerable
- Listable by a recursive procedure that eventually emits every member, without necessarily deciding non-membership.
References
- Church, A. (1936). “An Unsolvable Problem of Elementary Number Theory.” American Journal of Mathematics, 58(2), 345–363. doi:10.2307/2371045.
- Kleene, S. C. (1936). “λ-definability and recursiveness.” Duke Mathematical Journal, 2(2), 340–353. doi:10.1215/S0012-7094-36-00227-2.
- Turing, A. M. (1936). “On Computable Numbers, with an Application to the Entscheidungsproblem.” Proceedings of the London Mathematical Society, s2-42(1), 230–265. doi:10.1112/plms/s2-42.1.230.
- Turing, A. M. (1937). “Computability and λ-definability.” The Journal of Symbolic Logic, 2(4), 153–163. doi:10.2307/2268280.
- Post, E. L. (1936). “Finite Combinatory Processes, Formulation 1.” The Journal of Symbolic Logic, 1(3), 103–105. doi:10.2307/2269031.
- Kalmár, L. (1959). “An Argument Against the Plausibility of Church’s Thesis.” In A. Heyting (ed.), Constructivity in Mathematics, 72–80. Amsterdam: North-Holland.
- Szabó, M. (2018). “Kalmár’s Argument Against the Plausibility of Church’s Thesis.” History and Philosophy of Logic, 39(2), 140–157. doi:10.1080/01445340.2017.1396520.
- Copeland, B. J. (2025 archive). “The Church–Turing Thesis.” Stanford Encyclopedia of Philosophy. Archived entry.