Logic and Computability

A proof separates two distinct tasks: choosing starting assumptions and drawing valid consequences from them. The assumptions are axioms; the permitted deduction steps are rules of inference. For instance, given the statement \(P\) and the rule “\(P\) implies \(Q\),” we are permitted to infer \(Q\).

Coming up with a proof requires creative exploration: you have to navigate an enormous space of possibilities, try intermediate ideas, and find a path that connects your assumptions to the target claim. Checking an existing proof, by contrast, requires no guesswork at all. You simply inspect each statement in order, confirming that it is either an accepted axiom or the result of applying an allowed rule to earlier lines.

This is the foundational bridge to computation. Once proofs are expressed in precise notation, verifying them requires no human intuition—a proof is simply a finite object that an algorithm can inspect symbol by symbol. The checker’s job is strictly mechanical: it verifies that the conclusion follows from the chosen axioms, leaving the question of whether those axioms accurately describe reality for another day.

Once we write down explicit rules, an algorithm can easily check whether an argument follows them. But this raises a deeper, more dangerous question: are the rules themselves trustworthy? Could a set of seemingly innocent axioms and deduction steps secretly allow us to prove both a statement and its exact opposite? A logical system that never generates such a contradiction is called consistent. Without consistency, mathematical reasoning collapses—if a system can prove both \(P\) and “not \(P\),” the rules allow you to derive literally any claim, true or false, rendering all proofs meaningless.

In the early twentieth century, David Hilbert set out to put all of mathematics on an unshakeable foundation. His strategy was radical: turn mathematics upon itself. While a mathematical theorem might speak about infinitely many numbers or vast geometric spaces, the written proof of that claim is always finite—just a concrete string of symbols on a page. Hilbert realized that proofs could therefore be studied as physical, mathematical objects in their own right. He proposed using safe, transparent reasoning about finite symbols—known as finitary methods—to prove that the formal rules could never lead to a contradiction.

This grand ambition—known as Hilbert’s program—separated mathematics into two levels: the formal deductions carried out inside the system, and the reasoning about those proofs from the outside. But securing the reliability of mathematical logic sparked an equally profound question about its automation: if proof checking is purely mechanical, can a procedure always determine whether a given statement has a proof at all? Answering that requires us to examine the critical gap between checking a proof and searching for one.

Imagine someone hands you a proposed proof for a mathematical statement \(P\). As we have seen, a computer can mechanically check each deduction line by line. If every step obeys the rules, the argument is accepted and \(P\) is proven. But what if the checker rejects the argument? A flaw in the proof only discredits that specific attempt—it does not mean \(P\) is false. Another, more subtle proof might easily succeed. Checking settles whether a supplied argument is valid, but it leaves open whether the statement itself is provable.

Now suppose you are given a statement \(P\) with no proof at all. Can a machine discover one from scratch? Because formal proofs are finite strings of symbols written in a fixed alphabet, a computer can systematically generate every conceivable text string, ordered by length: first strings of one symbol, then two, then three, and so on. Running our mechanical checker on each candidate in sequence creates an automatic proof search. If a valid proof of \(P\) exists, this exhaustive search is guaranteed to eventually construct it, confirm it, and halt with “yes.”

The trouble arises when a statement has no proof. Each rejected candidate merely rules out one string; it never proves that all future candidates will fail. Because there are infinitely many strings to test, the machine has no stopping condition—it simply loops forever, unable to distinguish between a proof that is just around the corner and a proof that does not exist. This reveals the critical distinction between searching and deciding. A true decision procedure for a decision problem cannot loop indefinitely: it must terminate in a finite number of steps on every input, delivering a definitive “yes” or “no.”

Could a more sophisticated method succeed where brute-force enumeration fails? Perhaps an algorithm could inspect the axioms and the target statement directly, bypassing exhaustive search altogether. The failure of one search strategy does not mean every strategy must fail. But to determine whether an all-powerful decision procedure is possible, we first need a rigorous, mathematical definition of what an “algorithm” actually is. That necessity brings us directly to the foundations of computation.

