01 · Logic

This is Part I's first hearing, the discipline standing closest to the courtroom itself — logic is where philosophy and computing were still, for a while, one undivided family.

What happened when the laws of thought became a machine?

On 10 August 1937, a twenty-one-year-old graduate student named Claude Shannon submitted a master's thesis to MIT's electrical engineering department. Its claim was almost embarrassingly simple to state: the algebra George Boole had invented in 1854 to describe human reasoning — an algebra of true and false, of "and," "or," and "not" — was also the algebra of switches wired in series and parallel. A closed switch is 1; an open switch is 0. Two switches in series compute AND; two in parallel compute OR. Shannon showed that any relay circuit could be simplified the way a logician simplifies a formula, and that any Boolean formula could, in turn, be built out of relays. The published version, "A Symbolic Analysis of Relay and Switching Circuits" (Transactions of the American Institute of Electrical Engineers 57, 1938: 713–723), led the psychologist Howard Gardner, in 1985, to call it "possibly the most important, and also the most famous, master's thesis of the century" (History of Information). Logic had been a description of thought for two thousand years. After Shannon, it was also a wiring diagram.

That collision was not a straight line, and the straight line usually told is wrong. Aristotle's Prior Analytics had fixed logic's shape for two millennia: the syllogism, a machine of exactly three lines — "All Greeks are mortal; Socrates is a Greek; therefore Socrates is mortal" — valid by form alone, regardless of what the words meant. It was rigorous, and it was also nearly frozen; logicians spent centuries cataloguing which syllogistic figures were valid rather than extending the method. Boole's An Investigation of the Laws of Thought (1854) broke the freeze by algebraizing it: propositions became equations over 0 and 1, "and" became multiplication, "or" became addition, and inference became solving. This looks, in hindsight, like a rediscovery of Leibniz's seventeenth-century dream of a calculus ratiocinator — a calculus for settling arguments — and it is tempting to tell the story as an unbroken inheritance. It was not. Boole did not know of Leibniz's anticipations of his algebra when Laws of Thought appeared; he learned of them afterward, from Robert Leslie Ellis, and was reportedly delighted rather than deflated to find Leibniz had glimpsed the same terrain two centuries earlier (SEP, Leibniz's Influence on 19th-Century Logic). Gottlob Frege, by contrast, did claim Leibniz's mantle deliberately when he built the next floor. The seam between the two disciplines was rediscovered at least as often as it was handed down — evidence, again, that both keep arriving at the same idea because they are excavating the same ground independently, not passing a single torch hand to hand.

Frege's Begriffsschrift (1879) is the second principle this chapter needs: quantification. Boole's algebra could say "some men are wise" only clumsily, as a fact about classes; it had no clean way to express "for every x, if x is a man, x is mortal" as a single manipulable structure with a variable running through it. Frege built exactly that — a notation, admittedly nothing like the ∀ and ∃ symbols used today, but expressively equivalent to them, in which generality and existence become operators binding a variable inside a formula. This is the single move that let logic swallow the reasoning used throughout ordinary mathematics, not just its syllogistic fragment — and it is also, not incidentally, the ancestor of the variable in every programming language: a slot that a quantifier, or a for loop, ranges over.

The third principle is the split Shannon's circuits do not resolve: proof is not truth. In 1929, in his doctoral dissertation under Hans Hahn, Kurt Gödel proved first-order logic complete — answering a question Hilbert and Ackermann had posed the year before, he showed that every logically valid formula of first-order logic has a formal proof, and (the companion property, soundness) that every provable formula is valid. Two years later, the same man showed the coin's other face: any consistent formal system rich enough to contain elementary arithmetic must be incomplete — it contains true arithmetical statements it cannot prove. First-order logic itself is complete; arithmetic built on top of it is not. The two results are not in tension, because they answer different questions about different systems, but together they mean something exact and permanent: mechanizing inference (soundness and completeness for logic) is not the same project as mechanizing all of mathematical truth (which Gödel showed cannot be finished). A circuit can decide whether an argument's form is valid. It cannot decide whether every true statement about numbers has a proof, because some do not.

