Definition
Computability is the study of which problems can in principle be solved by an algorithm — a finite, mechanical procedure that terminates with the right answer on every input. It is a question of possibility, not practicality: a problem is computable if some such procedure exists, however slow, memory-hungry, or impractical it might be.
The field draws a sharp line through the space of problems. On one side are the computable problems, for which an algorithm exists; on the other are problems that no algorithm can settle, no matter how clever the design or how powerful the hardware. The line is fixed by a single mathematical model — the Turing machine — and protected by the Church-Turing thesis, which claims that any reasonable formalization of "mechanical procedure" gives the same answer. The most famous problem on the wrong side of that line is Turing's halting problem.
Why it matters
How it works
The Turing machine as a fixed reference point
A Turing machine is a deliberately impoverished mathematical device: a finite control reading and writing symbols on an unbounded tape, one step at a time. Despite the spartan design, Turing showed in 1936 that this machine can simulate any procedure that human computers (people, originally) carried out by following fixed rules. Anything computable by a finite, definite recipe is computable on a Turing machine; anything not computable on a Turing machine is not computable at all, in the sense the field has settled on.
Computability theory works by taking this machine as the canonical definition of "algorithm" and then asking, of any problem you can state precisely, whether some Turing machine decides it. The answer divides problems into two classes — and the dividing line, far from being a matter of engineering, turns out to be a hard mathematical fact.
The Church-Turing thesis: a thesis, not a theorem
In 1936, three independent characterizations of "effectively computable function" appeared: Alonzo Church's lambda calculus, Alan Turing's machines, and Kurt Gödel's general recursive functions. They turned out to define exactly the same class. Every subsequent attempt — register machines, Markov algorithms, Post systems, cellular automata, modern instruction-set architectures, quantum circuits restricted to classical outputs — has produced the same class. The Church-Turing thesis is the empirical claim that this class is exactly the class of functions computable by any mechanical procedure whatsoever.
It is not a theorem and cannot be one, because "mechanical procedure" is an informal notion. But its empirical force is overwhelming. Hofstadter offers a stronger isomorphism reading: any two computational formalisms can be put into structure-preserving correspondence, so they are not merely equivalent in extension but equivalent in mechanism. This stronger thesis underwrites the move of treating Turing machines, lambda calculus, neural networks, DNA, and formal systems as different presentations of one abstract object — the meta-claim that makes large parts of the cognitive-science project intelligible.
Bounded loops versus free loops: BlooP, FlooP, and why GlooP cannot exist
Hofstadter's toy languages bracket the territory. BlooP allows only bounded loops — LOOP n TIMES, where n is fixed before the loop begins. Every BlooP program halts on every input. The functions BlooP computes are exactly the primitive recursive ones: addition, multiplication, exponentiation, primality, divisibility, and essentially every "ordinary" total function from numbers to numbers. Crucially, BlooP can decide the Proof-Pair(m, n) predicate — whether m encodes a valid proof of theorem n — because checking a proof is a bounded walk down a finite list.
FlooP adds free loops (MU-LOOP, LOOP FOREVER) that may never terminate. FlooP computes exactly the partial recursive functions — the full class of computable functions in the Church-Turing sense. FlooP can ask "is n the Gödel number of a theorem of TNT?" by searching the infinite space of candidate proofs m, halting iff a witness is found. The price is that you cannot in general predict whether a FlooP program will halt. GlooP, a hypothetical even-more-powerful language, would compute "more" than FlooP — but the Church-Turing thesis says GlooP cannot exist. FlooP is already the architectural ceiling.
The halting problem and the diagonal argument
The halting problem asks: is there an algorithm H(p, x) that, given any program p and input x, decides whether p(x) halts? Turing's answer is no, and the argument is a diagonalization. Assume H exists. Construct D(p): "if H(p, p) says p(p) halts, loop forever; otherwise halt." Now consider D(D). If D(D) halts, then by D's definition H(D, D) reported halt — but D then loops, contradiction. If D(D) loops, then H(D, D) reported non-halt — but D then halts, contradiction. H cannot exist.
The argument has the same shape as Gödel's: build an object that diagonalizes against the supposed deciding procedure, so the procedure must contradict itself on the diagonal case. Gödel diagonalized against provability; Turing diagonalized against halting; Tarski diagonalized against truth. Each of the 1930s limitative results carves out a property that seems like it should be expressible inside a sufficiently rich system but turns out to be expressible only from outside it.
Decidable, recursively enumerable, and the gap between them
Computability theory refines the binary computable/uncomputable split into a richer hierarchy. A set of numbers (or problems) is decidable — equivalently recursive — if some Turing machine halts on every input with a yes/no answer for membership. It is recursively enumerable (r.e.) if some Turing machine halts and says "yes" on exactly the members, but may loop forever on non-members. Every decidable set is r.e.; the reverse fails. The set of halting programs is the paradigm r.e.-but-not-decidable set: you can list the halters by simulating in parallel and reporting whichever finishes, but no algorithm decides non-halters in finite time.
This distinction matters because much of mathematics and computer science lives in the gap. The theorems of any consistent, sufficiently strong axiomatic system form an r.e. set — you can enumerate them by mechanically generating proofs — but the set of true arithmetic sentences is not even r.e. (Tarski). The class of programs that terminate is r.e. but not decidable. The class of programs equivalent to a given program is neither (Rice's theorem). Most interesting properties of programs sit on the wrong side of the line.
Why patching does not escape: the infinite tower
A natural reaction to undecidability: if a single algorithm cannot decide some property, add the answer as a new axiom or instruction. Hofstadter walks through what this buys you. Add the Gödel sentence G of TNT as an axiom — the resulting system TNT+G is itself a new formal system, with its own Gödel sentence G' that it cannot prove. Add G'; you get G''. The tower of patches is infinite, and at no finite stage is the system complete. Tarski's resolution of the truth-undefinability paradox has the same shape: truth for language L must be defined in a strictly stronger meta-language L', then L'', and so on.
The computability moral is the same. There is no clever extension of the Turing-machine model — no oracle, no extra instruction, no parallelism, no quantum trick — that decides the halting problem of itself. You can build a machine with an oracle for the halting problem of plain Turing machines, but then the halting problem for oracle machines is undecidable to them. Limitation is not a property of any particular formalism; it is a property of the level at which a system tries to reason about itself.
Why it bounds practical engineering
Knowing where the line lies changes what tools you can promise. A linter that finds every infinite loop is impossible; a linter that finds many infinite loops by heuristics is achievable, and the difference is not marketing. A program analyzer that decides whether arbitrary code is "safe" is impossible; one that detects many known unsafe patterns is real and useful. A theorem prover that decides every arithmetic claim is impossible; one that proves many useful claims is the basis of modern formal-methods work. Selling the impossible version is fraud; building the achievable version is engineering. Computability theory is, in this sense, deeply applied — it shapes the contracts under which real software can be sold and trusted.
How Priest frames the punchline
Graham Priest reaches the same destination by a shorter route. Leibniz dreamed of a characteristica universalis — a language in which every dispute is settled by calculation. Modern symbolic logic supplies the language; the remaining question is whether some calculating procedure always delivers the answer. Turing's 1936 result says no, even for the limited domain of mathematical claims. The Halting Theorem marks a hard, permanent boundary on what computation — and therefore formal reasoning — can do, resting on the Church-Turing thesis and powered by the diagonal self-reference that also drives Gödel's theorem in the next topic. The number of possible problems is, in a precise sense, strictly larger than the number of possible algorithms, so most problems have no algorithm at all. The halting problem just hands us one concrete witness.