Consider a task we can easily carry out by hand: finding the greatest common divisor of \(48\) and \(18\). Euclid’s algorithm solves this by repeatedly replacing a pair of positive integers \((a, b)\) by the second number and the remainder on division:

\[(48,18)\longrightarrow(18,12)\longrightarrow(12,6)\longrightarrow(6,0).\]

Once the second number hits zero, the procedure returns \(6\). The arithmetic is straightforward, but whenever we claim to possess an algorithm, two fundamental questions demand proof: why is the final answer correct? and why must the procedure eventually stop?

The first question concerns correctness. When dividing \(a\) by \(b\), we write \(a = qb + r\), with \(0 \leq r < b\). Notice that any divisor that divides both \(a\) and \(b\) must also divide their remainder \(r = a - qb\). Conversely, any divisor that divides both \(b\) and \(r\) must also divide \(a = qb + r\). Replacing \((a, b)\) by \((b, r)\) therefore preserves their set of common divisors without losing or introducing any factors. The greatest common divisor is an invariant: it stays strictly constant across every step of the run. When the algorithm finally arrives at the pair \((g, 0)\), the greatest common divisor of \(g\) and \(0\) is trivially \(g\). Because the invariant was preserved at every step, \(g\) must be the true greatest common divisor of the starting pair.

The second question concerns termination. An invariant alone only guarantees that if the algorithm stops, the answer will be right—it does not prove the algorithm will ever finish. (For instance, an infinite loop that endlessly prints \((48, 18)\) preserves the invariant, but it never produces an answer.) Euclid’s algorithm is guaranteed to terminate because at each step, the second entry \(b\) is replaced by the remainder \(r\), and the remainder is strictly smaller than \(b\) while remaining non-negative (\(0 \leq r < b\)). A strictly decreasing sequence of non-negative integers cannot continue forever; it must eventually reach zero.

These are completely separate arguments. An algorithm requires both a reason to trust its result (correctness via an invariant) and a reason to expect that result in finite time (termination via a strictly decreasing metric).

Imagine pausing a computation halfway through—for instance, freezing Euclid’s algorithm at the pair \((18, 12)\), just before the next division. What is the absolute minimum information you would need to record so that someone else could resume the work without missing a beat? You need the numbers currently held in memory, and you need to know which instruction to carry out next. You do not need the historical path that brought you there.

That complete, self-contained snapshot of a computational process is called its configuration. What belongs inside a configuration depends entirely on where the machine is allowed to pause. If we only pause between full division steps, recording the integer pair is sufficient because the next instruction is always fixed. But if we pause mid-division inside a physical processor, the pair alone is not enough: the configuration must also store intermediate registers, carry bits, and the current line of the instruction counter.

A single step that updates one configuration into the next is called a transition. Beginning from an initial input, the computation advances through a sequence of discrete configurations:

\[C_0 \longrightarrow C_1 \longrightarrow C_2 \longrightarrow \cdots \longrightarrow C_{\text{final}}.\]

This entire sequence is called a run. A deterministic algorithm supplies an unambiguous rulebook: given any valid configuration, the next transition is uniquely determined. When the run enters a designated stopping configuration, the computation halts and outputs its result.

Notice a subtle asymmetry: while a deterministic configuration uniquely determines where to go next, it does not necessarily reveal where you came from. In Euclid’s algorithm, both the starting pair \((48, 18)\) and the starting pair \((30, 18)\) step directly into \((18, 12)\). Looking at \((18, 12)\) alone, you cannot reconstruct which pair started the run. The forward step is deterministic, but it is not reversible. This distinction between forward execution and backward reversibility will prove fundamental when we examine information loss and the foundations of quantum computation.

In Euclid’s algorithm, an instruction such as “divide \(a\) by \(b\)” seems elementary, but it still hides significant complexity: division is itself a multi-step routine of subtractions, shifts, and comparisons. If we want to prove mathematical theorems about the limits of computation in general, we cannot rely on convenient, high-level commands. We must break computation down into its simplest, irreducible physical operations.

In 1936, Alan Turing formalized this idea with the theoretical model now known as a Turing machine. A Turing machine strips computing down to four basic components:

• A tape divided into discrete cells extending as far as needed, each holding a single symbol from a finite alphabet (or a blank symbol \(\square\)).
• A read/write head positioned over exactly one cell at any given moment.
• A finite control state that keeps track of the machine’s internal status.
• A fixed rule table (or transition function). For each combination of current control state and symbol read by the head, the table specifies three atomic actions: which symbol to write, which direction to move the head (one cell left or right), and which control state to enter next.

When the machine enters a designated halting state, it stops, leaving its final answer written on the tape. A configuration of a Turing machine is completely specified by the contents of its tape, the position of the head, and its current control state.

Turing’s most transformative breakthrough was recognizing that a rule table is itself finite data. Because it consists of a finite list of discrete rules, we can encode the entire machine as a single string of symbols on a tape. This means one machine can read the encoded description of any other machine, along with an input, and faithfully imitate its behavior step by step. A machine designed to carry out this simulation is called a universal machine.

The universal machine unifies hardware and software: code is simply data. A computer program can accept another program as input, simulate it, analyze it, or even process its own description. This power of self-reference is neither mystical nor paradoxical—it is simply a finite procedure inspecting a finite string of text. Yet, as we will see next, this exact self-referential capability reveals the ultimate boundaries of what algorithms can decide.

We have defined computation using a remarkably primitive device: a tape, a read/write head, and a finite rule table. Why should a limitation of this bare-bones machine tell us anything about the limits of calculation in general? Could a richer, more sophisticated mathematical model compute functions that a Turing machine cannot?

In the 1930s, several mathematicians independently proposed completely different formalisms for computation. Alonzo Church’s lambda calculus dispensed with tapes and state machines altogether, defining computation through rules for substituting and evaluating function expressions. Kurt Gödel and Stephen Kleene developed recursive functions, building calculations out of basic arithmetic operations and composition rules. Later decades added register machines, cellular automata, and modern programming languages.

Despite their radically different designs, every one of these formal models turns out to compute the exact same class of functions as Turing machines. Any calculation carried out in lambda calculus, recursive functions, or a modern programming language can be simulated step by step on a Turing machine, and vice versa. Because each of these models is a precisely defined mathematical system, their equivalence is not a philosophical opinion—it is a rigorous mathematical theorem proved by explicit simulation.

The Church–Turing thesis takes the crucial next step: it states that any calculation that can be carried out by an effective mechanical method can be carried out by a Turing machine. Notice why this is called a thesis rather than a theorem. While a Turing machine is a formally defined mathematical object, “effective mechanical method” is an informal, intuitive notion of what a step-by-step procedure can do. We cannot write a formal proof equating an informal intuition to a mathematical definition; instead, the proven equivalence of every formal model ever proposed provides overwhelming evidence that the Turing machine captures the full reach of mechanical calculation. Whenever we prove a theorem that no Turing machine can solve a given problem, the Church–Turing thesis tells us that no algorithm of any kind can solve it either.

Crucially, the Church–Turing thesis is a statement about computability—whether a function can be computed in finite time at all—not about efficiency, which asks how much time or memory the calculation requires. This distinction is vital for quantum computing. In the standard quantum model, the allowed physical operations have precise mathematical descriptions that a classical Turing machine can simulate in principle, albeit often at an astronomical cost in time and memory. Consequently, quantum computers do not violate the Church–Turing thesis: they cannot compute functions that are uncomputable by a Turing machine. Rather, their power lies in dramatically reducing the computational resources needed for certain problems that are already computable—a difference we will explore when we turn to quantum algorithms.

Given a computer program and its input, can we always determine in advance whether the run will eventually stop or continue forever? For many specific programs, the answer is straightforward: in Section 1.2.1 we proved that Euclid’s algorithm always terminates by tracking a strictly decreasing nonnegative integer, and it is just as easy to spot a simple infinite loop. Simply running a program for a fixed number of steps—say, a million or a trillion—is not a general test, because if the program is still running when the timer expires, we only know that it has not halted yet, not whether it will halt on the very next step or loop forever. Can a cleverer algorithm inspect any program and input and always decide whether the computation halts?