The fourth principle turns logic from a way of checking arguments into a way of writing programs. Robert Kowalski's 1979 slogan "Algorithm = Logic + Control" (Communications of the ACM 22, no. 7: 424–436) proposed splitting any procedure into a logic component — what is true, stated declaratively — and a control component — how a machine searches for it. Alain Colmerauer and Philippe Roussel had already built the proof of concept in Marseille in the summer of 1972, working out the top-down search strategy with Kowalski himself during his visits from Edinburgh: Prolog, a language in which a program is literally a set of logical clauses, and running the program means asking the machine to prove a theorem from them by resolution (Kowalski, "The Early Years of Logic Programming"). For the first time, writing a specification and writing an executable were, formally, the same act.

The fifth principle is the deepest handshake between the two courts in this entire book: the Curry–Howard correspondence. In 1934, Haskell Curry noticed that the types assignable to the combinators of combinatory logic matched, term for term, the axioms of intuitionistic implicational logic ("Functionality in Combinatory Logic," PNAS 20). William Howard extended the observation to full natural deduction and the lambda calculus in 1969, though the paper that made it famous, "The Formulae-as-Types Notion of Construction," was not published until 1980, in a festschrift for Curry. The correspondence says something stronger than analogy: a proposition is a type, a proof of that proposition is a program of that type, and simplifying a proof — removing a detour — is running the program one step. Logic and computation are not two things that resemble each other; under Curry–Howard, for a wide and growing class of systems, they are the same thing described twice. Modern proof assistants (Coq, Agda, Lean) are, quite literally, programming languages in which a well-typed program is a certificate that a theorem is true.

The people, briefly. Boole was self-taught, working as a schoolmaster in Lincoln before a professorship at Cork; Frege spent most of his career unread, his logic noticed chiefly because Bertrand Russell wrote to him in 1902 to point out a contradiction in it. Kurt Gödel worked in near isolation in Vienna and later Princeton, distrustful to the point of starving himself in his final year. Haskell Curry and William Howard are barely names outside logic departments — fitting, for a correspondence whose own publication was delayed eleven years, as if the ideas in this chapter have a habit of arriving before anyone is ready to print them.

Connections

Chapter 00 is this chapter's parent: the Frege–Russell–Hilbert–Gödel–Turing pipeline is narrated there in full; this chapter stays inside logic's own family quarrel. Chapter 09 returns to 1936 to ask what the Church–Turing thesis actually claims. Chapter 11 owns Shannon's later severing of information from meaning in 1948; this chapter's Shannon stops at 1937, where circuits meet Boole and nothing yet has been said about meaning. Chapter 12 takes Curry–Howard to its full depth, through Brouwer's intuitionism and mechanized mathematics.

Open questions

If Boole and Leibniz, and later Frege, kept independently finding the same seam, is a mathematized logic something humanity was always going to discover once algebra and doubt about the syllogism coincided — or was the coincidence itself contingent? And if proof and program are truly the same object under Curry–Howard, which discipline should be said to have discovered the other: did computing find out it was secretly doing logic, or did logic find out it was secretly executable?

Go deeper

• Ernest Nagel and James R. Newman, Gödel's Proof, New York University Press, 1958 — still the clearest short account of what completeness and incompleteness do and do not say.
• Claude Shannon, "A Symbolic Analysis of Relay and Switching Circuits," Transactions of the American Institute of Electrical Engineers 57 (1938): 713–723; William Howard, "The Formulae-as-Types Notion of Construction," in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, eds. J.P. Seldin and J.R. Hindley, Academic Press, 1980 (written 1969).
• Gödel's Incompleteness Theorems, Stanford Encyclopedia of Philosophy.