Suppose, for the sake of contradiction, that such a universal halting decider exists. Call it \(H(P, x)\), where \(P\) is the text description of a program and \(x\) is its input. Because \(H\) is assumed to be a genuine decision procedure, it must terminate in a finite number of steps on every pair \((P, x)\), answering “halts” if \(P\) eventually stops on input \(x\) and “does not halt” if \(P\) runs forever on \(x\).

Because programs are simply finite strings of data (as we saw with the universal machine in Section 1.2.3), we can use \(H\) as a subroutine inside a new, adversarial program \(D\). The program \(D\) accepts a single string \(p\)—representing a program description—as its input and carries out two instructions:

1. First, \(D\) runs \(H(p, p)\): it asks the decider what happens when the program described by \(p\) is given its own text description as input.
2. Second, \(D\) deliberately does the exact opposite of \(H\)’s prediction. If \(H(p, p)\) answers “halts,” \(D\) intentionally enters an endless loop. If \(H(p, p)\) answers “does not halt,” \(D\) immediately halts. (If \(p\) is not a valid program description, \(D\) simply halts.)

Because \(D\) is built entirely out of explicit, mechanical operations, \(D\) is itself a valid program with its own finite text description, which we call \(d\). Now feed \(d\) as the input to \(D\), and ask: what does \(H(d, d)\) predict about the run \(D(d)\)?

Either answer destroys the decider. If \(H(d, d)\) answers “halts,” then \(D(d)\) receives that prediction, follows its second rule, and enters an infinite loop—so \(D(d)\) never halts, contradicting \(H\)’s answer. Conversely, if \(H(d, d)\) answers “does not halt,” then \(D(d)\) follows its second rule and immediately stops—so \(D(d)\) halts, again contradicting \(H\)’s answer. Since constructing \(D\) from \(H\) used only standard programming operations, the contradiction proves that our starting assumption is impossible: no general algorithm \(H\) can exist. This landmark theorem is the undecidability of the halting problem.

Keep the exact scope of this theorem in mind. It does not prevent us from proving that individual programs terminate—we already proved termination for Euclid’s algorithm—nor does it forbid automated verification tools that decide halting for broad families of well-structured programs while answering “unknown” on cases they cannot resolve. What is mathematically impossible is a single, universal algorithm that always terminates with a definite, correct yes-or-no verdict for every program and input.

We can now bring the computational limits of Section 1.3.2 directly back to the logical questions of Section 1.1. In doing so, we must distinguish two fundamental boundaries that apply to different kinds of objects. An undecidable problem is a limit on algorithms: it is a decision problem (such as the halting problem) for which no single procedure always terminates with the correct yes-or-no answer. An incomplete theory, by contrast, is a limit on proofs within a fixed axiom system: it is a formal theory in which some statement \(P\) can neither be proved nor refuted from the axioms—that is, neither \(P\) nor its negation \(\neg P\) has a formal proof.

Although undecidability concerns procedures and incompleteness concerns axiom systems, the two limits are deeply intertwined. Recall from Section 1.1.3 that if a consistent theory with mechanically listable axioms were complete—proving either \(P\) or \(\neg P\) for every statement \(P\)—we could build a decision procedure simply by enumerating candidate proofs until either a proof of \(P\) or a proof of \(\neg P\) appeared. Because the step-by-step execution of a Turing machine can be expressed as a statement about integers, a complete and consistent axiom system for arithmetic would allow us to decide whether any program halts! Since the halting problem is undecidable, no such axiom system can be complete.

More precisely, the Gödel–Rosser theorem (first proved by Kurt Gödel in 1931 and strengthened by J. Barkley Rosser in 1936) applies to any formal theory that is consistent, whose axioms can be effectively listed by an algorithm, and that is expressive enough to formulate basic arithmetic on the integers (such as Peano arithmetic). Any theory meeting these three conditions is necessarily incomplete: it contains an arithmetic sentence \(P\) for which neither \(P\) nor \(\neg P\) is provable.

Can we repair this gap simply by adding the undecided sentence \(P\) as a new axiom? Adding \(P\) settles \(P\) itself, of course—but as long as the enlarged axiom system remains consistent and mechanically listable, the Gödel–Rosser theorem applies all over again, producing a brand-new undecided sentence. Every hypothesis of the theorem is essential: simple logical theories that cannot express full arithmetic can be both consistent and complete, whereas an inconsistent theory trivially proves every sentence.

Finally, Gödel’s second incompleteness theorem delivers the verdict on Hilbert’s consistency program from Section 1.1.2. Under the same conditions, a consistent theory strong enough to describe arithmetic and its own proof-checking rules cannot prove the formal sentence asserting its own consistency. While a stronger mathematical theory can prove that a weaker one is consistent, doing so merely shifts our reliance onto the stronger theory’s axioms.

For our study of computation, the lesson is clear: making logical and computational rules explicit enables mechanical verification and universal simulation, while simultaneously revealing absolute boundaries that no algorithm—classical or quantum—can cross. Within the vast domain of tasks that do admit algorithms, however, a new physical question awaits: when a computation runs on a physical device, what happens to the information it processes along the way?

In a deterministic computation, the future is never ambiguous: each running configuration has a single, uniquely determined next configuration, while a halting configuration simply stops. Whenever the computation can continue, the present snapshot completely fixes what happens next.

Does knowing the later configuration also tell us which earlier configuration produced it? Determinism makes no such promise. Recall the transitions from Euclid’s algorithm that we encountered in Section 1.2.2:

\[(30,18)\longrightarrow(18,12),\qquad(48,18)\longrightarrow(18,12).\]

If we inspect the calculation when it holds the pair \((18,12)\), we know exactly how to continue the run to \((12,6)\) and then \((6,0)\). Yet from \((18,12)\) alone, it is impossible to tell whether the previous pair was \((30,18)\), \((48,18)\), or any other pair \((18q+12,18)\). Distinct computational histories have merged into a single configuration, discarding the quotient \(q\) that distinguished them.

To undo a step and run a computation backward, we must be able to recover the exact earlier configuration from the resulting configuration alone. That requires a stricter condition than determinism: different inputs must always produce different outputs. A transition rule with this property is called one-to-one, and logical reversibility requires every elementary step of a computation to obey this condition.

When a one-to-one transition also reaches every configuration in a fixed state space, it forms a bijection: a one-to-one correspondence in which every configuration has both a unique successor and a unique predecessor. On such a state space, the reverse transformation is itself a well-defined deterministic rule everywhere.

Knowing what happens next is therefore only half the story. We must now ask whether ordinary calculations that seem to throw information away can be redesigned so that no histories ever merge.

At first glance, most everyday calculations appear inherently irreversible because the functions they compute are many-to-one. Consider the logical AND operation on two bits: it returns \(0\) on three different inputs—\(00\), \(01\), and \(10\)—and returns \(1\) only on \(11\). If a logic gate overwrites its inputs and keeps only the single answer bit \(0\), there is no way to recover which of the three inputs occurred.

Yet obtaining an answer need not mean throwing away the input that produced it. If instead of keeping \(f(x)\) alone we retain the input alongside the output, forming the pair \((x,f(x))\), then different inputs \(x\) always yield different output pairs—even when \(f\) itself is many-to-one. For AND, keeping both input bits and writing their conjunction into an extra target bit (initialized to \(0\)) maps the four starting configurations \(000\), \(010\), \(100\), and \(110\) to four distinct outputs: \(000\), \(010\), \(100\), and \(111\).

Of course, simply adding extra storage is not yet a complete computational architecture. To compute reversibly in practice, we must build complex operations out of reversible elementary gates, specify the initial values of any extra workspace bits, and clear temporary intermediate results without erasing them and losing information. Designing those gates and uncomputing temporary workspace is the central task of Chapter 2.

Why should we go to such lengths to avoid erasing information? The reason is physical as well as logical. As we noted at the opening of this chapter, every computation is carried out by a physical system. At the smallest scales, the laws of quantum mechanics that govern isolated physical systems run backward just as deterministically as they run forward; between observations, their evolution loses no information. Any computer built to harness quantum mechanics must therefore reach useful answers through reversible transformations. We have moved from the foundational question of computability—“Can this task be computed at all?”—to the physical question that launches the next chapter: “How can its computation preserve information?”